git.iko.soy/Idris-dev
on master help sign in
Renamed `DepPair` to DPair
commitfd2501b6771c80a0756459a4429d74e159c2ff15 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateMon 8 Feb 2016, 14:00 (11 years ago) parent5e0e4e9
10 files changed+30−30
compare with master
unifiedsplit
CHANGELOG+1−1 libs/prelude/Builtins.idr+7−7 libs/prelude/Prelude/Pairs.idr+7−7 libs/prelude/Prelude/Show.idr+1−1 src/Idris/AbsSyntaxTree.hs+2−2 test/disambig002/disambig002.idr+4−4 test/meta002/Tacs.idr+4−4 test/meta002/expected+1−1 test/reg001/reg001.idr+1−1 test/reg064/reg064.idr+2−2
CHANGELOG+1−1
@@ -20,7 +20,7 @@ Minor language changes
2020
2121* The '[static]' annotation is changed to '%static' to be consistent with the
2222 other annotations.
23−* `Sigma` has been renamed to `DepPair`.
23+* `Sigma` has been renamed to `DPair`.
2424* Accessor functions for dependent pairs have been renamed to bring them into
2525 line with standard accessor functions for pairs. The function `getWitness`
2626 is now `fst`, and `getProof` is `snd`.
libs/prelude/Builtins.idr+7−7
@@ -46,16 +46,16 @@ namespace Builtins
4646 |||
4747 ||| @a the value to place in the type.
4848 ||| @P the dependent type that requires the value.
49− data DepPair : (a : Type) -> (P : a -> Type) -> Type where
50− MkDepPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DepPair a P
49+ data DPair : (a : Type) -> (P : a -> Type) -> Type where
50+ MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
5151
5252 Sigma : (a : Type) -> (P : a -> Type) -> Type
53− Sigma wit prf = DepPair wit prf
54− %deprecate Sigma "This name is being deprecated in favour of `DepPair`."
53+ Sigma wit prf = DPair wit prf
54+ %deprecate Sigma "This name is being deprecated in favour of `DPair`."
5555
56− MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DepPair a P
57− MkSigma wit prf = MkDepPair wit prf
58− %deprecate MkSigma "This constructor is being deprecated in favour of `MkDepPair`."
56+ MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DPair a P
57+ MkSigma wit prf = MkDPair wit prf
58+ %deprecate MkSigma "This constructor is being deprecated in favour of `MkDPair`."
5959
6060||| The empty type, also known as the trivially false proposition.
6161|||
libs/prelude/Prelude/Pairs.idr+7−7
@@ -34,20 +34,20 @@ using (a : Type, P : a -> Type)
3434 getProof : (x : Subset a P) -> P (getWitness x)
3535 getProof (Element x pf) = pf
3636
37− namespace DepPair
38− fst : DepPair a P -> a
37+ namespace DPair
38+ fst : DPair a P -> a
3939 fst (x ** pf) = x
4040
41− snd : (x : DepPair a P) -> P (fst x)
41+ snd : (x : DPair a P) -> P (fst x)
4242 snd (x ** pf) = pf
4343
44− getWitness : DepPair a P -> a
44+ getWitness : DPair a P -> a
4545 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`."
4747
48− getProof : (x : DepPair a P) -> P (fst x)
48+ getProof : (x : DPair a P) -> P (fst x)
4949 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`."
5151
5252 -- Polymorphic (class-based) projections have been removed
5353 -- 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 (DepPair a p) where
195+(Show a, {y : a} -> Show (p y)) => Show (DPair a p) where
196196 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1615,8 +1615,8 @@ modDocName :: Name
16151615modDocName = sMN 0 "ModuleDocs"
16161616
16171617-- Defined in builtins.idr
1618−sigmaTy = sNS (sUN "DepPair") ["Builtins"]
1619−sigmaCon = sNS (sUN "MkDepPair") ["Builtins"]
1618+sigmaTy = sNS (sUN "DPair") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
16201620
16211621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
16221622piBind = piBindp expl
test/disambig002/disambig002.idr+4−4
@@ -54,7 +54,7 @@ filterTag : {A : Type} ->
5454 {P : A -> Type} ->
5555 Dec1 P ->
5656 Vect n A ->
57− DepPair Nat (\ m => Vect m (DepPair A P))
57+ DPair Nat (\ m => Vect m (DPair 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 (DepPair A P))
69+ (n : Nat ** Vect n (DPair A P))
7070toVect fA d1P = filterTag d1P (toVect fA)
7171
7272sigmaUniqueLemma1 : {A : Type} ->
@@ -74,7 +74,7 @@ sigmaUniqueLemma1 : {A : Type} ->
7474 Unique1 {t0 = A} P ->
7575 (a : A) ->
7676 (p : P a) ->
77− (ss : Vect n (DepPair A P)) ->
77+ (ss : Vect n (DPair A P)) ->
7878 Elem a (map fst ss) ->
7979 Elem (a ** p) ss
8080
@@ -83,5 +83,5 @@ toVectComplete : {A : Type} ->
8383 (fA : Finite A) ->
8484 (d1P : Dec1 P) ->
8585 Unique1 {t0 = A} P ->
86− (s : DepPair A P) ->
86+ (s : DPair A P) ->
8787 Elem s (snd (toVect fA d1P))
test/meta002/Tacs.idr+4−4
@@ -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 `(MkDepPair ~(Var tH) ~(Var tmH) : DepPair Ty (Tm []))
211+ fill `(MkDPair ~(Var tH) ~(Var tmH) : DPair Ty (Tm []))
212212 solve
213213 focus tmH
214214 mkTerm [] tm
@@ -287,14 +287,14 @@ namespace STLC
287287 apply `(UnitCon {env=~(Var envH)})
288288 []
289289 solve
290− testElab : DepPair Ty (Tm [])
290+ testElab : DPair Ty (Tm [])
291291 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
292292
293− testElab2 : DepPair Ty (Tm [])
293+ testElab2 : DPair Ty (Tm [])
294294 testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
295295
296296 -- Doesn't work! :-)
297− testElab3 : DepPair Ty (Tm [])
297+ testElab3 : DPair 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:
test/meta002/expected+1−1
@@ -1,6 +1,6 @@
11Tacs.idr:298:15:
22When checking right hand side of testElab3 with expected type
3− DepPair Ty (Tm [])
3+ DPair Ty (Tm [])
44
55Unifying ty and ARR ty t would lead to infinite value
66AgdaStyleReflection.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)
162162
163163interface Set univ => HasPower univ where
164164 Powerset : (a : univ) ->
165− DepPair univ (\Pa => (c : univ) ->
165+ DPair univ (\Pa => (c : univ) ->
166166 (isSubsetOf c a) -> member c Pa)
167167
168168powerset : HasPower univ => univ -> univ
test/reg064/reg064.idr+2−2
@@ -1,7 +1,7 @@
11sigmaEq2 : {A : Type} ->
22 {P : A -> Type} ->
3− {s1: DepPair A P} ->
4− {s2: DepPair A P} ->
3+ {s1: DPair A P} ->
4+ {s2: DPair A P} ->
55 fst s1 = fst s2 ->
66 snd s1 = snd s2 ->
77 s1 = s2