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

Don't search locals when doing defaulthints

Browse Source 
If we do, we might solve something we shouldn't because we're not
checking determining arguments. In 'defaults' mode, we should *only*
apply default hints - we'll go back to the locals in a final pass.
This commit is contained in:
Edwin Brady 2020-02-09 22:44:04 +00:00
parent 625027f278
commit f9a3ed2e0c
2 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Core/AutoSearch.idr
View File

@ -442,6 +442,8 @@ checkConcreteDets fc defaults env top (NTCon tfc tyn t a args)
concreteDets fc defaults env top 0 (detArgs sd) args
else
do sd <- getSearchData fc defaults tyn
log 10 $ "Determining arguments for " ++ show !(toFullNames tyn)
++ " " ++ show (detArgs sd)
concreteDets fc defaults env top 0 (detArgs sd) args
checkConcreteDets fc defaults env top _
= pure ()
@ -479,9 +481,11 @@ searchType {vars} fc rigc defaults trying depth def checkdets top env target
when checkdets $
checkConcreteDets fc defaults env top
(NTCon tfc tyn t a args)
tryUnify
(searchLocal fc rigc defaults trying' depth def top env nty)
(tryGroups Nothing nty (hintGroups sd))
if defaults
then tryGroups Nothing nty (hintGroups sd)
else tryUnify
(searchLocal fc rigc defaults trying' depth def top env nty)
(tryGroups Nothing nty (hintGroups sd))
else throw (CantSolveGoal fc [] top)
_ => do logNF 10 "Next target: " env nty
searchLocal fc rigc defaults trying' depth def top env nty

1
src/Core/UnifyState.idr
View File

@ -432,6 +432,7 @@ 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 fc ++ " " ++ show n
logTermNF 10 "New search type" env ty
idx <- addDef n hole
addGuessName fc n idx
pure (idx, Meta fc n idx envArgs)