Commit d02988ff authored by Heiko Becker's avatar Heiko Becker

Try fixing translator, not working yet

parent a28258ab
......@@ -230,12 +230,12 @@ Proof.
apply RmaxAbs; eauto.
Lemma validErrorboundCorrectConstant_eval E1 E2 A m n nR Gamma:
eval_exp E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma:
eval_exp E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR M0 ->
exists nF m',
eval_exp E2 defVars (toRExp (Const m n)) nF m'.
eval_exp E2 Gamma (toRExp (Const m n)) nF m'.
intros eval_real subexpr_ok error_valid intv_valid A_const.
intros eval_real .
repeat eexists.
rewrite Rabs_eq_Qabs.
Subproject commit c760e35a371970c83a07a154bb67d4b842115a1f
Subproject commit 19c41e5bac090d86a4245e2b6054ef710c42a402
open preamble
open AbbrevsTheory MachineTypeTheory ExpressionsTheory CommandsTheory
open AbbrevsTheory MachineTypeTheory ExpressionsTheory CommandsTheory DaisyMapTheory
val _ = new_theory "daisyParser";
......@@ -377,11 +377,11 @@ val parsePrecond_def = Define `
| _ => NONE`;
val defaultAbsenv_def = Define
`defaultAbsenv:analysisResult = \e. ((0,0),0)`;
`defaultAbsenv:analysisResult = DaisyMapTree_empty`;
val updAbsenv_def = Define
`updAbsenv (e:real exp) (iv:interval) (err:real) (A:analysisResult) =
\e'. if (e = e') then (iv,err) else A e'`;
DaisyMapTree_insert e (iv,err) A`;
(** Abstract environment parser: *)
(* The abstract environment should be encoded in the following format: *)
open preamble
open simpLib realTheory realLib RealArith stringTheory
open simpLib (* realTheory *)realLib RealArith stringTheory
open ml_translatorTheory ml_translatorLib realProgTheory cfTacticsLib ioProgLib
open ml_translatorTheory ml_translatorLib RatProgTheory cfTacticsLib ioProgLib
open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
ErrorBoundsTheory IntervalArithTheory DaisyTactics IntervalValidationTheory
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment