← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/AIM5/PolyDep/EqBase.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/AIM5/PolyDep/EqBase.agda
1
 
module EqBase where
2
 
import PolyDepPrelude
3
 
open PolyDepPrelude using
4
 
  ( Bool; true; false; _&&_
5
 
  ; Unit; unit
6
 
  ; Pair; pair
7
 
  ; Either; left; right
8
 
  ; Absurd
9
 
  ; Datoid; datoid; pElem
10
 
  ; True )
11
 
 
12
 
And = Pair
13
 
 
14
 
data Sigma (A : Set)(B : A -> Set) : Set where
15
 
  si : (a : A) -> (b : B a) -> Sigma A B
16
 
 
17
 
Eq : Set -> Set -> Set
18
 
Eq a b = a -> b -> Bool
19
 
 
20
 
eqEmpty : Eq Absurd Absurd
21
 
eqEmpty () -- empty
22
 
 
23
 
 
24
 
eqUnit : Eq Unit Unit
25
 
eqUnit unit unit = true
26
 
 
27
 
eqPair : {A1 A2 B1 B2 : Set} ->
28
 
         (Eq     A1          A2) ->
29
 
         (Eq        B1          B2) ->
30
 
         Eq (And A1 B1) (And A2 B2)
31
 
eqPair ea eb (pair a b) (pair a' b') = ea a a' && eb b b'
32
 
 
33
 
caseOn : (D : Datoid)
34
 
         {B1 B2 : pElem D -> Set}
35
 
         (ifTrue : (b : pElem D) -> B1 b -> B2 b -> Bool)
36
 
         (a b : pElem D)
37
 
         (pa : B1 a)
38
 
         (pb : B2 b)
39
 
         (e : Bool)
40
 
         (cast : True e -> B1 a -> B1 b)
41
 
         -> Bool
42
 
caseOn D ifTrue a b pa pb (false) cast = false
43
 
caseOn D ifTrue a b pa pb (true)  cast = ifTrue b (cast unit pa) pb
44
 
 
45
 
eqEither : {A1 A2 B1 B2 : Set}
46
 
           (eq1 : A1 -> B1 -> Bool)
47
 
           (eq2 : A2 -> B2 -> Bool)
48
 
         -> Either A1 A2 -> Either B1 B2 -> Bool
49
 
eqEither eq1 eq2 (left  a1) (left  b1) = eq1 a1 b1
50
 
eqEither eq1 eq2 (right a2) (right b2) = eq2 a2 b2
51
 
eqEither eq1 eq2 _          _          = false
52
 
 
53
 
{-
54
 
            case x of {
55
 
              (inl x') ->
56
 
                case y of {
57
 
                  (inl x0) -> eq1 x' x0;
58
 
                  (inr y') -> false@_;};
59
 
              (inr y') ->
60
 
                case y of {
61
 
                  (inl x') -> false@_;
62
 
                  (inr y0) -> eq2 y' y0;};}
63
 
-}
64
 
{-
65
 
 
66
 
eqSigma2 (D : Datoid)
67
 
         (|B1 |B2 : pElem D -> Set)
68
 
         (ifTrue : (b : pElem D) -> Eq (B1 b) (B2 b))
69
 
         (x : Sigma pElem D B1)
70
 
         (y : Sigma pElem D B2)
71
 
  : Bool
72
 
  = case x of {
73
 
      (si a pa) ->
74
 
        case y of {
75
 
          (si b pb) ->
76
 
            caseOn D ifTrue a b pa pb (D.eq a b) (D.subst B1);};}
77
 
 
78
 
eqSigma (D : Datoid)(|B1 : (a : pElem D) -> Set)(|B2 : (a : pElem D) -> Set)
79
 
  : ((a : pElem D) -> Eq (B1 a) (B2 a)) ->
80
 
     Eq (Sigma pElem D B1) (Sigma pElem D B2)
81
 
  = eqSigma2 D
82
 
 
83
 
eqSigmaLocalLet (D : Datoid)
84
 
                (|B1 |B2 : pElem D -> Set)
85
 
                (ifTrue : (b : pElem D) -> Eq (B1 b) (B2 b))
86
 
                (x : Sigma pElem D B1)
87
 
                (y : Sigma pElem D B2)
88
 
  : Bool
89
 
  = case x of {
90
 
      (si a pa) ->
91
 
        case y of {
92
 
          (si b pb) ->
93
 
            let caseOn (e : Bool)(cast : True e -> B1 a -> B1 b) : Bool
94
 
                  = case e of {
95
 
                      (false) -> false@_;
96
 
                      (true) -> ifTrue b (cast tt@_ pa) pb;}
97
 
            in  caseOn (D.eq a b) (D.subst B1);};}
98
 
 
99
 
 
100
 
eqSum' (D : Datoid)
101
 
     (|B1 |B2 : (a : pElem D) -> Set)
102
 
  : ((a : pElem D) -> Eq (B1 a) (B2 a)) ->
103
 
     Eq (Sum pElem D B1) (Sum pElem D B2)
104
 
  = \(e : (a : pElem D) -> Eq (B1 a) (B2 a)) ->
105
 
    \(p1 : Sum pElem D B1) ->
106
 
    \(p2 : Sum pElem D B2) ->
107
 
    caseOn D e p1.fst p2.fst p1.snd p2.snd (D.eq p1.fst p2.fst)
108
 
      (D.subst B1)
109
 
 
110
 
 
111
 
eqSum : (D : Datoid)
112
 
        {B1 B2 : (a : pElem D) -> Set}
113
 
  -> ((a : pElem D) -> Eq (B1 a) (B2 a)) ->
114
 
     Eq (Sum pElem D B1) (Sum pElem D B2)
115
 
eqSum e p1 p2 =
116
 
    caseOn D e p1.fst p2.fst p1.snd p2.snd (D.eq p1.fst p2.fst)
117
 
      (D.subst B1)
118
 
-}