coq_obj.v 18.8 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
25
26
27
28
29
30
31
32
33
34
35
36
Lemma Istrue_eq b : b = true -> Istrue b.
Proof.
  intro e.
  rewrite e.
  exact Istrue_true.
Defined.

Lemma Istrue_eq_inv b : Istrue b -> b = true.
Proof.
  intro e.
  inversion e.
  reflexivity.
Defined.

37
38
Definition isProp A := forall x y : A, x = y.

39
40
41
42
43
44
45
46
47
Module String_dec.
  Definition U := string.
  Definition eq_dec := string_dec.
End String_dec.

Module String_UIP := Eqdep_dec.DecidableEqDep (String_dec).

Section domains.

48
49
50
51
52
  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).
53

54
55
56
57
58
59
60
61
  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 :=
62
    match d with
63
64
      | nil => ""%string
      | cons l _ => l
65
66
    end.

67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
  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 :=
89
    match d with
90
      | nil => false
91
      | cons l2 d =>
92
        if (string_dec l l2) then true else mem l d
93
94
    end.

95
  Fixpoint mem_pos l d : Istrue (mem l d) -> Pos2 l d.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
96
  Proof.
97
    destruct d as [ | l2 d ].
98
99
    simpl.
    - intro H; inversion H.
100
    - simpl.
101
102
103
104
105
106
107
108
109
110
111
      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.
112
113
  Defined.

114
  Lemma Pos_tail l l2 d : l <> l2 -> Position l l2 d -> Pos2 l d.
115
  Proof.
116
117
118
119
120
    intros n p.
    destruct p.
    - destruct (n e).
    - assumption.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
121

122
  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
123
  Proof.
124
    destruct d as [ | l2 d ].
125
126
    simpl.
    - intros _ H; inversion H.
127
    - simpl.
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
      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).
145

146
  Fixpoint df_in_eq l d {struct d} : Istrue (duplicate_free d) -> in_eq l d.
147
  Proof.
148
149
150
    destruct d as [ | l2 d].
    - intros _ H1 H2.
      inversion H1.
151
    - simpl.
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
      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.
177

178
179
End domains.

180
Infix "∈" := (Pos2) (at level 60).
181

182
Definition subset d1 d2 : Type := forall l, (l  d1) -> (l  d2).
183

184
Infix "⊂" := subset (at level 60).
185

186
Section types.
187
188
  (* Object types are records of types, we define them as association lists *)

189
190
191
  Inductive type :=
  | Empty_type
  | Cons_type : string -> type -> type -> type.
192

193
End types.
194

195
Section assoc.
196

197
  Fixpoint domain A :=
198
    match A with
199
200
      | Empty_type => nil
      | Cons_type l _ C => cons l (domain C)
201
202
    end.

203
  Fixpoint assoc A l (H : l  domain A) : type.
204
  Proof.
205
206
207
208
209
210
211
212
213
    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.
214

215
End assoc.
216
217

(* Scope of object types *)
218
Bind Scope obj_type_scope with type.
219
220
221
222
Delimit Scope obj_type_scope with ty.
(* Scope of object type fields (pairs of strings and types) *)
Delimit Scope type_field_scope with tf.

223
224
Section subtyping.

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

227
  Fixpoint type_dec (A B : type) : {A = B} + {A <> B}.
228
229
230
  Proof.
    decide equality.
    apply string_dec.
231
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
232

233
  (* Definition of the subtyping relation: A <: B if B is a subset of A. *)
234
  Fixpoint Subtype A B {struct B} : Type :=
235
    match B with
236
237
238
      | 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
239
    end.
240
241
242

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

243
244
245
  Lemma subtype_tail {A} {B} l C :
    A <: B ->
         Cons_type l C A <: B.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
246
  Proof.
247
248
249
250
251
252
253
254
255
    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
256

257
  Lemma subtype_refl A : A <: A.
258
  Proof.
259
    induction A as [ | l A HA B HB ].
260
261
    - intuition.
    - simpl.
262
      exists (PCons _ (At_head l l (domain B) eq_refl)).
263
      simpl.
264
265
266
267
268
      split.
      + reflexivity.
      + apply subtype_tail.
        assumption.
  Defined.
269

270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
  Fixpoint subtype_dec (A B : type) : bool.
  Proof.
    destruct B as [ | l B1 B2 ].
    - exact true.
    - case_eq (mem l (domain A)).
      + intro H.
        apply Istrue_eq in H.
        apply mem_pos in H.
        case (type_dec (assoc A l H) B1); intro.
        * exact (subtype_dec A B2).
        * exact false.
      + intro; exact false.
  Defined.

  Definition subtype_dec_correct A B : Istrue (subtype_dec A B) -> A <: B.
  Proof.
    admit.
  Qed.

289
290
  Fixpoint domain_subtype {A} {B} :
    A <: B -> domain B  domain A.
291
  Proof.
292
293
294
295
296
297
298
299
300
301
    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.
302
303
  Defined.

304
305
  Fixpoint assoc_subtype {A} {B} (st : A <: B) l H :
    assoc B l H = assoc A l (domain_subtype st l H).
306
  Proof.
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
    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).
325
326
  Defined.

327
  Theorem subtype_trans {A} B {C} : A <: B -> B <: C -> A <: C.
328
  Proof.
329
    induction C as [ | lC C1 C2].
330
    - trivial.
331
332
333
334
335
336
    - intros stAB (HdBC, (HeqBC, HstBC)).
      exists (domain_subtype stAB lC HdBC).
      split.
      + rewrite <- (assoc_subtype stAB lC HdBC).
        assumption.
      + intuition.
337
338
339
  Qed.
End subtyping.

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

342
343
Definition insert (lA : string * type) (A2 : type) :=
  let (l, A) := lA in Cons_type l A A2.
344

345
      (* Notations for object pretypes:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
346
347
348
349
   [ "l₁" : A ; "l₂" : A ;  ; "lₙ" : A ]
 *)
Notation "l : A" := (l%string, A) (at level 50) : type_field_scope.
Notation "[ x1 ; .. ; xn ]" :=
350
  (insert x1%tf .. (insert xn%tf Empty_type) ..) : obj_type_scope.
351
Notation "l : A :: B" := (Cons_type l A B) (at level 100) : type_field_scope.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
352
353
354

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

358
   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
359
    - in each ς binder
360
    - to type each t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
361
362
363
    - to list the labels

   Since we cannot construct an object without breaking the invariant, we define
364
   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
365
366
367

   *)

368
  (* We have to axiomatize the type of methods because
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
369
370
371
372
373
374
   Method A B := Obj A -> Obj B has a negative occurence of Obj which blocks
   the recursive definition
   *)

  Parameter Method : type -> type -> Type.

375
  Inductive Preobject {A : type} : forall (d : list string), Type :=
376
  | poempty : Preobject nil
377
378
  | pocons : forall {d} (l : string) (H : l  domain A) (Hn : Istrue (negb (mem l d))),
               Method A (assoc A l H) ->
379
380
               Preobject d ->
               Preobject (cons l d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
381

382
383
  Definition Preobj A d := @Preobject A d.
  Definition Obj (A : type) := Preobj A (domain A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
384

385
386
387
388
389
390
391
  (* 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.
392
  Proof.
393
394
395
    destruct e as [ o | A' e ].
    - exact A.
    - exact (expr_type A' e).
396
  Defined.
397
398

  Fixpoint expr_obj {A : type} (e : Expr A) : Obj (expr_type e).
399
  Proof.
400
401
402
    destruct e as [ o | A' e ].
    - exact o.
    - exact (expr_obj A' e).
403
  Defined.
404
405

  Fixpoint expr_st {A : type} (e : Expr A) : (expr_type e) <: A.
406
  Proof.
407
408
409
    destruct e as [ o | A' e ].
    - apply subtype_refl.
    - apply (subtype_trans A' (expr_st A' e) s).
410
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
411

412
413
  Definition Obj_to_expr {A} : Obj A -> Expr A := Eobj A.

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
414
  (* End of the axiomatisation of methods: Method A B is equivalent to Obj A -> Obj B. *)
415
416
417
  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
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
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482


  (* 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
483
484
485
486
487
488
489
490
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.

491
Infix "⊙" := assoc (at level 50).
492
493

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

496
497
Definition Make_lmeth l A H m : Lmethod A :=
  (existT _ l (existT _ H m)).
498

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
499
Notation "l = 'ς' ( x !: A ) m" :=
500
  (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
501

502
Notation "o ↑ A" := (@Obj_to_expr A%ty o) (at level 100).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
503
504
505

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

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

509
510
  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
511
  Proof.
512
513
514
515
516
    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.
517
      assumption.
518
    - apply (preselect l A d potl p).
519
520
  Defined.

521
522
  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.
523
  Proof.
524
525
526
527
528
529
530
    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).
531
      assumption.
532
533
534
    - 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
535
536
  Defined.

537
  Definition obj_select l {A} (a : Obj A) (H : l  domain A) : Expr (assoc A l H).
538
  Proof.
539
540
    rewrite <- (obj_po_sub l a H).
    exact (Eval_meth (preselect l a H) (Eobj A a)).
541
542
  Defined.

543
  Definition obj_update l {A} (a : Obj A) (H : l  domain A) (m : Method A (assoc A l H)) : Obj A.
544
  Proof.
545
546
    rewrite <- (obj_po_sub l a H) in m.
    exact (preupdate l a H m).
547
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
548

549
  Definition select l {A} (a : Expr A) (H : l  domain A) : Expr (assoc A l H).
550
  Proof.
551
552
    rewrite (assoc_subtype (expr_st a) l H).
    exact (obj_select l (expr_obj a) (domain_subtype (expr_st a) l H)).
553
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
554

555
556
  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
557

558
  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
559
  Proof.
560
561
562
563
564
565
566
567
568
569
    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.
570

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
571
572
End semantics.

573
574
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
575

576
577
(* It is often practical to let some methods undefined.
   An easy way to do so is to define an initial object
578
   of each type and define some methods by update. *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
579
Section init.
580

581
  Definition loop_method A l H: Method A ((A  l) H) :=
582
    Make_meth (fun a => @select l A a H).
583

584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
  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.
606

607
608
  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
609

610
611
  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
612
613
End init.

614
(* Definition of objects without respecting the order of labels given by the type. *)
615
616
Definition lmeth_label A (lm : Lmethod A) :=
  let (l, _) := lm in l.
617
Definition lmeth_H A (lm : Lmethod A) : (lmeth_label A lm)  domain A.
618
619
620
621
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
  assumption.
Defined.
622
Definition lmeth_meth A (lm : Lmethod A) : Method A ((A  (lmeth_label A lm)) (lmeth_H A lm)).
623
624
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
625
  unfold lmeth_H.
626
627
628
  assumption.
Defined.

629
Definition pocons_3 {A} (lm : Lmethod A) (a : Expr A) : Expr A :=
630
  update (lmeth_label A lm) a (lmeth_H A lm) (lmeth_meth A lm).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
631

632
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
633

634
Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope.
635
636
637
638

(* 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
639
640
Section examples.
  (* Encodding of booleans *)
641
642
643
  Definition BoolT A : type :=
    [ "else" : A ; "if" : A ; "then" : A ]%ty.

644
645
  Definition init_bool A : Expr (BoolT A) := init (BoolT A) Istrue_true.

646
  Definition trueT A : Expr (BoolT A) :=
647
    pocons_3 ("if" = ς(x !: BoolT A) (x # "then"))%meth (init_bool A).
648
649

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

652
653
654
655
  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
656
657
658
659

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

660
661
  Definition init_arr A B := init (Arrow A B) Istrue_true.

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

665
666
  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
667
668
End examples.

669
670
671
672
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).