Commit 2f4a741c authored by Heiko Becker's avatar Heiko Becker
Browse files

Initial commit to public version of Icing

parent 60674ca1
*Theory*
*.dat
*.uo
*.ui
[submodule "FloVer"]
path = FloVer
url = git-rts@gitlab.mpi-sws.org:AVA/FloVer.git
This diff is collapsed.
(**
This file defines the CakeML connection function "toCML" from section 4.4
The correctness proofs from section 5.4 are at the end.
Theorem "toCML_equiv" is Theorem 5.5 in the paper
**)
open patternTheory valueTreesTheory SyntaxTheory
SemanticsTheory CompilerTacticsLib CompilerProofsTheory;
open astTheory fpSemTheory evaluateTheory semanticPrimitivesTheory
namespaceTheory namespacePropsTheory terminationTheory miscTheory;
open machine_ieeeTheory binary_ieeeTheory;
open flourPreamble;
val _ = new_theory "CakeMLconn";
open ListProgTheory ml_translatorLib ml_progLib;
val _ = translation_extends "ListProg";
Globals.max_print_depth := (~1);
(* val _ = translation_extends "basisProg"; *)
val state = get_env (ml_translatorLib.get_ml_prog_state());
val ffi_state = get_state (ml_translatorLib.get_ml_prog_state());
(* TODO: To HOL4? *)
val float_eq_not_id_nan = store_thm (
"float_eq_not_id_nan",
``!x. ~ float_equal x x <=> float_is_nan x``,
rpt strip_tac \\ fs[float_equal_def, float_compare_def, float_is_nan_def]
\\ Cases_on `float_value x` \\ fs[]);
val fp64_eq_not_id_nan = store_thm (
"fp64_eq_not_id_nan",
``!x. fp64_equal x x = F <=> fp64_isNan x``,
rpt strip_tac \\ fs[fp64_equal_def, fp64_isNan_def]
\\ irule float_eq_not_id_nan \\ fs[]);
(* Operator translations *)
val toUop_def = Define `
toUop (valueTrees$Neg) = FP_Neg /\
toUop (valueTrees$Sqrt) = FP_Sqrt`;
val toBop_def = Define `
toBop (valueTrees$Plus) = fpSem$FP_Add /\
toBop (valueTrees$Minus) = FP_Sub /\
toBop (valueTrees$Mult) = FP_Mul /\
toBop (valueTrees$Div) = FP_Div `;
val toTop_def = Define `
toTop (Fma) = FP_Fma `;
val toCmp_def = Define `
toCmp (valueTrees$Less) = FP_Less /\
toCmp (valueTrees$Leq) = FP_LessEqual /\
toCmp (valueTrees$Eq) = FP_Equal `;
(* Expression translations for true, false, nil and cons *)
val true_exp_def = Define `
true_exp = ast$App (Opb Leq) [ast$Lit (IntLit 0); ast$Lit (IntLit 0)]`;
val false_exp_def = Define `
false_exp = ast$App (Opb Leq) [ast$Lit (IntLit 1); ast$Lit (IntLit 0)]`;
val nil_exp_def = Define
`nil_exp = ast$Con (SOME (Short"[]")) []`;
val cons_exp_def = Define `
cons_exp e1 el = ast$Con (SOME (Short "::")) [e1; el]`;
(* EVAL ``evaluate ^ffi_state ^state [cons_exp (Lit (Word64 0w)) nil_exp]`` *)
val map_name_def = Define `
map_name = Var (Long "List" (Short "map"))`;
(* EVAL ``nsLookup (^state).v (Long"List"(Short"map"))`` *)
(*
REWRITE_RULE [ml_progTheory.eval_rel_def, ml_translatorTheory.Eval_def]
(hol2deep ``(MAP:(num -> num) -> num list -> num list) (\x.x) []``);
*)
(* EVAL_RULE
(ONCE_REWRITE_RULE [map_1_v_def]
(EVAL
``evaluate (^ffi_state with clock:=100) ^state
[ast$App Opapp [ast$App Opapp [map_name; Fun "x" (ast$Var (Short "x"))]; nil_exp]]``)) *)
val fold_name_def = Define `
fold_name = Var (Long "List" (Short "foldr"))`;
(* EVAL ``nsLookup (^state).v (Long"List"(Short"foldr"))`` *)
val ith_name_def = Define `
ith_name = Var (Long "List" (Short "nth"))`;
val vTree2CML_def = Define `
vTree2CML (Wconst w) = (ast$Lit (Word64 w)) /\
vTree2CML (UnVal uop e) =
(ast$App (FP_uop (toUop uop)) [vTree2CML e]) /\
vTree2CML (BinVal b e1 e2) =
(ast$App (FP_bop (toBop b)) [vTree2CML e1; vTree2CML e2]) /\
vTree2CML (TerVal top e1 e2 e3) =
(ast$App (FP_top (toTop top)) [vTree2CML e1; vTree2CML e2; vTree2CML e3]) /\
vTree2CML (Scope sc e) = vTree2CML e`;
val valTrees2CML_def = Define `
valTrees2CML [] = nil_exp /\
valTrees2CML (v::vl) = cons_exp (vTree2CML v) (valTrees2CML vl)`;
val expToCML_def = Define `
expToCML (Var v) = (ast$Var (mk_id [] v)) /\
expToCML (Wconst w) = (ast$Lit (Word64 w)) /\
expToCML (Ith n e) = (ast$App Opapp [ast$App Opapp [ith_name; expToCML e]; ast$Lit (IntLit (&n))]) /\
expToCML (List []) = nil_exp /\
expToCML (List (e::el)) = cons_exp (expToCML e) (expToCML (List el)) /\
expToCML (Unop uop e) =
(ast$App (FP_uop (toUop uop)) [expToCML e]) /\
expToCML (Binop b e1 e2) =
(ast$App (FP_bop (toBop b)) [expToCML e1; expToCML e2]) /\
expToCML (Terop top e1 e2 e3) =
(ast$App (FP_top (toTop top)) [expToCML e1; expToCML e2; expToCML e3]) /\
expToCML (Syntax$Let x e1 e2) =
(ast$Let (SOME x) (expToCML e1) (expToCML e2)) /\
expToCML (Cond c e1 e2) =
ast$If (cexpToCML c)
(expToCML e1)
(expToCML e2) /\
expToCML (Map x f e) =
ast$App Opapp
[ast$App Opapp [map_name; (Fun x (expToCML f))];
expToCML e] /\
expToCML (Fold (x,y) f i e) =
ast$App Opapp
[ast$App Opapp
[ast$App Opapp
[fold_name; (Fun y (Fun x (expToCML f)))];
expToCML i];
(expToCML e)] /\
expToCML (Mapvl x f vl) =
ast$App Opapp
[ast$App (Opapp)
[map_name; (Fun x (expToCML f))];
(valTrees2CML vl)] /\
expToCML (Foldvl (x,y) f i vl) =
ast$App Opapp
[ast$App Opapp
[ast$App Opapp
[fold_name; (Fun y (Fun x (expToCML f)))];
expToCML i];
(valTrees2CML vl)] /\
expToCML (Scope sc e) = expToCML e
/\
cexpToCML (Bconst b) = (if b then true_exp else false_exp) /\
cexpToCML (Pred NaN e) =
(ast$If (ast$App (FP_cmp FP_Equal) [expToCML e; expToCML e]) (false_exp) (true_exp)) /\
cexpToCML (Cmp cmp e1 e2) =
(ast$App (FP_cmp (toCmp cmp) ) [expToCML e1; expToCML e2]) /\
cexpToCML (Cscope sc c) = cexpToCML c`;
val toFlourVal_def = Define `
toFlourVal (Litv l) =
(case l of
| Word64 w => SOME (Val (valueTrees$Wconst w))
| _ => NONE) /\
toFlourVal (Conv (SOME ts) vl) =
(case ts, vl of
| (TypeStamp s 0), [] =>
if (s = "True")
then SOME (Cval (valueTrees$Bconst T))
else if (s = "False")
then SOME (Cval (valueTrees$Bconst F))
else NONE
| (TypeStamp "[]" 1), [] => SOME (Lval [])
| (TypeStamp "::" 1), vl =>
(case vl of
| [] => NONE
| Litv (Word64 w)::[Conv ts vl] =>
(case toFlourVal (Conv ts vl) of
|SOME (Lval vres) => SOME (Lval ((valueTrees$Wconst w)::vres))
| _ => NONE)
| _ => NONE)
| _, _ => NONE) /\
toFlourVal _ = NONE`;
val fromFlourVal_def = Define `
fromFlourVal (Val v) = Litv (Word64 (tree2IEEE v)) /\
fromFlourVal (Cval b) = Boolv (cTree2IEEE b) /\
fromFlourVal (Lval []) = Conv (SOME (TypeStamp "[]" 1)) [] /\
fromFlourVal (Lval (v::vl)) =
Conv (SOME (TypeStamp "::" 1))
((fromFlourVal (Val v))::[fromFlourVal (Lval vl)])`;
val tofML_env_def = Define `
tofML_env (env:v sem_env) =
\x. (case nsLookup env.v (mk_id [] x) of
| NONE => NONE
| SOME v => toFlourVal v)`;
val isFlourVal_def = Define `
isFlourVal (Litv (Word64 w)) = T /\
isFlourVal (Conv ts vl) =
(case vl of
| [] => ts = SOME (TypeStamp "[]" 1)
| v1::vl =>
LENGTH (v1::vl) = 2 /\
ts = SOME (TypeStamp "::" 1) /\
(case v1, vl of
| Litv (Word64 w), [Conv ts vl] => isFlourVal (Conv ts vl)
| _, _ => F)) /\
isFlourVal _ = F`;
val expToCML_env_def = Define `
expToCML_env E (Wconst w):(tvarN, tvarN, v) namespace = nsEmpty /\
expToCML_env E (Syntax$Var w) =
(case E w of
|SOME v => nsBind w (fromFlourVal v) nsEmpty
|NONE => nsEmpty) /\
expToCML_env E (Ith _ e) = expToCML_env E e /\
expToCML_env E (List []) = nsEmpty /\
expToCML_env E (List (e::el)) = nsAppend (expToCML_env E e) (expToCML_env E (List el)) /\
expToCML_env E (Unop _ e) = expToCML_env E e /\
expToCML_env E (Binop b e1 e2) = nsAppend (expToCML_env E e1) (expToCML_env E e2) /\
expToCML_env E (Terop _ e1 e2 e3) =
nsAppend (nsAppend (expToCML_env E e1) (expToCML_env E e2)) (expToCML_env E e3) /\
expToCML_env E (Let x e1 e2) = nsAppend (expToCML_env E e1) (expToCML_env E e2) /\
expToCML_env E (Cond c e1 e2) =
(nsAppend (nsAppend (cexpToCML_env E c) (expToCML_env E e1)) (expToCML_env E e2)) /\
expToCML_env E (Map x f e) =
(nsAppend (expToCML_env E f) (expToCML_env E e)) /\
expToCML_env E (Mapvl x f vl) = expToCML_env E f /\
expToCML_env E (Fold p f s e) =
(nsAppend (nsAppend (expToCML_env E f) (expToCML_env E s)) (expToCML_env E e)) /\
expToCML_env E (Foldvl p f s vl) =
(nsAppend (expToCML_env E f) (expToCML_env E s)) /\
expToCML_env E (Scope _ e) = expToCML_env E e
/\
cexpToCML_env E (Syntax$Bconst b) = nsEmpty /\
cexpToCML_env E (Pred p e) = expToCML_env E e /\
cexpToCML_env E (Cmp _ e1 e2) = nsAppend (expToCML_env E e1) (expToCML_env E e2) /\
cexpToCML_env E (Cscope _ ce) = cexpToCML_env E ce`;
val _ = export_theory();
This diff is collapsed.
(**
This file contains the definitions of
bottomUp (here:bottomUpApp), optimizeGreedy (here:optimizeGreedy),
optimizeCond (here:optimizeCond), and compileIEEE754 (here:compileIEEE754)
defined in section 4 of the paper
**)
open patternTheory valueTreesTheory SemanticsTheory rewriteRulesTheory;
open machine_ieeeTheory binary_ieeeLib optionTheory;
open flourPreamble;
val _ = new_theory "Compiler";
(**
fastML compiler - Version 1
**)
val bottomUpExp_def = tDefine
"bottomUpExp"
`bottomUpExp (f:expr -> expr) (g:cexpr->cexpr) (Wconst w) = f (Wconst w) /\
bottomUpExp f g (Var v) = f (Var v) /\
bottomUpExp f g (List l) = f (List (bottomUpExpL f g l)) /\
bottomUpExp f g (Ith n e) = f (Ith n (bottomUpExp f g e)) /\
bottomUpExp f g (Unop uop e) = f (Unop uop (bottomUpExp f g e)) /\
bottomUpExp f g (Binop bop e1 e2) =
f (Binop bop (bottomUpExp f g e1) (bottomUpExp f g e2)) /\
bottomUpExp f g (Terop top e1 e2 e3) =
f (Terop top (bottomUpExp f g e1) (bottomUpExp f g e2) (bottomUpExp f g e3)) /\
bottomUpExp f g (Let x e1 e2) =
f (Let x (bottomUpExp f g e1) (bottomUpExp f g e2)) /\
bottomUpExp f g (Cond c e1 e2) =
f (Cond (bottomUpCexp f g c) (bottomUpExp f g e1) (bottomUpExp f g e2)) /\
bottomUpExp f g (Scope Opt e) = f (Scope Opt (bottomUpExp f g e)) /\
bottomUpExp f g (Map x h e) = f (Map x (bottomUpExp f g h) (bottomUpExp f g e)) /\
bottomUpExp f g (Mapvl x h vl) = f (Mapvl x (bottomUpExp f g h) vl) /\
bottomUpExp f g (Fold p h i e) =
f (Fold p (bottomUpExp f g h) (bottomUpExp f g i) (bottomUpExp f g e)) /\
bottomUpExp f g (Foldvl p h i vl) =
f (Foldvl p (bottomUpExp f g h) (bottomUpExp f g i) vl)
/\
bottomUpCexp f g (Bconst b) = g (Bconst b) /\
bottomUpCexp f g (Pred p e) = g (Pred p (bottomUpExp f g e)) /\
bottomUpCexp f g (Cmp cmp e1 e2) =
g (Cmp cmp (bottomUpExp f g e1) (bottomUpExp f g e2)) /\
bottomUpCexp f g (Cscope Opt ce) = g (Cscope Opt (bottomUpCexp f g ce))
/\
bottomUpExpL f g [] = [] /\
bottomUpExpL f g (e::el) = (bottomUpExp f g e) :: (bottomUpExpL f g el)`
(WF_REL_TAC
`measure
(\x.
case x of
|INL (_, _, x) => expr_size x
|INR (INL (_, _, x)) => cexpr_size x
| INR (INR (_,_,x)) => expr1_size x)`
\\ fs[]);
val bottomUpLoge_def = tDefine
"bottomUpLoge"
`bottomUpLoge (f:expr -> expr#'a list) (g:cexpr->cexpr#'b list) (Wconst w)
:expr#'a list # 'b list=
(let (res, log) = f (Wconst w) in
(res, log ,[])) /\
bottomUpLoge f g (Var v) =
(let (res, log) = f (Var v) in
(res, log, [])) /\
bottomUpLoge f g (List el) =
(let
(res, logA, logB) = bottomUpLogel f g el;
(res_l, logL) = f (List res);
in
(res_l, logL ++ logA, logB)) /\
bottomUpLoge f g (Ith n e) =
(let
(res, logA, logB) = bottomUpLoge f g e;
(res_i, logiA) = f (Ith n res)
in
(res_i, logiA ++ logA, logB)) /\
bottomUpLoge f g (Unop uop e) =
(let
(res_e, logA, logB) = bottomUpLoge f g e;
(res_u, logU) = f (Unop uop res_e);
in
(res_u, logU ++ logA, logB)) /\
bottomUpLoge f g (Binop bop e1 e2) =
(let
(res_e1, logA1, logB1) = bottomUpLoge f g e1;
(res_e2, logA2, logB2) = bottomUpLoge f g e2;
(res_b, logB) = f (Binop bop res_e1 res_e2);
in
(res_b, logB++ (logA1 ++ logA2), logB1 ++ logB2)) /\
bottomUpLoge f g (Terop top e1 e2 e3) =
(let
(res_e1, logA1, logB1) = bottomUpLoge f g e1;
(res_e2, logA2, logB2) = bottomUpLoge f g e2;
(res_e3, logA3, logB3) = bottomUpLoge f g e3;
(res_t, logT) = f (Terop top res_e1 res_e2 res_e3);
in
(res_t, logT++ (logA1 ++ logA2 ++ logA3), logB1 ++ logB2 ++ logB3)) /\
bottomUpLoge f g (Let x e1 e2) =
(let
(res_e1, logA1, logB1) = bottomUpLoge f g e1;
(res_e2, logA2, logB2) = bottomUpLoge f g e2;
(res_b, logB) = f (Let x res_e1 res_e2);
in
(res_b, logB++ (logA1 ++ logA2), logB1 ++ logB2)) /\
bottomUpLoge f g (Cond c e1 e2) =
(let
(res_c, logAc, logBc) = bottomUpLogc f g c;
(res_e1, logA1, logB1) = bottomUpLoge f g e1;
(res_e2, logA2, logB2) = bottomUpLoge f g e2;
(res_t, logT) = f (Cond c res_e1 res_e2);
in
(res_t, logT++(logAc ++ logA1 ++ logA2), APPEND logBc (APPEND logB1 logB2))) /\
bottomUpLoge f g (Scope Opt e) =
(let
(res_e, logA, logB) = bottomUpLoge f g e;
(res_s, logS) = f (Scope Opt res_e)
in
(res_s, logS ++ logA, logB)) /\
bottomUpLoge f g (Map x h e) =
(let
(res_h, log_hA, log_hB) = bottomUpLoge f g h;
(res_e, log_eA, log_eB) = bottomUpLoge f g e;
(res_m, log_mA) = f (Map x res_h res_e);
in
(res_m, (log_mA ++ log_eA ++ log_hA), log_eB ++ log_hB)) /\
bottomUpLoge f g (Mapvl x h vl) =
(let
(res_h, log_hA, log_hB) = bottomUpLoge f g h;
(res_m, log_mA) = f (Mapvl x res_h vl);
in
(res_m, log_mA ++ log_hA, log_hB)) /\
bottomUpLoge f g (Fold x h i e) =
(let
(res_h, log_hA, log_hB) = bottomUpLoge f g h;
(res_i, log_iA, log_iB) = bottomUpLoge f g i;
(res_e, log_eA, log_eB) = bottomUpLoge f g e;
(res_m, log_mA) = f (Fold x res_h res_i res_e);
in
(res_m, log_mA ++ log_eA ++ log_iA ++ log_hA,
log_eB ++ log_iB ++ log_hB)) /\
bottomUpLoge f g (Foldvl x h i vl) =
(let
(res_h, log_hA, log_hB) = bottomUpLoge f g h;
(res_i, log_iA, log_iB) = bottomUpLoge f g i;
(res_m, log_mA) = f (Foldvl x res_h res_i vl);
in
(res_m, log_mA ++ log_iA ++ log_hA,
log_iB ++ log_hB))
/\
bottomUpLogc f g (Bconst b) :cexpr#'a list # 'b list =
(let (res_b, logB) = g (Bconst b) in
(res_b, [], logB)) /\
bottomUpLogc f g (Pred p e) =
(let (res_e, logA1, logB1) = bottomUpLoge f g e;
(res_p, logB) = g (Pred p res_e);
in
(res_p, logA1, logB ++ logB1)) /\
bottomUpLogc f g (Cmp cmp e1 e2) =
(let
(res_e1, logA1, logB1) = bottomUpLoge f g e1;
(res_e2, logA2, logB2) = bottomUpLoge f g e2;
(res_b, logB) = g (Cmp cmp res_e1 res_e2);
in
(res_b, (logA1 ++ logA2), logB++(logB1 ++ logB2))) /\
bottomUpLogc f g (Cscope Opt ce) =
(let
(res_e, logA, logB) = bottomUpLogc f g ce;
(res_s, logS) = g (Cscope Opt res_e)
in
(res_s, logA, logS++logB))
/\
bottomUpLogel f g [] = ([], [], []) /\
bottomUpLogel f g (e::el) =
(let
(el_new, log_elA, log_elB) = bottomUpLogel f g el;
(e_new, log_eA, log_eB) = bottomUpLoge f g e;
in
(e_new :: el_new, log_eA ++ log_elA, log_eB ++ log_elB))`
(WF_REL_TAC
`measure
(\x.
case x of
|INL (_, _, x) => expr_size x
|INR (INL (_, _, x)) => cexpr_size x
| INR (INR (_,_,x)) => expr1_size x)`
\\ fs[]);
val appAtOpt_def = tDefine
"appAtOpt"
`appAtOpt f g (List el) = List (appAtOptL f g el) /\
appAtOpt f g (Ith n e) = Ith n (appAtOpt f g e) /\
appAtOpt f g (Scope Opt e) = Scope Opt (bottomUpExp f g e) /\
appAtOpt f g (Unop u e) = Unop u (appAtOpt f g e) /\
appAtOpt f g (Binop b e1 e2) = Binop b (appAtOpt f g e1) (appAtOpt f g e2) /\
appAtOpt f g (Terop t e1 e2 e3) =
Terop t (appAtOpt f g e1) (appAtOpt f g e2) (appAtOpt f g e3) /\
appAtOpt f g(Let x e1 e2) = Let x (appAtOpt f g e1) (appAtOpt f g e2) /\
appAtOpt f g (Cond c e1 e2) =
Cond (appAtCOpt f g c) (appAtOpt f g e1) (appAtOpt f g e2) /\
appAtOpt f g (Map x h e) = Map x (appAtOpt f g h) (appAtOpt f g e) /\
appAtOpt f g (Mapvl x h vl) = Mapvl x (appAtOpt f g h) vl /\
appAtOpt f g (Fold p h i e) =
Fold p (appAtOpt f g h) (appAtOpt f g i) (appAtOpt f g e) /\
appAtOpt f g (Foldvl p h i vl) =
Foldvl p (appAtOpt f g h) (appAtOpt f g i) vl /\
appAtOpt f g e = e
/\
appAtCOpt f g (Pred p e) = Pred p (appAtOpt f g e) /\
appAtCOpt f g (Cmp cmp e1 e2) = Cmp cmp (appAtOpt f g e1) (appAtOpt f g e2) /\
appAtCOpt f g (Cscope Opt e) = Cscope Opt (bottomUpCexp f g e) /\
appAtCOpt f g e = e
/\
appAtOptL f g [] = [] /\
appAtOptL f g (e::el) = (appAtOpt f g e) :: (appAtOptL f g el)`
(WF_REL_TAC
`measure
(\x.
case x of
|INL (_, _, x) => expr_size x
|INR (INL (_, _, x)) => cexpr_size x
| INR (INR (_,_,x)) => expr1_size x)`
\\ fs[]);
val appAndLogOpt_def = tDefine
"appAndLogOpt"
`appAndLogOpt f g (List el) =
(let
(resl, logAl, logBl) = appAndLogOptL f g el
in
(List resl, logAl, logBl)) /\
appAndLogOpt f g (Ith n e) =
(let
(res_e, logA, logB) = appAndLogOpt f g e
in
(Ith n res_e, logA, logB)) /\
appAndLogOpt f g (Scope Opt e) =
(let (res, logA, logB) = (bottomUpLoge f g e) in
(Scope Opt res, logA, logB)) /\
appAndLogOpt f g (Unop u e) =
(let (res, logA, logB) = (appAndLogOpt f g e) in
(Unop u res, logA, logB)) /\
appAndLogOpt f g (Binop b e1 e2) =
(let
(res1, logA1, logB1) = (appAndLogOpt f g e1);
(res2, logA2, logB2) = (appAndLogOpt f g e2)
in
(Binop b res1 res2, logA1 ++ logA2, logB1 ++ logB2)) /\
appAndLogOpt f g (Terop t e1 e2 e3) =
(let
(res1, logA1, logB1) = (appAndLogOpt f g e1);
(res2, logA2, logB2) = (appAndLogOpt f g e2);
(res3, logA3, logB3) = (appAndLogOpt f g e3)
in
(Terop t res1 res2 res3, logA1 ++ logA2 ++ logA3, logB1 ++ logB2 ++ logB3)) /\
appAndLogOpt f g(Let x e1 e2) =
(let
(res1, logA1, logB1) = (appAndLogOpt f g e1);
(res2, logA2, logB2) = (appAndLogOpt f g e2)
in
(Let x res1 res2, logA1 ++ logA2, logB1 ++ logB2)) /\
appAndLogOpt f g (Cond c e1 e2) =
(let
(c1, logAC1, logBC1) = (appAndLogCOpt f g c);
(res1, logA1, logB1) = (appAndLogOpt f g e1);
(res2, logA2, logB2) = (appAndLogOpt f g e2)
in
(Cond c1 res1 res2, logAC1 ++ logA1 ++ logA2, logBC1 ++ logB1 ++ logB2)) /\
appAndLogOpt f g (Map x h e) =
(let
(res_h, log_hA, log_hB) = appAndLogOpt f g h;
(res_e, log_eA, log_eB) = appAndLogOpt f g e;
in
(Map x res_h res_e, log_eA ++ log_hA, log_eB ++ log_hB)) /\
appAndLogOpt f g (Mapvl x h vl) =
(let
(res_h, log_hA, log_hB) = appAndLogOpt f g h;
in
(Mapvl x res_h vl, log_hA, log_hB)) /\
appAndLogOpt f g (Fold x h i e) =
(let
(res_h, log_hA, log_hB) = appAndLogOpt f g h;
(res_i, log_iA, log_iB) = appAndLogOpt f g i;
(res_e, log_eA, log_eB) = appAndLogOpt f g e;
in
(Fold x res_h res_i res_e,
log_eA ++ log_iA ++ log_hA,
log_eB ++ log_iB ++ log_hB)) /\
appAndLogOpt f g (Foldvl x h i vl) =
(let
(res_h, log_hA, log_hB) = appAndLogOpt f g h;
(res_i, log_iA, log_iB) = appAndLogOpt f g i;
in
(Foldvl x res_h res_i vl, log_iA ++ log_hA, log_iB ++ log_hB)) /\
appAndLogOpt f g e = (e, [], [])
/\
appAndLogCOpt f g (Pred p e) =
(let
(res, logA, logB) = appAndLogOpt f g e
in
(Pred p res, logA, logB)) /\
appAndLogCOpt f g (Cmp cmp e1 e2) =
(let
(res1, logA1, logB1) = (appAndLogOpt f g e1);
(res2, logA2, logB2) = (appAndLogOpt f g e2)
in
(Cmp cmp res1 res2, logA1 ++ logA2, logB1 ++ logB2)) /\
appAndLogCOpt f g (Cscope Opt e) =
(let (res, logA, logB) = (bottomUpLogc f g e) in
(Cscope Opt res, logA, logB)) /\
appAndLogCOpt f g e = (e, [], [])
/\
appAndLogOptL f g [] = ([], [], []) /\
appAndLogOptL f g (e::el) =
(let
(el_res, logAl, logBl) = appAndLogOptL f g el;
(e_res, logA, logB) = appAndLogOpt f g e;
in