add comments, fix fc on an error, add constructor for U

TODO.md

@@ -1,6 +1,8 @@
 
 ## TODO
 
+- [ ] review pattern matching. goal is to have a sane context on the other end. secondary goal - bring it closer to the paper.
+
 - [x] redo code to determine base path
 - [ ] save/load results of processing a module
   - [ ] keep each module separate in context

port/Lib/Elab.newt

@@ -951,7 +951,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
     makeConstr : List Bind -> List Pattern -> M (List (String × Pattern))
     makeConstr Nil Nil = pure $ Nil
     -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$>
-    makeConstr Nil (pat :: pats) = error ctx.ctxFC "too many patterns"
+    makeConstr Nil (pat :: pats) = error (getFC pat) "too many patterns"
     makeConstr ((MkBind nm Implicit x) :: xs) Nil = do
       rest <- makeConstr xs Nil
       pure $ (nm, PatWild emptyFC Implicit) :: rest
@@ -1017,19 +1017,21 @@ splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args)
 splitArgs tm args = (tm, args)
 
 
-mkPat : TopContext -> (Raw × Icit) -> M Pattern
+mkPat : (Raw × Icit) -> M Pattern
-mkPat top (RAs fc as tm, icit) = do
+mkPat (RAs fc as tm, icit) = do
-  pat <- mkPat top (tm, icit)
+
+  pat <- mkPat (tm, icit)
   case pat of
     (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
     (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}"
     t => error fc "Can't put as on non-constructor \{show tm}"
-mkPat top (tm, icit) = do
+mkPat (tm, icit) = do
+  top <- get
   case splitArgs tm Nil of
     ((RVar fc nm), b) => case lookupRaw nm top of
                 (Just (MkEntry _ name type (DCon k str))) => do
                   -- TODO check arity, also figure out why we need reverse
-                  bpat <- traverse (mkPat top) b
+                  bpat <- traverse (mkPat) b
                   pure $ PatCon fc icit name bpat Nothing
                 -- This fires when a global is shadowed by a pattern var
                 -- Just _ => error (getFC tm) "\{show nm} is not a data constructor"
@@ -1044,10 +1046,10 @@ mkPat top (tm, icit) = do
 
 
 
-makeClause : TopContext -> (Raw × Raw) -> M Clause
+makeClause : (Raw × Raw) -> M Clause
-makeClause top (lhs, rhs) = do
+makeClause (lhs, rhs) = do
   let (nm, args) = splitArgs lhs Nil
-  pats <- traverse (mkPat top) args
+  pats <- traverse mkPat args
   pure $ MkClause (getFC lhs) Nil pats rhs
 
 
@@ -1069,7 +1071,7 @@ checkWhere ctx decls body ty = do
   unless (name == name') $ \ _ => error defFC "Expected def for \{name}"
   -- REVIEW is this right, cribbed from my top level code
   top <- get
-  clauses' <- traverse (makeClause top) clauses
+  clauses' <- traverse makeClause clauses
   vty <- eval ctx.env CBN funTy
   debug $ \ _ => "\{name} vty is \{show vty}"
   let ctx' = extend ctx name vty
@@ -1087,7 +1089,7 @@ checkWhere ctx decls body ty = do
   ty' <- checkWhere ctx' decls' body ty
   pure $ LetRec sigFC name funTy tm ty'
 
-
+-- checks the body after we're done with a case tree branch
 checkDone : Context -> List (String × Pattern) -> Raw -> Val -> M Tm
 checkDone ctx Nil body ty = do
   debug $ \ _ => "DONE-> check body \{show body} at \{show ty}"
@@ -1264,6 +1266,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
         (Unsolved _ k xs _ _ _) => do
           top <- get
           mc <- readIORef top.metaCtx
+          -- TODO - only hit the relevant ones
           ignore $ solveAutos 0
           forceType ctx.env scty'
 
@@ -1277,6 +1280,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
       -- default cases
       cons <- getConstructors ctx (getFC pat) scty'
       debug $ \ _ => "CONS \{show $ map fst cons}"
+      -- TODO collect the wild-card only cases into one
       alts <- traverse (buildCase ctx prob scnm scty') cons
       debug $ \ _ => "GOTALTS \{show alts}"
       when (length' (mapMaybe id alts) == 0) $ \ _ => error (fc) "no alts for \{show scty'}"
@@ -1353,7 +1357,7 @@ check ctx tm ty = do
       top <- get
       clauses <- for alts $ \case
         (MkAlt pat rawRHS) => do
-          pat' <- mkPat top (pat, Explicit)
+          pat' <- mkPat (pat, Explicit)
           pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS
       -- buildCase expects scrutinee to be a name in the context, so we need to let it.
       -- if it's a Bnd and not shadowed we could skip the let, but that's messy.

port/Lib/ProcessDecl.newt

@@ -139,7 +139,7 @@ processDecl ns  (PFunc fc nm used ty src) = do
     _ => pure MkUnit
   setDef (QN ns nm) fc ty' (PrimFn src used)
 
-processDecl ns (Def fc nm claused) = do
+processDecl ns (Def fc nm clauses) = do
   putStrLn "-----"
   putStrLn "Def \{show nm}"
   top <- get
@@ -155,16 +155,16 @@ processDecl ns (Def fc nm claused) = do
 
   debug $ \ _ => "\{nm} vty is \{show vty}"
 
-
   -- I can take LHS apart syntactically or elaborate it with an infer
-  claused' <- traverse (makeClause top) claused
+  clauses' <- traverse makeClause clauses
-  tm <- buildTree (mkCtx fc) (MkProb claused' vty)
+  tm <- buildTree (mkCtx fc) (MkProb clauses' vty)
   -- putStrLn "Ok \{render 90 $ pprint Nil tm}"
 
   mc <- readIORef top.metaCtx
   let mlen = length' mc.metas - mstart
   solveAutos mstart
   -- TODO - make nf that expands all metas and drop zonk
+  -- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure.
   -- Day1.newt is a test case
   -- tm' <- nf Nil tm
   tm' <- zonk top 0 Nil tm

src/Lib/Elab.idr

@@ -889,11 +889,9 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
 
     makeConstr : List Bind -> List Pattern -> M (List (String, Pattern))
     makeConstr [] [] = pure $ []
-    -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$>
+    makeConstr [] (pat :: pats) = error (getFC pat) "too many patterns"
-    makeConstr [] (pat :: pats) = error ctx.ctxFC "too many patterns"
     makeConstr ((MkBind nm Implicit x) :: xs) [] = pure $ (nm, PatWild emptyFC Implicit) :: !(makeConstr xs [])
     makeConstr ((MkBind nm Auto x) :: xs) [] = pure $ (nm, PatWild emptyFC Auto) :: !(makeConstr xs [])
-    -- FIXME need a proper error, but requires wiring M three levels down
     makeConstr ((MkBind nm Explicit x) :: xs) [] = error ctx.ctxFC "not enough patterns"
     makeConstr ((MkBind nm Explicit x) :: xs) (pat :: pats) =
       if getIcit pat == Explicit

src/Main.idr

@@ -55,8 +55,9 @@ writeSource fn = do
   docs <- compile
   let src = unlines $
         [ "\"use strict\";"
-        ,  "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" ]
+        , "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })"
-        ++ map (render 90) docs
+        , "const U = { tag: \"U\" };"
+        ] ++ map (render 90) docs
   Right _ <- writeFile fn src
     | Left err => fail (show err)
   Right _ <- chmodRaw fn 493 | Left err => fail (show err)