add operators

README.md

@@ -42,17 +42,17 @@ and I need this information for the typechecking.
 
 ## Issues
 
-- I need to do some erasure of values unused at runtime
+- I should do some erasure of values unused at runtime
 - I'm a little fuzzy on the "right way" to deal with constraints from unification
 - I'm a little fuzzy on how much to evaluate and when
 - I'm not postponing anything, and I suspect I will need to
 
 ## References
 
-"Unifiers as Equivalences" has unification with types.  Look into adapting some of that (or at least read/understand it).  Indexed types are mentioned here.
-
 "Elaborating Dependent (Co)pattern Matching" describes building case trees. Section 5.2 has the algorithm.
 
 "A prettier printer" was the basis of the pretty printer.
 
 "Elaboration Zoo" was a resource for typechecking and elaboration. In particular pattern unification and handling of implicits is based on that.
+
+"Unifiers as Equivalences" has unification with types.  Look into adapting some of that (or at least read/understand it).  Indexed types are mentioned here.

TODO.md

@@ -1,22 +1,27 @@
 
 ## TODO
 
+I may be done with `U` - I keep typing `Type`.
+
+- [ ] type constructors are no longer generated?  And seem to have 0 arity.
 - [x] there is some zero argument application in generated code
 - [x] get equality.newt to work
   - [x] broken again because I added J, probably need to constrain scrutinee to value
 - [x] inline metas.  Maybe zonk after TC/elab
 - [x] implicit patterns
-- [ ] pair syntax (should this be a comma operator)
+- [x] operators
-- [ ] list syntax
+- [x] pair syntax (via comma operator)
-- [ ] operators
+- [ ] matching on operators
+- [x] SKIP list syntax
+  - Agda doesn't have it, clashes with pair syntax
 - [ ] import
-- [ ] add {{ }} and solving autos (or maybe just `auto` keyword)
+- [ ] autos / typeclass resolution
-  - considering various solutions.  Perhaps marking the data type as solvable, if we had types on metas.
+  - keep as implicit and do auto if the type constructor is flagged auto
   - keep as implicit and mark auto, behavior overlaps a lot with implicit
-  - but we might want to solve right away when creating the implicit
+  - have separate type of implict with `{{}}`
-  - later we might need postpone
+  - Can we solve right away when creating the implicit, or do we need postpone?
 - [ ] do blocks
-- [ ] some solution for `+` (classes? ambiguity?)
+- [ ] some solution for `+` problem (classes? ambiguity?)
 - [ ] show compiler failure in the editor (exit code != 0)
 - [ ] write js files into `out` directory
 - [ ] detect extra clauses in case statements
@@ -30,3 +35,4 @@
 - [ ] magic nat (codegen as number with appropriate pattern matching)
 - [ ] magic tuple? (codegen as array)
 - [ ] magic newtype? (drop in codegen)
+- [ ] records / copatterns

newt/equality.newt

@@ -0,0 +1,24 @@
+module Equality
+
+data Eq : {A : U} -> A -> A -> U where
+  Refl : {A : U} {a : A} -> Eq a a
+
+-- Some magic is not happening here.
+
+sym : {A : U} {x y : A} -> Eq x y -> Eq y x
+sym Refl = Refl
+
+trans : {A : U} {x y z : A} -> Eq x y -> Eq y z -> Eq x z
+trans Refl Refl = Refl
+
+coerce : {A B : U} -> Eq A B -> A -> B
+coerce Refl a = a
+
+J : {A : U} ->
+    {C : (x y : A) -> Eq x y -> U} ->
+    (c : (x : _) -> C x x Refl) ->
+    (x y : A) ->
+    (p : Eq x y) ->
+    C x y p
+-- this was failing until I constrained scrutinee to the constructor + args
+J c x y Refl = c x

newt/oper.newt

@@ -0,0 +1,41 @@
+module Oper
+
+-- These are hard-coded at the moment
+-- For now they must be of the form _op_, we'll circle back
+-- with a different parser, but that works today.
+
+-- this will be parsed as a top level decl, collected in TopContext, and
+-- injected into the Parser. It'll need to be passed around or available
+-- for read in the monad.
+
+-- long term, I might want TopContext in the parser, and parse a top-level
+-- declaration at a time (for incremental updates), but much longer term.
+
+infixl 4 _+_
+infixl 4 _-_
+infixl 5 _*_
+infixl 5 _/_
+
+ptype Int
+ptype String
+ptype JVoid
+
+-- If we had a different quote here, we could tell vscode it's javascript.
+-- or actually just switch modes inside pfunc
+pfunc log : String -> JVoid := "(x) => console.log(x)"
+pfunc plus : Int -> Int -> Int := "(x,y) => x + y"
+pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
+
+-- We now have to clean JS identifiers
+_+_ : Int -> Int -> Int
+_+_ x y = plus x y
+
+test : Int -> Int
+test x = 42 + x * 3 + 2
+
+infixr 2 _,_
+data Pair : U -> U -> U where
+  _,_ : {A B : U} -> A -> B -> Pair A B
+
+blah : Int -> Int -> Int -> Pair Int (Pair Int Int)
+blah x y z = (x , y, z)

newt/tutorial.newt

@@ -0,0 +1,15 @@
+-- Files begin with a module declaration, modules not implemented yet
+module Tutorial
+
+
+-- import Prelude  not implemented yet
+
+-- declare a primitive type
+ptype Int
+
+-- declare a more complex primitive type
+ptype Array : U -> U
+
+-- declare a primitive function
+pfunc alength : {a : U} -> Array a -> Int := "(x) => x.length"
+

newt/typeclass.newt

@@ -2,6 +2,8 @@ module TypeClass
 
 -- experiment on one option for typeclass (we don't have record yet)
 
+-- this would be nicer with records and copatterns
+
 -- we need a bit more than this, but
 data Monad : (U -> U) -> U where
   MkMonad : { M : U -> U } ->

src/Lib/Parser.idr

@@ -1,5 +1,6 @@
 module Lib.Parser
 import Lib.Types
+import Debug.Trace
 
 -- The FC stuff is awkward later on. We might want bounds on productions
 -- But we might want to consider something more generic and closer to lean?
@@ -29,7 +30,7 @@ import Data.Maybe
 -- the future.
 
 
-ident = token Ident
+ident = token Ident <|> token MixFix
 
 uident = token UIdent
 
@@ -87,14 +88,14 @@ pArg = (Explicit,) <$> atom <|> (Implicit,) <$> braces typeExpr
 
 
 -- starter pack, but we'll move some to prelude
-operators : List (String, Int, Fixity)
+-- operators : List (String, Int, Fixity)
-operators = [
+-- operators = [
-  ("=",2,Infix),
+--   ("=",2,Infix),
-  ("+",4,InfixL),
+--   ("+",4,InfixL),
-  ("-",4,InfixL),
+--   ("-",4,InfixL),
-  ("*",5,InfixL),
+--   ("*",5,InfixL),
-  ("/",5,InfixL)
+--   ("/",5,InfixL)
-]
+-- ]
 
 parseApp : Parser Raw
 parseApp = do
@@ -111,12 +112,18 @@ parseOp = parseApp >>= go 0
       do
         fc <- getPos
         op <- token Oper
-        let Just (p,fix) = lookup op operators
+        ops <- getOps
-         | Nothing => fail "expected operator"
+        let op' = "_" ++ op ++ "_"
+        let Just (p,fix) = lookup op' ops
+          -- this is eaten, but we need `->` and `:=` to not be an operator to have fatal here
+         | Nothing => case op of
+          "->" => fail "no infix decl for \{op}"
+          ":=" => fail "no infix decl for \{op}"
+          op => fatal "no infix decl for \{op}"
         if p >= prec then pure () else fail ""
         let pr = case fix of InfixR => p; _ => p + 1
         right <- go pr !(parseApp)
-        go prec (RApp fc (RApp fc (RVar fc op) left Explicit) right Explicit)
+        go prec (RApp fc (RApp fc (RVar fc op') left Explicit) right Explicit)
       <|> pure left
 
 export
@@ -262,6 +269,18 @@ parseImport = DImport <$> getPos <* keyword "import" <* commit <*> uident
 
 -- Do we do pattern stuff now? or just name = lambda?
 
+parseMixfix : Parser Decl
+parseMixfix = do
+  fc <- getPos
+  fix <- InfixL <$ keyword "infixl"
+     <|> InfixR <$ keyword "infixr"
+     <|> Infix <$ keyword "infix"
+  mustWork $ do
+    prec <- token Number
+    op <- token MixFix
+    addOp op (cast prec) fix
+    pure $ PMixFix fc op (cast prec) fix
+
 export
 parseDef : Parser Decl
 parseDef = do
@@ -318,7 +337,7 @@ parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*
 
 export
 parseDecl : Parser Decl
-parseDecl = parsePType <|> parsePFunc <|> parseImport <|> parseNorm <|> parseData <|> parseSig <|> parseDef
+parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseImport <|> parseNorm <|> parseData <|> parseSig <|> parseDef
 
 export
 parseMod : Parser Module

src/Lib/Parser/Impl.idr

@@ -19,6 +19,12 @@ TokenList = List BTok
 public export
 data Fixity = InfixL | InfixR | Infix
 
+export
+Show Fixity where
+  show InfixL = "infixl"
+  show InfixR = "infixr"
+  show Infix = "infix"
+
 -- I was going to use a record, but we're peeling this off of bounds at the moment.
 public export
 FC : Type
@@ -54,27 +60,32 @@ showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ g
 -- Result of a parse
 public export
 data Result : Type -> Type where
-  OK : a -> (toks : TokenList) -> (com : Bool) -> Result a
+  OK : a -> (toks : TokenList) -> (com : Bool) -> List (String, Int, Fixity) -> Result a
-  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool)  -> Result a
+  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> List (String, Int, Fixity) -> Result a
 
 export
 Functor Result where
-  map f (OK a toks com ) = OK (f a) toks com
+  map f (OK a toks com ops) = OK (f a) toks com ops
-  map _ (Fail fatal err toks com) = Fail fatal err toks com
+  map _ (Fail fatal err toks com ops) = Fail fatal err toks com ops
 
 -- So sixty just has a newtype function here now (probably for perf).
 -- A record might be more ergonomic, but would require a record impl before
 -- self hosting.
 
--- We keep the line and column for indents. The idea being that we check
+-- FC is a line and column for indents. The idea being that we check
 -- either the col < tokCol or line == tokLine, enabling sameLevel.
 
--- dunno why I'm making that a pair..
+-- This is a Reader in FC
-export
+
-data Parser a = P (TokenList -> Bool -> (lc : FC) -> Result a)
+-- we need State for operators (or postpone that to elaboration)
+-- Since I've already built out the pratt stuff, I guess I'll
+-- leave it in the parser for now
 
 export
-runP : Parser a -> TokenList -> Bool -> FC -> Result a
+data Parser a = P (TokenList -> Bool -> List (String, Int, Fixity) -> (lc : FC) -> Result a)
+
+export
+runP : Parser a -> TokenList -> Bool -> List (String, Int, Fixity) -> FC -> Result a
 runP (P f) = f
 
 error : TokenList -> String -> Error
@@ -83,71 +94,80 @@ error ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (line,
 
 export
 parse : Parser a -> TokenList -> Either Error a
-parse pa toks = case runP pa toks False (-1,-1) of
+parse pa toks = case runP pa toks False [] (-1,-1) of
-  Fail fatal err toks com => Left err
+  Fail fatal err toks com ops => Left err
-  OK a [] _ => Right a
+  OK a [] _ _ => Right a
-  OK a ts _ => Left (error ts "Extra toks")
+  OK a ts _ _ => Left (error ts "Extra toks")
 
 -- I think I want to drop the typeclasses for v1
 
 export
 fail : String -> Parser a
-fail msg = P $ \toks,com,col => Fail False (error toks msg) toks com
+fail msg = P $ \toks,com,ops,col => Fail False (error toks msg) toks com ops
 
 export
 fatal : String -> Parser a
-fatal msg = P $ \toks,com,col => Fail False (error toks msg) toks com
+fatal msg = P $ \toks,com,ops,col => Fail True (error toks msg) toks com ops
 
 -- mustWork / commit copied from Idris, but I may switch to the parsec consumption thing.
 export
 mustWork : Parser a -> Parser a
-mustWork (P pa) = P $ \ toks, com, col => case (pa toks com col) of
+mustWork (P pa) = P $ \ toks, com, ops, col => case (pa toks com ops col) of
-    Fail x err xs y => Fail True err xs y
+    Fail x err xs y ops => Fail True err xs y ops
     res => res
 
+export
+getOps : Parser (List (String, Int, Fixity))
+getOps = P $ \ toks, com, ops, col => OK ops toks com ops
+
+export
+addOp : String -> Int -> Fixity -> Parser ()
+addOp nm prec fix = P $ \ toks, com, ops, col =>
+  OK () toks com ((nm, prec, fix) :: ops)
+
 export
 Functor Parser where
-  map f (P pa) = P $ \ toks, com, col => map f (pa toks com col)
+  map f (P pa) = P $ \ toks, com, ops, col => map f (pa toks com ops col)
 
 export
 Applicative Parser where
-  pure pa = P (\ toks, com, col => OK pa toks com)
+  pure pa = P (\ toks, com, ops, col => OK pa toks com ops)
-  P pab <*> P pa = P $ \toks,com,col =>
+  P pab <*> P pa = P $ \toks,com,ops,col =>
-    case pab toks com col of
+    case pab toks com ops col of
-      Fail fatal err toks com => Fail fatal err toks com
+      Fail fatal err toks com ops => Fail fatal err toks com ops
-      OK f toks com =>
+      OK f toks com ops =>
-        case pa toks com col of
+        case pa toks com ops col of
-          (OK x toks com) => OK (f x) toks com
+          (OK x toks com ops) => OK (f x) toks com ops
-          (Fail fatal err toks com) => Fail fatal err toks com
+          (Fail fatal err toks com ops) => Fail fatal err toks com ops
 
 -- REVIEW it would be nice if the second argument was lazy...
 export
 (<|>) : Parser a -> Lazy (Parser a) -> Parser a
-(P pa) <|> (P pb) = P $ \toks,com,col =>
+(P pa) <|> (P pb) = P $ \toks,com,ops,col =>
-  case pa toks False col of
+  case pa toks False ops col of
-    OK a toks' _ => OK a toks' com
+    OK a toks' _ ops => OK a toks' com ops
-    Fail True  err toks' com   => Fail True err toks' com
+    Fail True  err toks' com ops  => Fail True err toks' com ops
-    Fail fatal err toks' True  => Fail fatal err toks' com
+    Fail fatal err toks' True ops => Fail fatal err toks' com ops
-    Fail fatal err toks' False => pb toks com col
+    Fail fatal err toks' False ops => pb toks com ops col
 
 export
 Monad Parser where
-  P pa >>= pab = P $ \toks,com,col =>
+  P pa >>= pab = P $ \toks,com,ops,col =>
-    case pa toks com col of
+    case pa toks com ops col of
-      (OK a toks com) => runP (pab a) toks com col
+      (OK a toks com ops) => runP (pab a) toks com ops col
-      (Fail fatal err xs x) => Fail fatal err xs x
+      (Fail fatal err xs x ops) => Fail fatal err xs x ops
 
 
 -- do we need this?
 pred : (BTok -> Bool) -> String -> Parser String
-pred f msg = P $ \toks,com,col =>
+pred f msg = P $ \toks,com,ops,col =>
   case toks of
-    (t :: ts) => if f t then OK (value t) ts com else Fail False (error toks "\{msg} at \{show $ kind t}:\{value t}") toks com
+    (t :: ts) => if f t then OK (value t) ts com ops else Fail False (error toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops
-    [] => Fail False (error toks "\{msg} at EOF") toks com
+    [] => Fail False (error toks "\{msg} at EOF") toks com ops
 
 export
 commit : Parser ()
-commit = P $ \toks,com,col => OK () toks True
+commit = P $ \toks,com,ops,col => OK () toks True ops
 
 mutual
   export some : Parser a -> Parser (List a)
@@ -164,32 +184,31 @@ mutual
 -- withIndentationBlock - sets the col
 export
 getPos : Parser FC
-getPos = P $ \toks,com, (l,c) => case toks of
+getPos = P $ \toks,com, ops, (l,c) => case toks of
-  [] => OK emptyFC toks com
+  [] => OK emptyFC toks com ops
-  (t :: ts) => OK (start t) toks com
+  (t :: ts) => OK (start t) toks com ops
 
 ||| Start an indented block and run parser in it
 export
 startBlock : Parser a -> Parser a
-startBlock (P p) = P $ \toks,com,(l,c) => case toks of
+startBlock (P p) = P $ \toks,com,ops,(l,c) => case toks of
-  [] => p toks com (l,c)
+  [] => p toks com ops (l,c)
   (t :: _) =>
     -- If next token is at or before the current level, we've got an empty block
     let (tl,tc) = start t
-    in p toks com (tl,ifThenElse (tc <= c) (c + 1) tc)
+    in p toks com ops (tl,ifThenElse (tc <= c) (c + 1) tc)
-    -- in p toks com (tl,tc)
 
 ||| Assert that parser starts at our current column by
 ||| checking column and then updating line to match the current
 export
 sameLevel : Parser a -> Parser a
-sameLevel (P p) = P $ \toks,com,(l,c) => case toks of
+sameLevel (P p) = P $ \toks,com,ops,(l,c) => case toks of
-  [] => p toks com (l,c)
+  [] => p toks com ops (l,c)
   (t :: _) =>
     let (tl,tc) = start t
-    in if tc == c then p toks com (tl, c)
+    in if tc == c then p toks com ops (tl, c)
-    else if c < tc then Fail False (error toks "unexpected indent") toks com
+    else if c < tc then Fail False (error toks "unexpected indent") toks com ops
-    else Fail False (error toks "unexpected indent") toks com
+    else Fail False (error toks "unexpected indent") toks com ops
 
 export
 someSame : Parser a -> Parser (List a)
@@ -202,12 +221,12 @@ manySame pa = many $ sameLevel pa
 ||| requires a token to be indented?
 export
 indented : Parser a -> Parser a
-indented (P p) = P $ \toks,com,(l,c) => case toks of
+indented (P p) = P $ \toks,com,ops,(l,c) => case toks of
-  [] => p toks com (l,c)
+  [] => p toks com ops (l,c)
   (t::_) =>
     let (tl,tc) = start t
-    in if tc > c || tl == l then p toks com (l,c)
+    in if tc > c || tl == l then p toks com ops (l,c)
-    else Fail False (error toks "unexpected outdent") toks com
+    else Fail False (error toks "unexpected outdent") toks com ops
 
 export
 token' : Kind -> Parser String

src/Lib/ProcessDecl.idr

@@ -29,6 +29,9 @@ collectDecl (x :: xs) = x :: collectDecl xs
 
 export
 processDecl : Decl -> M ()
+
+processDecl (PMixFix{})  = pure ()
+
 processDecl (TypeSig fc nm tm) = do
   top <- get
   let Nothing := lookup nm top

src/Lib/Syntax.idr

@@ -104,6 +104,7 @@ data Decl
   | Data FC Name Raw (List Decl)
   | PType FC Name (Maybe Raw)
   | PFunc FC Name Raw String
+  | PMixFix FC Name Nat Fixity
 
 
 public export
@@ -143,6 +144,7 @@ Show Decl where
   show (DCheck _ x y) = foo ["DCheck", show x, show y]
   show (PType _ name ty) = foo ["PType", name, show ty]
   show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src]
+  show (PMixFix _ nm prec fix) = foo ["PMixFix", nm, show prec, show fix]
 
 export covering
 Show Module where
@@ -239,3 +241,4 @@ Pretty Module where
         doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
         doDecl (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
         doDecl (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
+        doDecl (PMixFix _ _ _ fix) = text (show fix)

src/Lib/Token.idr

@@ -10,6 +10,7 @@ data Kind
   | UIdent
   | Keyword
   | Oper
+  | MixFix
   | Number
   | StringKind
   | Symbol
@@ -28,6 +29,7 @@ Show Kind where
   show UIdent   = "UIdent"
   show Keyword = "Keyword"
   show Oper    = "Oper"
+  show MixFix = "MixFix"
   show Number  = "Number"
   show Symbol  = "Symbol"
   show Space  = "Space"
@@ -44,6 +46,7 @@ Eq Kind where
   UIdent  == UIdent = True
   Keyword == Keyword = True
   Oper    == Oper = True
+  MixFix  == MixFix = True
   Number  == Number = True
   Symbol  == Symbol = True
   Space   == Space = True

src/Lib/Tokenizer.idr

@@ -5,7 +5,8 @@ import Text.Lexer.Tokenizer
 import Lib.Token
 
 keywords : List String
-keywords = ["let", "in", "where", "case", "of", "data", "U", "ptype", "pfunc", "module"]
+keywords = ["let", "in", "where", "case", "of", "data", "U",
+            "ptype", "pfunc", "module", "infixl", "infixr", "infix"]
 
 specialOps : List String
 specialOps = ["->", ":", "=>", ":="]
@@ -49,9 +50,11 @@ rawTokens
   <|> match (upper <+> many identMore) checkUKW
   <|> match (some digit) (Tok Number)
   <|> match (is '#' <+> many alpha) (Tok Pragma)
+  <|> match (exact "_" <+> (some opChar <|> exact ",") <+> exact "_") (Tok MixFix)
   <|> match (quo <+> manyUntil quo ((esc any <+> any) <|> any) <+> opt quo) (Tok StringKind . unquote)
   <|> match (lineComment (exact "--")) (Tok Space)
   <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space)
+  <|> match (exact ",") (\s => Tok Oper s)
   <|> match (some opChar) (\s => Tok Oper s)
   <|> match symbol (Tok Symbol)
   <|> match spaces (Tok Space)

tests/black/oper.newt

@@ -0,0 +1,41 @@
+module Oper
+
+-- These are hard-coded at the moment
+-- For now they must be of the form _op_, we'll circle back
+-- with a different parser, but that works today.
+
+-- this will be parsed as a top level decl, collected in TopContext, and
+-- injected into the Parser. It'll need to be passed around or available
+-- for read in the monad.
+
+-- long term, I might want TopContext in the parser, and parse a top-level
+-- declaration at a time (for incremental updates), but much longer term.
+
+infixl 4 _+_
+infixl 4 _-_
+infixl 5 _*_
+infixl 5 _/_
+
+ptype Int
+ptype String
+ptype JVoid
+
+-- If we had a different quote here, we could tell vscode it's javascript.
+-- or actually just switch modes inside pfunc
+pfunc log : String -> JVoid := "(x) => console.log(x)"
+pfunc plus : Int -> Int -> Int := "(x,y) => x + y"
+pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
+
+-- We now have to clean JS identifiers
+_+_ : Int -> Int -> Int
+_+_ x y = plus x y
+
+test : Int -> Int
+test x = 42 + x * 3 + 2
+
+infixr 2 _,_
+data Pair : U -> U -> U where
+  _,_ : {A B : U} -> A -> B -> Pair A B
+
+blah : Int -> Int -> Int -> Pair Int (Pair Int Int)
+blah x y z = (x , y, z)