Commit dd39d141 authored by Heiko Becker's avatar Heiko Becker

Fix resolution errors

parent 3f4d2136
......@@ -17,6 +17,8 @@ open AbbrevsTheory MachineTypeTheory TypingTheory RealSimpsTheory IntervalArithT
val _ = new_theory "FPRangeValidator";
val _ = temp_overload_on("abs",``real$abs``);
val FPRangeValidator_def = Define `
FPRangeValidator (e:real exp) A (typeMap: real exp -> mType option) =
case typeMap e of
......
......@@ -7,6 +7,8 @@ open FPRangeValidatorTheory IntervalValidationTheory TypingTheory ErrorValidatio
val _ = new_theory "IEEE_connection";
val _ = temp_overload_on("abs",``real$abs``);
val dmode_def = Define `dmode = roundTiesToEven`;
val eval_exp_float_def = Define `
......@@ -340,6 +342,34 @@ val float_to_real_round_zero_is_zero = store_thm (
\\ fs [round_roundTiesToEven_is_plus_zero,
round_roundTiesToEven_is_minus_zero, zero_to_real]);
val noDowncast_def = Define `
(noDowncast (Var v) = T) /\
(noDowncast (Const _ _) = T) /\
(noDowncast (Unop _ e) = noDowncast e) /\
(noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
(noDowncast (Downcast _ _) = F)`;
val is64BitEval_def = Define `
(is64BitEval ((Const m c):real exp) = (m = M64)) /\
(is64BitEval (Unop _ e) = is64BitEval e) /\
(is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\
(is64BitEval (Downcast m e) = is64BitEval e) /\
(is64BitEval ((Var v):real exp) = T)`;
val typeMap_eq_typeExp = Q.prove(`!e. typeMap Gamma e e = typeExpression Gamma e`,
Induct \\ fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] );
val typing_is_64bit = store_thm("typing_is_64bit",
``!e.
noDowncast e /\ is64BitEval e /\ (!v. v IN domain(usedVars e) ==> Gamma v = SOME M64) ==>
(typeMap Gamma e) e = SOME M64``
Induct
\\ rpt strip_tac \\ simp[Once typeMap_def] \\ fs[is64BitEval_def, noDowncast_def]
>- (first_x_assum irule \\ fs[usedVars_def])
>- (fs [Once typeExpression_def]
\\ first_x_assum irule
>- (
val bstep_gives_IEEE2 = store_thm ("bstep_gives_IEEE2",
``!(e:word64 exp) E1 E2 Gamma vR A P fVars dVars .
typeCheck (toRExp e) Gamma (\_. SOME M64) /\
......
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