Commit 35989490 authored by Magnus Myreen's avatar Magnus Myreen

Improve generated CakeML code

parent 27105163
......@@ -96,6 +96,116 @@ val parseexp_side_true = prove(
val res = translate dParse_def;
(* improve function definitions a little *)
val const_1_over_2_pow_11_def = Define `
const_1_over_2_pow_11 = 1 / 2 pow 11`
val const_1_over_2_pow_24_def = Define `
const_1_over_2_pow_24 = 1 / 2 pow 24`
val const_1_over_2_pow_53_def = Define `
const_1_over_2_pow_53 = 1 / 2 pow 53`
val const_1_over_2_pow_11_eq = EVAL ``const_1_over_2_pow_11``;
val const_1_over_2_pow_24_eq = EVAL ``const_1_over_2_pow_24``;
val const_1_over_2_pow_53_eq = EVAL ``const_1_over_2_pow_53``;
val _ = translate const_1_over_2_pow_11_eq;
val _ = translate const_1_over_2_pow_24_eq;
val _ = translate const_1_over_2_pow_53_eq;
val _ = translate (MachineTypeTheory.mTypeToQ_def
|> REWRITE_RULE [GSYM const_1_over_2_pow_11_def,
GSYM const_1_over_2_pow_24_def,
GSYM const_1_over_2_pow_53_def]);
val isMorePrecise_eq = prove(
``isMorePrecise m1 m2 =
case m1 of
| M0 => T
| M64 => (case m2 of M0 => F | _ => T)
| M32 => (case m2 of M0 => F | M64 => F | _ => T)
| M16 => (case m2 of M16 => T | _ => F)``,
Cases_on `m1` \\ Cases_on `m2` \\ EVAL_TAC);
val _ = translate isMorePrecise_eq;
fun LET_CONV var_name body =
(UNBETA_CONV body THENC
RATOR_CONV (ALPHA_CONV (mk_var(var_name, type_of body))) THENC
REWR_CONV (GSYM LET_THM));
val absIntvUpd_eq =
IntervalArithTheory.absIntvUpd_def
|> SPEC_ALL
|> CONV_RULE (RAND_CONV (LET_CONV "lo1" ``IVlo iv1`` THENC
LET_CONV "lo2" ``IVlo iv2`` THENC
LET_CONV "hi1" ``IVhi iv1`` THENC
LET_CONV "hi2" ``IVhi iv2``));
val addInterval_eq =
IntervalArithTheory.addInterval_def
|> REWRITE_RULE [absIntvUpd_eq]
val _ = translate addInterval_eq
val multInterval_eq =
IntervalArithTheory.multInterval_def
|> REWRITE_RULE [absIntvUpd_eq]
val _ = translate multInterval_eq
val maxValueM0_def =
let val tm = EVAL ``maxValue M0`` |> concl |> rand in
Define `maxValueM0 = ^tm` end |> translate;
val maxValueM16_def =
let val tm = EVAL ``maxValue M16`` |> concl |> rand in
Define `maxValueM16 = ^tm` end |> translate;
val maxValueM32_def =
let val tm = EVAL ``maxValue M32`` |> concl |> rand in
Define `maxValueM32 = ^tm` end |> translate;
val maxValueM64_def =
let val tm = EVAL ``maxValue M64`` |> concl |> rand in
Define `maxValueM64 = ^tm` end |> translate;
val maxValue_eq = prove(
``maxValue m =
case m of
| M0 => maxValueM0
| M16 => maxValueM16
| M32 => maxValueM32
| M64 => maxValueM64``,
Cases_on `m` \\ EVAL_TAC)
|> translate;
val minValueM0_def =
let val tm = EVAL ``minValue M0`` |> concl |> rand in
Define `minValueM0 = ^tm` end |> translate;
val minValueM16_def =
let val tm = EVAL ``minValue M16`` |> concl |> rand in
Define `minValueM16 = ^tm` end |> translate;
val minValueM32_def =
let val tm = EVAL ``minValue M32`` |> concl |> rand in
Define `minValueM32 = ^tm` end |> translate;
val minValueM64_def =
let val tm = EVAL ``minValue M64`` |> concl |> rand in
Define `minValueM64 = ^tm` end |> translate;
val minValue_eq = prove(
``minValue m =
case m of
| M0 => minValueM0
| M16 => minValueM16
| M32 => minValueM32
| M64 => minValueM64``,
Cases_on `m` \\ EVAL_TAC)
|> translate;
val res = translate CertificateCheckerCmd_def;
val invertinterval_side_def = fetch "-" "invertinterval_side_def";
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment