From 558e7722b877907faa266c8825af2554c40a8f9e Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 16 Oct 2024 07:36:29 -0700 Subject: [PATCH] =?UTF-8?q?[=20unify=20]=20Don't=20add=20constraints=20for?= =?UTF-8?q?=20vvar=20with=20spine.=20=20Constrain=20vvar=20instead=20of=20?= =?UTF-8?q?=CE=B7=20expanding.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- TODO.md | 2 ++ newt/Tree.newt | 14 +++++++------- src/Lib/Elab.idr | 22 ++++++++++------------ src/Lib/Types.idr | 2 +- 4 files changed, 20 insertions(+), 20 deletions(-) diff --git a/TODO.md b/TODO.md index 1c96454..890eba9 100644 --- a/TODO.md +++ b/TODO.md @@ -7,8 +7,10 @@ - [ ] consider making meta application implicit in term, so its more readable when printed - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people leave that implicit for efficiency. I think it would also make printing more readable. + - When printing `Value`, I now print the spine size instead of spine. - [x] eval for case (see order.newt) - [ ] dynamic pattern unification (add test case first) + - Possibly the cause of issue in code commented out in `TestCase4.newt` - [x] switch from commit/mustWork to checking progress - [x] type constructors are no longer generated? And seem to have 0 arity. - [x] raw let is not yet implemented (although define used by case tree building) diff --git a/newt/Tree.newt b/newt/Tree.newt index 168b66e..f61448b 100644 --- a/newt/Tree.newt +++ b/newt/Tree.newt @@ -59,12 +59,13 @@ data T23 : Bnd -> Bnd -> Nat -> U where -- 56: infixl 5 _*_ -infixl 1 _,_ +infixr 1 _,_ +infixr 1 _**_ data Sg : (A : U) -> (A -> U) -> U where - _,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B + _**_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B data _*_ : (A B : U) -> U where - Foo : {A B : U} -> A -> B -> A * B + _,_ : {A B : U} -> A -> B -> A * B TooBig : Bnd -> Bnd -> Nat -> U TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h) @@ -72,12 +73,11 @@ TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h) insert : {h : Nat} {l u : Bnd} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h insert (MkI x lx xu) (leaf lu) = ? insert (MkI x lx xu) (node2 x1 t t1) = ? --- TODO - unify error the typ insert (MkI x lx xu) (node3 y z tly tyz tzu) = case cmp x y of -- u := N y is not solved at this time inl xy => case insert (MkI {_} {N y} x lx xy) tly of - -- It's having trouble with Foo because of a spine length issue - -- Idris says this isn't covering, even with just `inl a` , `inr a` - inl (v , (Foo tlv tvy)) => inl (y, node2 v tlv tvy, node2 z tyz tzy) + -- NOW down to a non-linear issue now. + -- Possibly due to the meta being applied to an extra argument + inl (v ** (tlv , tvy)) => inl (y ** (node2 v tlv tvy, node2 z tyz tzu)) inr x1 => ? inr x1 => ? diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 8b3e4ed..8235f94 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -93,7 +93,7 @@ parameters (ctx: Context) then do debug "\{show k} \{show acc}" - error fc "non-linear pattern" + error fc "non-linear pattern: \{show sp}" else go xs (k :: acc) go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}" @@ -194,9 +194,6 @@ parameters (ctx: Context) debug "env \{show ctx.env}" debug "types \{show $ ctx.types}" case (t',u') of - (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 [<]) (VMeta fc k sp, VMeta fc' k' sp' ) => if k == k' then unifySpine l (k == k') sp sp' -- TODO, might want to try the other way, too. @@ -207,11 +204,14 @@ parameters (ctx: Context) (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 - (VVar fc k sp, u) => pure $ MkResult[(k, u)] - (t, VVar fc k sp) => pure $ MkResult[(k, t)] + (VVar fc k [<], u) => pure $ MkResult[(k, u)] + (t, VVar fc k [<]) => pure $ MkResult[(k, t)] + + (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 [<]) -- REVIEW - consider separate value for DCon/TCon (VRef fc k def sp, VRef fc' k' def' sp' ) => @@ -578,9 +578,7 @@ checkDone ctx [] body ty = do -- 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` - -- NOW In Tree.newt we have a case/case unification that might - -- have succeeded if it was left as a functino call. + -- we don't have anything like `vapp` for case ty <- quote (length ctx.env) ty ty <- eval ctx.env CBV ty debug "check at \{show ty}" @@ -647,7 +645,8 @@ check ctx tm ty = case (tm, !(forceType ty)) of -- Maybe we can let the scrutinee and jump into the middle? (sc, scty) <- infer ctx rsc scty <- forceMeta scty - debug "SCTM/TY \{pprint (names ctx) sc} \{show scty}" + debug "SCTM \{pprint (names ctx) sc}" + debug "SCTY \{show scty}" let scnm = fresh "sc" top <- get @@ -697,7 +696,6 @@ check ctx tm ty = case (tm, !(forceType ty)) of (t@(RLam fc nm icit tm), ty) => error fc "Expected pi type, got \{!(prvalCtx ty)}" - -- NOW Test1.newt passes with Explicit, TestCase4.newt passes with Implicit (tm, ty@(VPi fc nm' Implicit a b)) => do let names = toList $ map fst ctx.types debug "XXX edge add implicit lambda {\{nm'} : \{show a}} to \{show tm} " diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index e0a8ac6..13ee679 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -225,7 +225,7 @@ covering export Show Val where show (VVar _ k sp) = "(%var \{show k} \{show sp})" show (VRef _ nm _ sp) = "(%ref \{nm} \{show sp})" - show (VMeta _ ix sp) = "(%meta \{show ix} \{show sp})" + show (VMeta _ ix sp) = "(%meta \{show ix} \{show $ length sp})" 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})"