diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 2db5cf0..bf8cd5f 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -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) diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index abaf1b6..9e3ce76 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -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 diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index 466134d..93223f2 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -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) $ diff --git a/src/TTImp/Elab/Hole.idr b/src/TTImp/Elab/Hole.idr index 38b1a5c..766d85a 100644 --- a/src/TTImp/Elab/Hole.idr +++ b/src/TTImp/Elab/Hole.idr @@ -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) diff --git a/tests/ttimp/basic003/expected b/tests/ttimp/basic003/expected index dd8fe06..e59f476 100644 --- a/tests/ttimp/basic003/expected +++ b/tests/ttimp/basic003/expected @@ -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! diff --git a/tests/ttimp/qtt002/expected b/tests/ttimp/qtt002/expected index 8ffd0b9..a556967 100644 --- a/tests/ttimp/qtt002/expected +++ b/tests/ttimp/qtt002/expected @@ -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! diff --git a/tests/ttimp/search005/expected b/tests/ttimp/search005/expected index 75d73f6..377d4b8 100644 --- a/tests/ttimp/search005/expected +++ b/tests/ttimp/search005/expected @@ -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))]