cleanup

TODO.md

@@ -17,6 +17,7 @@
   - [ ] Duplicate data constructors point to `data`
   - [ ] Allow Qualified names in surface syntax
   - Don't disambiguate on type for now
+  - [ ] Could we disambiguate just Data constructors on type?
 - [x] change "in prefix position" and "trailing operator" errors to do sections
 - [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly
   - There may be ambiguity issues at the parsing level, but we don't have typecase, so.

src/Lib/Elab.newt

@@ -636,10 +636,8 @@ freshMeta ctx fc ty kind = do
   -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
   pure $ applyBDs 0 (Meta fc qn) ctx.bds
   where
-    -- hope I got the right order here :)
     applyBDs : Int -> Tm -> List BD -> Tm
     applyBDs k t Nil = t
-    -- review the order here
     applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k)
     applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs
 
@@ -1353,32 +1351,33 @@ showDef ctx names n v = do
   pure "= \{vv}"
 
 -- desugar do
-undo : FC -> List DoStmt -> M Raw
+undo : List DoStmt -> M Raw
-undo prev Nil = error prev "do block must end in expression"
+-- Should be unreachable in practice
-undo prev ((DoExpr fc tm) :: Nil) = pure tm
+undo Nil = error emptyFC "do block must end in expression"
--- TODO decide if we want to use >> or just >>=
+undo ((DoExpr fc tm) :: Nil) = pure tm
-undo prev ((DoExpr fc tm) :: xs) = do
+undo (tm :: Nil) = error (getFC tm) "do block must end in expression"
-  xs' <- undo fc xs
+undo ((DoExpr fc tm) :: xs) = do
-  -- output is bigger, not sure if it helps inference or not
+  xs' <- undo xs
+  -- Not sure if it helps inference or not (and now fails with erasure thing)
   -- pure $ RApp fc (RApp fc (RVar fc "_>>_") tm Explicit) xs' Explicit
-  pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit
+  pure $ RApp fc (RApp fc (RVar fc "bind") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit
-undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs
+undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs
-undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
+undo ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
   top <- getTop
   case lookupRaw nm top of
     Just _ => do
       let nm = "$sc"
-      xs' <- undo fc xs
+      xs' <- undo xs
       rest <- pure $ RCase fc (RVar fc nm) Nothing (MkAlt left (Just xs') :: Nil)
       pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
         (RLam fc (BI fc nm Explicit Many) rest) Explicit
     Nothing => do
-      xs' <- undo fc xs
+      xs' <- undo xs
       pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
         (RLam fc (BI fc' nm Explicit Many) xs') Explicit
-undo prev ((DoArrow fc left right alts) :: xs) = do
+undo ((DoArrow fc left right alts) :: xs) = do
   let nm = "$sc"
-  xs' <- undo fc xs
+  xs' <- undo xs
   rest <- pure $ RCase fc (RVar fc nm) Nothing (MkAlt left (Just xs') :: alts)
   pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
     (RLam fc (BI fc nm Explicit Many) rest) Explicit
@@ -1453,8 +1452,8 @@ check ctx tm ty = do
       let tm' = RCase fc a Nothing (MkAlt (RVar (getFC b) "True") (Just b) :: MkAlt (RVar (getFC c) "False") (Just c)  :: Nil) in
       check ctx tm' ty
     (RDo fc stmts, ty) => do
-      stmts' <- undo fc stmts
+      body <- undo stmts
-      check ctx stmts' ty
+      check ctx body ty
     (RCase fc rsc mty alts, ty) => do
       (sc, scty) <- case mty of
         Nothing => infer ctx rsc
@@ -1537,7 +1536,6 @@ check ctx tm ty = do
 
     (tm, ty) => do
       (tm', ty') <- infer ctx tm
-      -- REVIEW - should we look at `tm` to know how many to insert? Is there a case where this helps?
       (tm', ty') <- insert ctx tm' ty'
 
       let names = map fst ctx.types

src/Lib/Erasure.newt

@@ -96,8 +96,7 @@ erase env t sp = case t of
   (Bnd fc k) => do
     case getAt (cast k) env of
       Nothing => error fc "bad index \{show k}"
-      -- This is working, but empty FC
+      Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here - see Elab.lookupName)"
-      Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)"
       Just (nm, Many, ty) => eraseSpine env t sp ty
   (UU fc) => eraseSpine env t sp (Just $ UU fc)
   (Lit fc lit) => eraseSpine env t sp Nothing

src/Lib/Syntax.newt

@@ -35,6 +35,11 @@ data DoStmt : U where
   DoLet : (fc : FC) -> String -> Raw -> DoStmt
   DoArrow : (fc : FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt
 
+instance HasFC DoStmt where
+  getFC (DoExpr fc _) = fc
+  getFC (DoArrow fc _ _ _) = fc
+  getFC (DoLet fc _ _) = fc
+
 Decl : U
 data Raw : U where
   RVar : (fc : FC) -> (nm : Name) -> Raw

src/Prelude.newt

@@ -3,7 +3,7 @@ module Prelude
 id : ∀ a. a → a
 id x = x
 
-the : (a : U) → a → a
+the : (0 a : U) → a → a
 the _ a = a
 
 const : ∀ a b. a → b → a