edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-25 05:43:19 +03:00
Code Issues Projects Releases Wiki Activity

Store number of locals in holes

Browse Source 
This gives useful information for expression search, because we can add
lambdas while we're still building the environment, and start looking at
locals after that.
This commit is contained in:
Edwin Brady 2019-06-02 01:23:01 +01:00
parent bf70aa07d2
commit af79e57ae2
15 changed files with 84 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/AutoSearch.idr
View File

@ -64,7 +64,7 @@ searchIfHole fc defaults ispair (S depth) def top env arg
defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
| Nothing => throw (CantSolveGoal fc [] top)
let Hole inv = definition gdef
let Hole _ inv = definition gdef
| _ => pure () -- already solved
let top' = if ispair
then type gdef

11
src/Core/Context.idr
View File

@ -238,7 +238,7 @@ data Def : Type where
(datacons : List Name) ->
(typehints : List (Name, Bool)) ->
Def
Hole : (invertible : Bool) -> Def
Hole : (numlocs : Nat) -> (invertible : Bool) -> Def
BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def
-- Constraints are integer references into the current map of
-- constraints in the UnifyState (see Core.UnifyState)
@ -258,7 +258,7 @@ Show Def where
= "TyCon " ++ show t ++ " " ++ show a ++ " " ++ show cons
show (ExternDef arity) = "<external def with arith " ++ show arity ++ ">"
show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
show (Hole inv) = "Hole"
show (Hole _ inv) = "Hole"
show (BySearch c depth def) = "Search in " ++ show def
show (Guess tm cs) = "Guess " ++ show tm ++ " when " ++ show cs
show ImpBind = "Bound name"
@ -277,7 +277,7 @@ TTC Def where
toBuf b (TCon t arity parampos detpos datacons _)
= do tag 4; toBuf b t; toBuf b arity; toBuf b parampos
toBuf b detpos; toBuf b datacons
toBuf b (Hole invertible) = do tag 5; toBuf b invertible
toBuf b (Hole locs invertible) = do tag 5; toBuf b locs; toBuf b invertible
toBuf b (BySearch c depth def)
= do tag 6; toBuf b c; toBuf b depth; toBuf b def
toBuf b (Guess guess constraints) = do tag 7; toBuf b guess; toBuf b constraints
@ -299,8 +299,9 @@ TTC Def where
4 => do t <- fromBuf r b; a <- fromBuf r b
ps <- fromBuf r b; dets <- fromBuf r b; cs <- fromBuf r b
pure (TCon t a ps dets cs [])
5 => do i <- fromBuf r b
pure (Hole i)
5 => do l <- fromBuf r b
i <- fromBuf r b
pure (Hole l i)
6 => do c <- fromBuf r b; depth <- fromBuf r b
def <- fromBuf r b
pure (BySearch c depth def)

6
src/Core/LinearCheck.idr
View File

@ -139,7 +139,7 @@ mutual
| Nothing => updateHoleUsageArgs useInHole var args
-- only update for holes with no definition yet
case definition gdef of
Hole _ =>
Hole _ _ =>
do let ty = type gdef
ty' <- updateHoleType useInHole var ty args
updateTy i ty'
@ -216,14 +216,14 @@ mutual
Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| _ => throw (UndefinedName fc n)
let expand = case (definition gdef, rig) of
(Hole _, _) => False
(Hole _ _, _) => False
(_, Rig0) => False
_ => True
if expand
then expandMeta rig erase env n idx (definition gdef) args
else do let ty : ClosedTerm
= case definition gdef of
Hole _ => unusedHoleArgs args (type gdef)
Hole _ _ => unusedHoleArgs args (type gdef)
_ => type gdef
nty <- nf defs env (embed ty)
lcheckMeta rig erase env fc n idx args [] nty

17
src/Core/TTC.idr
View File

@ -202,9 +202,10 @@ mutual
TTC (Term vars) where
toBuf b (Local {name} fc c idx y)
= if idx < 244
then toBuf b (prim__truncBigInt_B8 (12 + cast idx))
else do tag 0;
toBuf b fc -- toBuf b name
then do toBuf b (prim__truncBigInt_B8 (12 + cast idx))
toBuf b name
else do tag 0
toBuf b name
toBuf b idx
toBuf b (Ref fc nt name)
= do tag 1;
@ -246,9 +247,9 @@ mutual
fromBuf r b
= case !getTag of
0 => do fc <- fromBuf r b; -- name <- fromBuf r b
0 => do fc <- fromBuf r b; name <- fromBuf r b
idx <- fromBuf r b
pure (Local {name=UN "_"} fc Nothing idx (mkPrf idx))
pure (Local {name} fc Nothing idx (mkPrf idx))
1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b
pure (Ref fc nt name)
2 => do fc <- fromBuf {a = FC} r b; -- n <- fromBuf r b
@ -280,10 +281,10 @@ mutual
pure (PrimVal fc c)
10 => do fc <- fromBuf r b; pure (Erased fc)
11 => do fc <- fromBuf r b; pure (TType fc)
idxp => do -- fc <- fromBuf r b; -- name <- fromBuf r b
idxp => do -- fc <- fromBuf r b;
name <- fromBuf r b
let idx = fromInteger (prim__sextB8_BigInt idxp - 12)
pure (Local {name=UN "_"}
emptyFC Nothing idx (mkPrf idx))
pure (Local {name} emptyFC Nothing idx (mkPrf idx))
export
TTC Pat where

12
src/Core/Unify.idr
View File

@ -300,7 +300,7 @@ instantiate : {auto c : Ref Ctxt Defs} ->
Core ()
instantiate {newvars} loc env mname mref mdef locs otm tm
= do log 5 $ "Instantiating " ++ show tm ++ " in " ++ show newvars
let Hole _ = definition mdef
let Hole _ _ = definition mdef
| def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
case fullname mdef of
PV pv pi => throw (PatternVariableUnifies loc env (PV pv pi) otm)
@ -374,7 +374,7 @@ isDefInvertible : {auto c : Ref Ctxt Defs} ->
Int -> Core Bool
isDefInvertible i
= do defs <- get Ctxt
Just (Hole t) <- lookupDefExact (Resolved i) (gamma defs)
Just (Hole _ t) <- lookupDefExact (Resolved i) (gamma defs)
| _ => pure False
pure t
@ -490,7 +490,7 @@ mutual
Just mdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => throw (UndefinedName nfc mname)
let inv = case definition mdef of
Hole i => i
Hole _ i => i
_ => isPatName n
if inv
then unifyInvertible mode loc env mname mref margs margs' Nothing
@ -578,7 +578,7 @@ mutual
" with " ++ show qtm)
case !(patternEnv env args) of
Nothing =>
do Just (Hole inv) <- lookupDefExact (Resolved mref) (gamma defs)
do Just (Hole _ inv) <- lookupDefExact (Resolved mref) (gamma defs)
| _ => unifyPatVar mode loc env mname mref args tmnf
if inv
then unifyHoleApp mode loc env mname mref margs margs' tmnf
@ -940,7 +940,7 @@ setInvertible : {auto c : Ref Ctxt Defs} ->
setInvertible loc i
= updateDef (Resolved i)
(\old => case old of
Hole _ => Just (Hole True)
Hole locs _ => Just (Hole locs True)
_ => Nothing)
public export
@ -1056,7 +1056,7 @@ checkDots
Just ndef <- lookupDefExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
let h = case ndef of
Hole _ => True
Hole _ _ => True
_ => False
when (not (isNil (constraints cs)) || h) $

2
src/Core/UnifyState.idr
View File

@ -348,7 +348,7 @@ newMeta : {auto c : Ref Ctxt Defs} ->
newMeta {vars} fc rig env n ty nocyc
= do let hty = abstractEnvType fc env ty
let hole = record { noCycles = nocyc }
(newDef fc n rig [] hty Public (Hole False))
(newDef fc n rig [] hty Public (Hole (length env) False))
log 5 $ "Adding new meta " ++ show (n, fc, rig)
logTerm 10 ("New meta type " ++ show n) hty
idx <- addDef n hole

2
src/TTImp/Elab/Ambiguity.idr
View File

@ -295,7 +295,7 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
holeIn gam tm
= case getFn tm of
Meta _ _ idx _ =>
do Just (Hole _) <- lookupDefExact (Resolved idx) gam
do Just (Hole _ _) <- lookupDefExact (Resolved idx) gam
| _ => pure False
pure True
_ => pure False

4
src/TTImp/Elab/App.idr
View File

@ -179,7 +179,7 @@ mutual
Env Term vars -> Term vars -> Term vars -> Core Bool
solveIfUndefined env (Meta fc mname idx args) soln
= do defs <- get Ctxt
Just (Hole _) <- lookupDefExact (Resolved idx) (gamma defs)
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
| pure False
case !(patternEnvTm env args) of
Nothing => pure False
@ -253,7 +253,7 @@ mutual
pure ()
case elabMode elabinfo of
InLHS _ => -- reset hole and redo it with the unexpanded definition
do updateDef (Resolved idx) (const (Just (Hole False)))
do updateDef (Resolved idx) (const (Just (Hole 0 False)))
solveIfUndefined env metaval argv
pure ()
_ => pure ()

4
src/TTImp/Elab/ImplicitBind.idr
View File

@ -164,7 +164,7 @@ bindUnsolved {vars} fc elabmode _
(Env Term vars', Term vars', Term vars', SubVars outer vars'))) ->
Core ()
mkImplicit defs outerEnv subEnv (n, rig, (vs ** (env, tm, exp, sub)))
= do Just (Hole _) <- lookupDefExact n (gamma defs)
= do Just (Hole _ _) <- lookupDefExact n (gamma defs)
| _ => pure ()
bindtm <- makeBoundVar n rig outerEnv
sub subEnv
@ -304,7 +304,7 @@ implicitBind : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
implicitBind n
= do defs <- get Ctxt
Just (Hole _) <- lookupDefExact n (gamma defs)
Just (Hole _ _) <- lookupDefExact n (gamma defs)
| _ => pure ()
updateDef n (const (Just ImpBind))
removeHoleName n

27
src/TTImp/Interactive/ExprSearch.idr
View File

@ -87,12 +87,15 @@ searchIfHole fc opts defining topty env arg
defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
| Nothing => pure []
let Hole inv = definition gdef
let Hole _ inv = definition gdef
| _ => pure [(appInf arg,
!(normaliseHoles defs env (metaApp arg)))]
-- already solved
tms <- search fc rig (record { depth = k} opts)
defining topty (Resolved hole)
-- When we solve an argument, we're also building a lambda
-- expression for its environment, so we need to apply it to
-- the current environment to use it as an argument.
traverse (\tm => pure (appInf arg,
!(normaliseHoles defs env
(applyTo fc (embed tm) env)))) tms
@ -368,22 +371,22 @@ searchType : {auto c : Ref Ctxt Defs} ->
FC -> RigCount -> SearchOpts -> Env Term vars -> Maybe RecData ->
ClosedTerm ->
Nat -> Term vars -> Core (List (Term vars))
searchType fc rig opts env defining topty k (Bind bfc n (Pi c info ty) sc)
searchType fc rig opts env defining topty (S k) (Bind bfc n (Pi c info ty) sc)
= do let env' : Env Term (n :: _) = Pi c info ty :: env
log 10 $ "Introduced lambda, search for " ++ show sc
scVal <- searchType fc rig opts env' defining topty k sc
pure (map (Bind bfc n (Lam c info ty)) scVal)
searchType {vars} fc rig opts env defining topty Z (Bind bfc n (Pi c info ty) sc)
= -- try a local before creating a lambda...
tryUnify
(searchLocal fc rig opts env (Bind bfc n (Pi c info ty) sc) topty defining)
(do defs <- get Ctxt
let n' = UN (getArgName defs n vars !(nf defs env ty))
let env' : Env Term (n' :: _) = Pi c info ty :: env
let sc' = renameTop n' sc
log 10 $ "Introduced lambda, search for " ++ show sc'
scVal <- searchType fc rig opts env' defining topty Z sc'
pure (map (Bind bfc n' (Lam c info ty)) scVal))
getSuccessful fc rig opts False env ty topty defining
[searchLocal fc rig opts env (Bind bfc n (Pi c info ty) sc) topty defining,
(do defs <- get Ctxt
let n' = UN (getArgName defs n vars !(nf defs env ty))
let env' : Env Term (n' :: _) = Pi c info ty :: env
let sc' = renameTop n' sc
log 10 $ "Introduced lambda, search for " ++ show sc'
scVal <- searchType fc rig opts env' defining topty Z sc'
pure (map (Bind bfc n' (Lam c info ty)) scVal))]
searchType fc rig opts env defining topty _ ty
= case getFnArgs ty of
(Ref rfc (TyCon t ar) n, args) =>
@ -431,7 +434,7 @@ search fc rig opts defining topty n_in
-- The definition should be 'BySearch' at this stage,
-- if it's arising from an auto implicit
case definition gdef of
Hole _ => searchHole fc rig opts defining n Z topty defs gdef
Hole locs _ => searchHole fc rig opts defining n locs topty defs gdef
BySearch _ _ _ => searchHole fc rig opts defining n
!(getArity defs [] (type gdef))
topty defs gdef

2
tests/Main.idr
View File

@ -16,7 +16,7 @@ ttimpTests
"record001", "record002",
"rewrite001",
"qtt001", "qtt002", "qtt003",
"search001", "search002", "search003", "search004",
"search001", "search002", "search003", "search004", "search005",
"with001"]
chdir : String -> IO Bool

26
tests/ttimp/search005/Vect.yaff Normal file
View File

@ -0,0 +1,26 @@
data Bool : Type where
False : Bool
True : Bool
not : Bool -> Bool
not False = True
not True = False
data Nat : Type where
Z : Nat
S : Nat -> Nat
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
data Vect : ? -> Type -> Type where
Nil : Vect Z a
Cons : a -> Vect k a -> Vect (S k) a
append : Vect n a -> Vect m a -> Vect (plus n m) a
append Nil ys = ?appNil
append (Cons x xs) ys = ?appCons

5
tests/ttimp/search005/expected Normal file
View File

@ -0,0 +1,5 @@
Processing as TTImp
Written TTC
Yaffle> \0 {m:31} : Main.Nat => \0 {a:30} : Type => \ys : (Main.Vect {m:31}[1] {a:30}[0]) => ys[0]
Yaffle> \0 {m:43} : Main.Nat => \0 {a:42} : Type => \0 {k:41} : Main.Nat => \x : {a:42}[1] => \xs : (Main.Vect {k:41}[1] {a:42}[2]) => \ys : (Main.Vect {m:43}[4] {a:42}[3]) => (Main.Cons (Main.plus {k:41}[3] {m:43}[5]) {a:42}[4] x[2] (Main.append {m:43}[5] {a:42}[4] {k:41}[3] xs[1] ys[0]))
Yaffle> Bye for now!

3
tests/ttimp/search005/input Normal file
View File

@ -0,0 +1,3 @@
:es appNil
:es appCons
:q

3
tests/ttimp/search005/run Executable file
View File

@ -0,0 +1,3 @@
$1 Vect.yaff < input
rm -rf build