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.