git.iko.soy/Idris-dev
on master help sign in
Reorganise dependent pair types in Prelude.
e541d7eMatus Tejiscak
libs/prelude/Builtins.idr+4−11
compare with master
unifiedsplit
@@ -3,19 +3,12 @@
3%access public
3%access public
4%default total
4%default total
5
5
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.
7||| @ a the type of the witness
8||| @ a the type of the witness
8||| @ P the type of the proof
9||| @ P the type of the proof
9−data Exists : (a : Type) -> (P : a -> Type) -> Type where
10+data Pair : (a : Type) -> (P : a -> Type) -> Type where
10− Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P
11+ pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair 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
19
12
20||| The eliminator for the empty type.
13||| The eliminator for the empty type.
21FalseElim : _|_ -> a
14FalseElim : _|_ -> 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
1098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1099
1099
1100-- Defined in builtins.idr
1100-- Defined in builtins.idr
1101−sigmaTy = sUN "Exists"
1101+sigmaTy = sUN "Pair"
1102−existsCon = sUN "Ex_intro"
1102+existsCon = sUN "pair"
1103
1103
1104piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1104piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1105piBind = piBindp expl
1105piBind = piBindp expl
src/Idris/Delaborate.hs+2−2
@@ -92,13 +92,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
92 | n == eqCon = PRefl un (de env [] r)
92 | n == eqCon = PRefl un (de env [] r)
93 | n == sUN "lazy" = de env [] r
93 | n == sUN "lazy" = de env [] r
94 deFn env (P _ n _) [ty, Bind x (Lam _) r]
94 deFn env (P _ n _) [ty, Bind x (Lam _) r]
95− | n == sUN "Exists"
95+ | n == sUN "Pair"
96 = PDPair un IsType (PRef un x) (de env [] ty)
96 = PDPair un IsType (PRef un x) (de env [] ty)
97 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
97 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
98 deFn env (P _ n _) [_,_,l,r]
98 deFn env (P _ n _) [_,_,l,r]
99 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
99 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
100 | n == eqTy = PEq un (de env [] l) (de env [] r)
100 | 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
102 (de env [] r)
102 (de env [] r)
103 deFn env f@(P _ n _) args
103 deFn env f@(P _ n _) args
104 | n `elem` map snd env
104 | n `elem` map snd env