git.iko.soy/Idris-dev
on master help sign in
Renamed `UniquePair` to `UPair`.
commit5e0e4e9cae46499ea60c236197ff6560ae96a08b authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateMon 8 Feb 2016, 12:12 (11 years ago) parent006bd17
4 files changed+10−19
compare with master
unifiedsplit
CHANGELOG+1−2 libs/prelude/Builtins.idr+4−12 src/Idris/AbsSyntaxTree.hs+2−2 test/unique001/unique001c.idr+3−3
CHANGELOG+1−2
@@ -20,8 +20,7 @@ Minor language changes
2020
2121* The '[static]' annotation is changed to '%static' to be consistent with the
2222 other annotations.
23−* `UPair` and `Sigma` have been renamed `UniquePair` and `DepPair`
24− respectivly.
23+* `Sigma` has been renamed to `DepPair`.
2524* Accessor functions for dependent pairs have been renamed to bring them into
2625 line with standard accessor functions for pairs. The function `getWitness`
2726 is now `fst`, and `getProof` is `snd`.
libs/prelude/Builtins.idr+4−12
@@ -27,23 +27,15 @@ namespace Builtins
2727 ||| UniqueTypes.
2828 ||| @A the type of the left elements in the pair
2929 ||| @B the type of the left elements in the pair
30− data UniquePair : (A : AnyType) -> (B : AnyType) -> AnyType where
30+ data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
3131 ||| A pair of elements
3232 ||| @a the left element of the pair
3333 ||| @b the right element of the pair
34− MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
34+ MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
3535
3636 -- Usage hints for erasure analysis
37− %used MkUniquePair a
38− %used MkUniquePair b
39−
40− UPair : (A : AnyType) -> (B : AnyType) -> AnyType
41− UPair a b = UniquePair a b
42− %deprecate UPair "This name is being deprecated in favour of `UniquePair`"
43−
44− MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
45− MkUPair a b = MkUniquePair a b
46− %deprecate MkUPair "This name is being deprecated in favour of `MkUniquePair`"
37+ %used MkUPair a
38+ %used MkUPair b
4739
4840 ||| Dependent pairs aid in the construction of dependent types by
4941 ||| providing evidence that some value resides in the type.
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1567,8 +1567,8 @@ falseTy = sUN "Void"
15671567pairTy = sNS (sUN "Pair") ["Builtins"]
15681568pairCon = sNS (sUN "MkPair") ["Builtins"]
15691569
1570−upairTy = sNS (sUN "UniquePair") ["Builtins"]
1571−upairCon = sNS (sUN "MkUniquePair") ["Builtins"]
1570+upairTy = sNS (sUN "UPair") ["Builtins"]
1571+upairCon = sNS (sUN "MkUPair") ["Builtins"]
15721572
15731573eqTy = sUN "="
15741574eqCon = sUN "Refl"
test/unique001/unique001c.idr+3−3
@@ -11,7 +11,7 @@ data UTree : UniqueType where
1111 ULeaf : UTree
1212 UNode : UTree -> Int -> UTree -> UTree
1313
14−dup : UTree -> UniquePair UTree UTree
14+dup : UTree -> UPair UTree UTree
1515dup ULeaf = (ULeaf, ULeaf)
1616dup (UNode l y r) = let (l1, l2) = dup l
1717 (r1, r2) = dup r in
@@ -42,5 +42,5 @@ uconst x y = x
4242data MPair : AnyType -> AnyType -> AnyType where
4343 MkMPair : {a, b : Type*} -> a -> b -> MPair a b
4444
45−ndup : {a : UniqueType} -> a -> UniquePair a a
46−ndup {a} x = (\f : Int -> a => MkUniquePair (f 0) (f 1)) (uconst x)
45+ndup : {a : UniqueType} -> a -> UPair a a
46+ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)