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

Don't add implicits after non-given explicits. (#918)

Browse Source
This commit is contained in:
Nicolas A. Schmidt 2021-01-20 20:13:07 +01:00 committed by GitHub
parent 4e94298acb
commit 61761f4c27
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 59 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
src/TTImp/TTImp.idr
View File

@ -496,26 +496,31 @@ findImplicits tm = []
export
implicitsAs : {auto c : Ref Ctxt Defs} ->
Defs -> List Name -> RawImp -> Core RawImp
implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) [] tm
where
setAs : List (Maybe Name) -> RawImp -> Core RawImp
setAs is (IApp loc f a)
= do f' <- setAs is f
-- Takes the function application expression which is the lhs of a clause
-- and decomposes it into the underlying function symbol and the variables
-- bound by appearing as arguments, and then passes this onto `findImps`.
-- More precisely, implicit and explicit arguments are recorded separately,
-- into `is` and `es` respectively.
setAs : List (Maybe Name) -> List (Maybe Name) -> RawImp -> Core RawImp
setAs is es (IApp loc f a)
= do f' <- setAs is (Nothing :: es) f
pure $ IApp loc f' a
setAs is (IAutoApp loc f a)
= do f' <- setAs (Nothing :: is) f
setAs is es (IAutoApp loc f a)
= do f' <- setAs (Nothing :: is) es f
pure $ IAutoApp loc f' a
setAs is (INamedApp loc f n a)
= do f' <- setAs (Just n :: is) f
setAs is es (INamedApp loc f n a)
= do f' <- setAs (Just n :: is) (Just n :: es) f
pure $ INamedApp loc f' n a
setAs is (IWithApp loc f a)
= do f' <- setAs is f
setAs is es (IWithApp loc f a)
= do f' <- setAs is es f
pure $ IWithApp loc f' a
setAs is (IVar loc n)
setAs is es (IVar loc n)
= case !(lookupTyExact n (gamma defs)) of
Nothing => pure $ IVar loc n
Just ty => pure $ impAs loc
!(findImps is !(nf defs [] ty)) (IVar loc n)
!(findImps is es !(nf defs [] ty)) (IVar loc n)
where
-- If there's an @{c} in the list of given implicits, that's the next
-- autoimplicit, so don't rewrite the LHS and update the list of given
@ -529,20 +534,35 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
pure (x :: ns')
updateNs n [] = Nothing
findImps : List (Maybe Name) -> NF [] -> Core (List (Name, PiInfo RawImp))
findImps ns (NBind fc x (Pi _ _ Explicit _) sc)
= findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc False)))
-- Finds the missing implicits which should be added to the lhs of the
-- original pattern clause.
--
-- The first argument, `ns`, specifies which implicit variables alredy
-- appear in the lhs, and therefore need not be added.
-- The second argument, `es`, specifies which *explicit* variables appear
-- in the lhs: this is used to determine when to stop searching for further
-- implicits to add.
findImps : List (Maybe Name) -> List (Maybe Name) -> NF [] -> Core (List (Name, PiInfo RawImp))
-- don't add implicits coming after explicits that aren't given
findImps ns es (NBind fc x (Pi _ _ Explicit _) sc)
= case es of
-- Explicits were skipped, therefore all explicits are given anyway
Just (UN "_") :: _ => findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False)))
-- Explicits weren't skipped, so we need to check
_ => case updateNs x es of
Nothing => pure [] -- explicit wasn't given
Just es' => findImps ns es' !(sc defs (toClosure defaultOpts [] (Erased fc False)))
-- if the implicit was given, skip it
findImps ns (NBind fc x (Pi _ _ AutoImplicit _) sc)
findImps ns es (NBind fc x (Pi _ _ AutoImplicit _) sc)
= case updateNs x ns of
Nothing => -- didn't find explicit call
pure $ (x, AutoImplicit) :: !(findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc False))))
Just ns' => findImps ns' !(sc defs (toClosure defaultOpts [] (Erased fc False)))
findImps ns (NBind fc x (Pi _ _ p _) sc)
pure $ (x, AutoImplicit) :: !(findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False))))
Just ns' => findImps ns' es !(sc defs (toClosure defaultOpts [] (Erased fc False)))
findImps ns es (NBind fc x (Pi _ _ p _) sc)
= if Just x `elem` ns
then findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc False)))
else pure $ (x, forgetDef p) :: !(findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc False))))
findImps _ _ = pure []
then findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False)))
else pure $ (x, forgetDef p) :: !(findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False))))
findImps _ _ _ = pure []
impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp
impAs loc' [] tm = tm
@ -558,7 +578,7 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
INamedApp loc' tm n
(IAs loc' UseLeft n (Implicit loc' True))
impAs loc' (_ :: ns) tm = impAs loc' ns tm
setAs is tm = pure tm
setAs is es tm = pure tm
export
definedInBlock : Namespace -> -- namespace to resolve names

3
tests/Main.idr
View File

@ -111,7 +111,8 @@ idrisTestsRegression = MkTestPool []
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035"]
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
"reg036"]
idrisTests : TestPool
idrisTests = MkTestPool []

10
tests/idris2/reg036/Test.idr Normal file
View File

@ -0,0 +1,10 @@
module Test
interface Foo a where
bar : a -> {auto ok: ()} -> a
foo : Void -> {auto ok: ()} -> Void
foo = ?foo_hole
baz : a -> b -> c -> {auto x : a} -> a
baz {} = x

1
tests/idris2/reg036/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Test (Test.idr)

3
tests/idris2/reg036/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 Test.idr --check
rm -rf build