git.iko.soy/Idris-dev
on master help sign in
Updates to renaming dependent pairs.

+ Added deprecation warning for use of old name. + Updated tests to use new name. + Updated existing code to use new name.

commited2bda5e7978bea8ee8e65138b82482051142a1d authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateThu 10 Dec 2015, 16:10 (11 years ago) parent8ed216a
13 files changed+45−49
compare with master
unifiedsplit
libs/effects/Effect/Logging/Category.idr+1−1 libs/effects/Effect/Logging/Default.idr+1−1 libs/prelude/Builtins.idr+2 libs/prelude/Prelude/Pairs.idr+3−1 libs/prelude/Prelude/Show.idr+1−1 test/disambig002/disambig002.idr+10−12 test/meta002/Tacs.idr+4−5 test/meta002/expected+1−1 test/proof002/Reflect.idr+2−4 test/proof002/expected+1−1 test/proof002/test030.idr−1 test/reg001/reg001.idr+13−14 test/reg064/reg064.idr+6−7
libs/effects/Effect/Logging/Category.idr+1−1
@@ -147,7 +147,7 @@ logN : (Show a, Eq a) => (l : Nat)
147147 -> (cs : List a)
148148 -> (m : String)
149149 -> Eff () [LOG a]
150−logN l cs msg = call $ Log (getProof lvl) cs msg
150+logN l cs msg = call $ Log (snd lvl) cs msg
151151 where
152152 lvl : (n ** LogLevel n)
153153 lvl = case cast {to=String} (cast {to=Int} l) of
libs/effects/Effect/Logging/Default.idr+1−1
@@ -84,7 +84,7 @@ log l msg = call $ Log l msg
8484||| @l The level to log.
8585||| @m The message to log.
8686logN : (l : Nat) -> {auto prf : LTE l 70} -> (m : String) -> Eff () [LOG]
87−logN l msg = call $ Log (getProof lvl) msg
87+logN l msg = call $ Log (snd lvl) msg
8888 where
8989 lvl : (n ** LogLevel n)
9090 lvl = case cast {to=String} (cast {to=Int} l) of
libs/prelude/Builtins.idr+2
@@ -47,9 +47,11 @@ namespace Builtins
4747
4848 Sigma : (a : Type) -> (P : a -> Type) -> Type
4949 Sigma wit prf = DepPair wit prf
50+ %deprecate Sigma "This name is being deprecated in favour of `DepPair`."
5051
5152 MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DepPair a P
5253 MkSigma wit prf = MkDepPair wit prf
54+ %deprecate MkSigma "This constructor is being deprecated in favour of `MkDepPair`."
5355
5456||| The empty type, also known as the trivially false proposition.
5557|||
libs/prelude/Prelude/Pairs.idr+3−1
@@ -43,9 +43,11 @@ using (a : Type, P : a -> Type)
4343
4444 getWitness : DepPair a P -> a
4545 getWitness = fst
46+ %deprecate DepPair.getWitness "This is being deprecated in favour of `fst`."
4647
47− getProof : (x : Sigma a P) -> P (fst x)
48+ getProof : (x : DepPair a P) -> P (fst x)
4849 getProof = snd
50+ %deprecate DepPair.getProof "This is being deprecated in favour of `snd`."
4951
5052 -- Polymorphic (class-based) projections have been removed
5153 -- because type-directed name disambiguation works better.
libs/prelude/Prelude/Show.idr+1−1
@@ -192,5 +192,5 @@ Show a => Show (Maybe a) where
192192 showPrec d (Left x) = showCon d "Left" $ showArg x
193193 showPrec d (Right x) = showCon d "Right" $ showArg x
194194
195−(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
195+(Show a, {y : a} -> Show (p y)) => Show (DepPair a p) where
196196 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
test/disambig002/disambig002.idr+10−12
@@ -6,7 +6,7 @@ Dec0 : Type -> Type
66Dec0 = Dec
77
88Dec1 : {A : Type} -> (P : A -> Type) -> Type
9−Dec1 {A} P = (a : A) -> Dec0 (P a)
9+Dec1 {A} P = (a : A) -> Dec0 (P a)
1010
1111Unique : Type -> Type
1212Unique t = (p : t) -> (q : t) -> p = q
@@ -53,8 +53,8 @@ namespace Finite
5353filterTag : {A : Type} ->
5454 {P : A -> Type} ->
5555 Dec1 P ->
56− Vect n A ->
57− Sigma Nat (\ m => Vect m (Sigma A P))
56+ Vect n A ->
57+ DepPair Nat (\ m => Vect m (DepPair A P))
5858filterTag d1P Nil = (_ ** Nil)
5959filterTag d1P (a :: as) with (filterTag d1P as)
6060 | (_ ** tail) with (d1P a)
@@ -66,7 +66,7 @@ toVect : {A : Type} ->
6666 {P : A -> Type} ->
6767 Finite A ->
6868 Dec1 P ->
69− (n : Nat ** Vect n (Sigma A P))
69+ (n : Nat ** Vect n (DepPair A P))
7070toVect fA d1P = filterTag d1P (toVect fA)
7171
7272sigmaUniqueLemma1 : {A : Type} ->
@@ -74,16 +74,14 @@ sigmaUniqueLemma1 : {A : Type} ->
7474 Unique1 {t0 = A} P ->
7575 (a : A) ->
7676 (p : P a) ->
77− (ss : Vect n (Sigma A P)) ->
78− Elem a (map getWitness ss) ->
77+ (ss : Vect n (DepPair A P)) ->
78+ Elem a (map fst ss) ->
7979 Elem (a ** p) ss
8080
8181toVectComplete : {A : Type} ->
8282 {P : A -> Type} ->
83− (fA : Finite A) ->
84− (d1P : Dec1 P) ->
83+ (fA : Finite A) ->
84+ (d1P : Dec1 P) ->
8585 Unique1 {t0 = A} P ->
86− (s : Sigma A P) ->
87− Elem s (getProof (toVect fA d1P))
88−
89−
86+ (s : DepPair A P) ->
87+ Elem s (snd (toVect fA d1P))
test/meta002/Tacs.idr+4−5
@@ -208,7 +208,7 @@ namespace STLC
208208
209209 -- Now we put this hole variable into our sigma constructor
210210 -- prior to elaboration, so it doesn't disappear too soon
211− fill `(MkSigma ~(Var tH) ~(Var tmH) : Sigma Ty (Tm []))
211+ fill `(MkDepPair ~(Var tH) ~(Var tmH) : DepPair Ty (Tm []))
212212 solve
213213 focus tmH
214214 mkTerm [] tm
@@ -287,18 +287,17 @@ namespace STLC
287287 apply `(UnitCon {env=~(Var envH)})
288288 []
289289 solve
290− testElab : Sigma Ty (Tm [])
290+ testElab : DepPair Ty (Tm [])
291291 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
292292
293− testElab2 : Sigma Ty (Tm [])
293+ testElab2 : DepPair Ty (Tm [])
294294 testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
295295
296296 -- Doesn't work! :-)
297− testElab3 : Sigma Ty (Tm [])
297+ testElab3 : DepPair Ty (Tm [])
298298 testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
299299 (Lam "x" (App (Var 0) (Var 0)))))
300300 -- Error is:
301301 -- Tacs.idr line 247 col 14:
302302 -- When elaborating right hand side of testElab3:
303303 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value
304−
test/meta002/expected+1−1
@@ -1,6 +1,6 @@
11Tacs.idr:298:15:
22When checking right hand side of testElab3 with expected type
3− Sigma Ty (Tm [])
3+ DepPair Ty (Tm [])
44
55Unifying ty and ARR ty t would lead to infinite value
66AgdaStyleReflection.idr:328:5:
test/proof002/Reflect.idr+2−4
@@ -44,7 +44,7 @@ using (xs : List a, ys : List a, G : List (List a))
4444 let (yl ** (yr, yprf)) = expr_r ey in
4545 appRExpr _ _ xr yr xprf yprf
4646 where
47− appRExpr : (xs', ys' : List a) ->
47+ appRExpr : (xs', ys' : List a) ->
4848 {G : List (List a)} -> {xs, ys : List a} ->
4949 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
5050 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))
@@ -206,6 +206,4 @@ Reflect.bp1 = proof {
206206-- prover.
207207
208208syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
209− getJust (prove (getProof x)) ItIsJust
210−
211−
209+ getJust (prove (snd x)) ItIsJust
test/proof002/expected+1−1
@@ -12,7 +12,7 @@ When checking an application of function Reflect.getJust:
1212 Type mismatch between
1313 IsJust (Just x1) (Type of ItIsJust)
1414 and
15− IsJust (prove (getProof x)) (Expected type)
15+ IsJust (prove (snd x)) (Expected type)
1616
1717 Specifically:
1818 Type mismatch between
test/proof002/test030.idr−1
@@ -10,4 +10,3 @@ total
1010testReflect1 : (xs, ys : List a) ->
1111 ((xs ++ (x :: ys ++ xs)) = ((xs ++ [x]) ++ (ys ++ xs)))
1212testReflect1 {a} xs ys = AssocProof a
13−
test/reg001/reg001.idr+13−14
@@ -37,7 +37,7 @@ filterTagP {n = S m} p (a :: as) q with (p a)
3737 **
3838 ((a ** believe_me Oh)
3939 ::
40− (fst (getProof (filterTagP p as (believe_me Oh)))),
40+ (fst (snd (filterTagP p as (believe_me Oh)))),
4141 Oh
4242 )
4343 )
@@ -95,7 +95,7 @@ mytranspose (x :: y :: xs)
9595
9696using (A : Type, B : A->Type, C : Type)
9797 foo2 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)
98− foo2 f p = f (getWitness p) (getProof p)
98+ foo2 f p = f (fst p) (snd p)
9999
100100
101101m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->
@@ -144,7 +144,7 @@ X : Nat -> Type
144144X t = (c : Nat ** So (c < 5))
145145
146146column : X t -> Nat
147−column = getWitness
147+column = fst
148148
149149data Action = Left | Ahead | Right
150150
@@ -161,31 +161,31 @@ isSubsetOf : Set univ => univ -> univ -> Type
161161isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
162162
163163interface Set univ => HasPower univ where
164− Powerset : (a : univ) ->
165− Sigma univ (\Pa => (c : univ) ->
164+ Powerset : (a : univ) ->
165+ DepPair univ (\Pa => (c : univ) ->
166166 (isSubsetOf c a) -> member c Pa)
167167
168168powerset : HasPower univ => univ -> univ
169−powerset {univ} a = getWitness (Powerset a)
169+powerset {univ} a = fst (Powerset a)
170170
171171mapFilter : (alpha -> beta) ->
172− (alpha -> Bool) ->
173− Vect n alpha ->
172+ (alpha -> Bool) ->
173+ Vect n alpha ->
174174 (n : Nat ** Vect n beta)
175175mapFilter f p Nil = (_ ** Nil)
176176mapFilter f p (a :: as) with (p a)
177− | True = (_ ** (f a) :: (getProof (mapFilter f p as)))
177+ | True = (_ ** (f a) :: (snd (mapFilter f p as)))
178178 | False = mapFilter f p as
179179
180180hVectEx1 : HVect [String, List Nat, Nat, (Nat, Nat)]
181181hVectEx1 = ["Hello",[1,2,3],42,(0,10)]
182−
182+
183183vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]
184184vecfoo = put (S (S Z)) hVectEx1
185185
186186foom : Monad m => Int -> m Int
187−foom = pure
188−
187+foom = pure
188+
189189bar : IO ()
190190bar = case foom 5 of
191191 Nothing => print 42
@@ -193,7 +193,7 @@ bar = case foom 5 of
193193
194194Max : (Nat -> Type) -> Type
195195Max p = (Nat , (k : Nat) -> p k -> Nat)
196−
196+
197197maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat
198198maxEquiv a n1 pr1 = snd a n1 pr1
199199
@@ -207,4 +207,3 @@ data Kappa : (r : Rho) -> Type where K : Kappa r
207207kappa : Kappa (rho r) -> Kappa (rho r)
208208kappa {r} k = k' where -- k' : Kappa (rho r)
209209 k' = k
210−
test/reg064/reg064.idr+6−7
@@ -1,9 +1,8 @@
1−sigmaEq2 : {A : Type} ->
2− {P : A -> Type} ->
3− {s1: Sigma A P} ->
4− {s2: Sigma A P} ->
5− getWitness s1 = getWitness s2 ->
6− getProof s1 = getProof s2 ->
1+sigmaEq2 : {A : Type} ->
2+ {P : A -> Type} ->
3+ {s1: DepPair A P} ->
4+ {s2: DepPair A P} ->
5+ fst s1 = fst s2 ->
6+ snd s1 = snd s2 ->
77 s1 = s2
88sigmaEq2 {A} {P} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl
9−