source: Papers/polymorphic-variants-2012/testb.ma @ 2549

Last change on this file since 2549 was 2514, checked in by sacerdot, 7 years ago

All .ma files committed: some of them are just in-progress.

File size: 1.7 KB
Line 
1include "variants.ma".
2
3coercion sub_expr2 : ∀l:list tag_. Type[0] → Type[0]
4 ≝ sub_expr on _l: list tag_ to Type[0] → Type[0].
5
6definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝
7 λE,f,e.
8  match e return λe. is_in … [plus] e → nat with
9  [ Plus x y ⇒ λH. f x + f y
10  | _ ⇒ λH:False. ?
11  ] (se_el_in ?? e).
12elim H qed.
13
14definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝
15 λE,f,e.
16  match e return λe. is_in … [mul] e → nat with
17  [ Mul x y ⇒ λH. f x * f y
18  | _ ⇒ λH:False. ?
19  ] (se_el_in ?? e).
20elim H qed.
21
22definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝
23 λE,f,e.
24  match e return λe. is_in … [plus;mul] e → nat with
25  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
26  | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
27  | _ ⇒ λH:False. ?
28  ] (se_el_in ?? e).
29[2,3: % | elim H]
30qed.
31
32definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝
33 λE,f,e.
34  match e return λe. is_in … [plus;mul;num] e → nat with
35  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
36  | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
37  | Num n ⇒ λH. n
38  ] (se_el_in ?? e).
39% qed.
40
41(*CSC: not accepted :-(
42inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const.
43*)
44
45inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.
46
47coercion K.
48
49let rec eval_final_expr e on e : nat ≝
50 match e with
51 [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e'].
52cases e' try #x try #y %
53qed.
54
55example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
56% qed.
Note: See TracBrowser for help on using the repository browser.