From 0589a30d403470af4defde3c9d037d0ac58cf830 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 13 Nov 2024 20:21:33 -0800 Subject: [PATCH] Address a few issues in Combinatory.newt --- TODO.md | 1 + newt-vscode/src/extension.ts | 2 +- newt/Combinatory.newt | 16 ++++---- src/Lib/Elab.idr | 71 ++++++++++++++++++------------------ src/Lib/Eval.idr | 47 +++++++++++++----------- 5 files changed, 72 insertions(+), 65 deletions(-) diff --git a/TODO.md b/TODO.md index 9464bf6..94286ed 100644 --- a/TODO.md +++ b/TODO.md @@ -6,6 +6,7 @@ - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this. - [ ] Remove context lambdas when printing solutions (show names from context) - maybe build list of names and strip λ, then call pprint with names +- [ ] Revisit substitution in case building - [ ] Check for shadowing when declaring dcon - [ ] Require infix decl before declaring names (helps find bugs) - [ ] sugar for typeclasses diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 5a7fdfb..450d8ba 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -16,7 +16,7 @@ export function activate(context: vscode.ExtensionContext) { const config = vscode.workspace.getConfiguration("newt"); const cmd = config.get("path", "build/exec/newt"); const command = `${cmd} ${fileName}`; - exec(command, { cwd }, (err, stdout, _stderr) => { + exec(command, { cwd, maxBuffer: 1024*1024*10 }, (err, stdout, _stderr) => { // I think I ignored 1 here because I wanted failure to launch if (err && err.code !== 1) { vscode.window.showErrorMessage(`newt error: ${err}`); diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt index 97adfaf..d05e96d 100644 --- a/newt/Combinatory.newt +++ b/newt/Combinatory.newt @@ -49,14 +49,13 @@ data Env : Ctx -> U where -- lookup Here (x ::: y) = x -- lookup (There 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 -- TODO MixFix - this was ⟦_⟧ eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ) --- TODO unification error in direct application +-- there was a unification error in direct application 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 @@ -76,8 +75,11 @@ sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} → Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y)) sapp (CApp K t) I = t sapp (CApp K t) (CApp K u) = CApp K (CApp t u) -sapp (CApp K t) u = ? -- CApp (CApp B t) u +-- was out of pattern because of unexpanded lets. +sapp (CApp K t) u = CApp (CApp B t) u +-- TODO unsolved meta, out of pattern fragment sapp t (CApp K u) = ? -- CApp (CApp C t) u +-- TODO unsolved meta, out of pattern fragment sapp t u = ? -- CApp (CApp S t) u abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env)) @@ -87,11 +89,11 @@ abs I = CApp K I abs B = CApp K B abs C = CApp K C abs (CApp t u) = sapp (abs t) (abs u) --- -- TODO lookup2 is getting stuck -abs (CVar Here) = ? -- I -abs (CVar (There i)) = ? -- CApp K (Var i) +-- -- TODO lookup2 was getting stuck, needed to bounce the types in a rewritten env. +abs (CVar Here) = I +abs (CVar (There i)) = CApp K (CVar i) translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm) -translate (App t u) = ? -- CApp (translate t) (translate u) +translate (App t u) = CApp (translate t) (translate u) translate (Lam t) = abs (translate t) translate (Var i) = CVar i diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index a91f811..38399ed 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -19,8 +19,8 @@ import Lib.Syntax -- dom gamma ren data Pden = PR Nat Nat (List Nat) -showEnv : Context -> M String -showEnv ctx = +showCtx : Context -> M String +showCtx ctx = unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) [] where isVar : Nat -> Val -> Bool @@ -195,8 +195,10 @@ solve env m sp t = do let l = length env debug "meta \{show meta}" ren <- invert l sp + -- force unlet + hack <- quote l t + t <- eval env CBN hack catchError {e=Error} (do - tm <- rename m ren l t let tm = lams (length sp) tm @@ -220,8 +222,6 @@ solve env m sp t = do debug "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}" debug "because \{showError "" err}" addConstraint env m sp t) - --throwError err) - unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult unifySpine env mode False _ _ = error emptyFC "unify failed at head" -- unreachable now @@ -277,13 +277,13 @@ unify env mode t u = do -- 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 + Normal => case !(tryEval env u) of Just v => unify env mode t' v Nothing => error fc "Failed to unify \{show t'} and \{show u'}" (_,t, VVar fc k [<]) => case mode of Pattern => pure $ MkResult[(k, t)] - Normal => case !(tryEval t) of + Normal => case !(tryEval env t) of Just v => unify env mode v u' Nothing => error fc "Failed to unify \{show t'} and \{show u'}" @@ -301,21 +301,18 @@ unify env mode t u = do -- REVIEW - consider separate value for DCon/TCon (_, 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. - - -- if k == k' then do - -- debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}" - -- unifySpine l (k == k') sp sp' - -- else + -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y do - Nothing <- tryEval t' - | Just v => unify env mode v u' - Nothing <- tryEval u' - | Just v => unify env mode t' v - if k == k' - then unifySpine env mode (k == k') sp sp' - else error fc "vref mismatch \{show t'} \{show u'}" + -- catchError {e = Error} (unifySpine env mode (k == k') sp sp') $ \ err => do + Nothing <- tryEval env t' + | Just v => do + debug "tryEval \{show t'} to \{show v}" + unify env mode v u' + Nothing <- tryEval env u' + | Just v => unify env mode t' v + if k == k' + then unifySpine env mode (k == k') sp sp' + else error fc "vref mismatch \{show t'} \{show u'}" (_, VU _, VU _) => pure neutral -- Lennart.newt cursed type references itself @@ -690,19 +687,21 @@ checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm checkDone ctx [] body ty = do debug "DONE-> check body \{show body} at \{show ty}" -- TODO better dump context function - -- debugM $ showEnv ctx - -- -- Hack to try to get Combinatory working. - -- env' <- for ctx.env $ \ val => do - -- ty <- quote (length ctx.env) val - -- eval ctx.env CBN ty - -- types' <- for ctx.types $ \case - -- (nm,ty) => do - -- nty <- quote (length ctx.env) ty - -- ty' <- eval ctx.env CBN nty - -- pure (nm, ty') - -- let ctx = { env := env', types := types' } ctx - -- debug "AFTER" - -- debugM $ showEnv ctx + debugM $ showCtx ctx + -- Hack to try to get Combinatory working + -- we're trying to subst in solutions here. + env' <- for ctx.env $ \ val => do + ty <- quote (length ctx.env) val + -- This is not getting vars under lambdas + eval ctx.env CBV ty + types' <- for ctx.types $ \case + (nm,ty) => do + nty <- quote (length env') ty + ty' <- eval env' CBV nty + pure (nm, ty') + let ctx = { env := env', types := types' } ctx + debug "AFTER" + debugM $ showCtx ctx -- I'm running an eval here to run case statements that are -- unblocked by lets in the env. (Tree.newt:cmp) -- The case eval code only works in the Tm -> Val case at the moment. @@ -825,7 +824,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do case pat of PatCon _ _ _ _ => do -- expand vars that may be solved, eval top level functions - scty' <- unlet ctx.env scty >>= forceType + scty' <- unlet ctx.env scty >>= forceType ctx.env debug "EXP \{show scty} -> \{show scty'}" -- this is per the paper, but it would be nice to coalesce -- default cases @@ -857,7 +856,7 @@ undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Expli undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs undo ((DoArrow fc nm tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc nm Explicit !(undo xs)) Explicit -check ctx tm ty = case (tm, !(forceType ty)) of +check ctx tm ty = case (tm, !(forceType ctx.env ty)) of (RDo fc stmts, ty) => check ctx !(undo stmts) ty (RCase fc rsc alts, ty) => do (sc, scty) <- infer ctx rsc diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 5e33b21..93789f7 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -38,25 +38,13 @@ vapp (VLam _ _ t) u = t $$ u vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u) vapp (VRef fc nm def sp) u = pure $ VRef fc nm def (sp :< u) vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u) -vapp t u = error' "impossible in vapp \{show t} to \{show u}" +vapp t u = error' "impossible in vapp \{show t} to \{show u}\n" export vappSpine : Val -> SnocList Val -> M Val vappSpine t [<] = pure t vappSpine t (xs :< x) = vapp !(vappSpine t xs) x -export -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 - case !(vappSpine vtm sp) of - VCase{} => pure Nothing - v => pure $ Just v - _ => pure Nothing -tryEval _ = pure Nothing - lookupVar : Env -> Nat -> Maybe Val @@ -81,17 +69,34 @@ unlet env t@(VVar fc k sp) = case lookupVar env k of pure t unlet env x = pure x +export +tryEval : Env -> Val -> M (Maybe Val) +tryEval env (VRef fc k _ sp) = + case lookup k !(get) of + Just (MkEntry name ty (Fn tm)) => + catchError {e=Error} ( + do + debug "app \{name} to \{show sp}" + vtm <- eval [] CBN tm + debug "tm is \{pprint [] tm}" + case !(vappSpine vtm sp) of + VCase{} => pure Nothing + v => pure $ Just v) + (\ _ => pure Nothing) + _ => pure Nothing +tryEval _ _ = pure Nothing + -- Force far enough to compare types export -forceType : Val -> M Val -forceType (VMeta fc ix sp) = case !(lookupMeta ix) of +forceType : Env -> Val -> M Val +forceType env (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 = do - Just x' <- tryEval x + (Solved _ k t) => vappSpine t sp >>= forceType env +forceType env x = do + Just x' <- tryEval env x | _ => pure x - forceType x' + forceType env x' evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val) evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) = @@ -108,7 +113,7 @@ evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) = go env (arg :: args) (nm :: nms) = go (arg :: env) args nms go env args [] = Just <$> vappSpine !(eval env mode t) ([<] <>< args) go env [] rest = pure Nothing --- This is an attempt to handle unlet for +-- REVIEW - this is handled in the caller already evalCase env mode sc@(VVar fc k sp) alts = case lookupVar env k of Just tt@(VVar fc' k' sp') => do debug "lookup \{show k} is \{show tt}" @@ -159,7 +164,7 @@ eval env mode tm@(Case fc sc alts) = do -- TODO we need to be able to tell eval to expand aggressively here. sc' <- eval env mode sc sc' <- unlet env sc' -- try to expand lets from pattern matching - sc' <- forceType sc' + sc' <- forceType env sc' pure $ fromMaybe (VCase fc !(eval env mode sc) alts) !(evalCase env mode sc' alts)