diff --git a/TODO.md b/TODO.md index 8d5d4ac..9464bf6 100644 --- a/TODO.md +++ b/TODO.md @@ -1,7 +1,7 @@ ## TODO -- [x] forall / ∀ sugar +- [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine) - [x] Bad module name error has FC 0,0 instead of the module or name - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this. - [ ] Remove context lambdas when printing solutions (show names from context) diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt index 2b33020..97adfaf 100644 --- a/newt/Combinatory.newt +++ b/newt/Combinatory.newt @@ -57,16 +57,13 @@ lookup2 (x ::: env) (There i) = lookup2 env i -- TODO MixFix - this was ⟦_⟧ eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ) -- TODO unification error in direct application -eval (App t u) env = -- (eval t env) (eval u env) - let a = (eval t env) - b = (eval u env) - in a b +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 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) + K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> (τ ~> σ)) (\ env => \ x y => x) I : {Γ : Ctx} {σ : Type} → Comb Γ (σ ~> σ) (\ env => \ x => x) B : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => f (g x)) C : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> τ ~> (σ ~> τ')) (\ env => \ f g x => (f x) g) @@ -79,9 +76,9 @@ 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 -sapp t (CApp K u) = CApp (CApp C t) u -sapp t u = CApp (CApp S t) u +sapp (CApp K t) u = ? -- CApp (CApp B t) u +sapp t (CApp K u) = ? -- CApp (CApp C t) u +sapp t u = ? -- CApp (CApp S t) u abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env)) abs S = CApp K S @@ -90,6 +87,7 @@ 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) diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index e2c9fee..a91f811 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -19,6 +19,21 @@ import Lib.Syntax -- dom gamma ren data Pden = PR Nat Nat (List Nat) +showEnv : Context -> M String +showEnv ctx = + unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) [] + where + isVar : Nat -> Val -> Bool + isVar k (VVar _ k' [<]) = k == k' + isVar _ _ = False + + go : List String -> Nat -> List (Val, String, Val) -> List String -> M (List String) + go _ _ [] acc = pure acc + go names k ((v, n, ty) :: xs) acc = if isVar k v + -- TODO - use Doc and add <+/> as appropriate to printing + then go names (S k) xs (" \{n} : \{pprint names !(quote ctx.lvl ty)}":: acc) + else go names (S k) xs (" \{n} = \{pprint names !(quote ctx.lvl v)} : \{pprint names !(quote ctx.lvl ty)}":: acc) + dumpCtx : Context -> M String dumpCtx ctx = do let names = (toList $ map fst ctx.types) @@ -74,11 +89,12 @@ data UnifyMode = Normal | Pattern -- We need to switch to SortedMap here export -updateMeta : Context -> Nat -> (MetaEntry -> M MetaEntry) -> M () -updateMeta ctx ix f = do - mc <- readIORef ctx.metas +updateMeta : Nat -> (MetaEntry -> M MetaEntry) -> M () +updateMeta ix f = do + top <- get + mc <- readIORef top.metas metas <- go mc.metas - writeIORef ctx.metas $ {metas := metas} mc + writeIORef top.metas $ {metas := metas} mc where go : List MetaEntry -> M (List MetaEntry) go [] = error' "Meta \{show ix} not found" @@ -86,245 +102,243 @@ updateMeta ctx ix f = do go (x@((Solved _ k y)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs export -addConstraint : Context -> Nat -> SnocList Val -> Val -> M () -addConstraint ctx ix sp tm = do - mc <- readIORef ctx.metas - updateMeta ctx ix $ \case +addConstraint : Env -> Nat -> SnocList Val -> Val -> M () +addConstraint env ix sp tm = do + top <- get + mc <- readIORef top.metas + updateMeta ix $ \case (Unsolved pos k a b c cons) => do debug "Add constraint m\{show ix} \{show sp} =?= \{show tm}" - pure (Unsolved pos k a b c (MkMc (getFC tm) ctx sp tm :: cons)) + pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons)) (Solved _ k tm) => error' "Meta \{show k} already solved" pure () -parameters (ctx: Context) - -- return renaming, the position is the new VVar - invert : Nat -> SnocList Val -> M (List Nat) - invert lvl sp = go sp [] - where - go : SnocList Val -> List Nat -> M (List Nat) - go [<] acc = pure $ reverse acc - go (xs :< VVar fc k [<]) acc = do - if elem k acc - then do - debug "\{show k} \{show acc}" - -- when does this happen? - error fc "non-linear pattern: \{show sp}" - else go xs (k :: acc) - go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}" - -- REVIEW why am I converting to Tm? - -- we have to "lift" the renaming when we go under a lambda - -- I think that essentially means our domain ix are one bigger, since we're looking at lvl - -- in the codomain, so maybe we can just keep that value - rename : Nat -> List Nat -> Nat -> Val -> M Tm - rename meta ren lvl v = go ren lvl v - where - go : List Nat -> Nat -> Val -> M Tm - goSpine : List Nat -> Nat -> Tm -> SnocList Val -> M Tm - goSpine ren lvl tm [<] = pure tm - goSpine ren lvl tm (xs :< x) = do - xtm <- go ren lvl x - pure $ App emptyFC !(goSpine ren lvl tm xs) xtm - - go ren lvl (VVar fc k sp) = case findIndex (== k) ren of - Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" - 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) = do - -- So sometimes we have an unsolved meta in here which reference vars out of scope. - debug "rename Meta \{show ix} spine \{show sp}" - if ix == meta - -- REVIEW is this the right fc? - then error fc "meta occurs check" - else case !(lookupMeta ix) of - Solved fc _ val => do - debug "rename: \{show ix} is solved" - go ren lvl !(vappSpine val sp) - _ => do - debug "rename: \{show ix} is unsolved" - catchError {e=Error} (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) - go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc 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" - 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) +-- return renaming, the position is the new VVar +invert : Nat -> SnocList Val -> M (List Nat) +invert lvl sp = go sp [] + where + go : SnocList Val -> List Nat -> M (List Nat) + go [<] acc = pure $ reverse acc + go (xs :< VVar fc k [<]) acc = do + if elem k acc + then do + debug "\{show k} \{show acc}" + -- when does this happen? + error fc "non-linear pattern: \{show sp}" + else go xs (k :: acc) + go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}" - lams : Nat -> Tm -> Tm - lams 0 tm = tm - -- REVIEW can I get better names in here? - lams (S k) tm = Lam emptyFC "arg_\{show k}" (lams k tm) +-- REVIEW why am I converting to Tm? +-- we have to "lift" the renaming when we go under a lambda +-- I think that essentially means our domain ix are one bigger, since we're looking at lvl +-- in the codomain, so maybe we can just keep that value +rename : Nat -> List Nat -> Nat -> Val -> M Tm +rename meta ren lvl v = go ren lvl v + where + go : List Nat -> Nat -> Val -> M Tm + goSpine : List Nat -> Nat -> Tm -> SnocList Val -> M Tm + goSpine ren lvl tm [<] = pure tm + goSpine ren lvl tm (xs :< x) = do + xtm <- go ren lvl x + pure $ App emptyFC !(goSpine ren lvl tm xs) xtm + + go ren lvl (VVar fc k sp) = case findIndex (== k) ren of + Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" + 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) = do + -- So sometimes we have an unsolved meta in here which reference vars out of scope. + debug "rename Meta \{show ix} spine \{show sp}" + if ix == meta + -- REVIEW is this the right fc? + then error fc "meta occurs check" + else case !(lookupMeta ix) of + Solved fc _ val => do + debug "rename: \{show ix} is solved" + go ren lvl !(vappSpine val sp) + _ => do + debug "rename: \{show ix} is unsolved" + catchError {e=Error} (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) + go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc 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" + 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) + +lams : Nat -> Tm -> Tm +lams 0 tm = tm +-- REVIEW can I get better names in here? +lams (S k) tm = Lam emptyFC "arg_\{show k}" (lams k tm) + +export +unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult + +export +solve : Env -> (k : Nat) -> SnocList Val -> Val -> M () +solve env m sp t = do + meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m + | _ => error (getFC t) "Meta \{show m} already solved!" + debug "SOLVE \{show m} \{show kind} lvl \{show $ length env} sp \{show sp} is \{show t}" + let size = length $ filter (\x => x == Bound) $ toList ctx_.bds + debug "\{show m} size is \{show size} sps \{show $ length sp}" + let True = length sp == size + | _ => do + let l = length env + debug "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" + debug "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}" + addConstraint env m sp t + let l = length env + debug "meta \{show meta}" + ren <- invert l sp + catchError {e=Error} (do + + tm <- rename m ren l t + + let tm = lams (length sp) tm + top <- get + soln <- eval [] CBN tm + + updateMeta m $ \case + (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln + (Solved _ k x) => error' "Meta \{show ix} already solved!" + for_ cons $ \case + MkMc fc env sp rhs => do + val <- vappSpine soln sp + debug "discharge l=\{show $ length env} \{(show val)} =?= \{(show rhs)}" + unify env Normal val rhs) + (\case + Postpone fc ix msg => do + -- let someone else solve this and then check again. + debug "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}" + addConstraint env m sp t + err => do + debug "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}" + debug "because \{showError "" err}" + addConstraint env m sp t) + --throwError err) - export - unify : (l : Nat) -> UnifyMode -> Val -> Val -> M UnifyResult +unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult +unifySpine env mode False _ _ = error emptyFC "unify failed at head" -- unreachable now +unifySpine env mode True [<] [<] = pure (MkResult []) +unifySpine env mode True (xs :< x) (ys :< y) = [| unify env mode x y <+> (unifySpine env mode True xs ys) |] +unifySpine env mode True _ _ = error emptyFC "meta spine length mismatch" - export - solve : (lvl : Nat) -> (k : Nat) -> SnocList Val -> Val -> M () - solve l m sp t = do - meta@(Unsolved metaFC ix ctx ty kind cons) <- lookupMeta m - | _ => error (getFC t) "Meta \{show m} already solved!" - debug "SOLVE \{show m} \{show kind} lvl \{show l} sp \{show sp} is \{show t}" - let size = length $ filter (\x => x == Bound) $ toList ctx.bds - debug "\{show m} size is \{show size} sps \{show $ length sp}" - let True = length sp == size - | _ => do - debug "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" - debug "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}" - addConstraint ctx m sp t +unify env mode t u = do + debug "Unify lvl \{show $ length env}" + debug " \{show t}" + debug " =?= \{show u}" + t' <- forceMeta t >>= unlet env + u' <- forceMeta u >>= unlet env + debug "forced \{show t'}" + debug " =?= \{show u'}" + debug "env \{show env}" + -- debug "types \{show $ ctx.types}" + let l = length env + case (mode,t',u') of - debug "meta \{show meta}" - ren <- invert l sp - catchError {e=Error} (do + -- flex/flex + (_, VMeta fc k sp, VMeta fc' k' sp' ) => + if k == k' then unifySpine env mode (k == k') sp sp' + -- TODO, might want to try the other way, too. + else if length sp < length sp' + then solve env k' sp' (VMeta fc k sp) >> pure neutral + else solve env k sp (VMeta fc' k' sp') >> pure neutral + (_, t, VMeta fc' i' sp') => solve env i' sp' t >> pure neutral + (_, VMeta fc i sp, t' ) => solve env i sp t' >> pure neutral + (_, VPi fc _ _ a b, VPi fc' _ _ a' b') => do + let fresh = VVar fc l [<] + [| unify env mode a a' <+> unify (fresh :: env) mode !(b $$ fresh) !(b' $$ fresh) |] + (_, VVar fc k sp, (VVar fc' k' sp') ) => + if k == k' then unifySpine env mode (k == k') sp sp' + else case (mode, sp, sp') of + (Pattern, [<],[<]) => if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] + _ => error fc "Failed to unify \{show t'} and \{show u'}" - tm <- rename m ren l t - - let tm = lams (length sp) tm - top <- get - soln <- eval [] CBN tm - - updateMeta ctx m $ \case - (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln - (Solved _ k x) => error' "Meta \{show ix} already solved!" - for_ cons $ \case - MkMc fc ctx sp rhs => do - val <- vappSpine soln sp - debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}" - unify ctx.lvl Normal val rhs) - (\case - Postpone fc ix msg => do - -- let someone else solve this and then check again. - addConstraint ctx m sp t - pure () - err => throwError err) + -- we don't eta expand on LHS + (Normal, VLam fc _ t, VLam _ _ t') => do + let fresh = VVar fc l [<] + unify (fresh :: env) mode !(t $$ fresh) !(t' $$ fresh) + (Normal, t, VLam fc' _ t') => do + debug "ETA \{show t}" + let fresh = VVar fc' l [<] + unify (fresh :: env) mode !(t `vapp` fresh) !(t' $$ fresh) + (Normal, VLam fc _ t, t' ) => do + debug "ETA' \{show t'}" + let fresh = VVar fc l [<] + unify (fresh :: env) mode !(t $$ fresh) !(t' `vapp` fresh) - 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" + -- 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 env mode t' v + Nothing => error fc "Failed to unify \{show t'} and \{show u'}" - lookupVar : Nat -> Maybe Val - lookupVar k = let l = length ctx.env in - if k > l - then Nothing - else case getAt ((l `minus` k) `minus` 1) ctx.env of - Just v@(VVar fc k' sp) => if k == k' then Nothing else Just v - Just v => Just v - Nothing => Nothing + (_,t, VVar fc k [<]) => case mode of + Pattern => pure $ MkResult[(k, t)] + Normal => case !(tryEval t) of + Just v => unify env mode v u' + Nothing => error fc "Failed to unify \{show t'} and \{show u'}" - -- hoping to apply what we got via pattern matching - unlet : Val -> M Val - unlet t@(VVar fc k sp) = case lookupVar k of - Just tt@(VVar fc' k' sp') => do - debug "lookup \{show k} is \{show tt}" - if k' == k then pure t else (vappSpine (VVar fc' k' sp') sp >>= unlet) - Just t => vappSpine t sp - Nothing => do - debug "lookup \{show k} is Nothing in env \{show ctx.env}" - pure t - unlet x = pure x + (_, VLam fc _ t, VLam _ _ t') => + let fresh = VVar fc l [<] in + unify (fresh :: env) mode !(t $$ fresh) !(t' $$ fresh) + (_, t, VLam fc' _ t') => do + debug "ETA \{show t}" + let fresh = VVar fc' l [<] + unify (fresh :: env) mode !(t `vapp` fresh) !(t' $$ fresh) + (_, VLam fc _ t, t' ) => do + debug "ETA' \{show t'}" + let fresh = VVar fc l [<] + unify (fresh :: env) mode !(t $$ fresh) !(t' `vapp` fresh) - unify l mode t u = do - debug "Unify \{show ctx.lvl}" - debug " \{show l} \{show t}" - debug " =?= \{show u}" - t' <- forceMeta t >>= unlet - u' <- forceMeta u >>= unlet - debug "forced \{show t'}" - debug " =?= \{show u'}" - debug "env \{show ctx.env}" - debug "types \{show $ ctx.types}" - case (t',u') of + -- 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. - -- flex/flex - (VMeta fc k sp, VMeta fc' k' 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 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 mode (k == k') sp sp' - else if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] + -- if k == k' then do + -- debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}" + -- unifySpine l (k == k') sp sp' + -- else + 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'}" - -- 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'}" + (_, VU _, VU _) => pure neutral + -- Lennart.newt cursed type references itself + -- We _could_ look up the ref, eval against [] and vappSpine... + (_, 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 env mode t !(vappSpine !(eval [] CBN tm) sp') + _ => error fc' "unify failed \{show t'} =?= \{show u'} [no Fn]\n env is \{show env}" - (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'}" + (_, 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 env mode !(vappSpine !(eval [] CBN tm) sp) u + _ => error fc "unify failed \{show t'} [no Fn] =?= \{show u'}\n env is \{show env}" - (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) mode !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) - (VLam fc _ t, t' ) => do - debug "ETA' \{show t'}" - 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') => - -- 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 - do - 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 mode (k == k') sp sp' - else error fc "vref mismatch \{show t'} \{show u'}" - - (VU _, VU _) => pure neutral - -- Lennart.newt cursed type references itself - -- We _could_ look up the ref, eval against [] and vappSpine... - (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 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 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. - _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} \n env is \{show ctx.env} \{show $ map fst ctx.types}" - where - lookupVar : Nat -> Maybe Val - lookupVar k = let l = length ctx.env in - if k > l - then Nothing - else case getAt ((l `minus` k) `minus` 1) ctx.env of - Just (VVar{}) => Nothing - Just v => Just v - Nothing => Nothing + -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. + _ => error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" export unifyCatch : FC -> Context -> Val -> Val -> M () unifyCatch fc ctx ty' ty = do - res <- catchError (unify ctx ctx.lvl Normal ty' ty) $ \err => do + res <- catchError (unify ctx.env Normal ty' ty) $ \err => do let names = toList $ map fst ctx.types debug "fail \{show ty'} \{show ty}" a <- quote ctx.lvl ty' @@ -473,6 +487,9 @@ substVal k v tm = go tm go (VMeta fc ix sp) = VMeta fc ix (map go sp) go (VRef fc nm y sp) = VRef fc nm y (map go sp) go tm = tm + -- FIXME - do I need a Val closure like idris? + -- or env in unify... + -- or quote back -- go (VLam fc nm sc) = VLam fc nm sc -- go (VCase x sc xs) = ?rhs_2 -- go (VU x) = ?rhs_7 @@ -521,7 +538,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) Pattern ty' scty) + Just res <- catchError {e = Error} (Just <$> unify ctx'.env Pattern ty' scty) (\err => do debug "SKIP \{dcName} because unify error \{errorMsg err}" pure Nothing) @@ -552,7 +569,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) Pattern ty' scty) + Right res <- tryError {e = Error} (unify ctx'.env Pattern ty' scty) | Left err => do debug "SKIP \{dcName} because unify error \{errorMsg err}" pure Nothing @@ -672,14 +689,27 @@ makeClause top (lhs, rhs) = do checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm checkDone ctx [] body ty = do debug "DONE-> check body \{show body} at \{show ty}" - -- TODO dump context function - debugM $ dumpCtx ctx + -- 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 -- 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. -- we don't have anything like `vapp` for case ty <- quote (length ctx.env) ty - ty <- eval ctx.env CBV ty + ty <- eval ctx.env CBN ty + debug "check at \{show ty}" got <- check ctx body ty debug "DONE<- got \{pprint (names ctx) got}" @@ -795,7 +825,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 scty >>= forceType + scty' <- unlet ctx.env scty >>= forceType debug "EXP \{show scty} -> \{show scty'}" -- this is per the paper, but it would be nice to coalesce -- default cases diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 2e314fb..5e33b21 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -57,13 +57,37 @@ tryEval (VRef fc k _ sp) = _ => pure Nothing tryEval _ = pure Nothing + + +lookupVar : Env -> Nat -> Maybe Val +lookupVar env k = let l = length env in + if k > l + then Nothing + else case getAt ((l `minus` k) `minus` 1) env of + Just v@(VVar fc k' sp) => if k == k' then Nothing else Just v + Just v => Just v + Nothing => Nothing + +-- hoping to apply what we got via pattern matching +export +unlet : Env -> Val -> M Val +unlet env t@(VVar fc k sp) = case lookupVar env k of + Just tt@(VVar fc' k' sp') => do + debug "lookup \{show k} is \{show tt}" + if k' == k then pure t else (vappSpine (VVar fc' k' sp') sp >>= unlet env) + Just t => vappSpine t sp >>= unlet env + Nothing => do + debug "lookup \{show k} is Nothing in env \{show env}" + pure t +unlet env x = pure x + + -- Force far enough to compare types export 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 = fromMaybe x <$> tryEval x forceType x = do Just x' <- tryEval x | _ => pure x @@ -75,13 +99,25 @@ evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) = then do debug "ECase \{nm} \{show sp} \{show nms} \{showTm t}" go env (sp <>> []) nms - else evalCase env mode sc xs + else case lookup nm !(get) of + (Just (MkEntry str type (DCon k str1))) => evalCase env mode sc xs + -- bail for a stuck function + _ => pure Nothing where go : Env -> List Val -> List String -> M (Maybe Val) 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 --- FIXME not good if stuck function +-- This is an attempt to handle unlet for +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}" + if k' == k then pure Nothing + else evalCase env mode !(vappSpine (VVar fc' k' sp') sp) alts + Just t => evalCase env mode !(vappSpine t sp) alts + Nothing => do + debug "lookup \{show k} is Nothing in env \{show env}" + pure Nothing evalCase env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u) evalCase env mode sc cc = do debug "CASE BAIL sc \{show sc} vs \{show cc}" @@ -122,6 +158,7 @@ eval env mode (Lit fc lit) = pure $ VLit fc lit 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' pure $ fromMaybe (VCase fc !(eval env mode sc) alts) !(evalCase env mode sc' alts) diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 6c23e05..81e5c4c 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -113,7 +113,7 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do val <- eval ctx.env CBN tm debug "SOLUTION \{pprint [] tm} evaled to \{show val}" let sp = makeSpine ctx.lvl ctx.bds - solve ctx ctx.lvl k sp val + solve ctx.env k sp val mc <- readIORef top.metas solveAutos mlen (take mlen mc.metas) solveAutos mlen (_ :: es) = solveAutos mlen es @@ -151,7 +151,12 @@ logMetas mstart = do tm <- quote ctx.lvl !(forceMeta ty) -- Now that we're collecting errors, maybe we simply check at the end -- TODO - log constraints? - addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints" + -- FIXME in Combinatory, the val doesn't match environment? + let msg = "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints" + msgs <- for cons $ \ (MkMc fc env sp val) => do + putStrLn " ENV \{show env}" + pure " (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}" + addError $ E (l,c) $ unlines ([msg] ++ msgs) export processDecl : Decl -> M () diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 858e432..ffc9d45 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -341,7 +341,7 @@ Show MetaKind where -- constrain meta applied to val to be a val public export -data MConstraint = MkMc FC Context (SnocList Val) Val +data MConstraint = MkMc FC Env (SnocList Val) Val public export data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved FC Nat Val diff --git a/tests/black/Concat.newt b/tests/black/Concat.newt index 271bf16..9e81168 100644 --- a/tests/black/Concat.newt +++ b/tests/black/Concat.newt @@ -32,6 +32,7 @@ replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b replace p Refl x = x cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b +cong f Refl = Refl thm : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys thm Nil ys = Refl