git.iko.soy/Idris-dev
on master help sign in
Renamed `DepPair` to DPair
fd2501bJan de Muijnck-Hughes
CHANGELOG+1−1
compare with master
unifiedsplit
@@ -20,7 +20,7 @@ Minor language changes
20
20
21* The '[static]' annotation is changed to '%static' to be consistent with the
21* The '[static]' annotation is changed to '%static' to be consistent with the
22 other annotations.
22 other annotations.
23−* `Sigma` has been renamed to `DepPair`.
23+* `Sigma` has been renamed to `DPair`.
24* Accessor functions for dependent pairs have been renamed to bring them into
24* Accessor functions for dependent pairs have been renamed to bring them into
25 line with standard accessor functions for pairs. The function `getWitness`
25 line with standard accessor functions for pairs. The function `getWitness`
26 is now `fst`, and `getProof` is `snd`.
26 is now `fst`, and `getProof` is `snd`.
libs/prelude/Builtins.idr+7−7
@@ -46,16 +46,16 @@ namespace Builtins
46 |||
46 |||
47 ||| @a the value to place in the type.
47 ||| @a the value to place in the type.
48 ||| @P the dependent type that requires the value.
48 ||| @P the dependent type that requires the value.
49− data DepPair : (a : Type) -> (P : a -> Type) -> Type where
49+ data DPair : (a : Type) -> (P : a -> Type) -> Type where
50− MkDepPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DepPair a P
50+ MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
51
51
52 Sigma : (a : Type) -> (P : a -> Type) -> Type
52 Sigma : (a : Type) -> (P : a -> Type) -> Type
53− Sigma wit prf = DepPair wit prf
53+ Sigma wit prf = DPair wit prf
54− %deprecate Sigma "This name is being deprecated in favour of `DepPair`."
54+ %deprecate Sigma "This name is being deprecated in favour of `DPair`."
55
55
56− MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DepPair a P
56+ MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DPair a P
57− MkSigma wit prf = MkDepPair wit prf
57+ MkSigma wit prf = MkDPair wit prf
58− %deprecate MkSigma "This constructor is being deprecated in favour of `MkDepPair`."
58+ %deprecate MkSigma "This constructor is being deprecated in favour of `MkDPair`."
59
59
60||| The empty type, also known as the trivially false proposition.
60||| The empty type, also known as the trivially false proposition.
61|||
61|||
libs/prelude/Prelude/Pairs.idr+7−7
@@ -34,20 +34,20 @@ using (a : Type, P : a -> Type)
34 getProof : (x : Subset a P) -> P (getWitness x)
34 getProof : (x : Subset a P) -> P (getWitness x)
35 getProof (Element x pf) = pf
35 getProof (Element x pf) = pf
36
36
37− namespace DepPair
37+ namespace DPair
38− fst : DepPair a P -> a
38+ fst : DPair a P -> a
39 fst (x ** pf) = x
39 fst (x ** pf) = x
40
40
41− snd : (x : DepPair a P) -> P (fst x)
41+ snd : (x : DPair a P) -> P (fst x)
42 snd (x ** pf) = pf
42 snd (x ** pf) = pf
43
43
44− getWitness : DepPair a P -> a
44+ getWitness : DPair a P -> a
45 getWitness = fst
45 getWitness = fst
46− %deprecate DepPair.getWitness "This is being deprecated in favour of `fst`."
46+ %deprecate DPair.getWitness "This is being deprecated in favour of `fst`."
47
47
48− getProof : (x : DepPair a P) -> P (fst x)
48+ getProof : (x : DPair a P) -> P (fst x)
49 getProof = snd
49 getProof = snd
50− %deprecate DepPair.getProof "This is being deprecated in favour of `snd`."
50+ %deprecate DPair.getProof "This is being deprecated in favour of `snd`."
51
51
52 -- Polymorphic (class-based) projections have been removed
52 -- Polymorphic (class-based) projections have been removed
53 -- because type-directed name disambiguation works better.
53 -- because type-directed name disambiguation works better.
libs/prelude/Prelude/Show.idr+1−1
@@ -192,5 +192,5 @@ Show a => Show (Maybe a) where
192 showPrec d (Left x) = showCon d "Left" $ showArg x
192 showPrec d (Left x) = showCon d "Left" $ showArg x
193 showPrec d (Right x) = showCon d "Right" $ showArg x
193 showPrec d (Right x) = showCon d "Right" $ showArg x
194
194
195−(Show a, {y : a} -> Show (p y)) => Show (DepPair a p) where
195+(Show a, {y : a} -> Show (p y)) => Show (DPair a p) where
196 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
196 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1615,8 +1615,8 @@ modDocName :: Name
1615modDocName = sMN 0 "ModuleDocs"
1615modDocName = sMN 0 "ModuleDocs"
1616
1616
1617-- Defined in builtins.idr
1617-- Defined in builtins.idr
1618−sigmaTy = sNS (sUN "DepPair") ["Builtins"]
1618+sigmaTy = sNS (sUN "DPair") ["Builtins"]
1619−sigmaCon = sNS (sUN "MkDepPair") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1620
1620
1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1622piBind = piBindp expl
1622piBind = piBindp expl
test/disambig002/disambig002.idr+4−4
@@ -54,7 +54,7 @@ filterTag : {A : Type} ->
54 {P : A -> Type} ->
54 {P : A -> Type} ->
55 Dec1 P ->
55 Dec1 P ->
56 Vect n A ->
56 Vect n A ->
57− DepPair Nat (\ m => Vect m (DepPair A P))
57+ DPair Nat (\ m => Vect m (DPair A P))
58filterTag d1P Nil = (_ ** Nil)
58filterTag d1P Nil = (_ ** Nil)
59filterTag d1P (a :: as) with (filterTag d1P as)
59filterTag d1P (a :: as) with (filterTag d1P as)
60 | (_ ** tail) with (d1P a)
60 | (_ ** tail) with (d1P a)
@@ -66,7 +66,7 @@ toVect : {A : Type} ->
66 {P : A -> Type} ->
66 {P : A -> Type} ->
67 Finite A ->
67 Finite A ->
68 Dec1 P ->
68 Dec1 P ->
69− (n : Nat ** Vect n (DepPair A P))
69+ (n : Nat ** Vect n (DPair A P))
70toVect fA d1P = filterTag d1P (toVect fA)
70toVect fA d1P = filterTag d1P (toVect fA)
71
71
72sigmaUniqueLemma1 : {A : Type} ->
72sigmaUniqueLemma1 : {A : Type} ->
@@ -74,7 +74,7 @@ sigmaUniqueLemma1 : {A : Type} ->
74 Unique1 {t0 = A} P ->
74 Unique1 {t0 = A} P ->
75 (a : A) ->
75 (a : A) ->
76 (p : P a) ->
76 (p : P a) ->
77− (ss : Vect n (DepPair A P)) ->
77+ (ss : Vect n (DPair A P)) ->
78 Elem a (map fst ss) ->
78 Elem a (map fst ss) ->
79 Elem (a ** p) ss
79 Elem (a ** p) ss
80
80
@@ -83,5 +83,5 @@ toVectComplete : {A : Type} ->
83 (fA : Finite A) ->
83 (fA : Finite A) ->
84 (d1P : Dec1 P) ->
84 (d1P : Dec1 P) ->
85 Unique1 {t0 = A} P ->
85 Unique1 {t0 = A} P ->
86− (s : DepPair A P) ->
86+ (s : DPair A P) ->
87 Elem s (snd (toVect fA d1P))
87 Elem s (snd (toVect fA d1P))
test/meta002/Tacs.idr+4−4
@@ -208,7 +208,7 @@ namespace STLC
208
208
209 -- Now we put this hole variable into our sigma constructor
209 -- Now we put this hole variable into our sigma constructor
210 -- prior to elaboration, so it doesn't disappear too soon
210 -- prior to elaboration, so it doesn't disappear too soon
211− fill `(MkDepPair ~(Var tH) ~(Var tmH) : DepPair Ty (Tm []))
211+ fill `(MkDPair ~(Var tH) ~(Var tmH) : DPair Ty (Tm []))
212 solve
212 solve
213 focus tmH
213 focus tmH
214 mkTerm [] tm
214 mkTerm [] tm
@@ -287,14 +287,14 @@ namespace STLC
287 apply `(UnitCon {env=~(Var envH)})
287 apply `(UnitCon {env=~(Var envH)})
288 []
288 []
289 solve
289 solve
290− testElab : DepPair Ty (Tm [])
290+ testElab : DPair Ty (Tm [])
291 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
291 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
292
292
293− testElab2 : DepPair Ty (Tm [])
293+ testElab2 : DPair Ty (Tm [])
294 testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
294 testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
295
295
296 -- Doesn't work! :-)
296 -- Doesn't work! :-)
297− testElab3 : DepPair Ty (Tm [])
297+ testElab3 : DPair Ty (Tm [])
298 testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
298 testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
299 (Lam "x" (App (Var 0) (Var 0)))))
299 (Lam "x" (App (Var 0) (Var 0)))))
300 -- Error is:
300 -- Error is:
test/meta002/expected+1−1
@@ -1,6 +1,6 @@
1Tacs.idr:298:15:
1Tacs.idr:298:15:
2When checking right hand side of testElab3 with expected type
2When checking right hand side of testElab3 with expected type
3− DepPair Ty (Tm [])
3+ DPair Ty (Tm [])
4
4
5Unifying ty and ARR ty t would lead to infinite value
5Unifying ty and ARR ty t would lead to infinite value
6AgdaStyleReflection.idr:328:5:
6AgdaStyleReflection.idr:328:5:
test/reg001/reg001.idr+1−1
@@ -162,7 +162,7 @@ isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
162
162
163interface Set univ => HasPower univ where
163interface Set univ => HasPower univ where
164 Powerset : (a : univ) ->
164 Powerset : (a : univ) ->
165− DepPair univ (\Pa => (c : univ) ->
165+ DPair univ (\Pa => (c : univ) ->
166 (isSubsetOf c a) -> member c Pa)
166 (isSubsetOf c a) -> member c Pa)
167
167
168powerset : HasPower univ => univ -> univ
168powerset : HasPower univ => univ -> univ
test/reg064/reg064.idr+2−2
@@ -1,7 +1,7 @@
1sigmaEq2 : {A : Type} ->
1sigmaEq2 : {A : Type} ->
2 {P : A -> Type} ->
2 {P : A -> Type} ->
3− {s1: DepPair A P} ->
3+ {s1: DPair A P} ->
4− {s2: DepPair A P} ->
4+ {s2: DPair A P} ->
5 fst s1 = fst s2 ->
5 fst s1 = fst s2 ->
6 snd s1 = snd s2 ->
6 snd s1 = snd s2 ->
7 s1 = s2
7 s1 = s2