include "variants.ma". coercion sub_expr2 : ∀l:list tag_. Type[0] → Type[0] ≝ sub_expr on _l: list tag_ to Type[0] → Type[0]. definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ λE,f,e. match e return λe. is_in … [plus] e → nat with [ Plus x y ⇒ λH. f x + f y | _ ⇒ λH:False. ? ] (se_el_in ?? e). elim H qed. definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ λE,f,e. match e return λe. is_in … [mul] e → nat with [ Mul x y ⇒ λH. f x * f y | _ ⇒ λH:False. ? ] (se_el_in ?? e). elim H qed. definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ λE,f,e. match e return λe. is_in … [plus;mul] e → nat with [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) | _ ⇒ λH:False. ? ] (se_el_in ?? e). [2,3: % | elim H] qed. definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ λE,f,e. match e return λe. is_in … [plus;mul;num] e → nat with [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) | Num n ⇒ λH. n ] (se_el_in ?? e). % qed. (*CSC: not accepted :-( inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. *) inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr. coercion K. let rec eval_final_expr e on e : nat ≝ match e with [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e']. cases e' try #x try #y % qed. example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6. % qed.