git.iko.soy/Idris-dev
on master help sign in
Allow explicit arguments for scoped implicits

Along with other recent patches, this fixes #3654, by allowing explicit arguments to be given for named scoped implicits in the same way as for top level implicits.

commit0734826dff7ad75c4af31ba7a2ebf392c45ca0b6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 14 Mar 2017, 10:04 (10 years ago) parentb7cf1ec
3 files changed+58−1
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+14 test/regression001/reg004.lidr+43 test/regression001/run+1−1
src/Idris/Elab/Term.hs+14
@@ -1502,7 +1502,21 @@ elab ist info emode opts fn tm
15021502 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
15031503 fullApp x = x
15041504
1505+ -- See if the name is listed as an implicit. If it is, return it, and
1506+ -- drop it from the rest of the list
1507+ findImplicit :: Name -> [PArg] -> (Maybe PArg, [PArg])
1508+ findImplicit n [] = (Nothing, [])
1509+ findImplicit n (i@(PImp _ _ _ n' _) : args)
1510+ | n == n' = (Just i, args)
1511+ findImplicit n (i@(PTacImplicit _ _ n' _ _) : args)
1512+ | n == n' = (Just i, args)
1513+ findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in
1514+ (arg, x : rest)
1515+
15051516 insertScopedImps fc ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs
1517+ | (Just arg, xs') <- findImplicit n xs,
1518+ not (toplevel_imp i)
1519+ = arg : insertScopedImps fc sc xs'
15061520 | tcimplementation i && not (toplevel_imp i)
15071521 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
15081522 | not (toplevel_imp i)
test/regression001/reg004.lidrnew file+43
@@ -0,0 +1,43 @@
1+> %default total
2+> %access public export
3+> %auto_implicits off
4+
5+> Natural : {F, G : Type -> Type} ->
6+> (Functor F) => (Functor G) =>
7+> (t : {A : Type} -> F A -> G A) ->
8+> Type
9+> Natural {F} {G} t = {A, B : Type} ->
10+> (f : A -> B) ->
11+> (x : F A) ->
12+> t (map f x) = map f (t x)
13+
14+> Monotone : {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>
15+> (LTE_B : B -> B -> Type) ->
16+> (LTE_C : C -> C -> Type) ->
17+> (measure : F B -> C) ->
18+> Type
19+> Monotone {B} {C} {F} LTE_B LTE_C measure =
20+> {A : Type} ->
21+> (f : A -> B) ->
22+> (g : A -> B) ->
23+> (p : (a : A) -> f a `LTE_B` g a) ->
24+> (x : F A) ->
25+> measure (map f x) `LTE_C` measure (map g x)
26+
27+> monotoneNaturalLemma: {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>
28+> (LTE_B : B -> B -> Type) ->
29+> (LTE_C : C -> C -> Type) ->
30+> (measure : F B -> C) ->
31+> Monotone LTE_B LTE_C measure ->
32+> (t : {A : Type} -> F A -> F A) ->
33+> Natural t ->
34+> Monotone LTE_B LTE_C (measure . t)
35+> monotoneNaturalLemma {B} {C} {F} LTE_B LTE_C m mm t nt = mmt where
36+> mmt : {A : Type} ->
37+> (f : A -> B) ->
38+> (g : A -> B) ->
39+> (p : (a : A) -> f a `LTE_B` g a) ->
40+> (x : F A) ->
41+> m (t {A = B} (map f x)) `LTE_C` m (t {A = B} (map g x))
42+> mmt = ?kika
43+
test/regression001/run+1−1
@@ -1,6 +1,6 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ --check \
3− reg001.idr reg002.idr reg003.idr reg036.idr reg037.idr \
3+ reg001.idr reg002.idr reg003.idr reg004.lidr reg036.idr reg037.idr \
44 reg038.idr reg046.idr \
55 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \
66 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \