From 09227e444a69fd452aa4628a35b638d6301ac9c2 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 4 Aug 2024 15:46:43 -0700 Subject: [PATCH] case checking partially working --- README.md | 16 ++++++- newt/test1.newt | 1 + newt/testcase.newt | 21 +++++++++ src/Lib/Check.idr | 98 +++++++++++++++++++++++++++++++++++------ src/Lib/Parser.idr | 4 +- src/Lib/Parser/Impl.idr | 6 ++- src/Lib/ProcessDecl.idr | 2 +- src/Lib/Syntax.idr | 6 +-- src/Lib/TT.idr | 17 +++++-- src/Lib/TopContext.idr | 8 +++- src/Lib/Types.idr | 28 ++++++++++-- 11 files changed, 174 insertions(+), 33 deletions(-) create mode 100644 newt/testcase.newt diff --git a/README.md b/README.md index 600446c..da1f71c 100644 --- a/README.md +++ b/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? diff --git a/newt/test1.newt b/newt/test1.newt index adbdba3..526b4e7 100644 --- a/newt/test1.newt +++ b/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 diff --git a/newt/testcase.newt b/newt/testcase.newt new file mode 100644 index 0000000..da5d41a --- /dev/null +++ b/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) diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 6e42d35..7e96bf2 100644 --- a/src/Lib/Check.idr +++ b/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 - _ => pure (VRef nm sp) + (Just (MkEntry name type (Fn t))) => vappSpine !(eval [] CBN t) 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 _) => pure $ Just (Ref nm Nothing, !(eval [] CBN ty)) + Just (MkEntry name ty def) => pure $ Just (Ref nm def, !(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 _) => pure (Ref nm Nothing, !(eval [] CBN ty)) + Just (MkEntry name ty def) => do + 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 diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 145dd7f..49d657e 100644 --- a/src/Lib/Parser.idr +++ b/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 diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 98d3c03..9c58b57 100644 --- a/src/Lib/Parser/Impl.idr +++ b/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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index f41ea64..8231ba8 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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 diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 3abdb01..03fa2a1 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 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 diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index 4a7f82a..35379f4 100644 --- a/src/Lib/TT.idr +++ b/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 -eval env mode (Ref x Nothing) = pure $ VRef x [<] +-- TODO - probably want to figure out gluing and handle constructors +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: diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index 3e5cb73..97b32bc 100644 --- a/src/Lib/TopContext.idr +++ b/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 [] = [] - go ((MkEntry nm _ _) :: xs) = MkEntry nm ty (Fn tm) :: xs + -- FIXME use a map, I want updates + go [] = ?addDEF_fail + go (x@(MkEntry nm _ _) :: xs) = if nm == name + then MkEntry nm ty (Fn tm) :: xs + else x :: go xs diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index b359d4b..76dc668 100644 --- a/src/Lib/Types.idr +++ b/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}"