type string = String type bool = True | False let gen_name = String type expr = | Const of int | Add of expr * expr | Mul of expr * expr type lexpr = | Var of string | LConst of int | LAdd of lexpr * lexpr | LMul of lexpr * lexpr | Let of string * lexpr * lexpr let rec expr_to_lexpr : expr -> lexpr = fun (e : expr) => match e with | Const(n) => LConst(n) | Add(e1,e2) => LAdd(expr_to_lexpr e1, expr_to_lexpr e2) | Mul(e1,e2) => LMul(expr_to_lexpr e1, expr_to_lexpr e2) end let ornament expr_to_lexpr : expr -> lexpr let rec mul_to_add : lexpr -> lexpr = fun (e : lexpr) => match e with | Var(x) => Var(x) | LAdd(a,b) => LAdd(a,b) | LConst(i) => LConst(i) | Let(a,b,c) => Let(a,b,c) | LMul(x,y) => match x with | LConst(i) => let n = gen_name in if eq i 2 then Let(n, y, LAdd(Var(n), Var(n))) else LMul(x,y) | LAdd(_,_) => LMul(x,y) | LMul(_,_) => LMul(x,y) | Var(_) => LMul(x,y) | Let(_,_,_) => LMul(x,y) end end let ornament mul_to_add' from mul_to_add with {expr_to_lexpr} -> {expr_to_lexpr}