Commit 5ce3684e authored by Magnus Myreen's avatar Magnus Myreen

Add I/O code to the end of transScript.sml

parent da20be68
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator cakeml/basis cakeml/characteristic
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......@@ -19,7 +19,8 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib
cakeml/translator/ml_translatorLib \
cakeml/basis/ioProgLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
......@@ -5,7 +5,7 @@ open gcdTheory
val _ = new_theory "realProg";
val _ = translation_extends "std_prelude";
val _ = translation_extends "ioProg";
(* real_of_int *)
......
......@@ -7,6 +7,7 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory DaisyTactics
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory CertificateCheckerTheory
open CertificateCheckerTheory daisyParserTheory
open cfTacticsLib ioProgLib
val _ = new_theory "trans";
......@@ -22,7 +23,7 @@ val runChecker_def = Define `
if CertificateCheckerCmd dCmd A P
then "True"
else "False"
| NONE => "parse failure"`;
| NONE => "parse failure"`;
(* TESTING STATEMENTS
EVAL ``case (EXPLODE "abc") of
......@@ -248,6 +249,54 @@ val precond_is_true = prove (
\\ qexists_tac `P` \\ fs []))
|> update_precondition;
val res' = translate runChecker_def;
val res = translate runChecker_def;
(* -- I/O rountines from here onwards -- *)
val main = process_topdecs`
fun main u =
write_list (runchecker (read_all []))`;
val res = ml_prog_update(ml_progLib.add_prog main I)
val st = get_ml_prog_state()
val main_spec = Q.store_thm("main_spec",
`app (p:'ffi ffi_proj) ^(fetch_v "main" st)
[Conv NONE []] (STDOUT out * STDIN inp F)
(POSTv uv. &UNIT_TYPE () uv *
(STDOUT (out ++ runChecker inp) *
STDIN "" T))`,
xcf "main" st
\\ qmatch_abbrev_tac`_ frame _`
\\ xlet`POSTv uv. &(LIST_TYPE CHAR [] uv) * frame`
>- (xcon \\ xsimpl \\ EVAL_TAC)
\\ qunabbrev_tac`frame`
\\ xlet`POSTv cv. &LIST_TYPE CHAR inp cv * STDIN "" T * STDOUT out`
>- (xapp \\ instantiate \\ xsimpl
\\ map_every qexists_tac[`STDOUT out`,`F`,`inp`]
\\ xsimpl)
\\ qmatch_abbrev_tac`_ frame _`
\\ qmatch_goalsub_abbrev_tac`STRCAT _ res`
\\ xlet`POSTv xv. &LIST_TYPE CHAR res xv * frame`
>- (xapp \\ instantiate \\ xsimpl)
\\ xapp \\ instantiate
\\ simp[Abbr`frame`]
\\ map_every qexists_tac[`STDIN "" T`,`out`]
\\ xsimpl);
val spec = main_spec |> UNDISCH_ALL |> add_basis_proj;
val name = "main"
val (semantics_thm,prog_tm) = call_thm st name spec;
val entire_program_def = Define`entire_program = ^prog_tm`;
val semantics_entire_program =
semantics_thm
|> PURE_ONCE_REWRITE_RULE[GSYM entire_program_def]
|> REWRITE_RULE [APPEND]
|> CONV_RULE(RENAME_VARS_CONV["io_events"])
|> DISCH_ALL |> GEN_ALL
|> CONV_RULE(RENAME_VARS_CONV["inp","cls"])
|> curry save_thm "semantics_entire_program";
val _ = export_theory();
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