From f6e47c8d22d09ae73f843c790a9e8c652da3d1fc Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 22 Aug 2024 13:33:16 -0700 Subject: [PATCH] more work on case --- README.md | 70 +++++++++++++++++++++++++++++++++++++++-- newt/testcase.newt | 8 +++++ src/Lib/Check.idr | 8 ++++- src/Lib/CompileExp.idr | 8 +---- src/Lib/ProcessDecl.idr | 23 +++++++++----- src/Lib/TT.idr | 31 +++++++++++++++++- src/Lib/Types.idr | 4 +++ src/Lib/Util.idr | 36 +++++++++++++++++++++ 8 files changed, 169 insertions(+), 19 deletions(-) create mode 100644 src/Lib/Util.idr diff --git a/README.md b/README.md index b217d95..07e3229 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,48 @@ -We're stopping at zoo4 for now. +Need eval for case. -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. +Need to typecheck case - learning stuff like `n = S k` is not happening and the final bit of the data constructor doesn't unify with the data type, because we're not handling `Bnd n =?= Val`. Cockx collects a list of constraints. We might want flags on unification to enable that? -Compiling to js including data. +I may want to collect a telescope instead of a type. + +Cockx lecture suggests something about going backwards. I'm thinking unifying the codomain of the DCon with the type of the TCon will give us some constraints like `n =?= S k`. + + +Cockx paper ยง5.2 builds type-correct case trees. It doesn't have indicies, but they can be mapped to additional equality arguments. We can follow suit, or try to do the translation on the fly. + +Proceed by: + +context is snoc, telescope is cons + +- [x] Add eval for case + - These are just neutral for now +- [x] Check data constructors + - I'm checking pi type, then checking codomain is application of appropriate type constructor +- [ ] Build case trees (Section 5.2) + Write this for a function, but start with `case` statement and singleton list. We'll end up with a longer list when we hit `Just x :: xs` etc. + Then add + +- [ ] Add primitives +- [ ] Compile and run something +- [ ] Add modules + +- [ ] Start translating self? v1 of cases requires a constructor and vars, var, or default. +narya has a `with_loc` + +> with_loc loc f runs the thunk f with loc as the new default location for val:emit and val:fatal. Note that with_loc None will clear the current default location, while merge_loc None will keep it. See val:merge_loc. + +So it's using ocaml `algaeff` package, with a reader effect for the location. I think it's accumulating a stack of them. Additionally `asai` has functions to emit messages that can pick up the location from context. + +This is interesting in that we could include location in context or the monad for cases where we have an error say unifying, and want to know what we were processing when it happened (either instead of or in addition to reporting some FC of the terms being unified). + +## Now + +- Eval case +- constraints from case + ### Main - [x] flag for debug? @@ -58,6 +94,7 @@ Code generation is partially done. before this (we could pull out default case too) - [ ] Javascript operators / primitives - [x] Don't do assign var to fresh var +- [ ] Write output file ### Parsing / Language @@ -70,6 +107,11 @@ Code generation is partially done. - [ ] Type at point for the editor +### Unification + +We're stopping at zoo4 for now. + + ### Typecheck / Elaboration - [ ] think about whether there needs to be a desugar step separate from check/infer @@ -77,6 +119,7 @@ Code generation is partially done. - [ ] Less expansion - Look at smallTT rules - Can we not expand top level - expand in unification and matching pi types? + - should the environment be lazy? - [ ] look into Lennart.newt issues - [ ] figure out how to add laziness (might have to be via the monad) @@ -165,3 +208,24 @@ Forward: pi-forall sticks equality into scope as something like let. Not sure if this is compatible with deBruijn. Possibly if we have everything at elab time? But if `x = y` then previous stuff has a different `x`? + + +## Dep Ty Check + +### pi-forall + +unify returns a list of Entry, but "either term is "ambiguous" (i.e. neutral), give up and succeed with an empty list" seems wrong. fine for case refinement I guess, but wrong for conversion checking? I suppose conv check could look for `[]`. + +TODO find out what it does for conv checking + +### idris / tiny idris + +TODO how does idris mnage this? + + +### narya + +TODO how does narya handle it? + +Mybe a Conor paper or a Cockx paper would also shed some light. And do ny "tutorial implementation" handle if properly? + diff --git a/newt/testcase.newt b/newt/testcase.newt index a8f4362..42ba0bc 100644 --- a/newt/testcase.newt +++ b/newt/testcase.newt @@ -13,6 +13,14 @@ plus = \ n m => case n of Z => m S k => S (plus k m) +-- Example from Jesper talk (translated to case tree) +max : Nat -> Nat -> Nat +max = \ n m => case n of + Z => m + S k => case m of + Z => S k + S l => S (max k l) + -- So this isn't working at the moment, I think I need -- to replace the n with S k -- diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 9acfb6f..6bf3af9 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -69,11 +69,17 @@ parameters (ctx: Context) Just x => goSpine ren lvl (Bnd fc $ cast x) sp go ren lvl (VRef fc nm def sp) = goSpine ren lvl (Ref fc nm def) sp go ren lvl (VMeta fc ix sp) = if ix == meta - then error emptyFC "meta occurs check" + -- REVIEW is this the right fc? + then error fc "meta occurs check" else goSpine ren lvl (Meta fc ix) sp go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar emptyFC lvl [<]))) go ren lvl (VPi fc n icit ty tm) = pure (Pi fc n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) go ren lvl (VU fc) = pure (U fc) + go ren lvl (VCase fc sc alts) = error fc "Case in solution" + -- This seems dicey, for VLam we eval and then process the levels. + -- Here we have raw Tm so we haven't even done occurs check. I'm thinking + -- we don't allow solutions with Case in them + -- pure (Case fc !(go ren lvl sc) alts) lams : Nat -> Tm -> Tm lams 0 tm = tm diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index f5386b1..9e90db8 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -9,6 +9,7 @@ import Data.List import Lib.Types -- Name / Tm import Lib.TopContext import Lib.TT -- lookupMeta +import Lib.Util public export data CExp : Type @@ -31,13 +32,6 @@ data CExp : Type where CRef : Name -> CExp CMeta : Nat -> CExp -funArgs : Tm -> (Tm, List Tm) -funArgs tm = go tm [] - where - go : Tm -> List Tm -> (Tm, List Tm) - go (App _ t u) args = go t (u :: args) - go t args = (t, args) - ||| I'm counting Lam in the term for arity. This matches what I need in ||| code gen. export diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 4954a05..010ff1b 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -2,19 +2,19 @@ module Lib.ProcessDecl import Data.IORef -import Lib.Types -import Lib.Parser -import Lib.TT -import Lib.TopContext import Lib.Check +import Lib.Parser import Lib.Syntax +import Lib.TopContext +import Lib.TT +import Lib.Types +import Lib.Util getArity : Tm -> Nat getArity (Pi x str icit t u) = S (getArity u) -- Ref or App (of type constructor) are valid getArity _ = Z - -- Can metas live in context for now? export @@ -84,10 +84,19 @@ processDecl (Data fc nm ty cons) = do -- expecting tm to be a Pi type (TypeSig fc nm' tm) => do ctx <- get - -- TODO check pi type ending in full tyty application - -- TODO count arity dty <- check (mkCtx ctx.metas) tm (VU fc) debug "dty \{nm'} is \{pprint [] dty}" + + -- We only check that codomain uses the right type constructor + -- We know it's in U because it's part of a checked Pi type + let (codomain, tele) = splitTele dty + -- for printing + let tnames = reverse $ map (\(MkBind _ nm _ _) => nm) tele + let (Ref _ hn _, args) := funArgs codomain + | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}" + when (hn /= nm) $ + error (getFC codomain) "Constructor codomain is \{pprint tnames codomain} rather than \{nm}" + modify $ setDef nm' dty (DCon (getArity dty) nm) pure nm' _ => throwError $ E (0,0) "expected constructor declaration" diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index 9d93ca3..068b8f3 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -106,6 +106,8 @@ lookup ctx nm = go ctx.types export eval : Env -> Mode -> Tm -> M Val + + -- REVIEW everything is evalutated whether it's needed or not -- It would be nice if the environment were lazy. -- e.g. case is getting evaluated when passed to a function because @@ -130,6 +132,24 @@ vappSpine : Val -> SnocList Val -> M Val vappSpine t [<] = pure t vappSpine t (xs :< x) = vapp !(vappSpine t xs) x +-- So we need: +-- - a Neutral case statement +-- - split out data / type constructors from VRef application +-- - should we sort out what the case tree really looks like first? + +-- Technically I don't need this now, as a neutral would be fine. + +evalAlt : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val) +-- FIXME spine length? Should this be VRef or do we specialize? +evalAlt env mode (VRef _ nm y sp) ((CaseCons name args t) :: xs) = + if nm == name + -- Here we bind the args and push on. Do we have enough? Too many? + then ?evalAlt_success + -- here we need to know if we've got a mismatched constructor or some function app + else ?evalAlt_what +evalAlt env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u) +evalAlt env mode sc _ = pure Nothing -- stuck + bind : Val -> Env -> Env bind v env = v :: env @@ -154,16 +174,24 @@ eval env mode (Meta fc i) = (Solved k t) => pure $ t eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t) eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b) +-- Here, we assume env has everything. We push levels onto it during type checking. +-- I think we could pass in an l and assume everything outside env is free and +-- translate to a level eval env mode (Bnd fc i) = case getAt i env of Just rval => pure rval Nothing => error' "Bad deBruin index \{show i}" -- We need a neutral and some code to run the case tree -eval env mode tm@(Case{}) = ?todo_eval_case + +eval env mode tm@(Case fc sc alts) = pure $ VCase fc !(eval env mode sc) alts + -- case !(evalAlt env mode !(eval env mode sc) alts) of + -- Just foo => ?goodAlt + -- Nothing => ?stuckAlt export quote : (lvl : Nat) -> Val -> M Tm + quoteSp : (lvl : Nat) -> Tm -> SnocList Val -> M Tm quoteSp lvl t [<] = pure t quoteSp lvl t (xs :< x) = @@ -178,6 +206,7 @@ quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<]) quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<])) quote l (VU fc) = pure (U fc) quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp +quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts -- Can we assume closed terms? -- ezoo only seems to use it at [], but essentially does this: diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index d64e21a..5c29199 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -180,6 +180,8 @@ data Val : Type where -- I wanted the Maybe Tm in here, but for now we're always expanding. -- Maybe this is where I glue VRef : FC -> (nm : String) -> Def -> (sp : SnocList Val) -> Val + -- neutral case + VCase : FC -> (sc : Val) -> List CaseAlt -> Val -- we'll need to look this up in ctx with IO VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val VLam : FC -> Name -> Closure -> Val @@ -187,6 +189,7 @@ data Val : Type where VU : FC -> Val + Show Closure covering export @@ -197,6 +200,7 @@ Show Val where show (VLam _ str x) = "(%lam \{str} \{show x})" show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show x}}. \{show y})" show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show x}). \{show y})" + show (VCase fc sc alts) = "(%case \{show sc} ...)" show (VU _) = "U" -- Not used - I was going to change context to have a List Binder diff --git a/src/Lib/Util.idr b/src/Lib/Util.idr new file mode 100644 index 0000000..add817c --- /dev/null +++ b/src/Lib/Util.idr @@ -0,0 +1,36 @@ +module Lib.Util + +import Lib.Types + +export +funArgs : Tm -> (Tm, List Tm) +funArgs tm = go tm [] + where + go : Tm -> List Tm -> (Tm, List Tm) + go (App _ t u) args = go t (u :: args) + go t args = (t, args) + + +public export +data Binder : Type where + MkBind : FC -> String -> Icit -> Tm -> Binder + +-- I don't have a show for terms without a name list +export +Show Binder where + show (MkBind _ nm icit t) = "[\{nm} \{show icit} : ...]" + +data Foo : Type -> Type where + MkFoo : Nat -> Foo a + +export +splitTele : Tm -> (Tm, List Binder) +splitTele = go [] + where + go : List Binder -> Tm -> (Tm, List Binder) + go ts (Pi fc nm icit t u) = go (MkBind fc nm icit t :: ts) u + go ts tm = (tm, reverse ts) + + +-- splitTele (Pi x str icit t u) = ?splitTele_rhs_6 +-- splitTele tm =