fact: Fixpoint compile_bexp (b: bexp) (d1: Z) (d0: Z) : code := match b with | TRUE => if d1 =? 0 then nil else Ibranch d1 :: nil | FALSE => if d0 =? 0 then nil else Ibranch d0 :: nil | EQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ibeq d1 d0 :: nil | LESSEQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ible d1 d0 :: nil | NOT b1 => compile_bexp b1 d0 d1 | AND b1 b2 => let code2 := compile_bexp b2 d1 d0 in let code1 := compile_bexp b1 0 (codelen code2 + d0) in code1 ++ code2 end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)