git.iko.soy/Idris-dev
on master help sign in
Renamed `UPair` to `UniquePair`
8ed216aJan de Muijnck-Hughes
libs/prelude/Builtins.idr+12−6
compare with master
unifiedsplit
@@ -27,11 +27,11 @@ 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 UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
30+ data UniquePair : (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− MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
34+ MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
35
35
36 ||| Dependent pairs aid in the construction of dependent types by
36 ||| Dependent pairs aid in the construction of dependent types by
37 ||| providing evidence that some value resides in the type.
37 ||| providing evidence that some value resides in the type.
@@ -40,10 +40,16 @@ namespace Builtins
40 ||| quantification - they consist of a witness for the existential
40 ||| quantification - they consist of a witness for the existential
41 ||| claim and a proof that the property holds for it.
41 ||| claim and a proof that the property holds for it.
42 |||
42 |||
43− ||| @ a the value to place in the type.
43+ ||| @a the value to place in the type.
44− ||| @ P the dependent type that requires the value.
44+ ||| @P the dependent type that requires the value.
45− data Sigma : (a : Type) -> (P : a -> Type) -> Type where
45+ data DepPair : (a : Type) -> (P : a -> Type) -> Type where
46− MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
46+ MkDepPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DepPair a P
47+
48+ Sigma : (a : Type) -> (P : a -> Type) -> Type
49+ Sigma wit prf = DepPair wit prf
50+
51+ MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DepPair a P
52+ MkSigma wit prf = MkDepPair wit prf
47
53
48||| The empty type, also known as the trivially false proposition.
54||| The empty type, also known as the trivially false proposition.
49|||
55|||
libs/prelude/Prelude/Pairs.idr+12−6
@@ -14,7 +14,7 @@ using (a : Type, P : a -> Type)
14 data Exists : (P : a -> Type) -> Type where
14 data Exists : (P : a -> Type) -> Type where
15 Evidence : .(x : a) -> (pf : P x) -> Exists P
15 Evidence : .(x : a) -> (pf : P x) -> Exists P
16
16
17− ||| Dependent pair where the second field is erased.
17+ ||| Dependent pair where the second field is erased.
18 data Subset : (a : Type) -> (P : a -> Type) -> Type where
18 data Subset : (a : Type) -> (P : a -> Type) -> Type where
19 Element : (x : a) -> .(pf : P x) -> Subset a P
19 Element : (x : a) -> .(pf : P x) -> Subset a P
20
20
@@ -34,12 +34,18 @@ 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 Sigma
37+ namespace DepPair
38− getWitness : Sigma a P -> a
38+ fst : DepPair a P -> a
39− getWitness (x ** pf) = x
39+ fst (x ** pf) = x
40
40
41− getProof : (x : Sigma a P) -> P (getWitness x)
41+ snd : (x : DepPair a P) -> P (fst x)
42− getProof (x ** pf) = pf
42+ snd (x ** pf) = pf
43+
44+ getWitness : DepPair a P -> a
45+ getWitness = fst
46+
47+ getProof : (x : Sigma a P) -> P (fst x)
48+ getProof = snd
43
49
44 -- Polymorphic (class-based) projections have been removed
50 -- Polymorphic (class-based) projections have been removed
45 -- because type-directed name disambiguation works better.
51 -- because type-directed name disambiguation works better.
src/Idris/AbsSyntaxTree.hs+4−4
@@ -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 "UPair") ["Builtins"]
1570+upairTy = sNS (sUN "UniquePair") ["Builtins"]
1571−upairCon = sNS (sUN "MkUPair") ["Builtins"]
1571+upairCon = sNS (sUN "MkUniquePair") ["Builtins"]
1572
1572
1573eqTy = sUN "="
1573eqTy = sUN "="
1574eqCon = sUN "Refl"
1574eqCon = sUN "Refl"
@@ -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 "Sigma") ["Builtins"]
1618+sigmaTy = sNS (sUN "DepPair") ["Builtins"]
1619−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDepPair") ["Builtins"]
1620
1620
1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1622piBind = piBindp expl
1622piBind = piBindp expl
test/unique001/unique001c.idr+3−7
@@ -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 -> UPair UTree UTree
14+dup : UTree -> UniquePair 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,9 +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 -> UPair a a
45+ndup : {a : UniqueType} -> a -> UniquePair a a
46−ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
46+ndup {a} x = (\f : Int -> a => MkUniquePair (f 0) (f 1)) (uconst x)
47−
48−
49−
50−