From 6baee23a73537c18f303427efbde8f451aac5dd9 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 2 Nov 2024 18:20:46 -0800 Subject: [PATCH] addZero now works distinguish two modes of unification while pattern matching we return constraints on variables, and normally we are more aggressive about evaluating when matching against a variable. fixes to `let` surface #check in vscode --- newt/Combinatory.newt | 35 ++++++++++++++++-- newt/Debug.newt | 36 ++++++++++++++++++ src/Lib/Elab.idr | 77 ++++++++++++++++++++++----------------- src/Lib/Eval.idr | 8 +++- src/Lib/ProcessDecl.idr | 22 +++++++---- src/Lib/Tokenizer.idr | 2 +- src/Lib/Types.idr | 8 +++- tests/black/CaseEval.newt | 5 ++- 8 files changed, 144 insertions(+), 49 deletions(-) create mode 100644 newt/Debug.newt diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt index 9bf5578..15781e6 100644 --- a/newt/Combinatory.newt +++ b/newt/Combinatory.newt @@ -26,8 +26,8 @@ Ctx : U Ctx = List Type data Ref : Type -> Ctx -> U where - Z : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ) - S : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ) + Here : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ) + There : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ) data Term : Ctx -> Type -> U where App : {Γ : Ctx} {σ τ : Type} -> Term Γ (σ ~> τ) -> Term Γ σ -> Term Γ τ @@ -35,6 +35,35 @@ data Term : Ctx -> Type -> U where Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ -- FIXME, I'm not getting an error for Nil, but it's shadowing Nil +infixr 7 _:::_ data Env : Ctx -> U where ENil : Env Nil - ECons : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ) + _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ) + +-- TODO there is a problem here with coverage checking +-- I suspect something is being split before it's ready + +-- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ +-- lookup Z (x ::: y) = x +-- lookup (S i) (x ::: env) = lookup i env + + +-- lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ +-- lookup2 (x ::: y) Here = x +-- lookup2 (x ::: env) (There i) = lookup2 env i + +-- -- MixFix - this was ⟦_⟧ +-- eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ) +-- eval (App t u) env = ? -- (eval t env) (eval u env) +-- eval (Lam t) env = \ x => ? -- eval t (x ::: env) +-- eval (Var i) env = lookup2 env i + +-- something really strange here, the arrow in the goal type is backwards... +foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> ξ)) +foo {σ} {τ} {ξ} = ? -- \ x y => x + +-- data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where +-- -- S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x)) +-- K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> τ ~> σ) (\ env => \ x => \ y => x) + + diff --git a/newt/Debug.newt b/newt/Debug.newt new file mode 100644 index 0000000..3fa1af7 --- /dev/null +++ b/newt/Debug.newt @@ -0,0 +1,36 @@ +module Debug + +data Unit : U where + MkUnit : Unit + +infixr 7 _::_ +data List : U -> U where + Nil : {A : U} -> List A + _::_ : {A : U} -> A -> List A -> List A + +-- prj/menagerie/papers/combinatory + +infixr 6 _~>_ +data Type : U where + ι : Type + _~>_ : Type -> Type -> Type + +A : U +A = Unit + +Val : Type -> U +Val ι = A +Val (x ~> y) = Val x -> Val y + +id : {a : U} -> a -> a +id x = x + +-- can't get Val to expand here. +#check (\ x => \ y => \ z => id (Val (x ~> y ~> z))) : Type -> Type -> Type -> U + +-- NOW something really strange here, the arrow in the goal type is backwards... +-- I think case eval is broken. + +foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> ξ)) +foo {σ} {τ} {ξ} = ? -- \ x y => x + diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index e6b06f3..70c7cc8 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -58,8 +58,8 @@ forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of (Solved _ k t) => vappSpine t sp >>= forceMeta forceMeta x = pure x -tryEval : String -> SnocList Val -> M (Maybe Val) -tryEval k sp = +tryEval : Val -> M (Maybe Val) +tryEval (VRef fc k _ sp) = case lookup k !(get) of Just (MkEntry name ty (Fn tm)) => do vtm <- eval [] CBN tm @@ -67,14 +67,14 @@ tryEval k sp = VCase{} => pure Nothing v => pure $ Just v _ => pure Nothing +tryEval _ = pure Nothing -- Force far enough to compare types forceType : Val -> M Val forceType (VMeta fc ix sp) = case !(lookupMeta ix) of (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp) (Solved _ k t) => vappSpine t sp >>= forceType -forceType x@(VRef fc nm _ sp) = fromMaybe x <$> tryEval nm sp -forceType x = pure x +forceType x = fromMaybe x <$> tryEval x public export record UnifyResult where @@ -88,6 +88,8 @@ Semigroup UnifyResult where Monoid UnifyResult where neutral = MkResult [] +data UnifyMode = Normal | Pattern + -- We need to switch to SortedMap here export updateMeta : Context -> Nat -> (MetaEntry -> M MetaEntry) -> M () @@ -157,7 +159,7 @@ parameters (ctx: Context) go ren lvl (VCase fc sc alts) = error fc "Case in solution" go ren lvl (VLit fc lit) = pure (Lit fc lit) go ren lvl (VLet fc name val body) = - pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) !(body $$ VVar fc lvl [<])) + pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) body) lams : Nat -> Tm -> Tm @@ -167,7 +169,7 @@ parameters (ctx: Context) export - unify : (l : Nat) -> Val -> Val -> M UnifyResult + unify : (l : Nat) -> UnifyMode -> Val -> Val -> M UnifyResult export solve : (lvl : Nat) -> (k : Nat) -> SnocList Val -> Val -> M () @@ -197,13 +199,13 @@ parameters (ctx: Context) MkMc fc ctx sp rhs => do val <- vappSpine soln sp debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}" - unify ctx.lvl val rhs + unify ctx.lvl Normal val rhs - unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult - unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now - unifySpine l True [<] [<] = pure (MkResult []) - unifySpine l True (xs :< x) (ys :< y) = [| unify l x y <+> (unifySpine l True xs ys) |] - unifySpine l True _ _ = error emptyFC "meta spine length mismatch" + unifySpine : Nat -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult + unifySpine l mode False _ _ = error emptyFC "unify failed at head" -- unreachable now + unifySpine l mode True [<] [<] = pure (MkResult []) + unifySpine l mode True (xs :< x) (ys :< y) = [| unify l mode x y <+> (unifySpine l mode True xs ys) |] + unifySpine l mode True _ _ = error emptyFC "meta spine length mismatch" lookupVar : Nat -> Maybe Val lookupVar k = let l = length ctx.env in @@ -226,7 +228,7 @@ parameters (ctx: Context) pure t unlet x = pure x - unify l t u = do + unify l mode t u = do debug "Unify \{show ctx.lvl}" debug " \{show l} \{show t}" debug " =?= \{show u}" @@ -240,32 +242,41 @@ parameters (ctx: Context) -- flex/flex (VMeta fc k sp, VMeta fc' k' sp' ) => - if k == k' then unifySpine l (k == k') sp sp' + if k == k' then unifySpine l mode (k == k') sp sp' -- TODO, might want to try the other way, too. else if length sp < length sp' then solve l k' sp' (VMeta fc k sp) >> pure neutral 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 [<]) |] + (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l mode a a' <+> unify (S l) mode !(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' + if k == k' then unifySpine l mode (k == k') sp sp' else if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] - -- attempt at building constraints - (VVar fc k [<], u) => pure $ MkResult[(k, u)] - (t, VVar fc k [<]) => pure $ MkResult[(k, t)] + -- We only want to do this for LHS pattern vars, otherwise, try expanding + (VVar fc k [<], u) => case mode of + Pattern => pure $ MkResult[(k, u)] + Normal => case !(tryEval u) of + Just v => unify l mode t' v + Nothing => error ctx.fc "Failed to unify \{show t'} and \{show u'}" - (VLam _ _ t, VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) + (t, VVar fc k [<]) => case mode of + Pattern => pure $ MkResult[(k, t)] + Normal => case !(tryEval t) of + Just v => unify l mode v u' + Nothing => error ctx.fc "Failed to unify \{show t'} and \{show u'}" + + (VLam _ _ t, VLam _ _ t') => unify (l + 1) mode !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) (t, VLam fc' _ t') => do debug "ETA \{show t}" - unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) + unify (l + 1) mode !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) (VLam fc _ t, t' ) => do debug "ETA' \{show t'}" - unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<]) + unify (l + 1) mode !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<]) -- REVIEW - consider separate value for DCon/TCon - (VRef fc k def sp, VRef fc' k' def' sp' ) => + (VRef fc k def sp, VRef fc' k' def' sp') => -- This is a problem for cmp (S x) (S y) =?= cmp x y, when the -- same is an equation in cmp. @@ -274,12 +285,12 @@ parameters (ctx: Context) -- unifySpine l (k == k') sp sp' -- else do - Nothing <- tryEval k sp - | Just v => unify l v u' - Nothing <- tryEval k' sp' - | Just v => unify l t' v + Nothing <- tryEval t' + | Just v => unify l mode v u' + Nothing <- tryEval u' + | Just v => unify l mode t' v if k == k' - then unifySpine l (k == k') sp sp' + then unifySpine l mode (k == k') sp sp' else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" (VU _, VU _) => pure neutral @@ -288,13 +299,13 @@ parameters (ctx: Context) (t, VRef fc' 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') + Just (MkEntry name ty (Fn tm)) => unify l mode t !(vappSpine !(eval [] CBN tm) sp') _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} [no Fn]\n env is \{show ctx.env} \{show $ map fst ctx.types}" (VRef fc k def sp, u) => do debug "expand %ref \{k} \{show sp} =?= \{show u}" case lookup k !(get) of - Just (MkEntry name ty (Fn tm)) => unify l !(vappSpine !(eval [] CBN tm) sp) u + Just (MkEntry name ty (Fn tm)) => unify l mode !(vappSpine !(eval [] CBN tm) sp) u _ => error ctx.fc "unify failed \{show t'} [no Fn] =?= \{show u'}\n env is \{show ctx.env} \{show $ map fst ctx.types}" -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. @@ -312,7 +323,7 @@ parameters (ctx: Context) unifyCatch : FC -> Context -> Val -> Val -> M () unifyCatch fc ctx ty' ty = do - res <- catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do + res <- catchError (unify ctx ctx.lvl Normal ty' ty) $ \(E x str) => do let names = toList $ map fst ctx.types debug "fail \{show ty'} \{show ty}" a <- quote ctx.lvl ty' @@ -509,7 +520,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do -- We get unification constraints from matching the data constructors -- codomain with the scrutinee type debug "unify dcon cod with scrut\n \{show ty'}\n \{show scty}" - Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) ty' scty) + Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) Pattern ty' scty) (\(E _ msg) => do debug "SKIP \{dcName} because unify error \{msg}" pure Nothing) @@ -540,7 +551,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do pure $ Just $ CaseCons dcName (map getName vars) tm _ => do - Right res <- tryError {e = Error} (unify ctx' (length ctx'.env) ty' scty) + Right res <- tryError {e = Error} (unify ctx' (length ctx'.env) Pattern ty' scty) | Left (E _ msg) => do debug "SKIP \{dcName} because unify error \{msg}" pure Nothing diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index b41f994..f57c17b 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -83,7 +83,7 @@ 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) -eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) (MkClosure env u) +eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) !(eval (VVar fc (length env) [<] :: env) mode u) -- 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 @@ -116,7 +116,7 @@ quote l (VMeta fc i sp) = (Solved _ k t) => quote l !(vappSpine t sp) 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 (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) !(u $$ VVar emptyFC l [<])) +quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) u) 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 @@ -128,6 +128,10 @@ export nf : Env -> Tm -> M Tm nf env t = quote (length env) !(eval env CBN t) +export +nfv : Env -> Tm -> M Tm +nfv env t = quote (length env) !(eval env CBV t) + export prvalCtx : {auto ctx : Context} -> Val -> M String prvalCtx v = pure $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v) diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index a233050..53d7da5 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -165,7 +165,7 @@ processDecl (Def fc nm clauses) = do let names = (toList $ map fst ctx.types) -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}" - let msg = "\{unlines (toList $ reverse env)} -----------\n goal \{pprint names ty'}" + let msg = "\{unlines (toList $ reverse env)} -----------\n \{pprint names ty'}\n \{showTm ty'}" info fc "User Hole\n\{msg}" (Unsolved (l,c) k ctx ty kind cons) => do tm <- quote ctx.lvl !(forceMeta ty) @@ -177,23 +177,29 @@ processDecl (Def fc nm clauses) = do modify $ setDef nm ty (Fn tm') processDecl (DCheck fc tm ty) = do + putStrLn "----- DCheck" top <- get - putStrLn "check \{show tm} at \{show ty}" - ty' <- check (mkCtx top.metas fc) tm (VU fc) - putStrLn "got type \{pprint [] ty'}" + + putStrLn "INFO at \{show fc}: check \{show tm} at \{show ty}" + ty' <- check (mkCtx top.metas fc) ty (VU fc) + putStrLn " got type \{pprint [] ty'}" vty <- eval [] CBN ty' - res <- check (mkCtx top.metas fc) ty vty - putStrLn "got \{pprint [] res}" + res <- check (mkCtx top.metas fc) tm vty + putStrLn " got \{pprint [] res}" norm <- nf [] res - putStrLn "norm \{pprint [] norm}" - putStrLn "NF " + putStrLn " NF \{pprint [] norm}" + norm <- nfv [] res + putStrLn " NFV \{pprint [] norm}" processDecl (Data fc nm ty cons) = do + putStrLn "-----" + putStrLn "process data \{nm}" top <- get tyty <- check (mkCtx top.metas fc) ty (VU fc) modify $ setDef nm tyty Axiom cnames <- for cons $ \x => case x of (TypeSig fc names tm) => do + debug "check dcon \{show names} \{show tm}" dty <- check (mkCtx top.metas fc) tm (VU fc) debug "dty \{show names} is \{pprint [] dty}" diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index dd01706..6502e01 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -23,7 +23,7 @@ identMore : Lexer identMore = alphaNum <|> exact "." <|> exact "'" <|> exact "_" singleton : Lexer -singleton = oneOf "()\\{}[]," +singleton = oneOf "()\\{}[],?" quo : Recognise True quo = is '"' diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 2435e87..fd60959 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -142,6 +142,10 @@ Show Tm where show (Case _ sc alts) = "(Case \{show sc} \{show alts})" show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})" +public export +showTm : Tm -> String +showTm = show + -- I can't really show val because it's HOAS... -- TODO derive @@ -228,7 +232,7 @@ data Val : Type where VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val VLam : FC -> Name -> Closure -> Val VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val - VLet : FC -> Name -> Val -> (b : Closure) -> Val + VLet : FC -> Name -> Val -> Val -> Val VU : FC -> Val VLit : FC -> Literal -> Val @@ -242,6 +246,7 @@ getValFC (VLam fc _ _) = fc getValFC (VPi fc _ _ a b) = fc getValFC (VU fc) = fc getValFC (VLit fc _) = fc +getValFC (VLet fc _ _ _) = fc public export @@ -260,6 +265,7 @@ Show Val where show (VCase fc sc alts) = "(%case \{show sc} ...)" show (VU _) = "U" show (VLit _ lit) = show lit + show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}" -- Not used - I was going to change context to have a List Binder -- instead of env, types, bds diff --git a/tests/black/CaseEval.newt b/tests/black/CaseEval.newt index a47596f..ce11220 100644 --- a/tests/black/CaseEval.newt +++ b/tests/black/CaseEval.newt @@ -15,4 +15,7 @@ two : Eq (plus (S Z) (S Z)) (S (S Z)) two = Refl three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z)) -three = Refl {Nat} {S (S (S Z))} +three = Refl + +addZero : {n : Nat} -> Eq (plus Z n) n +addZero {n} = Refl