mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-02 17:52:09 +03:00
More work on implicit search
Search on syntax rather than values, since this makes it easier to deal with local variables accurately, and since we need to go back to syntax anyway. We ensure that target types are normalised before search.
This commit is contained in:
Edwin Brady
parent
78fbfc84a8
commit
759524b838
@ -17,17 +17,8 @@ searchType : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) ->
|
||||
Env Term vars -> SearchEnv vars ->
|
||||
(target : NF vars) -> Core (NF vars)
|
||||
|
||||
export
|
||||
search : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) -> Env Term vars ->
|
||||
Core (Term vars)
|
||||
(defining : Name) -> (topTy : ClosedTerm) ->
|
||||
Env Term vars -> (target : Term vars) -> Core (Term vars)
|
||||
|
||||
record ArgInfo (vars : List Name) where
|
||||
constructor MkArgInfo
|
||||
@ -35,9 +26,7 @@ record ArgInfo (vars : List Name) where
|
||||
argRig : RigCount
|
||||
appInf : AppInfo
|
||||
metaApp : Term vars
|
||||
argType : Term vars -- ^ Needs to be Term, not NF, since solving other holes
|
||||
-- may mean the NF is no longer up to date (it may
|
||||
-- contain hole names)
|
||||
argType : Term vars
|
||||
|
||||
mkArgs : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
@ -57,48 +46,39 @@ mkArgs fc rigc env (NBind nfc x (Pi c p ty) sc)
|
||||
pure (MkArgInfo idx argRig (appInf Nothing p) arg argTy :: rest, restTy)
|
||||
mkArgs fc rigc env ty = pure ([], ty)
|
||||
|
||||
closureApply : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> Env Term vars -> Closure vars -> List (ArgInfo vars) ->
|
||||
Core (Term vars)
|
||||
closureApply fc env (MkClosure _ [] _ tm) args
|
||||
= pure (applyInfo fc tm (map (\i => (appInf i, metaApp i)) args))
|
||||
closureApply fc env (MkNFClosure nf) args
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
tm <- quote empty env nf
|
||||
pure (applyInfo fc tm (map (\i => (appInf i, metaApp i)) args))
|
||||
closureApply _ _ _ _ = throw (InternalError "Wrong argument form in AutoSearch")
|
||||
|
||||
searchIfHole : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) -> Env Term vars ->
|
||||
SearchEnv vars ->
|
||||
(defaults : Bool) -> (ispair : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : ClosedTerm) -> Env Term vars ->
|
||||
(arg : ArgInfo vars) ->
|
||||
Core ()
|
||||
searchIfHole fc defaults Z def top env locs arg
|
||||
= throw (CantSolveGoal fc env top) -- possibly should say depth limit hit?
|
||||
searchIfHole fc defaults (S depth) def top env locs arg
|
||||
searchIfHole fc defaults ispair Z def top env arg
|
||||
= throw (CantSolveGoal fc [] top) -- possibly should say depth limit hit?
|
||||
searchIfHole fc defaults ispair (S depth) def top env arg
|
||||
= do let hole = holeID arg
|
||||
let rig = argRig arg
|
||||
|
||||
defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
|
||||
| Nothing => throw (CantSolveGoal fc env top)
|
||||
| Nothing => throw (CantSolveGoal fc [] top)
|
||||
let Hole inv = definition gdef
|
||||
| _ => pure () -- already solved
|
||||
argTyNF <- nf defs env (argType arg)
|
||||
argdef <- searchType fc rig defaults depth def top env locs argTyNF
|
||||
vs <- unify InTerm fc env !(nf defs env (metaApp arg)) argdef
|
||||
let top' = if ispair
|
||||
then type gdef
|
||||
else top
|
||||
|
||||
argdef <- searchType fc rig defaults depth def top' env
|
||||
!(normaliseScope defs env (argType arg))
|
||||
vs <- unify InTerm fc env (metaApp arg) argdef
|
||||
let [] = constraints vs
|
||||
| _ => throw (CantSolveGoal fc env top)
|
||||
| _ => throw (CantSolveGoal fc [] top)
|
||||
pure ()
|
||||
|
||||
successful : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List (Core (NF vars)) ->
|
||||
Core (List (Either Error (NF vars, Defs, UState)))
|
||||
List (Core (Term vars)) ->
|
||||
Core (List (Either Error (Term vars, Defs, UState)))
|
||||
successful [] = pure []
|
||||
successful (elab :: elabs)
|
||||
= do ust <- get UST
|
||||
@ -121,14 +101,14 @@ successful (elab :: elabs)
|
||||
|
||||
exactlyOne : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> Env Term vars -> (topTy : Term vars) ->
|
||||
List (Core (NF vars)) ->
|
||||
Core (NF vars)
|
||||
FC -> Env Term vars -> (topTy : ClosedTerm) ->
|
||||
List (Core (Term vars)) ->
|
||||
Core (Term vars)
|
||||
exactlyOne fc env top [elab]
|
||||
= catch elab
|
||||
(\err => case err of
|
||||
CantSolveGoal _ _ _ => throw err
|
||||
_ => throw (CantSolveGoal fc env top))
|
||||
_ => throw (CantSolveGoal fc [] top))
|
||||
exactlyOne fc env top all
|
||||
= do elabs <- successful all
|
||||
case rights elabs of
|
||||
@ -137,99 +117,121 @@ exactlyOne fc env top all
|
||||
put Ctxt defs
|
||||
commit
|
||||
pure res
|
||||
[] => throw (CantSolveGoal fc env top)
|
||||
rs => do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
rs' <- traverse (Normalise.quote empty env) (map fst rs)
|
||||
throw (AmbiguousSearch fc env rs')
|
||||
[] => throw (CantSolveGoal fc [] top)
|
||||
rs => throw (AmbiguousSearch fc env (map fst rs))
|
||||
|
||||
-- We can only resolve things which are at any multiplicity. Expression
|
||||
-- search happens before linearity checking and we can't guarantee that just
|
||||
-- because something is apparently available now, it will be available by the
|
||||
-- time we get to linearity checking.
|
||||
getAllEnv : FC -> (done : List Name) ->
|
||||
Env Term vars -> List (Term (done ++ vars), Term (done ++ vars))
|
||||
getAllEnv fc done [] = []
|
||||
getAllEnv {vars = v :: vs} fc done (b :: env)
|
||||
= let rest = getAllEnv fc (done ++ [v]) env in
|
||||
if multiplicity b == RigW
|
||||
then let MkVar p = weakenVar {name=v} {inner=v :: vs} done First in
|
||||
(Local fc Nothing _ p,
|
||||
rewrite appendAssociative done [v] vs in
|
||||
weakenNs (done ++ [v]) (binderType b)) ::
|
||||
rewrite appendAssociative done [v] vs in rest
|
||||
else rewrite appendAssociative done [v] vs in rest
|
||||
|
||||
searchLocalWith : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : ClosedTerm) ->
|
||||
Env Term vars -> List (Term vars, Term vars) ->
|
||||
(target : NF vars) -> Core (Term vars)
|
||||
searchLocalWith fc rigc defaults depth def top env [] target
|
||||
= throw (CantSolveGoal fc [] top)
|
||||
searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) target
|
||||
= tryUnify
|
||||
(do defs <- get Ctxt
|
||||
nty <- nf defs env ty
|
||||
findPos defs prf id nty target)
|
||||
(searchLocalWith fc rigc defaults depth def top env rest target)
|
||||
where
|
||||
findDirect : Defs -> Term vars ->
|
||||
(Term vars -> Term vars) ->
|
||||
NF vars -> -- local's type
|
||||
(target : NF vars) ->
|
||||
Core (Term vars)
|
||||
findDirect defs prf f ty target
|
||||
= do (args, appTy) <- mkArgs fc rigc env ty
|
||||
-- TODO: Can only use the local if its type is not an unsolved hole
|
||||
ures <- unify InTerm fc env target appTy
|
||||
let [] = constraints ures
|
||||
| _ => throw (CantSolveGoal fc [] top)
|
||||
let candidate = applyInfo fc (f prf)
|
||||
(map (\i => (appInf i, metaApp i)) args)
|
||||
logTermNF 10 "Candidate " env candidate
|
||||
traverse (searchIfHole fc defaults False depth def top env) args
|
||||
pure candidate
|
||||
|
||||
findPos : Defs -> Term vars ->
|
||||
(Term vars -> Term vars) ->
|
||||
NF vars -> -- local's type
|
||||
(target : NF vars) ->
|
||||
Core (Term vars)
|
||||
findPos defs prf f nty@(NTCon pfc pn _ _ [(xp, xty), (yp, yty)]) target
|
||||
= tryUnify (findDirect defs prf f nty target)
|
||||
(do fname <- maybe (throw (CantSolveGoal fc [] top))
|
||||
pure
|
||||
(fstName defs)
|
||||
sname <- maybe (throw (CantSolveGoal fc [] top))
|
||||
pure
|
||||
(sndName defs)
|
||||
if isPairType pn defs
|
||||
then do empty <- clearDefs defs
|
||||
xtytm <- quote empty env xty
|
||||
ytytm <- quote empty env yty
|
||||
tryUnify
|
||||
(do xtynf <- evalClosure defs xty
|
||||
findPos defs prf
|
||||
(\arg => applyInfo fc (Ref fc Func fname)
|
||||
[(xp, xtytm),
|
||||
(yp, ytytm),
|
||||
(explApp Nothing, f arg)])
|
||||
xtynf target)
|
||||
(do ytynf <- evalClosure defs yty
|
||||
findPos defs prf
|
||||
(\arg => applyInfo fc (Ref fc Func sname)
|
||||
[(xp, xtytm),
|
||||
(yp, ytytm),
|
||||
(explApp Nothing, f arg)])
|
||||
ytynf target)
|
||||
else throw (CantSolveGoal fc [] top))
|
||||
findPos defs prf f nty target
|
||||
= findDirect defs prf f nty target
|
||||
|
||||
searchLocal : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) ->
|
||||
Env Term vars -> SearchEnv vars -> SearchEnv vars ->
|
||||
(target : NF vars) -> Core (NF vars)
|
||||
searchLocal fc rigc defaults depth def top env locs [] target
|
||||
= throw (CantSolveGoal fc env top)
|
||||
searchLocal {vars} fc rigc defaults depth def top env locs ((ty, c) :: rest) target
|
||||
= tryUnify
|
||||
(do defs <- get Ctxt
|
||||
findPos defs c id ty target)
|
||||
|
||||
-- do (args, appTy) <- mkArgs fc rigc env ty
|
||||
-- -- TODO: Can only use the local if it's not an unsolved hole
|
||||
-- ures <- unify InTerm fc env target appTy
|
||||
-- let [] = constraints ures
|
||||
-- | _ => throw (CantSolveGoal fc env top)
|
||||
-- candidate <- closureApply fc c args
|
||||
-- logTermNF 10 "Candidate " env candidate
|
||||
-- traverse (searchIfHole fc defaults depth def top env locs) args
|
||||
-- defs <- get Ctxt
|
||||
-- nf defs env candidate)
|
||||
(searchLocal fc rigc defaults depth def top env locs rest target)
|
||||
where
|
||||
findDirect : Defs -> Closure vars ->
|
||||
(Closure vars -> Closure vars) ->
|
||||
NF vars -> -- local's type
|
||||
(target : NF vars) ->
|
||||
Core (NF vars)
|
||||
findDirect defs prf f ty target
|
||||
= do (args, appTy) <- mkArgs fc rigc env ty
|
||||
-- TODO: Can only use the local if it's not an unsolved hole
|
||||
ures <- unify InTerm fc env target appTy
|
||||
let [] = constraints ures
|
||||
| _ => throw (CantSolveGoal fc env top)
|
||||
candidate <- closureApply fc env (f prf) args
|
||||
logTermNF 10 "Candidate " env candidate
|
||||
traverse (searchIfHole fc defaults depth def top env locs) args
|
||||
defs <- get Ctxt
|
||||
nf defs env candidate
|
||||
(defining : Name) -> (topTy : ClosedTerm) ->
|
||||
Env Term vars ->
|
||||
(target : NF vars) -> Core (Term vars)
|
||||
searchLocal fc rig defaults depth def top env target
|
||||
= searchLocalWith fc rig defaults depth def top env (getAllEnv fc [] env) target
|
||||
|
||||
findPos : Defs -> Closure vars ->
|
||||
(Closure vars -> Closure vars) ->
|
||||
NF vars -> -- local's type
|
||||
(target : NF vars) ->
|
||||
Core (NF vars)
|
||||
findPos defs prf f ty@(NTCon pfc pn _ _ [(xp, xty), (yp, yty)]) target
|
||||
= tryUnify (findDirect defs prf f ty target)
|
||||
(do log 0 (show (pn, isPairType pn defs, fstName defs))
|
||||
fname <- maybe (throw (CantSolveGoal fc env top))
|
||||
pure
|
||||
(fstName defs)
|
||||
sname <- maybe (throw (CantSolveGoal fc env top))
|
||||
pure
|
||||
(sndName defs)
|
||||
if isPairType pn defs
|
||||
then tryUnify
|
||||
(do xtynf <- evalClosure defs xty
|
||||
logNF 0 "Trying fst" env xtynf
|
||||
findPos defs prf
|
||||
(\arg => MkNFClosure $ NApp fc (NRef Func fname)
|
||||
[(xp, xty),
|
||||
(yp, yty),
|
||||
(explApp Nothing, f arg)])
|
||||
xtynf target)
|
||||
(do ytynf <- evalClosure defs yty
|
||||
findPos defs prf
|
||||
(\arg => MkNFClosure $ NApp fc (NRef Func sname)
|
||||
[(xp, xty),
|
||||
(yp, yty),
|
||||
(explApp Nothing, f arg)])
|
||||
ytynf target)
|
||||
else throw (CantSolveGoal fc env top))
|
||||
findPos defs prf f ty target
|
||||
= findDirect defs prf f ty target
|
||||
isPairNF : Env Term vars -> NF vars -> Defs -> Core Bool
|
||||
isPairNF env (NTCon _ n _ _ _) defs
|
||||
= pure $ isPairType n defs
|
||||
isPairNF env (NBind fc b (Pi _ _ _) sc) defs
|
||||
= isPairNF env !(sc defs (toClosure defaultOpts env (Erased fc))) defs
|
||||
isPairNF _ _ _ = pure False
|
||||
|
||||
searchName : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) ->
|
||||
Env Term vars -> SearchEnv vars -> (target : NF vars) ->
|
||||
(defining : Name) -> (topTy : ClosedTerm) ->
|
||||
Env Term vars -> (target : NF vars) ->
|
||||
(Name, GlobalDef) ->
|
||||
Core (NF vars)
|
||||
searchName fc rigc defaults depth def top env locs target (n, ndef)
|
||||
Core (Term vars)
|
||||
searchName fc rigc defaults depth def top env target (n, ndef)
|
||||
= do defs <- get Ctxt
|
||||
let ty = type ndef
|
||||
let namety : NameType
|
||||
@ -241,29 +243,29 @@ searchName fc rigc defaults depth def top env locs target (n, ndef)
|
||||
(args, appTy) <- mkArgs fc rigc env nty
|
||||
ures <- unify InTerm fc env target appTy
|
||||
let [] = constraints ures
|
||||
| _ => throw (CantSolveGoal fc env top)
|
||||
| _ => throw (CantSolveGoal fc [] top)
|
||||
ispair <- isPairNF env nty defs
|
||||
let candidate = applyInfo fc (Ref fc namety n)
|
||||
(map (\i => (appInf i, metaApp i)) args)
|
||||
logTermNF 10 "Candidate " env candidate
|
||||
traverse (searchIfHole fc defaults depth def top env locs) args
|
||||
defs <- get Ctxt
|
||||
nf defs env candidate
|
||||
|
||||
traverse (searchIfHole fc defaults ispair depth def top env) args
|
||||
pure candidate
|
||||
|
||||
searchNames : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) ->
|
||||
Env Term vars -> SearchEnv vars -> List Name ->
|
||||
(target : NF vars) -> Core (NF vars)
|
||||
searchNames fc rigc defaults depth defining topty env locs [] target
|
||||
= throw (CantSolveGoal fc env topty)
|
||||
searchNames fc rigc defaults depth defining topty env locs (n :: ns) target
|
||||
(defining : Name) -> (topTy : ClosedTerm) ->
|
||||
Env Term vars -> List Name ->
|
||||
(target : NF vars) -> Core (Term vars)
|
||||
searchNames fc rigc defaults depth defining topty env [] target
|
||||
= throw (CantSolveGoal fc [] topty)
|
||||
searchNames fc rigc defaults depth defining topty env (n :: ns) target
|
||||
= do defs <- get Ctxt
|
||||
visnsm <- traverse (visible (gamma defs) (currentNS defs)) (n :: ns)
|
||||
let visns = mapMaybe id visnsm
|
||||
exactlyOne fc env topty
|
||||
(map (searchName fc rigc defaults depth defining topty env locs target) visns)
|
||||
(map (searchName fc rigc defaults depth defining topty env target) visns)
|
||||
where
|
||||
visible : Context GlobalDef ->
|
||||
List String -> Name -> Core (Maybe (Name, GlobalDef))
|
||||
@ -277,9 +279,9 @@ searchNames fc rigc defaults depth defining topty env locs (n :: ns) target
|
||||
concreteDets : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> Bool ->
|
||||
Env Term vars -> Term vars ->
|
||||
Env Term vars -> (top : ClosedTerm) ->
|
||||
(pos : Nat) -> (dets : List Nat) ->
|
||||
List (AppInfo, Closure vars) ->
|
||||
(args : List (AppInfo, Closure vars)) ->
|
||||
Core ()
|
||||
concreteDets fc defaults env top pos dets [] = pure ()
|
||||
concreteDets {vars} fc defaults env top pos dets ((p, arg) :: args)
|
||||
@ -299,47 +301,56 @@ concreteDets {vars} fc defaults env top pos dets ((p, arg) :: args)
|
||||
concrete defs argnf False) args
|
||||
pure ()
|
||||
concrete defs (NApp _ (NMeta n i _) _) True
|
||||
= throw (DeterminingArg fc n i env top)
|
||||
= throw (DeterminingArg fc n i [] top)
|
||||
concrete defs (NApp _ (NMeta n i _) _) False
|
||||
= throw (CantSolveGoal fc env top)
|
||||
= throw (CantSolveGoal fc [] top)
|
||||
concrete defs tm top = pure ()
|
||||
|
||||
-- Declared at the top
|
||||
searchType fc rigc defaults depth def top env locs (NBind nfc x (Pi c p ty) sc)
|
||||
= pure (NBind nfc x (Lam c p ty)
|
||||
(\defs, arg => searchType fc rigc defaults depth def top env
|
||||
((ty, arg) :: locs) !(sc defs arg)))
|
||||
searchType {vars} fc rigc defaults depth def top env locs target@(NTCon tfc tyn t a args)
|
||||
= if a == length args
|
||||
then do logNF 10 "Next target: " env target
|
||||
sd <- getSearchData fc defaults tyn
|
||||
-- Check determining arguments are okay for 'args'
|
||||
concreteDets fc defaults env top 0 (detArgs sd) args
|
||||
tryGroups (hintGroups sd)
|
||||
else throw (CantSolveGoal fc env top)
|
||||
searchType fc rigc defaults depth def top env (Bind nfc x (Pi c p ty) sc)
|
||||
= pure (Bind nfc x (Lam c p ty)
|
||||
!(searchType fc rigc defaults depth def top
|
||||
(Pi c p ty :: env) sc))
|
||||
searchType {vars} fc rigc defaults depth def top env target
|
||||
= do defs <- get Ctxt
|
||||
nty <- nf defs env target
|
||||
case nty of
|
||||
NTCon tfc tyn t a args =>
|
||||
if a == length args
|
||||
then do logNF 10 "Next target: " env nty
|
||||
sd <- getSearchData fc defaults tyn
|
||||
-- Check determining arguments are okay for 'args'
|
||||
concreteDets fc defaults env top 0 (detArgs sd) args
|
||||
tryGroups nty (hintGroups sd)
|
||||
else throw (CantSolveGoal fc [] top)
|
||||
_ => do logNF 10 "Next target: " env nty
|
||||
searchLocal fc rigc defaults depth def top env nty
|
||||
where
|
||||
ambig : Error -> Bool
|
||||
ambig (AmbiguousSearch _ _ _) = True
|
||||
ambig _ = False
|
||||
|
||||
tryGroups : List (List Name) -> Core (NF vars)
|
||||
tryGroups [] = throw (CantSolveGoal fc env top)
|
||||
tryGroups (g :: gs)
|
||||
tryGroups : NF vars -> List (List Name) -> Core (Term vars)
|
||||
tryGroups nty [] = throw (CantSolveGoal fc [] top)
|
||||
tryGroups nty (g :: gs)
|
||||
= handleUnify
|
||||
(searchNames fc rigc defaults depth def top env locs g target)
|
||||
(searchNames fc rigc defaults depth def top env g nty)
|
||||
(\err => if ambig err || isNil gs
|
||||
then throw err
|
||||
else tryGroups gs)
|
||||
searchType fc rigc defaults depth def top env locs target
|
||||
= do logNF 10 "Next target: " env target
|
||||
searchLocal fc rigc defaults depth def top env locs locs target
|
||||
else tryGroups nty gs)
|
||||
|
||||
-- Declared at the top
|
||||
search fc rigc defaults depth def top env
|
||||
-- Declared in Core.Unify as:
|
||||
-- search : {auto c : Ref Ctxt Defs} ->
|
||||
-- {auto u : Ref UST UState} ->
|
||||
-- FC -> RigCount ->
|
||||
-- (defaults : Bool) -> (depth : Nat) ->
|
||||
-- (defining : Name) -> (topTy : Term vars) -> Env Term vars ->
|
||||
-- Core (Term vars)
|
||||
Core.Unify.search fc rigc defaults depth def top env
|
||||
= do defs <- get Ctxt
|
||||
target <- nf defs env top
|
||||
logNF 0 "Initial target: " env target
|
||||
tm <- searchType fc rigc defaults depth def top env [] target
|
||||
empty <- clearDefs defs
|
||||
quote empty env tm
|
||||
|
||||
logTerm 10 "Initial target: " top
|
||||
tm <- searchType fc rigc defaults depth def
|
||||
(abstractEnvType fc env top) env
|
||||
!(normaliseScope defs env top)
|
||||
defs <- get Ctxt
|
||||
quote defs env tm
|
||||
|
||||
@ -233,6 +233,7 @@ data Def : Type where
|
||||
(typehints : List (Name, Bool)) ->
|
||||
Def
|
||||
Hole : (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)
|
||||
Guess : (guess : ClosedTerm) -> (constraints : List Int) -> Def
|
||||
@ -247,6 +248,7 @@ Show Def where
|
||||
show (TCon t a ps ds cons hints)
|
||||
= "TyCon " ++ show t ++ " " ++ show a ++ " " ++ show cons
|
||||
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 = "Implicitly bound"
|
||||
|
||||
@ -260,7 +262,9 @@ TTC Def where
|
||||
= do tag 3; toBuf b t; toBuf b arity; toBuf b parampos
|
||||
toBuf b detpos; toBuf b datacons
|
||||
toBuf b (Hole invertible) = do tag 4; toBuf b invertible
|
||||
toBuf b (Guess guess constraints) = do tag 5; toBuf b guess; toBuf b constraints
|
||||
toBuf b (BySearch c depth def)
|
||||
= do tag 5; toBuf b c; toBuf b depth; toBuf b def
|
||||
toBuf b (Guess guess constraints) = do tag 6; toBuf b guess; toBuf b constraints
|
||||
toBuf b ImpBind = tag 6
|
||||
|
||||
fromBuf r b
|
||||
@ -278,9 +282,12 @@ TTC Def where
|
||||
pure (TCon t a ps dets cs [])
|
||||
4 => do i <- fromBuf r b;
|
||||
pure (Hole i)
|
||||
5 => do g <- fromBuf r b; cs <- fromBuf r b
|
||||
5 => do c <- fromBuf r b; depth <- fromBuf r b
|
||||
def <- fromBuf r b
|
||||
pure (BySearch c depth def)
|
||||
6 => do g <- fromBuf r b; cs <- fromBuf r b
|
||||
pure (Guess g cs)
|
||||
6 => pure ImpBind
|
||||
7 => pure ImpBind
|
||||
_ => corrupt "Def"
|
||||
|
||||
public export
|
||||
|
||||
@ -446,6 +446,15 @@ normaliseHoles : Defs -> Env Term free -> Term free -> Core (Term free)
|
||||
normaliseHoles defs env tm
|
||||
= quote defs env !(nfOpts withHoles defs env tm)
|
||||
|
||||
-- Normalise, but without normalising the types of binders. Dealing with
|
||||
-- binders is the slow part of normalisation so whenever we can avoid it, it's
|
||||
-- a big win
|
||||
export
|
||||
normaliseScope : Defs -> Env Term vars -> Term vars -> Core (Term vars)
|
||||
normaliseScope defs env (Bind fc n b sc)
|
||||
= pure $ Bind fc n b !(normaliseScope defs (b :: env) sc)
|
||||
normaliseScope defs env tm = normalise defs env tm
|
||||
|
||||
public export
|
||||
interface Convert (tm : List Name -> Type) where
|
||||
convert : Defs -> Env Term vars ->
|
||||
|
||||
@ -432,6 +432,7 @@ insertVar {n} {outer = (x :: xs)} (S i) (Later y)
|
||||
= let MkVar prf = insertVar {n} i y in
|
||||
MkVar (Later prf)
|
||||
|
||||
export
|
||||
weakenVar : (ns : List Name) -> {idx : Nat} -> .(IsVar name idx inner) ->
|
||||
Var (ns ++ inner)
|
||||
weakenVar [] x = MkVar x
|
||||
@ -852,7 +853,8 @@ export Show (Term vars) where
|
||||
showApp : Term vars -> List (AppInfo, Term vars) -> String
|
||||
showApp (Local {name} _ _ idx _) [] = show name ++ "[" ++ show idx ++ "]"
|
||||
showApp (Ref _ _ n) [] = show n
|
||||
showApp (Meta _ n _ args) [] = "?" ++ show n ++ "_" ++ show (length args)
|
||||
showApp (Meta _ n _ args) []
|
||||
= "?" ++ show n ++ "_" ++ show args
|
||||
showApp (Bind _ x (Lam c p ty) sc) []
|
||||
= "\\" ++ showCount c ++ show x ++ " : " ++ show ty ++
|
||||
" => " ++ show sc
|
||||
|
||||
@ -74,6 +74,15 @@ unify : Unify tm =>
|
||||
Core UnifyResult
|
||||
unify {c} {u} = unifyD c u
|
||||
|
||||
-- Defined in Core.AutoSearch
|
||||
export
|
||||
search : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
(defaults : Bool) -> (depth : Nat) ->
|
||||
(defining : Name) -> (topTy : Term vars) -> Env Term vars ->
|
||||
Core (Term vars)
|
||||
|
||||
ufail : FC -> String -> Core a
|
||||
ufail loc msg = throw (GenericMsg loc msg)
|
||||
|
||||
@ -609,6 +618,12 @@ data SolveMode = Normal -- during elaboration: unifies and searches
|
||||
| Defaults -- unifies and searches for default hints only
|
||||
| LastChance -- as normal, but any failure throws rather than delays
|
||||
|
||||
Eq SolveMode where
|
||||
Normal == Normal = True
|
||||
Defaults == Defaults = True
|
||||
LastChance == LastChance = True
|
||||
_ == _ = False
|
||||
|
||||
retry : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode -> Int -> Core UnifyResult
|
||||
@ -643,6 +658,22 @@ retryGuess mode smode (hid, (loc, hname))
|
||||
Nothing => pure False
|
||||
Just def =>
|
||||
case definition def of
|
||||
BySearch rig depth defining =>
|
||||
handleUnify
|
||||
(do tm <- search loc rig (smode == Defaults) depth defining
|
||||
(type def) []
|
||||
let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def
|
||||
logTerm 5 ("Solved " ++ show hname) tm
|
||||
addDef (Resolved hid) gdef
|
||||
removeGuess hid
|
||||
pure True)
|
||||
(\err => case err of
|
||||
DeterminingArg _ n i _ _ => ?setInvertible
|
||||
_ => do logTerm 5 ("Search failed for " ++ show hname)
|
||||
(type def)
|
||||
case smode of
|
||||
LastChance => throw err
|
||||
_ => pure False) -- Postpone again
|
||||
Guess tm constrs =>
|
||||
do cs' <- traverse (retry mode) constrs
|
||||
let csAll = unionAll cs'
|
||||
|
||||
@ -61,6 +61,7 @@ record UState where
|
||||
holes : IntMap (FC, Name) -- All metavariables with no definition yet.
|
||||
-- 'Int' is the 'Resolved' name
|
||||
guesses : IntMap (FC, Name) -- Names which will be defined when constraints solved
|
||||
-- (also includes auto implicit searches)
|
||||
currentHoles : IntMap (FC, Name) -- Holes introduced this elaboration session
|
||||
constraints : IntMap Constraint -- map for finding constraints by ID
|
||||
nextName : Int
|
||||
@ -300,6 +301,27 @@ newConstant {vars} fc rig env tm ty constrs
|
||||
envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
|
||||
rewrite sym (appendNilRightNeutral vars) in args
|
||||
|
||||
-- Create a new search with the given name and return type,
|
||||
-- and return a term which is the name applied to the environment
|
||||
-- (and which has the given type)
|
||||
export
|
||||
newSearch : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount -> Nat -> Name ->
|
||||
Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
|
||||
newSearch {vars} fc rig depth def env n ty
|
||||
= do let hty = abstractEnvType fc env ty
|
||||
let hole = newDef fc n rig hty Public (BySearch rig depth def)
|
||||
log 10 $ "Adding new search " ++ show n
|
||||
idx <- addDef n hole
|
||||
addGuessName fc n idx
|
||||
pure (idx, Meta fc n idx envArgs)
|
||||
where
|
||||
envArgs : List (Term vars)
|
||||
envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
|
||||
rewrite sym (appendNilRightNeutral vars) in args
|
||||
|
||||
|
||||
export
|
||||
tryErrorUnify : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
|
||||
@ -263,14 +263,14 @@ mutual
|
||||
let argTyG = gnf env argTy
|
||||
-- Can't use 'metaVar' to record it for binding because it's
|
||||
-- in a different scope... so it'll stay global
|
||||
(_, retTy) <- newMeta {vars = argn :: vars}
|
||||
fc Rig0 (Pi RigW Explicit argTy :: env)
|
||||
(_, retTy) <- newMeta -- {vars = argn :: vars}
|
||||
fc Rig0 env -- (Pi RigW Explicit argTy :: env)
|
||||
retn (TType fc)
|
||||
(argv, argt) <- check rig (nextLevel elabinfo)
|
||||
env arg (Just argTyG)
|
||||
let fntm = App fc tm (appInf Nothing Explicit) argv
|
||||
defs <- get Ctxt
|
||||
fnty <- nf defs env (Bind fc argn (Let RigW argv argTy) retTy)
|
||||
fnty <- nf defs env retTy -- (Bind fc argn (Let RigW argv argTy) retTy)
|
||||
logNF 10 "Function type" env fnty
|
||||
maybe (pure ()) (logGlue 10 "Expected type" env) expty
|
||||
checkAppWith rig elabinfo env fc fntm fnty expargs impargs kr expty
|
||||
|
||||
@ -189,6 +189,15 @@ metaVar fc rig env n ty
|
||||
= do (_, tm) <- newMeta fc rig env n ty
|
||||
pure tm
|
||||
|
||||
export
|
||||
searchVar : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount -> Nat -> Name ->
|
||||
Env Term vars -> Name -> Term vars -> Core (Term vars)
|
||||
searchVar fc rig depth def env n ty
|
||||
= do (_, tm) <- newSearch fc rig depth def env n ty
|
||||
pure tm
|
||||
|
||||
-- Elaboration info (passed to recursive calls)
|
||||
public export
|
||||
record ElabInfo where
|
||||
|
||||
@ -94,7 +94,19 @@ checkTerm rig elabinfo env (IApp fc fn arg) exp
|
||||
= checkApp rig elabinfo env fc fn [arg] [] exp
|
||||
checkTerm rig elabinfo env (IImplicitApp fc fn nm arg) exp
|
||||
= checkApp rig elabinfo env fc fn [] [(nm, arg)] exp
|
||||
|
||||
checkTerm rig elabinfo env (ISearch fc depth) (Just gexpty)
|
||||
= do est <- get EST
|
||||
nm <- genName "search"
|
||||
expty <- getTerm gexpty
|
||||
sval <- searchVar fc rig depth (defining est) env nm expty
|
||||
pure (sval, gexpty)
|
||||
checkTerm rig elabinfo env (ISearch fc depth) Nothing
|
||||
= do est <- get EST
|
||||
nmty <- genName "searchTy"
|
||||
ty <- metaVar fc Rig0 env nmty (TType fc)
|
||||
nm <- genName "search"
|
||||
sval <- searchVar fc rig depth (defining est) env nm ty
|
||||
pure (sval, gnf env ty)
|
||||
checkTerm rig elabinfo env (IBindHere fc binder sc) exp
|
||||
= checkBindHere rig elabinfo env fc binder sc exp
|
||||
checkTerm rig elabinfo env (IBindVar fc n) exp
|
||||
|
||||
@ -27,6 +27,11 @@ atom fname
|
||||
symbol "?"
|
||||
end <- location
|
||||
pure (Implicit (MkFC fname start end) False)
|
||||
<|> do start <- location
|
||||
symbol "%"
|
||||
exactIdent "search"
|
||||
end <- location
|
||||
pure (ISearch (MkFC fname start end) 1000)
|
||||
<|> do start <- location
|
||||
x <- name
|
||||
end <- location
|
||||
|
||||
@ -17,6 +17,7 @@ mutual
|
||||
(argTy : RawImp) -> (lamTy : RawImp) -> RawImp
|
||||
IApp : FC -> RawImp -> RawImp -> RawImp
|
||||
IImplicitApp : FC -> RawImp -> Maybe Name -> RawImp -> RawImp
|
||||
ISearch : FC -> (depth : Nat) -> RawImp
|
||||
|
||||
-- Any implicit bindings in the scope should be bound here, using
|
||||
-- the given binder
|
||||
@ -50,6 +51,8 @@ mutual
|
||||
= "(" ++ show f ++ " " ++ show a ++ ")"
|
||||
show (IImplicitApp fc f n a)
|
||||
= "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
|
||||
show (ISearch fc d)
|
||||
= "%search"
|
||||
show (IBindHere fc b sc)
|
||||
= "(%bindhere " ++ show sc ++ ")"
|
||||
show (IBindVar fc n) = "$" ++ n
|
||||
|
||||
Loading…
Reference in New Issue
Block a user