From 067a83960dae4ba8ce21a74800d5f835fb40baf2 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Fri, 2 Aug 2024 21:39:39 -0700
Subject: [PATCH] checkpoint before case

---
 src/Lib/Check.idr       | 11 ++++++++++-
 src/Lib/Parser.idr      |  2 +-
 src/Lib/ProcessDecl.idr | 21 ++++++++++++---------
 src/Lib/Syntax.idr      |  3 ++-
 src/Lib/TopContext.idr  | 10 ++++++++++
 src/Lib/Types.idr       |  4 ++--
 6 files changed, 37 insertions(+), 14 deletions(-)

diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 56084b2..6e42d35 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -168,7 +168,15 @@ infer : Context -> Raw  -> M  (Tm, Val)
 
 export
 check : Context -> Raw -> Val  -> M  Tm
+
+
+
+checkAlt : Context -> CaseAlt -> M ()
+
 check ctx tm ty = case (tm, !(forceType ty)) of
+  (RCase rsc alts, ty) => do
+    (sc, scty) <- infer ctx rsc
+    error [DS "implement check RCase sctype \{show scty}"]
   (RSrcPos x tm, ty) => check ({pos := x} ctx) tm ty
   -- Document a hole, pretend it's implemented
   (RHole, ty) => do
@@ -298,6 +306,7 @@ infer ctx tm = error [DS "Implement infer \{show tm}"]
 -- infer ctx (RLit (LInt i)) = ?rhs_11
 -- infer ctx (RLit (LBool x)) = ?rhs_12
 -- infer ctx (RCase tm xs) = ?rhs_9
--- infer ctx RImplicit = ?todo_meta2
+
 -- The idea here is to insert a hole for a parse error
+-- but the parser doesn't emit this yet.
 -- infer ctx (RParseError str) = ?todo_insert_meta
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index d931ba7..145dd7f 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -149,7 +149,7 @@ pPattern
 
 caseAlt : Parser CaseAlt
 caseAlt = do
-  pat <- pPattern -- term and sort it out later?
+  pat <- parseOp -- pPattern -- term and sort it out later?
   keyword "=>"
   commit
   t <- term
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 0eedf70..f41ea64 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -20,7 +20,6 @@ processDecl (TypeSig nm tm) = do
   putStrLn "got \{pprint [] ty'}"
   modify $ claim nm ty'
 
--- FIXME - this should be in another file
 processDecl (Def nm raw) = do
   putStrLn "-----"
   putStrLn "def \{show nm}"
@@ -43,6 +42,7 @@ processDecl (Def nm raw) = do
   for_ mc.metas $ \case
     (Solved k x) => pure ()
     (Unsolved (l,c) k xs) => do
+      -- should just print, but it's too subtle in the sea of messages
       -- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}"
       throwError $ E (l,c) "Unsolved meta \{show k}"
 
@@ -71,21 +71,24 @@ processDecl (Data nm ty cons) = do
   -- It seems like the FC for the errors are not here?
   ctx <- get
   tyty <- check (mkCtx ctx.metas) ty VU
-  -- TODO check tm is VU or Pi ending in VU
-  -- Maybe a pi -> binders function
-  -- TODO we're putting in axioms, we need constructors
-  -- for each constructor, check and add
+  -- FIXME we need this in scope, but need to update
   modify $ claim nm tyty
   ctx <- get
-  for_ cons $ \x => case x of
+  cnames <- for cons $ \x => case x of
       -- expecting tm to be a Pi type
       (TypeSig nm' tm) => do
           ctx <- get
           -- TODO check pi type ending in full tyty application
+          -- TODO count arity
           dty <- check (mkCtx ctx.metas) tm VU
-          modify $ claim nm' dty
-      _ => throwError $ E (0,0) "expected TypeSig"
-
+          modify $ defcon nm' 0 nm dty
+          pure nm'
+      _ => throwError $ E (0,0) "expected constructor declaration"
+  -- TODO check tm is VU or Pi ending in VU
+  -- Maybe a pi -> binders function
+  -- TODO we're putting in axioms, we need constructors
+  -- for each constructor, check and add
+  modify $ deftype nm tyty cnames
   pure ()
   where
     checkDeclType : Tm -> M ()
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index 59fb0dd..3abdb01 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -25,7 +25,7 @@ data Pattern
 
 -- could be a pair, but I suspect stuff will be added?
 public export
-data CaseAlt = MkAlt Pattern Raw
+data CaseAlt = MkAlt Raw Raw
 
 data Raw : Type where
   RVar : (nm : Name) -> Raw
@@ -113,6 +113,7 @@ Show Pattern where
   show PatWild = "PatWild"
   show (PatLit x) = foo ["PatLit" , show x]
 
+covering
 Show CaseAlt where
   show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
 
diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr
index 55363b4..3e5cb73 100644
--- a/src/Lib/TopContext.idr
+++ b/src/Lib/TopContext.idr
@@ -28,6 +28,16 @@ public export
 claim : String -> Tm -> TopContext -> TopContext
 claim name ty = { defs $= (MkEntry name ty Axiom ::) }
 
+
+public export
+deftype : String -> Tm -> List String -> TopContext -> TopContext
+deftype name ty cons = { defs $= (MkEntry name ty (TCon cons) :: )}
+
+public export
+defcon : String -> Nat -> String -> Tm -> TopContext -> TopContext
+defcon cname arity tyname ty = { defs $= (MkEntry cname ty (DCon arity tyname) ::) }
+
+
 -- TODO update existing, throw, etc.
 
 public export
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 75a167b..b359d4b 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -231,12 +231,12 @@ record MetaContext where
 
 
 public export
-data Def = Axiom | TCon (List String) | DCon Nat | Fn Tm
+data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm
 
 Show Def where
   show Axiom = "axiom"
   show (TCon strs) = "TCon \{show strs}"
-  show (DCon k) = "DCon \{show k}"
+  show (DCon k tyname) = "DCon \{show k} \{show tyname}"
   show (Fn t) = "Fn \{show t}"
 
 ||| entry in the top level context