From 086f3d654158b46735f8d7a1d2198fdf72761af8 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 14 Sep 2024 19:46:15 -0700
Subject: [PATCH] matching on mixfix

---
 TODO.md                 | 11 ++++++++---
 newt/oper.newt          |  3 +--
 src/Lib/Check.idr       |  2 +-
 src/Lib/Parser.idr      | 29 +++++++++++++++++++++++++++--
 src/Lib/ProcessDecl.idr | 31 ++++++++++++++++++++++++++++++-
 src/Lib/Syntax.idr      |  7 ++-----
 src/Lib/Tokenizer.idr   |  2 +-
 7 files changed, 70 insertions(+), 15 deletions(-)

diff --git a/TODO.md b/TODO.md
index b94ac0b..719255d 100644
--- a/TODO.md
+++ b/TODO.md
@@ -14,14 +14,17 @@ I may be done with `U` - I keep typing `Type`.
 - [x] operators
 - [x] pair syntax (via comma operator)
 - [ ] matching on operators
+  - [x] top level
+  - [ ] case statements   ********
 - [x] SKIP list syntax
   - Agda doesn't have it, clashes with pair syntax
 - [ ] import
 - [ ] autos / typeclass resolution
-  - 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
-  - have separate type of implict with `{{}}`
   - Can we solve right away when creating the implicit, or do we need postpone?
+  - options
+    - 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
+    - have separate type of implict with `{{}}`
 - [ ] do blocks
 - [ ] some solution for `+` problem (classes? ambiguity?)
 - [ ] show compiler failure in the editor (exit code != 0)
@@ -38,3 +41,5 @@ I may be done with `U` - I keep typing `Type`.
 - [ ] magic tuple? (codegen as array)
 - [ ] magic newtype? (drop in codegen)
 - [ ] records / copatterns
+
+- [ ] Read Ulf Norell thesis
diff --git a/newt/oper.newt b/newt/oper.newt
index 6e4164e..4517ee9 100644
--- a/newt/oper.newt
+++ b/newt/oper.newt
@@ -41,5 +41,4 @@ blah : Int -> Int -> Int -> Pair Int (Pair Int Int)
 blah x y z = (x, y, z)
 
 curryPlus : Pair Int Int -> Int
-curryPlus (_,_ a b) = a + b
--- curryPlus (a , b) = a + b
+curryPlus (a, b) = a + b
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 3e2e91b..14ff404 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -520,7 +520,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of
   (RHole fc, ty) => do
     ty' <- quote ctx.lvl ty
     let names = (toList $ map fst ctx.types)
-    -- I want to know which ones are defines. I should skip the `=` bit if they match
+    -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
     env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure "  \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}"
     let msg = unlines (toList $ reverse env) ++ "  -----------\n" ++ "  goal \{pprint names ty'}"
     putStrLn "INFO at \{show fc}: "
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 5c0cea1..06d93f6 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -258,16 +258,41 @@ parseMixfix = do
   addOp op (cast prec) fix
   pure $ PMixFix fc op (cast prec) fix
 
+-- We can be much more precise with a context
+raw2pat : Raw -> SnocList Pattern -> M Pattern
+raw2pat (RVar x nm) sp = ?rhs_1
+raw2pat (RApp x t u icit) sp = ?rhs_3
+raw2pat (RHole x) sp = ?rhs_11
+raw2pat (RU x) sp = ?rhs_4
+raw2pat (RLit x y) sp = ?rhs_8
+
+raw2pat (RLam x nm icit ty) sp = ?rhs_2
+raw2pat (RPi x nm icit ty sc) sp = ?rhs_5
+raw2pat (RLet x nm ty v sc) sp = ?rhs_6
+raw2pat (RAnn x tm ty) sp = ?rhs_7
+raw2pat (RCase x scrut alts) sp = ?rhs_9
+raw2pat (RImplicit x) sp = ?rhs_10
+raw2pat (RParseError x str) sp = ?rhs_12
+
+
+getName : Raw -> Parser String
+getName (RVar x nm) = pure nm
+getName (RApp x t u icit) = getName t
+getName tm = fail "bad LHS"
+
+
 export
 parseDef : Parser Decl
 parseDef = do
   fc <- getPos
-  nm <- ident <|> uident
+  t <- typeExpr
+  nm <- getName t
+  -- nm <- ident <|> uident
   pats <- many patAtom
   keyword "="
   body <- typeExpr
   -- these get collected later
-  pure $ Def fc nm [MkClause fc [] pats body]
+  pure $ Def fc nm [(t, body)] -- [MkClause fc [] t body]
 
 export
 parsePType : Parser Decl
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 19fa9dd..6b1edc4 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -27,6 +27,33 @@ collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
   else (Def fc nm cl :: collectDecl rest)
 collectDecl (x :: xs) = x :: collectDecl xs
 
+makeClause : TopContext -> (Raw, Raw) -> M Clause
+makeClause top (lhs, rhs) = do
+  let (nm, args) = splitArgs lhs []
+  pats <- traverse mkPat args
+  pure $ MkClause (getFC lhs) [] pats rhs
+  where
+
+    splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit))
+    splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args)
+    splitArgs tm args = (tm, args)
+
+    mkPat : (Raw, Icit) -> M Pattern
+    mkPat (tm, icit) = do
+      case splitArgs tm [] of
+        ((RVar fc nm), b) => case lookup nm top of
+                    (Just (MkEntry name type (DCon k str))) =>
+                      -- TODO check arity, also figure out why we need reverse
+                      pure $ PatCon fc icit nm !(traverse mkPat b)
+                    Just _ => error (getFC tm) "not a data constructor"
+                    Nothing => case b of
+                                    [] => pure $ PatVar fc icit nm
+                                    _ => error (getFC tm) "patvar applied to args"
+        ((RImplicit fc), []) => pure $ PatWild fc icit
+        ((RImplicit fc), _) => error fc "implicit pat can't be applied"
+        -- ((RLit x y), b) => ?rhs_19
+        (a,b) => error (getFC a) "expected pat var or constructor"
+
 export
 processDecl : Decl -> M ()
 
@@ -69,7 +96,9 @@ processDecl (Def fc nm clauses) = do
   vty <- eval empty CBN ty
   putStrLn "vty is \{show vty}"
 
-  tm <- buildTree (mkCtx ctx.metas fc) (MkProb clauses vty)
+  -- I can take LHS apart syntactically or elaborate it with an infer
+  clauses' <- traverse (makeClause ctx) clauses
+  tm <- buildTree (mkCtx ctx.metas fc) (MkProb clauses' vty)
   putStrLn "Ok \{pprint [] tm}"
   tm' <- zonk ctx 0 [] tm
   putStrLn "NF \{pprint[] tm'}"
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index 47da00c..7f26c46 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -98,7 +98,7 @@ data Decl : Type where
 
 data Decl
   = TypeSig FC Name Raw
-  | Def FC Name (List Clause)
+  | Def FC Name (List (Raw,Raw)) -- (List Clause)
   | DImport FC Name
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
@@ -231,10 +231,7 @@ Pretty Module where
       where
         doDecl : Decl -> Doc
         doDecl (TypeSig _ nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
-        doDecl (Def _ nm clauses) = spread $ map doClause clauses
-          where
-            doClause : Clause -> Doc
-            doClause (MkClause fc _ pats body) = text nm <+> spread (map pretty pats) <+> text "=" <+> nest 2 (pretty body)
+        doDecl (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> "=" <+> pretty b) clauses
         doDecl (DImport _ nm) = text "import" <+> text nm ++ line
         -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
         doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index 3d32ddc..47a6204 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -9,7 +9,7 @@ keywords = ["let", "in", "where", "case", "of", "data", "U",
             "ptype", "pfunc", "module", "infixl", "infixr", "infix"]
 
 specialOps : List String
-specialOps = ["->", ":", "=>", ":="]
+specialOps = ["->", ":", "=>", ":=", "="]
 
 checkKW : String -> Token Kind
 checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s