From 26ed1355f598be70db1fdb89bf89231f6eaf713b Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 7 Sep 2024 10:55:51 -0700 Subject: [PATCH] case statement fixes --- src/Lib/Check.idr | 77 ++++++++++++++++++++------------------------- src/Lib/Compile.idr | 2 -- src/Lib/TT.idr | 1 - src/Lib/Types.idr | 15 +-------- 4 files changed, 35 insertions(+), 60 deletions(-) diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index db9025e..529ddca 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -23,7 +23,7 @@ data Pden = PR Nat Nat (List Nat) forceMeta : Val -> M Val forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of (Unsolved pos k xs) => pure (VMeta fc ix sp) - (Solved k t) => vappSpine t sp + (Solved k t) => vappSpine t sp >>= forceMeta forceMeta x = pure x -- Lennart needed more forcing for recursive nat, @@ -57,9 +57,12 @@ parameters (ctx: Context) where go : SnocList Val -> List Nat -> M (List Nat) go [<] acc = pure $ reverse acc - go (xs :< VVar emptyFC k [<]) acc = do + go (xs :< VVar fc k [<]) acc = do if elem k acc - then error emptyFC "non-linear pattern" + then do + debug "\{show k} \{show acc}" + + error fc "non-linear pattern" else go xs (k :: acc) go _ _ = error emptyFC "non-variable in pattern" @@ -87,11 +90,8 @@ parameters (ctx: Context) 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) + -- for now, we don't do solutions with case in them. 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) go ren lvl (VLit fc lit) = pure (Lit fc lit) go ren lvl (VLet fc {}) = error fc "rename Let not implemented" @@ -134,16 +134,23 @@ parameters (ctx: Context) (VLam _ _ t, VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) (t, VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) (VLam fc _ t, t' ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<]) - (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l a a' <+> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<]) |] - (VVar fc k sp, VVar fc' k' sp' ) => + (VMeta fc k sp, VMeta fc' k' sp' ) => if k == k' then unifySpine l (k == k') sp sp' - else error emptyFC "vvar mismatch \{show k} \{show k'}" + else solve l k sp (VMeta fc' k' sp') >> pure neutral + (t, VMeta fc' i' sp') => solve l i' sp' t >> pure neutral + (VMeta fc i sp, t' ) => solve l i sp t' >> pure neutral + (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l a a' <+> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<]) |] + (VVar fc k sp, (VVar fc' k' sp') ) => + if k == k' then unifySpine l (k == k') sp sp' + else if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] + -- else error ctx.fc "unify error: vvar mismatch \{show k} \{show k'} \{show ctx.env}" -- attempt at building constraints -- and using them (VVar fc k sp, u) => case lookupVar k of Just v => unify l v u Nothing => pure $ MkResult[(k, u)] + (t, VVar fc k sp) => pure $ MkResult[(k, t)] (VRef fc k def sp, VRef fc' k' def' sp' ) => @@ -153,11 +160,6 @@ parameters (ctx: Context) -- REVIEW - consider forcing? else error emptyFC "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" - (VMeta fc k sp, VMeta fc' k' sp' ) => - if k == k' then unifySpine l (k == k') sp sp' - else solve l k sp (VMeta fc' k' sp') >> pure neutral - (t, VMeta fc' i' sp') => solve l i' sp' t >> pure neutral - (VMeta fc i sp, t' ) => solve l i sp t' >> pure neutral (VU _, VU _) => pure neutral -- Lennart.newt cursed type references itself -- We _could_ look up the ref, eval against [] and vappSpine... @@ -201,33 +203,17 @@ insert ctx tm ty = do insert ctx (App emptyFC tm m) !(b $$ mv) va => pure (tm, va) --- lookupName : Context -> Raw -> M (Maybe (Tm, Val)) --- lookupName ctx (RVar fc 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 def) => pure $ Just (Ref fc nm def, !(eval [] CBN ty)) --- Nothing => pure Nothing --- go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd fc i, ty) --- else go (i + 1) xs --- lookupName ctx _ = pure Nothing - - primType : FC -> String -> M Val primType fc nm = case lookup nm !(get) of Just (MkEntry name ty PrimTCon) => pure $ VRef fc name PrimTCon [<] _ => error fc "Primitive type \{show nm} not in scope" - export infer : Context -> Raw -> M (Tm, Val) export check : Context -> Raw -> Val -> M Tm - - - data Bind = MkBind String Icit Val Show Bind where @@ -309,13 +295,13 @@ extendPi ctx ty nms = pure (ctx, ty, nms <>> []) updateContext : Context -> List (Nat, Val) -> M Context updateContext ctx [] = pure ctx updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in - pure $ {env $= makeLet ix} ctx + pure $ {env $= replace ix val, bds $= replace ix Defined } ctx where - makeLet : Nat -> Env -> Env - makeLet _ [] = ?nothing_to_update - makeLet 0 ((VVar fc j [<]) :: xs) = val :: xs - makeLet 0 (_ :: xs) = ?not_a_var - makeLet (S k) (x :: xs) = x :: makeLet k xs + replace : Nat -> a -> List a -> List a + replace k x [] = [] + replace 0 x (y :: xs) = x :: xs + replace (S k) x (y :: xs) = y :: replace k x xs + -- ok, so this is a single constructor, CaseAlt -- since we've gotten here, we assume it's possible and we better have at least @@ -345,7 +331,9 @@ buildCase ctx prob scnm scty (dcName, _, ty) = do -- this puts the failure on the LHS -- unifying these should say say VVar 1 is Nat. -- ERROR at (23, 0): unify failed (%var 1 [< ]) =?= (%ref Nat [< ]) [no Fn] - res <- unify ctx' (length ctx.env) ty' scty + debug "unify dcon dom with scrut" + res <- unify ctx' (length ctx'.env) ty' scty + --res <- unify ctx' (length ctx.env) ty' scty debug "scty \{show scty}" debug "UNIFY results \{show res.constraints}" debug "before types: \{show ctx'.types}" @@ -496,15 +484,15 @@ check ctx tm ty = case (tm, !(forceType ty)) of let scnm = fresh "sc" -- FIXME FC let clauses = map (\(MkAlt pat rawRHS) =>MkClause fc [(scnm, pat)] [] rawRHS ) alts + + -- buildCase expects scrutinee to be a name in the context because + -- it's compared against the first part of Constraint. We could switch + -- to a level and only let if the scrutinee is not a var. let ctx' = extend ctx scnm scty cons <- getConstructors ctx' scty alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons - -- BROKEN, need scnm in scope for real. ctx' promises it, but we don't have a binder here - - pure $ Let fc scnm sc $ Case fc (Bnd fc 0) alts - -- buildTree ctx (MkProb{}) -- ?hole -- Document a hole, pretend it's implemented @@ -519,7 +507,10 @@ 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 emptyFC "?" Axiom -- TODO - probably want hole opt on Def + -- TODO mark this meta as a user hole + -- freshMeta ctx fc + pure $ Ref fc "?" Axiom + (t@(RLam fc nm icit tm), ty@(VPi fc' nm' icit' a b)) => do debug "icits \{nm} \{show icit} \{nm'} \{show icit'}" if icit == icit' then do diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index f1e1ec6..feb916c 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -60,8 +60,6 @@ mkEnv nm k env (x :: xs) = mkEnv nm (S k) (Dot (Var nm) "h\{show k}" :: env) xs envNames : Env -> List String --- If I was golfing, I'd be tempted to stick with deBruijn - ||| given a name, find a similar one that doesn't shadow in Env fresh : String -> JSEnv -> String fresh nm env = if free env nm then nm else go nm 1 diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index f1065d4..7a626d3 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -67,7 +67,6 @@ lookupMeta ix = do go (meta@(Unsolved _ k ys) :: xs) = if k == ix then pure meta else go xs go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs - export partial Show Context where show ctx = "Context \{show $ map fst $ ctx.types}" diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 2b557a9..eb0debe 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -147,8 +147,8 @@ Eq (Tm) where (Pi _ n icit t u) == (Pi _ n' icit' t' u') = icit == icit' && t == t' && u == u' _ == _ = False --- FIXME prec +||| Pretty printer for Tm. export pprint : List String -> Tm -> String pprint names tm = render 80 $ go names tm @@ -176,19 +176,6 @@ pprint names tm = render 80 $ go names tm go names (Lit _ lit) = text "\{show lit}" go names (Let _ nm t u) = text "let" <+> text nm <+> ":=" <+> go names t (nest 2 $ go names u) -public export -Pretty Tm where - pretty (Bnd _ k) = ?rhs_0 - pretty (Ref _ str mt) = text str - pretty (Meta _ k) = text "?m\{show k}" - pretty (Lam _ str t) = text "(\\ \{str} => " <+> pretty t <+> ")" - 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 PRETTY CASE" - pretty (Lit _ lit) = text (show lit) - pretty (Let _ _ _ _) = text "LET" - -- public export -- data Closure : Nat -> Type data Val : Type