edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-03 18:25:16 +03:00
Code Issues Projects Releases Wiki Activity

Fix 'last chance' auto search

Browse Source 
Need to record the solution as well as find it! Too much copying from
Blodwen without thinking here :)
This commit is contained in:
Edwin Brady 2019-06-17 12:35:42 +01:00
parent 6a72508e80
commit f1becb4ae0
2 changed files with 10 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Core/AutoSearch.idr
View File

@ -448,10 +448,11 @@ searchType {vars} fc rigc defaults trying depth def top env target
-- Core (Term vars)
Core.Unify.search fc rigc defaults depth def top env
= do defs <- get Ctxt
logTerm 2 "Initial target: " top
logTermNF 2 "Initial target: " env top
log 2 $ "Running search with defaults " ++ show defaults
tm <- searchType fc rigc defaults [] depth def
(abstractEnvType fc env top) env
top
logTerm 2 "Result" tm
defs <- get Ctxt
quote defs env tm
pure tm

10
src/Core/Unify.idr
View File

@ -1044,7 +1044,10 @@ retryGuess mode smode (hid, (loc, hname))
case smode of
LastChance =>
do log 5 $ "Last chance at " ++ show hname
search loc rig False depth defining (type def) []
tm <- search loc rig False depth defining (type def) []
let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def
logTerm 5 ("Solved " ++ show hname) tm
addDef (Resolved hid) gdef
pure True
_ => handleUnify
(do tm <- search loc rig (smode == Defaults) depth defining
@ -1056,7 +1059,7 @@ retryGuess mode smode (hid, (loc, hname))
pure True)
(\err => case err of
DeterminingArg _ n i _ _ =>
do logTerm 5 ("Failed (det " ++ show hname ++ ")")
do logTerm 5 ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
(type def)
setInvertible loc i
pure False -- progress made!
@ -1089,7 +1092,8 @@ solveConstraints : {auto c : Ref Ctxt Defs} ->
solveConstraints umode smode
= do ust <- get UST
progress <- traverse (retryGuess umode smode) (toList (guesses ust))
when (or (map Delay progress)) $ solveConstraints umode smode
when (or (map Delay progress)) $
solveConstraints umode smode
-- Replace any 'BySearch' with 'Hole', so that we don't keep searching
-- fruitlessly while elaborating the rest of a source file