git.iko.soy/Idris-dev
on master help sign in
Reorganise dependent pair types in Prelude.
commite541d7e689f1baff8675941c9ce68192b9d5ffe7 authorMatus Tejiscak <ziman@functor.sk> dateThu 22 May 2014, 17:39 (12 years ago) parent00793ac
4 files changed+40−15
compare with master
unifiedsplit
libs/prelude/Builtins.idr+4−11 libs/prelude/Prelude/Pairs.idr+32 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Delaborate.hs+2−2
libs/prelude/Builtins.idr+4−11
@@ -3,19 +3,12 @@
33%access public
44%default total
55
6−||| Dependent pairs, in their internal representation
6+||| Dependent pairs, in their internal representation.
7+||| Nothing is erased in this variant; for alternatives see Prelude.Pairs.
78||| @ a the type of the witness
89||| @ P the type of the proof
9−data Exists : (a : Type) -> (P : a -> Type) -> Type where
10− Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P
11−
12−||| The first projection from a dependent pair
13−getWitness : {P : a -> Type} -> Exists a P -> a
14−getWitness (a ** v) = a
15−
16−||| The second projection from a dependent pair
17−getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
18−getProof (a ** v) = v
10+data Pair : (a : Type) -> (P : a -> Type) -> Type where
11+ pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
1912
2013||| The eliminator for the empty type.
2114FalseElim : _|_ -> a
libs/prelude/Prelude/Pairs.idrnew file+32
@@ -0,0 +1,32 @@
1+module Prelude.Pairs
2+
3+%access public
4+%default total
5+
6+||| Dependent pair where the first field is erased.
7+data Exists : {a : Type} -> (P : a -> Type) -> Type where
8+ witness : .{x : a} -> (pf : P x) -> Exists P
9+
10+||| Dependent pair where the second field is erased.
11+data Subset : (a : Type) -> (P : a -> Type) -> Type where
12+ element : (x : a) -> .(pf : P x) -> Subset a P
13+
14+||| Class of dependent pair constructors.
15+class DependentPair f where
16+ ||| Project the first field from a dependent pair.
17+ getWitness : f a P -> a
18+
19+ ||| Project the second field from a dependent pair.
20+ getProof : (x : f a P) -> P (getWitness x)
21+
22+instance DependentPair Pair where
23+ getWitness (pair x pf) = x
24+ getProof (pair x pf) = pf
25+
26+instance DependentPair Exists where
27+ getWitness (witness x pf) = x
28+ getProof (witness x pf) = pf
29+
30+instance DependentPair Subset where
31+ getWitness (element x pf) = x
32+ getProof (element x pf) = pf
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1098,8 +1098,8 @@ elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defau
10981098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
10991099
11001100-- Defined in builtins.idr
1101−sigmaTy = sUN "Exists"
1102−existsCon = sUN "Ex_intro"
1101+sigmaTy = sUN "Pair"
1102+existsCon = sUN "pair"
11031103
11041104piBind :: [(Name, PTerm)] -> PTerm -> PTerm
11051105piBind = piBindp expl
src/Idris/Delaborate.hs+2−2
@@ -92,13 +92,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
9292 | n == eqCon = PRefl un (de env [] r)
9393 | n == sUN "lazy" = de env [] r
9494 deFn env (P _ n _) [ty, Bind x (Lam _) r]
95− | n == sUN "Exists"
95+ | n == sUN "Pair"
9696 = PDPair un IsType (PRef un x) (de env [] ty)
9797 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
9898 deFn env (P _ n _) [_,_,l,r]
9999 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
100100 | n == eqTy = PEq un (de env [] l) (de env [] r)
101− | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder
101+ | n == sUN "pair" = PDPair un IsTerm (de env [] l) Placeholder
102102 (de env [] r)
103103 deFn env f@(P _ n _) args
104104 | n `elem` map snd env