idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ fix ] add missing recursive calls

Browse Source
This commit is contained in:
Guillaume Allais 2022-10-21 20:55:56 +01:00 committed by G. Allais
parent 3f7cd84ccb
commit 86bd19b64d
2 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Core/TT.idr
View File

@ -1793,7 +1793,7 @@ addMetas res ns (TDelay fc x t y)
= addMetas res (addMetas res ns t) y = addMetas res (addMetas res ns t) y
addMetas res ns (TForce fc r x) = addMetas res ns x addMetas res ns (TForce fc r x) = addMetas res ns x
addMetas res ns (PrimVal fc c) = ns addMetas res ns (PrimVal fc c) = ns
addMetas res ns (Erased fc i) = ns addMetas res ns (Erased fc i) = foldr (flip $ addMetas res) ns i
addMetas res ns (TType fc u) = ns addMetas res ns (TType fc u) = ns
-- Get the metavariable names in a term -- Get the metavariable names in a term
@ -1828,7 +1828,7 @@ addRefs ua at ns (TDelay fc x t y)
= addRefs ua at (addRefs ua at ns t) y = addRefs ua at (addRefs ua at ns t) y
addRefs ua at ns (TForce fc r x) = addRefs ua at ns x addRefs ua at ns (TForce fc r x) = addRefs ua at ns x
addRefs ua at ns (PrimVal fc c) = ns addRefs ua at ns (PrimVal fc c) = ns
addRefs ua at ns (Erased fc i) = ns addRefs ua at ns (Erased fc i) = foldr (flip $ addRefs ua at) ns i
addRefs ua at ns (TType fc u) = ns addRefs ua at ns (TType fc u) = ns
-- As above, but for references. Also flag whether a name is under an -- As above, but for references. Also flag whether a name is under an

3
src/Core/Unify.idr
View File

@ -282,6 +282,7 @@ unifyArgs mode loc env _ _ = ufail loc ""
getVars : {vars : _} -> getVars : {vars : _} ->
List Nat -> List (NF vars) -> Maybe (List (Var vars)) List Nat -> List (NF vars) -> Maybe (List (Var vars))
getVars got [] = Just [] getVars got [] = Just []
getVars got (NErased fc (Dotted t) :: xs) = getVars got (t :: xs)
getVars got (NApp fc (NLocal r idx v) [] :: xs) getVars got (NApp fc (NLocal r idx v) [] :: xs)
= if inArgs idx got then Nothing = if inArgs idx got then Nothing
else do xs' <- getVars (idx :: got) xs else do xs' <- getVars (idx :: got) xs
@ -639,6 +640,8 @@ solveIfUndefined env metavar@(Meta fc mname idx args) soln
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs) Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
| _ => pure False | _ => pure False
updateSolution env metavar soln updateSolution env metavar soln
solveIfUndefined env (Erased _ (Dotted metavar)) soln
= solveIfUndefined env metavar soln
solveIfUndefined env metavar soln solveIfUndefined env metavar soln
= pure False = pure False