Commit 69e60d78 authored by Heiko Becker's avatar Heiko Becker

Fix bug in translationScript and fforward CakeML

parent cb3b7782
Subproject commit 645d4af010862abf8d2245a879b09d51e48d9afc
Subproject commit 1c47169d571439c9a00eaf31af90fadca2139402
......@@ -432,7 +432,7 @@ val runchecker_output_spec_def =
val main = process_topdecs`
fun main u =
case TextIO.inputLinesFrom (List.hd (CommandLine.arguments()))
of SOME lines =>
of Some lines =>
TextIO.print (runchecker lines)`;
(* fun main u = *)
(* write_list (runchecker (read_all []))`; *)
......@@ -449,9 +449,9 @@ val st = get_ml_prog_state()
val main_spec = Q.store_thm("main_spec",
`hasFreeFD fs inFS_fname fs (File fname)
cl = [pname; fname]
contents = lines_of (implode (THE (ALOOKUP fs.files (File fname)))) ==>
contents = lines_of (implode (THE (ALOOKUP fs.files (File fname)))) ==>
app (p:'ffi ffi_proj) ^(fetch_v "main" st)
[uv] (COMMANDLINE cl * STDIO fs)
[uv] (STDIO fs * COMMANDLINE cl)
(POSTv uv. &UNIT_TYPE () uv *
(STDIO (add_stdout fs (runchecker_output_spec contents))) * COMMANDLINE cl)`,
(* [Conv NONE []] (STDOUT out * STDERR err * STDIN inp F) *)
......@@ -462,23 +462,15 @@ val main_spec = Q.store_thm("main_spec",
xcf "main" st
\\ xlet_auto
>- (xcon \\ xsimpl \\ EVAL_TAC)
\\ xlet_auto
>- (xsimpl \\ qexistsl_tac [`STDIO fs`, `cl`]
\\ xsimpl)
\\ xlet_auto
>- (xsimpl)
\\ xlet_auto >- xsimpl
\\ xlet_auto >- (xsimpl)
\\ reverse(Cases_on`wfcl cl`)
>- (fs[COMMANDLINE_def] \\ xpull \\ rfs[])
\\ `FILENAME fname fnamev` by (fs[FILENAME_def,EVERY_MEM,wfcl_def,validArg_def])
\\ xlet`(POSTv sv. &OPTION_TYPE (LIST_TYPE STRING_TYPE)
(if inFS_fname fs (File fname) then SOME (all_lines fs (File fname))
else NONE) sv * STDIO fs *
COMMANDLINE [pname; fname])`
>- (xapp \\ instantiate \\ xsimpl)
\\ xmatch
\\ fs[OPTION_TYPE_def]
(* this part solves the validate_pat conjunct *)
\\ reverse conj_tac >- (EVAL_TAC \\ simp[])
>- (rfs[COMMANDLINE_def] \\ xpull)
\\ reverse (Cases_on `STD_streams fs`) >-(fs[STDIO_def] \\ xpull)
\\ xlet_auto_spec (SOME inputLinesFrom_spec)
>- (xsimpl \\ rfs[wfcl_def, validArg_def, EVERY_MEM])
\\ xmatch \\ fs[OPTION_TYPE_def]
\\ reverse conj_tac >- (EVAL_TAC \\ fs[])
\\ xlet_auto
>- (xsimpl)
\\ xapp \\ instantiate \\ xsimpl
......
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