mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 13:54:55 +03:00
Turn lets to lambdas in hole environments
This works better when lifting lemmas, and ensures that the type of everything will be shown and not normalised away
This commit is contained in:
Edwin Brady
parent
620ad8e706
commit
f5a5d01274
@ -406,6 +406,9 @@ record Defs where
|
||||
-- be interpreted however the specific code generator requires
|
||||
toCompile : List Name
|
||||
-- ^ Names which need to be compiled to run time case trees
|
||||
userHoles : NameMap ()
|
||||
-- ^ Metavariables the user still has to fill in. In practice, that's
|
||||
-- everything with a user accessible name and a definition of Hole
|
||||
|
||||
export
|
||||
clearDefs : Defs -> Core Defs
|
||||
@ -418,7 +421,7 @@ initDefs : Core Defs
|
||||
initDefs
|
||||
= do gam <- initCtxt
|
||||
pure (MkDefs gam [] ["Main"] defaults empty 100
|
||||
empty empty empty [] [] 5381 [] [] [] [] [])
|
||||
empty empty empty [] [] 5381 [] [] [] [] [] empty)
|
||||
|
||||
-- Label for context references
|
||||
export
|
||||
@ -446,12 +449,30 @@ initHash
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { ifaceHash = 5381 } defs)
|
||||
|
||||
export
|
||||
addUserHole : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
addUserHole n
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { userHoles $= insert n () } defs)
|
||||
|
||||
export
|
||||
clearUserHole : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
clearUserHole n
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { userHoles $= delete n } defs)
|
||||
|
||||
|
||||
export
|
||||
addDef : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> GlobalDef -> Core Int
|
||||
addDef n def
|
||||
= do defs <- get Ctxt
|
||||
(idx, gam') <- addCtxt n def (gamma defs)
|
||||
case definition def of
|
||||
PMDef _ _ _ _ => clearUserHole n
|
||||
_ => pure ()
|
||||
put Ctxt (record { gamma = gam' } defs)
|
||||
pure idx
|
||||
|
||||
@ -512,18 +533,18 @@ setLinearCheck i chk
|
||||
export
|
||||
setCtxt : {auto c : Ref Ctxt Defs} -> Context GlobalDef -> Core ()
|
||||
setCtxt gam
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { gamma = gam } defs)
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { gamma = gam } defs)
|
||||
|
||||
export
|
||||
resolveName : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core Int
|
||||
Name -> Core Int
|
||||
resolveName (Resolved idx) = pure idx
|
||||
resolveName n
|
||||
= do defs <- get Ctxt
|
||||
(i, gam') <- getPosition n (gamma defs)
|
||||
setCtxt gam'
|
||||
pure i
|
||||
= do defs <- get Ctxt
|
||||
(i, gam') <- getPosition n (gamma defs)
|
||||
setCtxt gam'
|
||||
pure i
|
||||
|
||||
-- Call this before trying alternative elaborations, so that updates to the
|
||||
-- context are put in the staging area rather than writing over the mutable
|
||||
@ -531,54 +552,54 @@ resolveName n
|
||||
-- Returns the old context (the one we'll go back to if the branch fails)
|
||||
export
|
||||
branch : {auto c : Ref Ctxt Defs} ->
|
||||
Core Defs
|
||||
Core Defs
|
||||
branch
|
||||
= do ctxt <- get Ctxt
|
||||
gam' <- branchCtxt (gamma ctxt)
|
||||
setCtxt gam'
|
||||
pure ctxt
|
||||
= do ctxt <- get Ctxt
|
||||
gam' <- branchCtxt (gamma ctxt)
|
||||
setCtxt gam'
|
||||
pure ctxt
|
||||
|
||||
-- Call this after trying an elaboration to commit any changes to the mutable
|
||||
-- array of definitions once we know they're correct. Only actually commits
|
||||
-- when we're right back at the top level
|
||||
export
|
||||
commit : {auto c : Ref Ctxt Defs} ->
|
||||
Core ()
|
||||
Core ()
|
||||
commit
|
||||
= do defs <- get Ctxt
|
||||
gam' <- commitCtxt (gamma defs)
|
||||
setCtxt gam'
|
||||
= do defs <- get Ctxt
|
||||
gam' <- commitCtxt (gamma defs)
|
||||
setCtxt gam'
|
||||
|
||||
export
|
||||
depth : {auto c : Ref Ctxt Defs} ->
|
||||
Core Nat
|
||||
Core Nat
|
||||
depth
|
||||
= do defs <- get Ctxt
|
||||
pure (branchDepth (gamma defs))
|
||||
= do defs <- get Ctxt
|
||||
pure (branchDepth (gamma defs))
|
||||
|
||||
-- Explicitly note that the name should be saved when writing out a .ttc
|
||||
export
|
||||
addToSave : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
Name -> Core ()
|
||||
addToSave n
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { toSave $= insert n () } defs)
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { toSave $= insert n () } defs)
|
||||
|
||||
-- Specific lookup functions
|
||||
export
|
||||
lookupExactBy : (GlobalDef -> a) -> Name -> Context GlobalDef ->
|
||||
Core (Maybe a)
|
||||
Core (Maybe a)
|
||||
lookupExactBy fn n gam
|
||||
= do Just gdef <- lookupCtxtExact n gam
|
||||
| Nothing => pure Nothing
|
||||
pure (Just (fn gdef))
|
||||
= do Just gdef <- lookupCtxtExact n gam
|
||||
| Nothing => pure Nothing
|
||||
pure (Just (fn gdef))
|
||||
|
||||
export
|
||||
lookupNameBy : (GlobalDef -> a) -> Name -> Context GlobalDef ->
|
||||
Core (List (Name, Int, a))
|
||||
Core (List (Name, Int, a))
|
||||
lookupNameBy fn n gam
|
||||
= do gdef <- lookupCtxtName n gam
|
||||
pure (map (\ (n, i, gd) => (n, i, fn gd)) gdef)
|
||||
= do gdef <- lookupCtxtName n gam
|
||||
pure (map (\ (n, i, gd) => (n, i, fn gd)) gdef)
|
||||
|
||||
export
|
||||
lookupDefExact : Name -> Context GlobalDef -> Core (Maybe Def)
|
||||
@ -618,7 +639,7 @@ reducibleIn nspace n _ = True
|
||||
|
||||
export
|
||||
setFlag : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> Name -> DefFlag -> Core ()
|
||||
FC -> Name -> DefFlag -> Core ()
|
||||
setFlag fc n fl
|
||||
= do defs <- get Ctxt
|
||||
Just def <- lookupCtxtExact n (gamma defs)
|
||||
|
||||
@ -59,7 +59,7 @@ mutual
|
||||
|
||||
-- The assumption here is that hole types are abstracted over the entire
|
||||
-- environment, so that they have the appropriate number of function
|
||||
-- arguments and lets are still in the right place
|
||||
-- arguments and there are no lets
|
||||
updateHoleType : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
(useInHole : Bool) ->
|
||||
@ -75,9 +75,6 @@ mutual
|
||||
pure (Bind bfc nm (Pi c' e ty) scty)
|
||||
else do scty <- updateHoleType useInHole var sc as
|
||||
pure (Bind bfc nm (Pi c e ty) scty)
|
||||
updateHoleType useInHole var (Bind bfc nm (Let c val ty) sc) as
|
||||
= do scty <- updateHoleType useInHole var sc as
|
||||
pure (Bind bfc nm (Let c val ty) scty)
|
||||
updateHoleType useInHole var (Bind bfc nm (Pi c e ty) sc) (a :: as)
|
||||
= do updateHoleUsage False var a
|
||||
scty <- updateHoleType useInHole var sc as
|
||||
|
||||
@ -41,6 +41,34 @@ getRigNeeded InType = Rig0 -- unrestricted usage in types
|
||||
getRigNeeded (InLHS Rig0) = Rig0
|
||||
getRigNeeded _ = Rig1
|
||||
|
||||
-- Make sure the types of holes have the references to solved holes normalised
|
||||
-- away (since solved holes don't get written to .tti)
|
||||
export
|
||||
normaliseHoleTypes : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Core ()
|
||||
normaliseHoleTypes
|
||||
= do ust <- get UST
|
||||
let hs = keys (holes ust)
|
||||
defs <- get Ctxt
|
||||
traverse (normaliseH defs) hs
|
||||
pure ()
|
||||
where
|
||||
updateType : Defs -> Int -> GlobalDef -> Core ()
|
||||
updateType defs i def
|
||||
= do ty' <- normaliseHoles defs [] (type def)
|
||||
addDef (Resolved i) (record { type = ty' } def)
|
||||
pure ()
|
||||
|
||||
normaliseH : Defs -> Int -> Core ()
|
||||
normaliseH defs i
|
||||
= case !(lookupCtxtExact (Resolved i) (gamma defs)) of
|
||||
Just gdef =>
|
||||
case definition gdef of
|
||||
Hole _ _ => updateType defs i gdef
|
||||
_ => pure ()
|
||||
Nothing => pure ()
|
||||
|
||||
export
|
||||
elabTermSub : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
@ -108,7 +136,7 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
-- Linearity checking looks in case blocks, so no
|
||||
-- need to check here.
|
||||
else pure chktm
|
||||
|
||||
normaliseHoleTypes
|
||||
-- Put the current hole state back to what it was (minus anything
|
||||
-- which has been solved in the meantime)
|
||||
when (not incase) $
|
||||
|
||||
@ -27,13 +27,22 @@ checkHole : {vars : _} ->
|
||||
checkHole rig elabinfo nest env fc n_in (Just gexpty)
|
||||
= do nm <- inCurrentNS (UN n_in)
|
||||
expty <- getTerm gexpty
|
||||
(idx, metaval) <- metaVarI fc rig env nm expty
|
||||
-- Turn lets into lambda before making the hole so that they
|
||||
-- get abstracted over in the hole (it's fine here, unlike other
|
||||
-- holes, because we're not trying to unify it so it's okay if
|
||||
-- applying the metavariable isn't a pattern form)
|
||||
let env' = letToLam env
|
||||
(idx, metaval) <- metaVarI fc rig env' nm expty
|
||||
-- Record the LHS for this hole in the metadata
|
||||
withCurrentLHS (Resolved idx)
|
||||
addUserHole nm
|
||||
pure (metaval, gexpty)
|
||||
checkHole rig elabinfo nest env fc n_in exp
|
||||
= do nmty <- genName "holeTy"
|
||||
ty <- metaVar fc Rig0 env nmty (TType fc)
|
||||
let env' = letToLam env
|
||||
ty <- metaVar fc Rig0 env' nmty (TType fc)
|
||||
nm <- inCurrentNS (UN n_in)
|
||||
(idx, metaval) <- metaVarI fc rig env nm ty
|
||||
(idx, metaval) <- metaVarI fc rig env' nm ty
|
||||
withCurrentLHS (Resolved idx)
|
||||
addUserHole nm
|
||||
pure (metaval, gnf env ty)
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%let Rig0 n Main.Nat (Main.S {k:20}) ((Main.Vect ((Main.plus {k:20}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:20}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTC
|
||||
Read TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%let Rig0 n ? (Main.S {k:20}) ((Main.Vect ((Main.plus {k:20}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:20}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:14} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just ws ((Main.Vect {k:14}) a) (%pi Rig0 Explicit Just y a (%let Rig1 zs ((Main.Vect (Main.S {k:14})) a) ((((Main.Cons [Just k = {k:14}]) [Just a = a]) y) ws) (%pi RigW Explicit Nothing a (%let Rig0 n Main.Nat (Main.S (Main.S {k:14})) ((Main.Vect ((Main.plus (Main.S (Main.S {k:14}))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:41} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:41}) a) (%pi RigW Explicit Just x a (%let Rig0 xs ((Main.Vect (Main.S {k:41})) a) ((((Main.Cons [Just k = {k:41}]) [Just a = a]) x) zs) (%let Rig0 n Main.Nat (Main.S {k:41}) ((Main.Vect ((Main.plus (Main.S {k:41})) m)) a))))))))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:69} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:69}) a) (%pi RigW Explicit Just x a (%let Rig0 xs ((Main.Vect (Main.S {k:69})) a) ((((Main.Cons [Just k = {k:69}]) [Just a = a]) x) zs) (%let Rig0 n Main.Nat (Main.S {k:69}) (%let Rig1 ts ((Main.Vect {k:69}) a) zs ((Main.Vect ((Main.plus (Main.S {k:69})) m)) a)))))))))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:14} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig1 Explicit Just ws ((Main.Vect {k:14}) a) (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:14})) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:14}))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:41} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:41}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:41})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:41})) m)) a))))))))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:69} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:69}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:69})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:69}) a) ((Main.Vect ((Main.plus (Main.S {k:69})) m)) a)))))))))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => ys[0]
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:22} : Main.Nat => \ys : (Main.Vect m[2] a[1]) => \xs : (Main.Vect {k:22}[1] a[2]) => \x : a[3] => (Main.Cons (Main.plus {k:22}[3] m[5]) a[4] x[0] (Main.append m[5] a[4] {k:22}[3] xs[1] ys[2]))
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => \0 n : Main.Nat => ys[1]
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:22} : Main.Nat => \ys : (Main.Vect m[2] a[1]) => \xs : (Main.Vect {k:22}[1] a[2]) => \x : a[3] => \0 n : Main.Nat => (Main.Cons (Main.plus {k:22}[4] m[6]) a[5] x[1] (Main.append m[6] a[5] {k:22}[4] xs[2] ys[3]))
|
||||
Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:191}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:191}]) z) y))]
|
||||
Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:298}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:298}]) z) w))]
|
||||
Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:448}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:448}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
|
||||
|
||||
Loading…
Reference in New Issue
Block a user