git.iko.soy/Idris-dev
on master help sign in
Renamed `UniquePair` to `UPair`.
5e0e4e9Jan de Muijnck-Hughes
CHANGELOG+1−2
compare with master
unifiedsplit
@@ -20,8 +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−* `UPair` and `Sigma` have been renamed `UniquePair` and `DepPair`
23+* `Sigma` has been renamed to `DepPair`.
24− respectivly.
25* 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
26 line with standard accessor functions for pairs. The function `getWitness`
25 line with standard accessor functions for pairs. The function `getWitness`
27 is now `fst`, and `getProof` is `snd`.
26 is now `fst`, and `getProof` is `snd`.
libs/prelude/Builtins.idr+4−12
@@ -27,23 +27,15 @@ namespace Builtins
27 ||| UniqueTypes.
27 ||| UniqueTypes.
28 ||| @A the type of the left elements in the pair
28 ||| @A the type of the left elements in the pair
29 ||| @B the type of the left elements in the pair
29 ||| @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
31 ||| A pair of elements
31 ||| A pair of elements
32 ||| @a the left element of the pair
32 ||| @a the left element of the pair
33 ||| @b the right element of the pair
33 ||| @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
35
35
36 -- Usage hints for erasure analysis
36 -- Usage hints for erasure analysis
37− %used MkUniquePair a
37+ %used MkUPair a
38− %used MkUniquePair b
38+ %used MkUPair 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`"
47
39
48 ||| Dependent pairs aid in the construction of dependent types by
40 ||| Dependent pairs aid in the construction of dependent types by
49 ||| providing evidence that some value resides in the type.
41 ||| providing evidence that some value resides in the type.
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1567,8 +1567,8 @@ falseTy = sUN "Void"
1567pairTy = sNS (sUN "Pair") ["Builtins"]
1567pairTy = sNS (sUN "Pair") ["Builtins"]
1568pairCon = sNS (sUN "MkPair") ["Builtins"]
1568pairCon = sNS (sUN "MkPair") ["Builtins"]
1569
1569
1570−upairTy = sNS (sUN "UniquePair") ["Builtins"]
1570+upairTy = sNS (sUN "UPair") ["Builtins"]
1571−upairCon = sNS (sUN "MkUniquePair") ["Builtins"]
1571+upairCon = sNS (sUN "MkUPair") ["Builtins"]
1572
1572
1573eqTy = sUN "="
1573eqTy = sUN "="
1574eqCon = sUN "Refl"
1574eqCon = sUN "Refl"
test/unique001/unique001c.idr+3−3
@@ -11,7 +11,7 @@ data UTree : UniqueType where
11 ULeaf : UTree
11 ULeaf : UTree
12 UNode : UTree -> Int -> UTree -> UTree
12 UNode : UTree -> Int -> UTree -> UTree
13
13
14−dup : UTree -> UniquePair UTree UTree
14+dup : UTree -> UPair UTree UTree
15dup ULeaf = (ULeaf, ULeaf)
15dup ULeaf = (ULeaf, ULeaf)
16dup (UNode l y r) = let (l1, l2) = dup l
16dup (UNode l y r) = let (l1, l2) = dup l
17 (r1, r2) = dup r in
17 (r1, r2) = dup r in
@@ -42,5 +42,5 @@ uconst x y = x
42data MPair : AnyType -> AnyType -> AnyType where
42data MPair : AnyType -> AnyType -> AnyType where
43 MkMPair : {a, b : Type*} -> a -> b -> MPair a b
43 MkMPair : {a, b : Type*} -> a -> b -> MPair a b
44
44
45−ndup : {a : UniqueType} -> a -> UniquePair a a
45+ndup : {a : UniqueType} -> a -> UPair a a
46−ndup {a} x = (\f : Int -> a => MkUniquePair (f 0) (f 1)) (uconst x)
46+ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)