case checking partially working

README.md

@@ -1,6 +1,20 @@
 
 We're stopping at zoo4.
 
+- [ ] empty data is broken when followed by a function, need to check that new indent level is deeper
+
+Going ahead with data. scratch.newt for starters, build out enough for plus to typecheck. See where we are at that point, and fix up the dependent stuff. Add another test case that exercises this.
+
+v1 of cases requires a constructor and vars, var, or default.
+
+When we do impossible, take agda approach
+
+- [ ] typecheck plus
+  - [ ] checkAlt
+  - [ ] process data decl should check some stuff
+- [ ] switch to FC
+
+- [ ] think about whether there needs to be a desugar step separate from check/infer
 
 - [ ] look into Lennart.newt issues
 - [ ] Type at point for the editor
@@ -11,7 +25,7 @@ We're stopping at zoo4.
   - [ ] Read data as real constructors
   - [ ] Typecheck / eval the same
   - [ ] Add elimination / case
-    - [ ] Maybe some test cases from pi-forall
+    - [ ] test cases. Maybe from pi-forall
 - [ ] Code Gen
 - [ ] Less expansion
   - Can we not expand top level - expand in unification and matching pi types?

newt/test1.newt

@@ -4,5 +4,6 @@ nat : U
 nat = {C : U} -> C -> (nat -> C) -> C
 
 -- TESTCASE This was broken when I wasn't expanding Ref ty in check
+-- Also broken when I tried to put Def in VRef
 succ : nat -> nat
 succ = \n => \ z s => s n

newt/testcase.newt

@@ -0,0 +1,21 @@
+module Scratch
+
+
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Vect : Nat -> U -> U where
+  Nil : {a : U} -> Vect Z a
+  Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a
+
+plus : Nat -> Nat -> Nat
+plus = \ n m => case n of
+  Z => m
+  S k => S (plus k m)
+
+length : {a : U} {n : Nat} -> Vect n a -> Nat
+length = \ v => case v of
+  Nil => Z
+  Cons x xs => S (length {a} xs)

src/Lib/Check.idr

@@ -26,12 +26,12 @@ forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
   (Solved k t) => vappSpine t sp
 forceMeta x = pure x
 
--- Lennart needed more forcing
+-- Lennart needed more forcing for recursive nat,
 forceType : Val -> M Val
-forceType (VRef nm sp) =
+forceType (VRef nm def sp) =
     case lookup nm !(get) of
-      (Just (MkEntry name type (Fn t))) => eval [] CBN t
+      (Just (MkEntry name type (Fn t))) => vappSpine !(eval [] CBN t) sp
-      _ => pure (VRef nm sp)
+      _ => pure (VRef nm def sp)
 forceType (VMeta ix sp) = case !(lookupMeta ix) of
   (Unsolved x k xs) => pure (VMeta ix sp)
   (Solved k t) => vappSpine t sp >>= forceType
@@ -67,7 +67,7 @@ parameters (ctx: Context)
       go ren lvl (VVar k sp) = case findIndex (== k) ren of
         Nothing => error [DS "scope/skolem thinger"]
         Just x => goSpine ren lvl (Bnd $ cast x) sp
-      go ren lvl (VRef nm sp) = goSpine ren lvl (Ref nm Nothing) sp
+      go ren lvl (VRef nm def sp) = goSpine ren lvl (Ref nm def) sp
       go ren lvl (VMeta ix sp) = if ix == meta
         then error [DS "meta occurs check"]
         else goSpine ren lvl (Meta ix) sp
@@ -113,7 +113,7 @@ parameters (ctx: Context)
       (VVar k sp,   VVar k' sp'  ) =>
         if k == k' then unifySpine l (k == k') sp sp'
         else error [DS "vvar mismatch \{show k} \{show k'}"]
-      (VRef k sp,   VRef k' sp'  ) =>
+      (VRef k def sp,   VRef k' def' sp'  ) =>
         if k == k' then unifySpine l (k == k') sp sp'
         -- REVIEW - consider forcing?
         else error [DS "vref mismatch \{show k} \{show k'}"]
@@ -125,7 +125,7 @@ parameters (ctx: Context)
       (VU, VU) => pure ()
       -- Lennart.newt cursed type references itself
       -- We _could_ look up the ref, eval against [] and vappSpine...
-      (t,         VRef k' sp') => do
+      (t,         VRef k' def sp') => do
         debug "expand \{show t} =?= %ref \{k'}"
         case lookup k' !(get) of
           Just (MkEntry name ty (Fn tm)) => unify l t !(vappSpine !(eval [] CBN tm) sp')
@@ -155,8 +155,7 @@ lookupName ctx (RVar nm) = go 0 ctx.types
   where
     go : Nat -> Vect n (String, Val)  -> M  (Maybe (Tm, Val))
     go i [] = case lookup nm !(get) of
-      Just (MkEntry name ty (Fn t)) => pure $ Just (Ref nm (Just t), !(eval [] CBN ty))
+      Just (MkEntry name ty def) => pure $ Just (Ref nm def, !(eval [] CBN ty))
-      Just (MkEntry name ty _) => pure $ Just (Ref nm Nothing, !(eval [] CBN ty))
       Nothing => pure Nothing
     go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd i, ty)
       else go (i + 1) xs
@@ -169,14 +168,84 @@ infer : Context -> Raw  -> M  (Tm, Val)
 export
 check : Context -> Raw -> Val  -> M  Tm
 
+-- FIXME we need to switch to FC
 
+checkAlt : Val -> Context -> Val -> RCaseAlt -> M CaseAlt
+checkAlt scty ctx ty (MkAlt ptm body) = do
+  -- we have a pattern term and a body
+  (con, args) <- getArgs ptm []
+  debug "ALT con \{con} args \{show args}"
+  let Just (MkEntry _ dcty (DCon arity _)) = lookup con !(get)
+    | _ => error [DS "expected datacon, got \{con}"]
+
+  -- arity is wrong, but we actually need the type anyway
+  -- in fact arity is for later (eval?) and we need to do implicits first
+  debug "arity is \{show arity} dcty \{pprint [] dcty}"
+  -- and then we run the names against the type
+  -- get all that into a context and run the body
+
+  -- So, how does this work?
+  -- The constructor has arguments
+  -- they may or may not be bound to names.
+  -- their types may depend on nameless arguments
+  -- the RHS is a function of some or all of this
+
+  -- I suspect I'll rewrite this a few times
+  vdcty <- eval [] CBN dcty
+  debug "go \{show vdcty} \{show ptm}"
+  alttm <- go vdcty ptm ctx
+  debug "GOT \{pprint (names ctx) alttm}"
+
+  -- package up the results into something.
+  -- REVIEW args, also probably want the tag not the name.
+  pure $ CaseCons con args alttm
+
+  where
+
+    go : Val -> Raw -> Context -> M Tm
+    go ctype (RSrcPos x tm) ctx = go ctype tm ctx
+    -- FIXME icit
+    go (VPi str Explicit a b) (RApp t (RSrcPos _ (RVar nm)) Explicit) ctx = do
+      debug "*** \{nm} : \{show a}"
+      let var = VVar (length ctx.env) [<]
+      let ctx' = extend ctx nm a
+      Lam nm <$> go !(b $$ var) t ctx'
+    go (VPi str Implicit a b) t ctx = do
+      let var = VVar (length ctx.env) [<]
+      let ctx' = extend ctx "_" a
+      Lam "_" <$> go !(b $$ var) t ctx'
+    -- same deal with _ for name
+    go (VPi str icit x y) (RApp t RImplicit icit') ctx = ?rhs_19
+    go (VPi str icit x y) tm ctx = error {ctx} [DS "Can't use \{show tm} as pattern"]
+
+    -- nameless variable
+    go ctype RImplicit ctx = ?rhs_2
+    go ctype (RVar nm) ctx = do
+      debug "*** end"
+      check ctx body ty
+      -- pure ctx -- this should be our constructor.
+    -- This happens if we run out of runway (more args and no pi)
+    go ctype tm ctx = error {ctx} [DS "unhandled in go \{show ctype} \{show tm}"]
+
+    getArgs : Raw -> List String -> M (String, List String)
+    getArgs (RVar nm) acc = pure (nm, acc)
+    -- TODO implicits
+    getArgs (RApp t (RSrcPos _ (RVar nm)) icit) acc = getArgs t (nm :: acc)
+    getArgs (RApp t (RVar nm) icit) acc = getArgs t (nm :: acc)
+    getArgs (RApp t RHole icit) acc = getArgs t ("_" :: acc)
+    getArgs (RSrcPos _ t) acc = getArgs t acc
+    getArgs tm _ = error [DS "Patterns must be constructor and vars, got \{show 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}"]
+    let (VRef nm (TCon cnames) sp) = scty
+      | _ => error [DS "expected TCon for scrutinee type, got: \{show scty}"]
+    debug "constructor names \{show cnames}"
+    alts' <- for alts $ checkAlt scty ctx ty
+    pure $ Case sc alts'
+    -- 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
@@ -190,7 +259,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     -- need to print 'warning' with position
     -- fixme - just put a name on it like idris and stuff it into top.
     -- error [DS "hole:\n\{msg}"]
-    pure $ Ref "?" Nothing
+    pure $ Ref "?" Axiom  -- TODO - probably want hole opt on Def
   (t@(RLam nm icit tm), ty@(VPi nm' icit' a b)) => do
           debug "icits \{nm} \{show icit} \{nm'} \{show icit'}"
           if icit == icit' then do
@@ -238,8 +307,9 @@ infer ctx (RVar nm) = go 0 ctx.types
   where
     go : Nat -> Vect n (String, Val)  -> M  (Tm, Val)
     go i [] = case lookup nm !(get) of
-      Just (MkEntry name ty (Fn t)) => pure (Ref nm (Just t), !(eval [] CBN ty))
+      Just (MkEntry name ty def) => do
-      Just (MkEntry name ty _) => pure (Ref nm Nothing, !(eval [] CBN ty))
+        debug "lookup \{name} as \{show def}"
+        pure (Ref nm def, !(eval [] CBN ty))
       Nothing => error [DS "\{show nm} not in scope"]
     go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty)
       else go (i + 1) xs

src/Lib/Parser.idr

@@ -147,7 +147,7 @@ pPattern
   <|> PatVar <$> ident
 
 
-caseAlt : Parser CaseAlt
+caseAlt : Parser RCaseAlt
 caseAlt = do
   pat <- parseOp -- pPattern -- term and sort it out later?
   keyword "=>"
@@ -258,7 +258,7 @@ parseDecl = parseImport <|> parseSig <|> parseDef <|> parseNorm <|> parseData
 export
 parseMod : Parser Module
 parseMod = do
-  sameLevel $ keyword "module"
+  keyword "module"
   name <- ident
   -- probably should be manySame, and we want to start with col -1
   -- if we enforce blocks indent more than parent

src/Lib/Parser/Impl.idr

@@ -76,7 +76,7 @@ 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 emptyPos of
+parse pa toks = case runP pa toks False (-1,-1) of
   Fail fatal err toks com => Left err
   OK a [] _ => Right a
   OK a ts _ => Left (error ts "Extra toks")
@@ -167,8 +167,10 @@ startBlock : Parser a -> Parser a
 startBlock (P p) = P $ \toks,com,(l,c) => case toks of
   [] => p toks com (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,tc)
+    in p toks com (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

src/Lib/ProcessDecl.idr

@@ -45,7 +45,7 @@ processDecl (Def nm raw) = 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}"
-
+  debug "Add def \{nm} \{pprint [] tm} : \{pprint [] ty}"
   put (addDef ctx nm tm ty)
 
 processDecl (DCheck tm ty) = do

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 Raw Raw
+data RCaseAlt = MkAlt Raw Raw
 
 data Raw : Type where
   RVar : (nm : Name) -> Raw
@@ -38,7 +38,7 @@ data Raw : Type where
   RSrcPos : SourcePos -> Raw -> Raw
   RAnn  : (tm : Raw) -> (ty : Raw) -> Raw
   RLit : Literal -> Raw
-  RCase : (scrut : Raw) -> (alts : List CaseAlt) -> Raw
+  RCase : (scrut : Raw) -> (alts : List RCaseAlt) -> Raw
   RImplicit : Raw
   RHole : Raw
   -- not used, but intended to allow error recovery
@@ -114,7 +114,7 @@ Show Pattern where
   show (PatLit x) = foo ["PatLit" , show x]
 
 covering
-Show CaseAlt where
+Show RCaseAlt where
   show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
 
 covering

src/Lib/TT.idr

@@ -117,7 +117,7 @@ export
 vapp : Val -> Val -> M Val
 vapp (VLam _ t) u = t $$ u
 vapp (VVar k sp) u = pure $ VVar k (sp :< u)
-vapp (VRef nm sp) u = pure $ VRef nm (sp :< u)
+vapp (VRef nm def sp) u = pure $ VRef nm def (sp :< u)
 vapp (VMeta k sp) u = pure $ VMeta k (sp :< u)
 vapp t u = error' "impossible in vapp \{show t} to \{show u}"
 
@@ -129,11 +129,19 @@ vappSpine t (xs :< x) = vapp !(vappSpine t xs) x
 bind : Val -> Env -> Env
 bind v env = v :: env
 
+-- So smalltt says:
+--   Smalltt has the following approach:
+--   - Top-level and local definitions are lazy.
+--   - We instantiate Pi types during elaboration with lazy values.
+--   - Applications headed by top-level variables are lazy.
+--   - Any other function application is call-by-value during evaluation.
+
 -- Do we want a def in here instead?  We'll need DCon/TCon eventually
 -- I need to be aggressive about reduction, I guess. I'll figure it out
 -- later, maybe need lazy glued values.
-eval env mode (Ref x (Just tm)) = eval env mode tm
+-- TODO - probably want to figure out gluing and handle constructors
-eval env mode (Ref x Nothing) = pure $ VRef x [<]
+eval env mode (Ref x (Fn tm)) = eval env mode tm
+eval env mode (Ref x def) = pure $ VRef x def [<]
 eval env mode (App t u) = vapp !(eval env mode t) !(eval env mode u)
 eval env mode U = pure VU
 eval env mode (Meta i) =
@@ -145,6 +153,7 @@ eval env mode (Pi x icit a b) = pure $ VPi x icit !(eval env mode a) (MkClosure
 eval env mode (Bnd i) = case getAt i env of
   Just rval => pure rval
   Nothing => error' "Bad deBruin index \{show i}"
+eval env mode (Case{}) = ?todo
 
 export
 quote : (lvl : Nat) -> Val -> M Tm
@@ -162,7 +171,7 @@ quote l (VMeta i sp) = quoteSp l (Meta i) sp
 quote l (VLam x t) = pure $ Lam x !(quote (S l) !(t $$ VVar l [<]))
 quote l (VPi x icit a b) = pure $ Pi x icit !(quote l a) !(quote (S l) !(b $$ VVar l [<]))
 quote l VU = pure U
-quote l (VRef n sp) = quoteSp l (Ref n Nothing) sp
+quote l (VRef n def sp) = quoteSp l (Ref n def) sp
 
 -- Can we assume closed terms?
 -- ezoo only seems to use it at [], but essentially does this:

src/Lib/TopContext.idr

@@ -44,8 +44,12 @@ public export
 addDef : TopContext -> String -> Tm -> Tm -> TopContext
 addDef tc name tm ty = { defs $= go } tc
   where
+  -- What did I do here?
     go : List TopEntry -> List TopEntry
     -- FIXME throw if we hit [] or is not an axiom
-    go [] = []
+    -- FIXME use a map, I want updates
-    go ((MkEntry nm _ _) :: xs) = MkEntry nm ty (Fn tm) :: xs
+    go [] = ?addDEF_fail
+    go (x@(MkEntry nm _ _) :: xs) = if nm == name
+      then MkEntry nm ty (Fn tm) :: xs
+      else x :: go xs
 

src/Lib/Types.idr

@@ -42,10 +42,21 @@ Show BD where
   show Defined = "def"
 
 public export
+data Tm : Type
+
+public export
+data CaseAlt : Type where
+  CaseDefault : Tm -> CaseAlt
+  -- I've also seen a list of stuff that gets replaced
+  CaseCons : (name : String) -> (args : List String) -> Tm ->  CaseAlt
+  -- CaseLit : Literal -> Tm ->  CaseAlt
+
+data Def : Type
+
 data Tm : Type where
   Bnd : Nat -> Tm
   -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
-  Ref : String -> Maybe Tm -> Tm
+  Ref : String -> Def -> Tm
   Meta : Nat -> Tm
   -- kovacs optimization, I think we can App out meta instead
   -- InsMeta : Nat -> List BD -> Tm
@@ -53,9 +64,14 @@ data Tm : Type where
   App : Tm -> Tm -> Tm
   U   : Tm
   Pi  : Name -> Icit -> Tm -> Tm -> Tm
+  -- REVIEW - do we want to just push it up like idris?
+  Case : Tm -> List CaseAlt -> Tm
 
 %name Tm t, u, v
 
+Show CaseAlt where
+  show alt = "FIXME"
+
 -- public export
 Show Tm where
   show (Bnd k) = "(Bnd \{show k})"
@@ -66,6 +82,7 @@ Show Tm where
   show U = "U"
   show (Pi str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
   show (Pi str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
+  show (Case sc alts) = "(Case \{show sc} \{show alts})"
 
 -- I can't really show val because it's HOAS...
 
@@ -107,6 +124,7 @@ pprint names tm = render 80 $ go names tm
       text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "=>" <+> go (nm :: names) u <+> ")"
     go names (Pi nm Explicit t u) =
       text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")"
+    go names (Case _ _) = "FIXME CASE"
 
 public export
 Pretty Tm where
@@ -117,6 +135,7 @@ Pretty Tm where
   pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
   pretty U = "U"
   pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")"
+  pretty (Case _ _) = text "FIXME CASE"
 
 -- public export
 -- data Closure : Nat -> Type
@@ -143,11 +162,11 @@ data Val : Type where
   VVar : (k : Nat) -> (sp : SnocList Val) -> Val
   -- I wanted the Maybe Tm in here, but for now we're always expanding.
   -- Maybe this is where I glue
-  VRef : (nm : String) -> (sp : SnocList Val) -> Val
+  VRef : (nm : String) -> Def -> (sp : SnocList Val) -> Val
   -- we'll need to look this up in ctx with IO
   VMeta : (ix : Nat) -> (sp : SnocList Val) -> Val
   VLam : Name -> Closure -> Val
-  VPi : Name -> Icit -> Lazy Val -> Closure -> Val
+  VPi : Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val
   VU : Val
 
 
@@ -156,7 +175,7 @@ Show Closure
 covering export
 Show Val where
   show (VVar k sp) = "(%var \{show k} \{show sp})"
-  show (VRef nm sp) = "(%ref \{nm} \{show sp})"
+  show (VRef nm _ sp) = "(%ref \{nm} \{show sp})"
   show (VMeta ix sp) = "(%meta \{show ix} \{show sp})"
   show (VLam str x) = "(%lam \{str} \{show x})"
   show (VPi str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
@@ -233,6 +252,7 @@ record MetaContext where
 public export
 data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm
 
+public export
 Show Def where
   show Axiom = "axiom"
   show (TCon strs) = "TCon \{show strs}"