source: Papers/polymorphic-variants-2012/test.ma @ 2402

Last change on this file since 2402 was 2402, checked in by sacerdot, 8 years ago

Progress on parametric types.

File size: 1.5 KB
Line 
1include "basics/lists/listb.ma".
2
3definition bool_to_Prop : bool → Prop ≝
4 λb. match b with [ true ⇒ True | false ⇒ False ].
5
6inductive expr (E: Type[0]) : Type[0] ≝
7   Num : nat -> expr E
8 | Plus : expr E -> expr E -> expr E
9 | Mul : expr E -> expr E -> expr E.
10
11inductive tag : Type[0] := num : tag | plus : tag | mul : tag.
12
13definition eq_tag : tag -> tag -> bool :=
14 λt1,t2.
15  match t1 with
16  [ num => match t2 with [num => true | _ => false]
17  | plus => match t2 with [plus => true | _ => false]
18  | mul => match t2 with [mul => true | _ => false]].
19
20definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
21 ** normalize /2/ % #abs destruct
22qed.
23
24definition tag_of_expr : ∀E:Type[0]. expr E -> tag :=
25 λE,e.
26   match e with
27   [ Num _ => num
28   | Plus _ _ => plus
29   | Mul _ _ => mul ].
30
31(*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝
32 λE,t,e. eq_tag t (tag_of_expr \ldots e).*)
33
34definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
35 λE,l,e. memb Tag (tag_of_expr ? e) l.
36
37record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝
38{
39  se_el :> expr E;
40  se_el_in: bool_to_Prop (is_in … l se_el)
41}.
42
43coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
44 ≝ sub_expr on _l: list tag to Type[0] → Type[0].
45
46coercion mk_sub_expr :
47 ∀l:list tag.∀E.∀e:expr E.
48  ∀p:bool_to_Prop (is_in ? l e).sub_expr l E
49 ≝ mk_sub_expr on e:expr E to sub_expr ? ?.
50
51(**************************************)
52
53definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.
Note: See TracBrowser for help on using the repository browser.