← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/prototyping/termrep/lambdapi/prelude.lp

  • 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:
src/prototyping/termrep/lambdapi/prelude.lp
1
 
 
2
 
let id    = (\ a x -> x) : forall (a : *) . a -> a 
3
 
let const = (\ a b x y -> x) : forall (a : *) (b : *) . a -> b -> a
4
 
 
5
 
let plus =
6
 
  natElim
7
 
    ( \ _ -> Nat -> Nat )           -- motive
8
 
    ( \ n -> n )                    -- case for Zero
9
 
    ( \ p rec n -> Succ (rec n) )   -- case for Succ
10
 
 
11
 
let pred =
12
 
  natElim
13
 
    ( \ _ -> Nat )
14
 
    Zero
15
 
    ( \ n' _rec -> n' )
16
 
 
17
 
let natFold =
18
 
  ( \ m mz ms -> natElim
19
 
                   ( \ _ -> m )
20
 
                   mz
21
 
                   ( \ n' rec -> ms rec ) )
22
 
  : forall (m : *) . m -> (m -> m) -> Nat -> m
23
 
 
24
 
let nat1Elim =
25
 
  ( \ m m0 m1 ms -> natElim m m0
26
 
                            (\ p rec -> natElim (\ n -> m (Succ n)) m1 ms p) )
27
 
  : forall (m : Nat -> *) . m 0 -> m 1 ->
28
 
     (forall n : Nat . m (Succ n) -> m (Succ (Succ n))) ->
29
 
     forall (n : Nat) . m n
30
 
 
31
 
let nat2Elim =
32
 
  ( \ m m0 m1 m2 ms -> nat1Elim m m0 m1
33
 
                                (\ p rec -> natElim (\ n -> m (Succ (Succ n))) m2 ms p) )
34
 
  : forall (m : Nat -> *) . m 0 -> m 1 -> m 2 ->
35
 
     (forall n : Nat . m (Succ (Succ n)) -> m (Succ (Succ (Succ n)))) ->
36
 
     forall (n : Nat) . m n
37
 
let inc = natFold Nat (Succ Zero) Succ
38
 
 
39
 
let finNat = finElim (\ _ _ -> Nat)
40
 
                     (\ _ -> Zero)
41
 
                     (\ _ _ rec -> Succ rec)
42
 
 
43
 
let Unit = Fin 1
44
 
let U = FZero 0
45
 
let unitElim =
46
 
  ( \ m mu -> finElim ( nat1Elim (\ n -> Fin n -> *)
47
 
                                 (\ _ -> Unit)
48
 
                                 (\ x -> m x)
49
 
                                 (\ _ _ _ -> Unit) )
50
 
                      ( natElim (\ n -> natElim (\ n -> Fin (Succ n) -> *)
51
 
                                                (\ x -> m x)
52
 
                                                (\ _ _ _ -> Unit)
53
 
                                                n (FZero n))
54
 
                                mu
55
 
                                (\ _ _ -> U) )
56
 
                      ( \ n f _ -> finElim (\ n f -> natElim (\ n -> Fin (Succ n) -> *)
57
 
                                                             (\ x -> m x)
58
 
                                                             (\ _ _ _ -> Unit)
59
 
                                                             n (FSucc n f))
60
 
                                           (\ _ -> U)
61
 
                                           (\ _ _ _ -> U)
62
 
                                           n f )
63
 
                      1 )
64
 
  : forall (m : Unit -> *) . m U -> forall (u : Unit) . m u
65
 
 
66
 
let Void = Fin 0
67
 
let voidElim =
68
 
  ( \ m -> finElim (natElim (\ n -> Fin n -> *)
69
 
                            (\ x -> m x)
70
 
                            (\ _ _ _ -> Unit))
71
 
                   (\ _ -> U)
72
 
                   (\ _ _ _ -> U)
73
 
                   0 )
74
 
  : forall (m : Void -> *) (v : Void) . m v
75
 
 
76
 
let Bool = Fin 2 
77
 
let False = FZero 1
78
 
let True  = FSucc 1 (FZero 0)
79
 
let boolElim =
80
 
  ( \ m mf mt -> finElim ( nat2Elim (\ n -> Fin n -> *)
81
 
                                    (\ _ -> Unit) (\ _ -> Unit)
82
 
                                    (\ x -> m x)
83
 
                                    (\ _ _ _ -> Unit) )
84
 
                         ( nat1Elim ( \ n -> nat1Elim (\ n -> Fin (Succ n) -> *)
85
 
                                                      (\ _ -> Unit)
86
 
                                                      (\ x -> m x)
87
 
                                                      (\ _ _ _ -> Unit)
88
 
                                                      n (FZero n))
89
 
                                    U mf (\ _ _ -> U) )
90
 
                         ( \ n f _ -> finElim ( \ n f -> nat1Elim (\ n -> Fin (Succ n) -> *)
91
 
                                                                  (\ _ -> Unit)
92
 
                                                                  (\ x -> m x)
93
 
                                                                  (\ _ _ _ -> Unit)
94
 
                                                                  n (FSucc n f) )
95
 
                                              ( natElim
96
 
                                                  ( \ n -> natElim
97
 
                                                             (\ n -> Fin (Succ (Succ n)) -> *)
98
 
                                                             (\ x -> m x)
99
 
                                                             (\ _ _ _ -> Unit)
100
 
                                                             n (FSucc (Succ n) (FZero n)) )
101
 
                                                  mt (\ _ _ -> U) )
102
 
                                              ( \ n f _ -> finElim
103
 
                                                             (\ n f -> natElim
104
 
                                                                         (\ n -> Fin (Succ (Succ n)) -> *)
105
 
                                                                         (\ x -> m x)
106
 
                                                                         (\ _ _ _ -> Unit)
107
 
                                                                         n (FSucc (Succ n) (FSucc n f)))
108
 
                                                             (\ _ -> U)
109
 
                                                             (\ _ _ _ -> U)
110
 
                                                             n f )
111
 
                                              n f )
112
 
                         2 )
113
 
  : forall (m : Bool -> *) . m False -> m True -> forall (b : Bool) . m b
114
 
 
115
 
let not = boolElim (\ _ -> Bool) True False
116
 
let and = boolElim (\ _ -> Bool -> Bool) (\ _ -> False) (id Bool)
117
 
let or  = boolElim (\ _ -> Bool -> Bool) (id Bool) (\ _ -> True)
118
 
let iff = boolElim (\ _ -> Bool -> Bool) not (id Bool)
119
 
let xor = boolElim (\ _ -> Bool -> Bool) (id Bool) not
120
 
 
121
 
let even    = natFold Bool True not
122
 
let odd     = natFold Bool False not
123
 
let isZero  = natFold Bool True (\ _ -> False)
124
 
let isSucc  = natFold Bool False (\ _ -> True)
125
 
 
126
 
let natEq =
127
 
  natElim
128
 
    ( \ _ -> Nat -> Bool )
129
 
    ( natElim
130
 
        ( \ _ -> Bool )
131
 
        True
132
 
        ( \ n' _ -> False ) )
133
 
    ( \ m' rec_m' -> natElim
134
 
                       ( \ _ -> Bool )
135
 
                       False
136
 
                       ( \ n' _ -> rec_m' n' ))
137
 
 
138
 
let Prop = boolElim (\ _ -> *) Void Unit
139
 
 
140
 
let pNatEqRefl =
141
 
  natElim
142
 
    (\ n -> Prop (natEq n n))
143
 
    U
144
 
    (\ n' rec -> rec)
145
 
  : forall (n : Nat) . Prop (natEq n n)
146
 
 
147
 
let Not = (\ a -> a -> Void) : * -> *
148
 
 
149
 
let leibniz =
150
 
  ( \ a b f -> eqElim a
151
 
                 (\ x y eq_x_y -> Eq b (f x) (f y))
152
 
                 (\ x -> Refl b (f x)) )
153
 
  : forall (a : *) (b : *) (f : a -> b) (x : a) (y : a) .
154
 
     Eq a x y -> Eq b (f x) (f y)
155
 
 
156
 
let symm =
157
 
  ( \ a -> eqElim a
158
 
             (\ x y eq_x_y -> Eq a y x)
159
 
             (\ x -> Refl a x) )
160
 
  : forall (a : *) (x : a) (y : a) .
161
 
     Eq a x y -> Eq a y x
162
 
 
163
 
let tran =
164
 
  ( \ a x y z eq_x_y -> eqElim a
165
 
                          (\ x y eq_x_y -> forall (z : a) . Eq a y z -> Eq a x z)
166
 
                          (\ x z eq_x_z -> eq_x_z)
167
 
                          x y eq_x_y z )
168
 
  : forall (a : *) (x : a) (y : a) (z : a) .
169
 
     Eq a x y -> Eq a y z -> Eq a x z
170
 
 
171
 
let apply =
172
 
  eqElim * (\ a b _ -> a -> b) (\ _ x -> x)
173
 
  : forall (a : *) (b : *) (p : Eq * a b) . a -> b
174
 
 
175
 
let p1IsNot0 =
176
 
  (\ p -> apply Unit Void
177
 
                (leibniz Nat *
178
 
                         (natElim (\ _ -> *) Void (\ _ _ -> Unit))
179
 
                         1 0 p)
180
 
                U)
181
 
  : Not (Eq Nat 1 0)
182
 
 
183
 
let p0IsNot1 =
184
 
  (\ p -> p1IsNot0 (symm Nat 0 1 p))
185
 
  : Not (Eq Nat 0 1)
186
 
 
187
 
let p0IsNoSucc = 
188
 
  natElim
189
 
    ( \ n -> Not (Eq Nat 0 (Succ n)) )
190
 
    p0IsNot1
191
 
    ( \ n' rec_n' eq_0_SSn' ->
192
 
      rec_n' (leibniz Nat Nat pred Zero (Succ (Succ n')) eq_0_SSn') )
193
 
 
194
 
let replicate =
195
 
  ( natElim
196
 
      ( \ n -> forall (a : *) . a -> Vec a n )
197
 
      ( \ a _ -> Nil a )
198
 
      ( \ n' rec_n' a x -> Cons a n' x (rec_n' a x) ) )
199
 
  : forall (n : Nat) . forall (a : *) . a -> Vec a n
200
 
 
201
 
let replicate' =
202
 
  (\ a n x -> natElim (Vec a)
203
 
                      (Nil a)
204
 
                      (\ n' rec_n' -> Cons a n' x rec_n') n)
205
 
  : forall (a : *) (n : Nat) . a -> Vec a n
206
 
 
207
 
let fromto =
208
 
  natElim
209
 
    ( \ n -> Vec Nat n )
210
 
    ( Nil Nat )
211
 
    ( \ n' rec_n' -> Cons Nat n' n' rec_n' )
212
 
 
213
 
let append =
214
 
  ( \ a -> vecElim a
215
 
             (\ m _ -> forall (n : Nat) . Vec a n -> Vec a (plus m n))
216
 
             (\ _ v -> v)
217
 
             (\ m v vs rec n w -> Cons a (plus m n) v (rec n w)))
218
 
  :  forall (a : *) (m : Nat) (v : Vec a m) (n : Nat) (w : Vec a n).
219
 
      Vec a (plus m n)
220
 
 
221
 
let tail' =
222
 
  (\ a -> vecElim a ( \ m v -> forall (n : Nat) . Eq Nat m (Succ n) -> Vec a n )
223
 
                    ( \ n eq_0_SuccN -> voidElim ( \ _ -> Vec a n )
224
 
                                                 ( p0IsNoSucc n eq_0_SuccN ) )
225
 
                    ( \ m' v vs rec_m' n eq_SuccM'_SuccN ->
226
 
                      eqElim Nat
227
 
                             (\ m' n e -> Vec a m' -> Vec a n)
228
 
                             (\ _ v -> v)
229
 
                             m' n
230
 
                             (leibniz Nat Nat pred (Succ m') (Succ n) eq_SuccM'_SuccN) vs))
231
 
  : forall (a : *) (m : Nat) . Vec a m -> forall (n : Nat) . Eq Nat m (Succ n) -> Vec a n
232
 
 
233
 
let tail =
234
 
  (\ a n v -> tail' a (Succ n) v n (Refl Nat (Succ n)))
235
 
  : forall (a : *) (n : Nat) . Vec a (Succ n) -> Vec a n
236
 
 
237
 
let at =
238
 
  (\ a -> vecElim a ( \ n v -> Fin n -> a )
239
 
                    ( \ f -> voidElim (\ _ -> a) f )
240
 
                    ( \ n' v vs rec_n' f_SuccN' ->
241
 
                      finElim ( \ n _ -> Eq Nat n (Succ n') -> a )
242
 
                              ( \ n e -> v )
243
 
                              ( \ n f_N _ eq_SuccN_SuccN' ->
244
 
                                rec_n' (eqElim Nat
245
 
                                               (\ x y e -> Fin x -> Fin y)
246
 
                                               (\ _ f -> f)
247
 
                                               n n'
248
 
                                               (leibniz Nat Nat pred
249
 
                                                        (Succ n) (Succ n') eq_SuccN_SuccN')
250
 
                                               f_N))
251
 
                              (Succ n')
252
 
                              f_SuccN'
253
 
                              (Refl Nat (Succ n'))))
254
 
  : forall (a : *) (n : Nat) . Vec a n -> Fin n -> a
255
 
 
256
 
let head =
257
 
  (\ a n v -> at a (Succ n) v (FZero n))
258
 
  : forall (a : *) (n : Nat) . Vec a (Succ n) -> a
259
 
 
260
 
let map =
261
 
  (\ a b f -> vecElim a ( \ n _ -> Vec b n )
262
 
                        ( Nil b )
263
 
                        ( \ n x _ rec -> Cons b n (f x) rec ))
264
 
  : forall (a : *) (b : *) (f : a -> b) (n : Nat) . Vec a n -> Vec b n
265
 
 
266
 
let p0PlusNisN =
267
 
  Refl Nat
268
 
  : forall n : Nat . Eq Nat (plus 0 n) n
269
 
 
270
 
let pNPlus0isN =
271
 
  natElim ( \ n -> Eq Nat (plus n 0) n )
272
 
          ( Refl Nat 0 )
273
 
          ( \ n' rec -> leibniz Nat Nat Succ (plus n' 0) n' rec )
274
 
  : forall n : Nat . Eq Nat (plus n 0) n
275
 
 
276