git.iko.soy/Idris-dev
on master help sign in
Renamed `UPair` to `UniquePair`
commit8ed216a5552385a5182a7eb7aa4535cbfc974691 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateThu 15 Oct 2015, 14:13 (11 years ago) parentfa36bbc
4 files changed+31−23
compare with master
unifiedsplit
libs/prelude/Builtins.idr+12−6 libs/prelude/Prelude/Pairs.idr+12−6 src/Idris/AbsSyntaxTree.hs+4−4 test/unique001/unique001c.idr+3−7
libs/prelude/Builtins.idr+12−6
@@ -27,11 +27,11 @@ 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 UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
30+ data UniquePair : (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− MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
34+ MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
3535
3636 ||| Dependent pairs aid in the construction of dependent types by
3737 ||| providing evidence that some value resides in the type.
@@ -40,10 +40,16 @@ namespace Builtins
4040 ||| quantification - they consist of a witness for the existential
4141 ||| claim and a proof that the property holds for it.
4242 |||
43− ||| @ a the value to place in the type.
44− ||| @ P the dependent type that requires the value.
45− data Sigma : (a : Type) -> (P : a -> Type) -> Type where
46− MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
43+ ||| @a the value to place in the type.
44+ ||| @P the dependent type that requires the value.
45+ data DepPair : (a : Type) -> (P : a -> Type) -> Type where
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
4753
4854||| The empty type, also known as the trivially false proposition.
4955|||
libs/prelude/Prelude/Pairs.idr+12−6
@@ -14,7 +14,7 @@ using (a : Type, P : a -> Type)
1414 data Exists : (P : a -> Type) -> Type where
1515 Evidence : .(x : a) -> (pf : P x) -> Exists P
1616
17− ||| Dependent pair where the second field is erased.
17+ ||| Dependent pair where the second field is erased.
1818 data Subset : (a : Type) -> (P : a -> Type) -> Type where
1919 Element : (x : a) -> .(pf : P x) -> Subset a P
2020
@@ -34,12 +34,18 @@ using (a : Type, P : a -> Type)
3434 getProof : (x : Subset a P) -> P (getWitness x)
3535 getProof (Element x pf) = pf
3636
37− namespace Sigma
38− getWitness : Sigma a P -> a
39− getWitness (x ** pf) = x
37+ namespace DepPair
38+ fst : DepPair a P -> a
39+ fst (x ** pf) = x
4040
41− getProof : (x : Sigma a P) -> P (getWitness x)
42− getProof (x ** pf) = pf
41+ snd : (x : DepPair a P) -> P (fst x)
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
4349
4450 -- Polymorphic (class-based) projections have been removed
4551 -- because type-directed name disambiguation works better.
src/Idris/AbsSyntaxTree.hs+4−4
@@ -1567,8 +1567,8 @@ falseTy = sUN "Void"
15671567pairTy = sNS (sUN "Pair") ["Builtins"]
15681568pairCon = sNS (sUN "MkPair") ["Builtins"]
15691569
1570−upairTy = sNS (sUN "UPair") ["Builtins"]
1571−upairCon = sNS (sUN "MkUPair") ["Builtins"]
1570+upairTy = sNS (sUN "UniquePair") ["Builtins"]
1571+upairCon = sNS (sUN "MkUniquePair") ["Builtins"]
15721572
15731573eqTy = sUN "="
15741574eqCon = sUN "Refl"
@@ -1615,8 +1615,8 @@ modDocName :: Name
16151615modDocName = sMN 0 "ModuleDocs"
16161616
16171617-- Defined in builtins.idr
1618−sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1619−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1618+sigmaTy = sNS (sUN "DepPair") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDepPair") ["Builtins"]
16201620
16211621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
16221622piBind = piBindp expl
test/unique001/unique001c.idr+3−7
@@ -11,7 +11,7 @@ data UTree : UniqueType where
1111 ULeaf : UTree
1212 UNode : UTree -> Int -> UTree -> UTree
1313
14−dup : UTree -> UPair UTree UTree
14+dup : UTree -> UniquePair UTree UTree
1515dup ULeaf = (ULeaf, ULeaf)
1616dup (UNode l y r) = let (l1, l2) = dup l
1717 (r1, r2) = dup r in
@@ -42,9 +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 -> UPair a a
46−ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
47−
48−
49−
50−
45+ndup : {a : UniqueType} -> a -> UniquePair a a
46+ndup {a} x = (\f : Int -> a => MkUniquePair (f 0) (f 1)) (uconst x)