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

Fix getRelevantArg

Browse Source 
IORes is a newtype again, so the chez tests are working again now
This commit is contained in:
Edwin Brady 2020-04-27 17:49:50 +01:00
parent bdefd1a195
commit 062a0846f2
1 changed files with 8 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/TTImp/ProcessData.idr
View File

@ -207,16 +207,15 @@ getRelevantArg defs i rel world (NBind fc _ (Pi rig _ val) sc)
(NPrimVal _ WorldType) =>
getRelevantArg defs (1 + i) rel False
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
_ => pure Nothing)
_ =>
-- if we haven't found a relevant argument yet, make
-- a note of this one and keep going. Otherwise, we
-- have more than one, so give up.
maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
getRelevantArg defs (1 + i) (Just i) False sc')
(const (pure Nothing))
rel)
rig
getRelevantArg defs i rel world (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc)
= getRelevantArg defs (1 + i) rel False
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRelevantArg defs i Nothing world (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
= getRelevantArg defs (1 + i) (Just i) world
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRelevantArg defs i (Just _) world (NBind _ _ (Pi _ _ _) sc) -- more than one relevant
= pure Nothing
getRelevantArg defs i rel world tm
= pure (maybe Nothing (\r => Just (world, r)) rel)