Commit a5b027b2 authored by Heiko Becker's avatar Heiko Becker

Update CakeML, add parser temp_overloads to fix bug

parent 9a318105
......@@ -11,6 +11,7 @@ open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory ErrorValidationTheory ssaPrgsTheory
val _ = new_theory "CertificateChecker";
val _ = temp_overload_on("abs",``real$abs``);
(** Certificate checking function **)
val CertificateChecker_def = Define
......
......@@ -4,6 +4,8 @@ open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyT
val _ = new_theory "Environments";
val _ = temp_overload_on("abs",``real$abs``);
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(defVars: num -> mType option) (A:analysisResult).
approxEnv emptyEnv defVars A LN LN emptyEnv) /\
......
......@@ -11,6 +11,7 @@ open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) (defVars: num -> mType option).
......
......@@ -15,6 +15,7 @@ open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val validErrorbound_def = Define `
validErrorbound e (typeMap: real exp -> mType option) (absenv:analysisResult) (dVars:num_set)=
......
......@@ -10,6 +10,7 @@ val _ = ParseExtras.temp_tight_equality()
val _ = new_theory "Expressions";
val _ = temp_overload_on("abs",``real$abs``);
(**
EXPRESSIONS WILL use binary operators.
Define them first
......
......@@ -9,6 +9,8 @@ open realTheory realLib sptreeTheory
val _ = new_theory "MachineType";
val _ = temp_overload_on("abs",``real$abs``);
val _ = Datatype `
mType = M0 | M16 | M32 | M64(* | M128 | M256 *)`;
......
......@@ -8,6 +8,9 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory;
val _ = new_theory "IntervalArith";
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
......
......@@ -14,6 +14,9 @@ open sptreeLib sptreeTheory
val _ = new_theory "IntervalValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
val validIntervalbounds_def = Define `
validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
......@@ -168,7 +171,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ `eval_exp E (toRMap Gamma) (toREval (Const m v)) v M0`
by (fs [toREval_def] \\ match_mp_tac Const_dist'
\\ fs[mTypeToQ_def]
\\ qexists_tac `0` \\ fs[perturb_def])
\\ fs[perturb_def])
\\ qexists_tac `v`
\\ fs [mTypeToQ_def]
\\ fs [validIntervalbounds_def, isSupersetInterval_def, IVhi_def, IVlo_def, toREval_def])
......
......@@ -5,6 +5,14 @@ val _ = ParseExtras.temp_tight_equality()
val _ = new_theory "RealSimps";
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val abs_leq_zero = store_thm (
"abs_leq_zero[simp]",
``!v. abs v <= 0 <=> v = 0``,
rw[realTheory.abs] \\ RealArith.REAL_ASM_ARITH_TAC);
val REAL_INV_LE_ANTIMONO = store_thm ("REAL_INV_LE_ANTIMONO",
``! x y. 0 < x /\ 0 < y ==> (inv x <= inv y <=> y <= x)``,
rpt strip_tac
......
open preamble
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics CertificateCheckerTheory
open FPRangeValidatorTheory IntervalValidationTheory TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
val f64_plus_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_add dmode f1 f2) ==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_add_def, fp64_to_float_float_to_fp64,
float_add_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)`
\\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]);
val f64_sub_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_sub dmode f1 f2) ==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_sub_def, fp64_to_float_float_to_fp64,
float_sub_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]
\\ Cases_on `float_value (float_negate (fp64_to_float f2))`
\\ fs [float_values]
\\ `(fp64_to_float f2).Exponent = UINT_MAXw`
by (fs [float_value_def]
\\ Cases_on `(fp64_to_float f2).Exponent = -(1w)`
\\ Cases_on `(fp64_to_float f2).Significand = 0w`
\\ fs [])
\\ `(fp64_to_float f2).Significand = 0w`
by (fs [float_value_def]
\\ Cases_on `(fp64_to_float f2).Exponent = -(1w)`
\\ Cases_on `(fp64_to_float f2).Significand = 0w`
\\ fs [])
\\ fs [float_negate_def, float_value_def]);
val f64_mul_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_mul dmode f1 f2) ==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_mul_def, fp64_to_float_float_to_fp64,
float_mul_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]
\\ Cases_on `r = 0`
\\ fs [float_values]);
val f64_div_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_div dmode f1 f2) /\
(float_value (fp64_to_float f2) = Infinity ==> F)==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_div_def, fp64_to_float_float_to_fp64,
float_div_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]
\\ Cases_on `r = 0`
\\ fs [float_values]);
val real_to_float_float_id = Q.prove (
`!f.
fp64_isFinite f /\
fp64_isNormal f /\
~ fp64_isZero f ==>
float_to_fp64 (real_to_float dmode (float_to_real (fp64_to_float f))) = f`,
rpt strip_tac
\\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
\\ fs[real_to_float_id]
\\ fs[float_to_fp64_fp64_to_float]);
``!ff:half.
validFloatValue (float_to_real ff) M16 ==>
float_to_real ((float_round roundTiesToEven F (float_to_real ff)):single) = float_to_real ((float_round roundTiesToEven F (float_to_real ff)):half)``
rw[]
\\ fs[validFloatValue_def]
>- (`float_is_finite ff` by (irule normal16_to_real_implies_finiteness \\ fs[])
\\ Q.ISPEC_THEN `ff` impl_subgoal_tac round_float_to_real_id \\ fs[]
>- (cheat)
\\ `float_value ff = Float (float_to_real ff)` by (irule normal16_is_float_value \\ fs[])
\\ Cases_on `float_to_real ff = 0`
\\ fs[]
>- (`2 * abs 0 <= ulp (:10#5)`
by (fs[ulp_def, ULP_def])
\\ `2 * abs 0 <= ulp (:23#8)`
by (fs[ulp_def, ULP_def])
\\ fs[round_roundTiesToEven_is_plus_zero, zero_to_real])
\\ rw[float_round_def, zero_to_real, float_is_zero_to_real]
>- (fs[round_def]
\\ every_case_tac \\ fs[]
\\ rveq
\\ TRY (
fs[float_minus_infinity_def, float_plus_infinity_def, float_to_real_def, threshold_def, float_negate_def, float_value_def]
\\ FAIL_TAC "")
\\ qpat_x_assum `closest_such _ _ _ = _` MP_TAC
(* \\ qpat_x_assum `float_to_real (closest_such _ _ _) = _` MP_TAC *)
\\ fs[closest_such_def]
\\ SELECT_ELIM_TAC
\\ rw[]
>- (qexists_tac `ff`
\\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS]
\\ first_x_assum (qspec_then `ff` mp_tac)
\\ fs[realTheory.REAL_SUB_REFL]
\\ strip_tac
\\ fs[float_to_real_eq]
\\ rveq
\\ rfs[]
\\ fs[float_is_zero_to_real])
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ fs[is_closest_def, IN_DEF]
(* (* \\ qpat_x_assum `!x._ ` (qspec_then `ff` assume_tac) mp_tac *) *)
\\ fs[]
\\ qpat_x_assum `float_to_real _ = _` mp_tac
\\ SELECT_ELIM_TAC
\\ rw[]
cheat
>- (Cases_on `ff`
\\ qexists_tac `float c (0w @@ c0) (0w @@ c1)`
\\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS, word_concat_0]
>- (fs[float_is_finite_def, float_value_def]
\\ every_case_tac \\ fs[float_Significand, float_Exponent, float_Sign, float_to_real_def]
(* \\ CCONTR_TAC \\ fs[] \\ rveq *)
(* \\ qpat_x_assum `!b. float_is_finite b ==> _` (qspec_then `x` impl_subgoal_tac) *)
(* \\ fs[] *)
(* \\ fs[] *)
(* ) *)
Subproject commit 04258e79d2ac3bf82db9804f9827f9e0544277a5
Subproject commit 9f7a2e8b53e4f091ae49340aed425376ed30ae26
......@@ -111,39 +111,39 @@ val str_of_num_def = Define `
else STRING (CHR ( (n MOD 10) + 48)) (str_of_num (n DIV 10))`
val type_to_string = Define `
(type_to_string (M16) = "MTYPE 16") /\
(type_to_string (M32) = "MTYPE 32") /\
(type_to_string (M64) = "MTYPE 64") /\
(type_of_string (_) = "FAIL"); (* FIXME *)
(type_to_string (M64) = "MTYPE 64")`; (* FIXME *)
(* (type_to_string (M128) = "MTYPE 128") /\ *)
(* (type_to_string (M256) = "MTYPE 256")`; *)
(* val pp_token_def = Define ` *)
(* pp_token (token:Token) = *)
(* case token of *)
(* | DLET => "Let" *)
(* | DRET => "Ret" *)
(* | DPRE => "PRE" *)
(* | DABS => "ABS" *)
(* | DCOND => "?" *)
(* | DGAMMA => "Gamma" *)
(* | DTYPE m => type_to_string m *)
(* | DVAR => "Var" *)
(* | DCONST num => str_of_num num *)
(* | DNEG => "~" *)
(* | DPLUS => "+" *)
(* | DSUB => "-" *)
(* | DMUL => "*" *)
(* | DDIV => "/" *)
(* | DFRAC => "#"`; *)
val pp_token_def = Define `
pp_token (token:Token) =
case token of
| DLET => "Let"
| DRET => "Ret"
| DPRE => "PRE"
| DABS => "ABS"
| DCOND => "?"
| DGAMMA => "Gamma"
| DTYPE m => type_to_string m
| DVAR => "Var"
| DCONST num => str_of_num num
| DNEG => "~"
| DPLUS => "+"
| DSUB => "-"
| DMUL => "*"
| DDIV => "/"
| DFRAC => "#"`;
(* val pp_token_correct = store_thm ("pp_token_correct", *)
(* ``!t. lex (pp_token t) = [t]``, *)
(* Induct_on `t` \\ EVAL_TAC fs[pp_token_def, lex_def] *)
(* ); *)
(* val str_join_def = Define ` *)
(* (str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\ *)
(* (str_join "" s2 = s2)`; *)
val str_join_def = Define `
(str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\
(str_join "" s2 = s2)`;
(* val str_join_empty = store_thm ("str_join_empty", *)
(* ``!s. str_join s "" = s``, *)
......
#!/bin/sh
find -type f -name "*Script.sml" -not -path "./cakeml/*" -not -path "./attic/*" -exec grep -n -H "cheat" {} \;
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