Commit 0e7eb8d8 authored by Heiko Becker's avatar Heiko Becker

WIP next steps for finite maps port

parent 583f101f
......@@ -43,4 +43,8 @@ val updDefVars_def = Define `
updDefVars (x:num) (m:mType) (defVars:num -> mType option) (y:num) :mType option =
if y = x then SOME m else defVars y`;
val _ = export_rewrites ["IVlo_def", "IVhi_def",
"emptyEnv_def", "updEnv_def",
"updDefVars_def"]
val _ = export_theory();
......@@ -71,21 +71,21 @@ val approxEnv_fVar_bounded = store_thm (
(fn thm => irule (SIMP_RULE std_ss [] thm))
approxEnv_ind
\\ rpt strip_tac
>- (fs [emptyEnv_def])
>- (fs [updEnv_def]
>- (fs [])
>- (fs []
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
\\ first_x_assum irule \\ fs[]
\\ rename1 `updDefVars x1 m1 defVars x2 = SOME m2`
\\ rename1 `defVars x2 = SOME m2`
\\ qexists_tac `x2` \\ fs[updDefVars_def])
>- (fs [updEnv_def, updDefVars_def]
>- (fs []
\\ rveq \\ fs[]
\\ EVERY_CASE_TAC
\\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexists_tac `x1`
\\ fs[])
>- (qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`, `E2`, `x`]
\\ fs[]));
\\ qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`, `E2`, `x`]
\\ fs[]);
val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
``!E1 Gamma A fVars dVars E2 x v v2 m iv e.
......
This diff is collapsed.
......@@ -152,17 +152,27 @@ end;
(* This variable is supposed to hold all defined functions *)
val eval_funs:term list ref = ref [];
open TextIO;
val t = TextIO.openIn("/home/hbecker/Downloads/test.txt");
inputLine(t);
closeIn(t);
val t2 = openIn("./test.txt");
inputLine(t2);
output(t2, "ABC\n");
closeOut(t2);
(* open TextIO; *)
(* val t = TextIO.openIn("/home/hbecker/Downloads/test.txt"); *)
(* inputLine(t); *)
(* closeIn(t); *)
(* val t2 = openIn("./test.txt"); *)
(* inputLine(t2); *)
(* output(t2, "ABC\n"); *)
(* closeOut(t2); *)
fun add_unevaluated_function (t:term) :unit =
eval_funs := t :: (!eval_funs);
let
val add_t = "val _ = DaisyTactics.eval_funs :=``" ^ term_to_string t ^ "`` :: (!DaisyTactics.eval_funs);"
val _ = adjoin_to_theory
{ sig_ps =
SOME (fn ppstrm => ()),
struct_ps =
SOME (fn ppstrm =>
PP.add_string ppstrm add_t)};
in
eval_funs := t :: (!eval_funs)
end;
fun Daisy_compute t =
let
......
......@@ -30,6 +30,8 @@ val typeExpression_def = Define `
| SOME m1 => if (morePrecise m1 m) then SOME m else NONE
| NONE => NONE`;
!eval_funs;
add_unevaluated_function ``typeExpression``;
val typeMap_def = Define `
......
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