coq_obj.v 18.2 KB
Newer Older
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
1
Require Import String.
2
3
4
5
Require Import Bool.
Require Eqdep_dec.
Require EqdepFacts.
Import EqNotations.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
6

7
8
Axiom fun_ext : forall A B (f g : A -> B),
                  (forall x, f x = g x) -> f = g.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
9

10
11
12
13
14
15
16
17
18
19
Lemma sigT_eq {U} {P} {A B : U} {HA : P A} {HB : P B} :
  forall e : A = B, (rew e in HA) = HB ->
                    existT P A HA = existT P B HB.
Proof.
  intros e He.
  destruct e.
  destruct He.
  reflexivity.
Defined.

20
21
22
Inductive Istrue : bool -> Prop :=
| Istrue_true : Istrue true.

23
24
Definition isProp A := forall x y : A, x = y.

25
26
27
28
29
30
31
32
33
Module String_dec.
  Definition U := string.
  Definition eq_dec := string_dec.
End String_dec.

Module String_UIP := Eqdep_dec.DecidableEqDep (String_dec).

Section domains.

34
35
36
37
38
  Inductive Position (l : string) : forall (l2 : string) (d : list string), Type :=
  | At_head l2 d : l = l2 -> Position l l2 d
  | In_tail l2 d : Pos2 l d -> Position l l2 d
  with Pos2 (l : string) : forall (d : list string), Type :=
  | PCons {hd tl} : Position l hd tl -> Pos2 l (cons hd tl).
39

40
41
42
43
44
45
46
47
  Definition PCons2 {l hd tl} : Pos2 l (cons hd tl) -> Position l hd tl.
  Proof.
    intro H.
    inversion H.
    assumption.
  Defined.

  Definition head (d : list string) : string :=
48
    match d with
49
50
      | nil => ""%string
      | cons l _ => l
51
52
    end.

53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
  Definition tail := @List.tail string.

  Definition PCons_destr l l2 d H : H = @PCons l l2 d (PCons2 H).
  Proof.
    refine (match H with PCons l2 d p => _ end).
    reflexivity.
  Defined.

  (* Destruction principle which doesn't destroy d *)
  Definition destruct_pos {l l2 d} H (P : Position l l2 d -> Type) :
    (forall e, P (At_head l l2 d e)) ->
    (forall (H : Pos2 l d),
       P (In_tail l l2 d H)) ->
    P H.
  Proof.
    intros IH1 IH2.
    induction H.
    - apply IH1.
    - apply IH2.
  Defined.

  Fixpoint mem l d :=
75
    match d with
76
      | nil => false
77
      | cons l2 d =>
78
        if (string_dec l l2) then true else mem l d
79
80
    end.

81
  Fixpoint mem_pos l d : Istrue (mem l d) -> Pos2 l d.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
82
  Proof.
83
    destruct d as [ | l2 d ].
84
85
    simpl.
    - intro H; inversion H.
86
    - simpl.
87
88
89
90
91
92
93
94
95
96
97
      case (string_dec l l2) as [ e | n ].
      + intro.
        apply PCons.
        apply At_head.
        assumption.
      + simpl.
        intro H.
        apply PCons.
        apply In_tail.
        apply mem_pos.
        assumption.
98
99
  Defined.

100
  Lemma Pos_tail l l2 d : l <> l2 -> Position l l2 d -> Pos2 l d.
101
  Proof.
102
103
104
105
106
    intros n p.
    destruct p.
    - destruct (n e).
    - assumption.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
107

108
  Fixpoint mem_pos_neg l d {struct d} : Istrue (negb (mem l d)) -> Pos2 l d -> False.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
109
  Proof.
110
    destruct d as [ | l2 d ].
111
112
    simpl.
    - intros _ H; inversion H.
113
    - simpl.
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
      case (string_dec l l2) as [ e | n ].
      + intro H; inversion H.
      + intro H.
        intro p.
        apply PCons2 in p.
        apply (Pos_tail l l2 d n) in p.
        apply (mem_pos_neg l d); assumption.
  Defined.

  (* Domains without duplicates have unique positions *)
  Fixpoint duplicate_free d :=
    match d with
      | nil => true
      | cons l d => negb (mem l d) && duplicate_free d
    end.

  Definition in_eq l d := isProp (Pos2 l d).
131

132
  Fixpoint df_in_eq l d {struct d} : Istrue (duplicate_free d) -> in_eq l d.
133
  Proof.
134
135
136
    destruct d as [ | l2 d].
    - intros _ H1 H2.
      inversion H1.
137
    - simpl.
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
      case_eq (mem l2 d).
      + intros _ H; inversion H.
      + intro Hm.
        assert (Istrue (negb (mem l2 d))) as Hm2 by (rewrite Hm; exact Istrue_true).
        simpl.
        intro df.
        assert (in_eq l d) as IH by intuition.
        clear df_in_eq.
        intros H1 H2.
        rewrite (PCons_destr _ _ _ H1).
        rewrite (PCons_destr _ _ _ H2).
        apply f_equal.
        generalize (PCons2 H1).
        generalize (PCons2 H2).
        intros H'2 H'1.
        destruct H'1; destruct H'2.
        * apply f_equal.
          apply String_UIP.UIP.
        * destruct e.
          destruct (mem_pos_neg _ _ Hm2 p).
        * destruct e.
          destruct (mem_pos_neg _ _ Hm2 p).
        * apply f_equal.
          apply IH.
  Defined.
163

164
165
End domains.

166
Infix "∈" := (Pos2) (at level 60).
167

168
Definition subset d1 d2 : Type := forall l, (l  d1) -> (l  d2).
169

170
Infix "⊂" := subset (at level 60).
171

172
Section types.
173
174
  (* Object types are records of types, we define them as association lists *)

175
176
177
  Inductive type :=
  | Empty_type
  | Cons_type : string -> type -> type -> type.
178

179
End types.
180

181
Section assoc.
182

183
  Fixpoint domain A :=
184
    match A with
185
186
      | Empty_type => nil
      | Cons_type l _ C => cons l (domain C)
187
188
    end.

189
  Fixpoint assoc A l (H : l  domain A) : type.
190
  Proof.
191
192
193
194
195
196
197
198
199
    destruct A as [ | lA A1 A2].
    - simpl in H.
      inversion H.
    - simpl in H.
      apply PCons2 in H.
      apply (destruct_pos H (fun H => type)).
      + intro; exact A1.
      + exact (assoc A2 l).
  Defined.
200

201
End assoc.
202
203

(* Scope of object types *)
204
Bind Scope obj_type_scope with type.
205
206
207
208
Delimit Scope obj_type_scope with ty.
(* Scope of object type fields (pairs of strings and types) *)
Delimit Scope type_field_scope with tf.

209
210
Section subtyping.

211
  Notation "A ⊙ l" := (assoc A%ty l%string) (at level 50).
212

213
  Fixpoint type_dec (A B : type) : {A = B} + {A <> B}.
214
215
216
  Proof.
    decide equality.
    apply string_dec.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
217
218
  Qed.

219
  (* Definition of the subtyping relation: A <: B if B is a subset of A. *)
220
  Fixpoint Subtype A B {struct B} : Type :=
221
    match B with
222
223
224
      | Empty_type => True
      | Cons_type l B1 B2 =>
        sigT (fun H => ((assoc A l H = B1) * Subtype A B2)%type)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
225
    end.
226
227
228

  Infix "<:" := Subtype (at level 60).

229
230
231
  Lemma subtype_tail {A} {B} l C :
    A <: B ->
         Cons_type l C A <: B.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
232
  Proof.
233
234
235
236
237
238
239
240
241
    induction B as [ | lB B1 B2].
    - intuition.
    - intros (H, (He, st)).
      exists (PCons _ (In_tail lB l (domain A) H)).
      split.
      + simpl.
        assumption.
      + intuition.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
242

243
  Lemma subtype_refl A : A <: A.
244
  Proof.
245
    induction A as [ | l A HA B HB ].
246
247
    - intuition.
    - simpl.
248
      exists (PCons _ (At_head l l (domain B) eq_refl)).
249
      simpl.
250
251
252
253
254
      split.
      + reflexivity.
      + apply subtype_tail.
        assumption.
  Defined.
255

256
257
  Fixpoint domain_subtype {A} {B} :
    A <: B -> domain B  domain A.
258
  Proof.
259
260
261
262
263
264
265
266
267
268
    intros st l H.
    destruct B as [ | lB B1 B2 ].
    - inversion H.
    - destruct st as (Ha, (He, Hst)).
      apply PCons2 in H.
      inversion H as [ l' d Hl Hd | l2 d Hp Hl Hd ].
      + rewrite Hl.
        assumption.
      + apply (domain_subtype A B2 Hst l).
        assumption.
269
270
  Defined.

271
272
  Fixpoint assoc_subtype {A} {B} (st : A <: B) l H :
    assoc B l H = assoc A l (domain_subtype st l H).
273
  Proof.
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
    destruct B as [ | lB B1 B2].
    - inversion H.
    - rewrite (PCons_destr _ _ (domain B2) H).
      simpl in H.
      generalize (PCons2 H).
      intro p.
      clear H.
      apply (destruct_pos p).
      + intro e.
        simpl.
        destruct e.
        destruct st as (Ha, (Heq, Hst)).
        symmetry.
        assumption.
      + intro H.
        simpl.
        destruct st as (Ha, (Heq, Hst)).
        apply (assoc_subtype A B2 _ l H).
292
293
  Defined.

294
  Theorem subtype_trans {A} B {C} : A <: B -> B <: C -> A <: C.
295
  Proof.
296
    induction C as [ | lC C1 C2].
297
    - trivial.
298
299
300
301
302
303
    - intros stAB (HdBC, (HeqBC, HstBC)).
      exists (domain_subtype stAB lC HdBC).
      split.
      + rewrite <- (assoc_subtype stAB lC HdBC).
        assumption.
      + intuition.
304
305
306
  Qed.
End subtyping.

307
Infix "<:" := Subtype (at level 60).
308

309
310
Definition insert (lA : string * type) (A2 : type) :=
  let (l, A) := lA in Cons_type l A A2.
311

312
      (* Notations for object pretypes:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
313
314
315
316
   [ "l₁" : A ; "l₂" : A ;  ; "lₙ" : A ]
 *)
Notation "l : A" := (l%string, A) (at level 50) : type_field_scope.
Notation "[ x1 ; .. ; xn ]" :=
317
  (insert x1%tf .. (insert xn%tf Empty_type) ..) : obj_type_scope.
318
Notation "l : A :: B" := (Cons_type l A B) (at level 100) : type_field_scope.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
319
320
321

Section objects.
  (* Objects are records of methods.
322
   A well-pretyped object of type A = [ l : A ]
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
323
324
   is of the form [ l = ς(x !: A) t ] where x : A  t : A

325
   The type A appears 3 times in the definition of well-pretyped object of type A :
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
326
    - in each ς binder
327
    - to type each t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
328
329
330
    - to list the labels

   Since we cannot construct an object without breaking the invariant, we define
331
   preobjects of type (A, f, d) such that Obj A = Preobject (A, assoc A, domain A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
332
333
334

   *)

335
  (* We have to axiomatize the type of methods because
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
336
337
338
339
340
341
   Method A B := Obj A -> Obj B has a negative occurence of Obj which blocks
   the recursive definition
   *)

  Parameter Method : type -> type -> Type.

342
  Inductive Preobject {A : type} : forall (d : list string), Type :=
343
  | poempty : Preobject nil
344
345
  | pocons : forall {d} (l : string) (H : l  domain A) (Hn : Istrue (negb (mem l d))),
               Method A (assoc A l H) ->
346
347
               Preobject d ->
               Preobject (cons l d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
348

349
350
  Definition Preobj A d := @Preobject A d.
  Definition Obj (A : type) := Preobj A (domain A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
351

352
353
354
355
356
357
358
  (* An expression of type B is an object of type A <: B coerced to type B. *)
  Inductive Expr (B : type) :=
  | Eobj : Obj B -> Expr B
  | Ecoerce A : Expr A -> (A <: B) -> Expr B.

  (* type, object and prooj of subtyping underlying an ecpression *)
  Fixpoint expr_type {A : type} (e : Expr A) : type.
359
  Proof.
360
361
362
    destruct e as [ o | A' e ].
    - exact A.
    - exact (expr_type A' e).
363
  Defined.
364
365

  Fixpoint expr_obj {A : type} (e : Expr A) : Obj (expr_type e).
366
  Proof.
367
368
369
    destruct e as [ o | A' e ].
    - exact o.
    - exact (expr_obj A' e).
370
  Defined.
371
372

  Fixpoint expr_st {A : type} (e : Expr A) : (expr_type e) <: A.
373
  Proof.
374
375
376
    destruct e as [ o | A' e ].
    - apply subtype_refl.
    - apply (subtype_trans A' (expr_st A' e) s).
377
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
378

379
380
  Definition Obj_to_expr {A} : Obj A -> Expr A := Eobj A.

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
381
  (* End of the axiomatisation of methods: Method A B is equivalent to Obj A -> Obj B. *)
382
383
384
  Parameter Eval_meth : forall {A} {B}, Method A B -> Expr A -> Expr B.
  Parameter Make_meth : forall {A} {B}, (Expr A -> Expr B) -> Method A B.
  Axiom beta : forall {A B} (f : Expr A -> Expr B) a, Eval_meth (Make_meth f) a = f a.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
385

386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449


  (* Destruction principle for non-empty lists *)
  Definition iscons (d : list string) := match d with nil => False | cons _ _ => True end.
  Lemma list_destr d : iscons d -> cons (head d) (tail d) = d.
  Proof.
    intro H.
    destruct d.
    - contradiction.
    - simpl.
      reflexivity.
  Defined.

  (* Destruction principle for preobjects *)
  Definition po_destr {A d} (po : Preobj A d) (Hnnil : iscons d) :
    sigT (fun H2 => sigT (fun Hn => sigT (fun m => sigT (fun tl =>
      po = rew (list_destr d Hnnil) in pocons (head d) H2 Hn m tl)))).
  Proof.
    destruct d as [ | l d'].
    - contradiction.
    - destruct po.
      + contradiction.
      + exists H.
               exists Hn.
               exists m.
               exists po.
               simpl in Hnnil.
               unfold list_destr.
               reflexivity.
  Defined.

  (* By construction, types of objects are duplication-free *)
  (* And domains of preobjects are included in domains of objects *)
  Fixpoint po_sub {A d} (po : Preobj A d) : d  domain A.
  Proof.
    destruct po.
    - intros l p.
      inversion p.
    - intros l2 p.
      apply PCons2 in p.
      destruct p.
      + destruct e.
        assumption.
      + exact (po_sub _ d po l2 p).
  Defined.

  Fixpoint po_df {A d} (po : Preobj A d) : Istrue (duplicate_free d).
  Proof.
    destruct d as [ | l d ].
    - reflexivity.
    - destruct (po_destr po I) as (H2, (Hn, (m, (potl, He)))).
      simpl.
      simpl in Hn.
      rewrite Hn.
      rewrite (po_df A d potl).
      reflexivity.
  Defined.

  Definition obj_in_eq A : Obj A -> forall l, in_eq l (domain A)
    := fun a l => df_in_eq l (domain A) (po_df a).

  Definition obj_po_sub l {A} (a : Obj A) (H : l  domain A) : po_sub a l H = H
    := obj_in_eq A a l _ _.

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
450
451
452
453
454
455
456
457
End objects.

Delimit Scope object_scope with obj.
Delimit Scope method_scope with meth.

Bind Scope method_scope with Method.
Bind Scope object_scope with Preobject.

458
Infix "⊙" := assoc (at level 50).
459
460

Definition Lmethod A := sigT (fun l2 =>
461
                                sigT (fun H => Method A ((A  l2) H))%type).
462

463
464
Definition Make_lmeth l A H m : Lmethod A :=
  (existT _ l (existT _ H m)).
465

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
466
Notation "l = 'ς' ( x !: A ) m" :=
467
  (Make_lmeth l A%ty (mem_pos l (domain A%ty) Istrue_true) (Make_meth (fun x : Expr A%ty => m%obj))) (at level 50) : method_scope.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
468

469
Notation "o ↑ A" := (@Obj_to_expr A%ty o) (at level 100).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
470
471
472

Section semantics.
  (* Selection and update go inside objects so they have to be defined on preobjects first. *)
473

474
  Definition empty_expression : Expr Empty_type := Eobj Empty_type (poempty).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
475

476
477
  Fixpoint preselect l {A d} (po : Preobj A d)
           (H : l  d) {struct H} : Method A (assoc A l (po_sub po l H)).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
478
  Proof.
479
480
481
482
483
    destruct H as [ hd tl ].
    destruct (po_destr po I) as (H2, (Hn, (m, (potl, He)))).
    rewrite He.
    destruct p as [ l' d e | l' d]; simpl.
    - destruct e.
484
      assumption.
485
    - apply (preselect l A d potl p).
486
487
  Defined.

488
489
  Fixpoint preupdate l {A d} (po : Preobj A d)
             (H : l  d) : Method A (assoc A l (po_sub po l H)) -> Preobj A d.
490
  Proof.
491
492
493
494
495
496
497
    destruct H as [ hd tl ].
    destruct (po_destr po I) as (H2, (Hn, (m2, (potl, He)))).
    rewrite He.
    destruct p as [ l' d e | l' d ].
    - destruct e.
      intro m.
      refine (pocons l H2 Hn _ potl).
498
      assumption.
499
500
501
    - intro m.
      apply (pocons l' H2 Hn m2).
      apply (preupdate l A d potl p m).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
502
503
  Defined.

504
  Definition obj_select l {A} (a : Obj A) (H : l  domain A) : Expr (assoc A l H).
505
  Proof.
506
507
    rewrite <- (obj_po_sub l a H).
    exact (Eval_meth (preselect l a H) (Eobj A a)).
508
509
  Defined.

510
  Definition obj_update l {A} (a : Obj A) (H : l  domain A) (m : Method A (assoc A l H)) : Obj A.
511
  Proof.
512
513
    rewrite <- (obj_po_sub l a H) in m.
    exact (preupdate l a H m).
514
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
515

516
  Definition select l {A} (a : Expr A) (H : l  domain A) : Expr (assoc A l H).
517
  Proof.
518
519
    rewrite (assoc_subtype (expr_st a) l H).
    exact (obj_select l (expr_obj a) (domain_subtype (expr_st a) l H)).
520
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
521

522
523
  Definition mem_select l {A} a (H : Istrue (mem l (domain A))) :=
    select l a (mem_pos l (domain A) H).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
524

525
  Definition update l {A} (a : Expr A) (H : l  domain A) : Method A (assoc A l H) -> Expr A.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
526
  Proof.
527
528
529
530
531
532
533
534
535
536
    intro m.
    refine (Ecoerce A (expr_type a) _ (expr_st a)).
    apply Eobj.
    apply (obj_update l (expr_obj a) (domain_subtype (expr_st a) l H)).
    apply Make_meth.
    intro self.
    apply (fun s => Ecoerce A (expr_type a) s (expr_st a)) in self.
    rewrite <- (assoc_subtype (expr_st a) l H).
    exact (Eval_meth m self).
  Defined.
537

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
538
539
End semantics.

540
541
Notation "a # l" := (mem_select l%string a%obj Istrue_true) (at level 50) : object_scope.
Notation "o ## l ⇐ 'ς' ( x !: A ) m" := (@update l%string A%ty o (mem_pos l (domain A%ty) Istrue_true) (Make_meth (fun x : Expr A%ty => m))) (at level 50).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
542

543
544
(* It is often practical to let some methods undefined.
   An easy way to do so is to define an initial object
545
   of each type and define some methods by update. *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
546
Section init.
547

548
  Definition loop_method A l H: Method A ((A  l) H) :=
549
    Make_meth (fun a => @select l A a H).
550

551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
  Fixpoint preinit A d (Hsub : d  domain A) (df : Istrue (duplicate_free d)) {struct d} :
    Preobj A d.
  Proof.
    destruct d as [ | l d ].
    - apply poempty.
    - apply (pocons l (Hsub l (PCons _ (At_head l l d eq_refl)))).
      + simpl in df.
        generalize df.
        case (mem l d); intuition.
      + apply loop_method.
      + apply preinit.
        * intros l2 H2.
          apply Hsub.
          apply PCons.
          apply In_tail.
          apply H2.
        * simpl in df.
          generalize df.
          case (mem l d); intuition.
          simpl in df0.
          inversion df0.
  Defined.
573

574
575
  Definition obj_init A : Istrue (duplicate_free (domain A)) -> Obj A :=
    preinit A (domain A) (fun _ H => H).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
576

577
578
  Definition init A : Istrue (duplicate_free (domain A)) -> Expr A :=
    fun df => Obj_to_expr (obj_init A df).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
579
580
End init.

581
(* Definition of objects without respecting the order of labels given by the type. *)
582
583
Definition lmeth_label A (lm : Lmethod A) :=
  let (l, _) := lm in l.
584
Definition lmeth_H A (lm : Lmethod A) : (lmeth_label A lm)  domain A.
585
586
587
588
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
  assumption.
Defined.
589
Definition lmeth_meth A (lm : Lmethod A) : Method A ((A  (lmeth_label A lm)) (lmeth_H A lm)).
590
591
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
592
  unfold lmeth_H.
593
594
595
  assumption.
Defined.

596
Definition pocons_3 A (lm : Lmethod A)
597
598
           (a : Expr A) :
  Expr A :=
599
  update (lmeth_label A lm) a (lmeth_H A lm) (lmeth_meth A lm).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
600

601
Notation "[ m1 ; .. ; mn ]" := (pocons_3 _ m1%meth (.. (pocons_3 _ mn%meth (init _ Istrue_true)) .. )) : object_scope.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
602

603
Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope.
604
605
606
607

(* Notation "a < b > .# l" := (preselect l%string _ _ _ a%obj _ b%obj) (at level 50) : object_scope. *)
Notation "o .## l ⇐ 'ς' ( x !: A ) m" := (preupdate l%string A%ty _ _ o (Make_meth A%ty _ (fun x => m))) (at level 50).

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
608
609
Section examples.
  (* Encodding of booleans *)
610
611
612
  Definition BoolT A : type :=
    [ "else" : A ; "if" : A ; "then" : A ]%ty.

613
614
  Definition init_bool A : Expr (BoolT A) := init (BoolT A) Istrue_true.

615
  Definition trueT A : Expr (BoolT A) :=
616
    pocons_3 _ ("if" = ς(x !: BoolT A) (x # "then"))%meth (init_bool A).
617
618

  Definition falseT A : Expr (BoolT A) :=
619
    pocons_3 _ ("if" = ς(x !: BoolT A) (x # "else"))%meth (init_bool A).
620

621
622
623
624
  Definition Ifthenelse A b (t e : Expr A) : Expr A :=
    (((b##"then"  ς(x !: BoolT A) t)##"else"  ς(x !: BoolT A) e)#"if")%obj.

  (* Encodding of the simply-pretyped λ-calculus *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
625
626
627
628

  Definition Arrow A B :=
    [ "arg" : A ; "val" : B ]%ty.

629
630
  Definition init_arr A B := init (Arrow A B) Istrue_true.

631
  Definition Lambda A B (f : Expr A -> Expr B) : Expr (Arrow A B) :=
632
    pocons_3 _ ("val" = ς(x !: Arrow A B) (f (x#"arg")))%meth (init_arr A B).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
633

634
635
  Definition App A B (f : Expr (Arrow A B)) (a : Expr A) : Expr B :=
    ((f##"arg"  ς(x !: Arrow A B) a)#"val")%obj.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
636
637
End examples.

638
639
640
641
Notation "'ifT' b 'then' t 'else' e" := (Ifthenelse _ b t e) (at level 50) : object_scope.
Infix "→" := Arrow (at level 50).
Notation "'λ' ( x !: A ) b" := (Lambda A _ (fun x : Expr A => b)) (at level 50).
Infix "@" := (App _ _) (at level 50).