Fix translation

cakeml @ daa2d5c0

-Subproject commit 800745426c5c2ef2f5c5475c26640641dd222f04
+Subproject commit daa2d5c014fffca8301ddca1a17592d13b452455

hol4/transScript.sml

 open preamble
 open simpLib realTheory realLib RealArith stringTheory
 
-open ml_translatorTheory ml_translatorLib cfTacticsLib basisProgTheory
+open ml_translatorTheory ml_translatorLib cfTacticsLib basis basisProgTheory
 
 open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
      ErrorBoundsTheory IntervalArithTheory DaisyTactics IntervalValidationTheory
@@ -65,12 +65,13 @@ val check_all_def = Define `
       | _ => "Failure: Number of Functions in certificate\n"`;
 
 val runChecker_def = Define `
-  runChecker (input:tvarN) =
-    let tokList = lex input in
-        case tokList of
+  runChecker (input:mlstring list) =
+    let inp = concat input in
+    let tokList = lex (explode inp) in
+      implode (case tokList of
             (* FIRST: number of iterations, SECOND: number of functions *)
           | DCONST n :: DCONST m :: tokRest => check_all m n tokRest
-          | _ => "failure no num of functions"`;
+          | _ => "failure no num of functions")`;
 
 (* for recursive translation *)
 
@@ -424,56 +425,108 @@ recInduct str_of_num_ind
 \\ match_mp_tac LESS_TRANS
 \\ qexists_tac `10 + 48` \\ fs []) |> update_precondition;
 
-
 val res = translate runChecker_def;
 
+val valid_runchecker_output_def = Define`
+  valid_runchecker_output file_contents output =
+    (runChecker file_contents = output)`;
+(* Although we have defined valid_wordfreq_output as a relation between
+   file_contents and output, it is actually functional (there is only one correct
+   output). We prove this below: existence and uniqueness. *)
+
+val valid_runchecker_output_exists = Q.store_thm("valid_runchecker_output_exists",
+  `∃output. valid_runchecker_output file_chars output`,
+  fs[valid_runchecker_output_def]);
+
+val runchecker_output_spec_def =
+  new_specification("runchecker_output_spec_def",["runchecker_output_spec"],
+    GEN_ALL valid_runchecker_output_exists |> SIMP_RULE std_ss [SKOLEM_THM]);
+
 (* -- I/O routines from here onwards -- *)
 
 val main = process_topdecs`
   fun main u =
-    write_list (runchecker (read_all []))`;
+    case TextIO.inputLinesFrom (List.hd (CommandLine.arguments()))
+    of SOME lines =>
+      TextIO.print (runchecker lines)`;
+  (* fun main u = *)
+  (*   write_list (runchecker (read_all []))`; *)
+
+val _ = append_prog main;
 
-val res = ml_prog_update(ml_progLib.add_prog main I)
+(* val res = ml_prog_update(ml_progLib.add_prog main I) *)
 val st = get_ml_prog_state()
 
+(* Specification of the runchecker function:
+   Running the checker on an input file inp appends the result of running
+   the function to STDOUT *)
+
 val main_spec = Q.store_thm("main_spec",
-  `app (p:'ffi ffi_proj) ^(fetch_v "main" st)
-     [Conv NONE []] (STDOUT out * STDERR err * STDIN inp F)
-     (POSTv uv. &UNIT_TYPE () uv *
-                STDOUT (out ++ runChecker inp) *
-                STDERR err *
-                STDIN "" T)`,
+  `hasFreeFD fs ∧ inFS_fname fs (File fname) ∧
+   cl = [pname; 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)
+    (POSTv uv. &UNIT_TYPE () uv *
+      (STDIO (add_stdout fs (runchecker_output_spec contents))) * COMMANDLINE cl)`,
+     (* [Conv NONE []] (STDOUT out * STDERR err * STDIN inp F) *)
+     (* (POSTv uv. &UNIT_TYPE () uv * *)
+     (*            STDOUT (out ++ runChecker inp) * *)
+     (*            STDERR err * *)
+     (*            STDIN "" T)`, *)
   xcf "main" st
-  \\ qmatch_abbrev_tac`_ frame _`
-  \\ xlet`POSTv uv. &(LIST_TYPE CHAR [] uv) * frame`
+  \\ xlet_auto
   >- (xcon \\ xsimpl \\ EVAL_TAC)
-  \\ qunabbrev_tac`frame`
-  \\ xlet`POSTv cv. &LIST_TYPE CHAR inp cv * STDERR err * STDIN "" T * STDOUT out`
-  >- (xapp \\ instantiate \\ xsimpl
-      \\ map_every qexists_tac[`STDERR err * STDOUT out`,`F`,`inp`]
+  \\ xlet_auto
+  >- (xsimpl \\ qexistsl_tac [`STDIO fs`, `cl`]
       \\ xsimpl)
-  \\ qmatch_abbrev_tac`_ frame _`
-  \\ qmatch_goalsub_abbrev_tac`STRCAT _ res`
-  \\ xlet`POSTv xv. &LIST_TYPE CHAR res xv * frame`
+  \\ 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)
-  \\ xapp \\ instantiate
-  \\ simp[Abbr`frame`]
-  \\ map_every qexists_tac[`STDERR err * STDIN "" T`,`out`]
+  \\ xmatch
+  \\ fs[OPTION_TYPE_def]
+  (* this part solves the validate_pat conjunct *)
+  \\ reverse conj_tac >- (EVAL_TAC \\ simp[])
+  \\ xlet_auto
+  >- (xsimpl)
+  \\ xapp \\ instantiate \\ xsimpl
+  \\ CONV_TAC(SWAP_EXISTS_CONV) \\ qexists_tac`fs` \\ xsimpl
+  \\ qmatch_abbrev_tac`STDIO (add_stdout _ xxxx) ==>> STDIO (add_stdout _ yyyy) * GC`
+  \\ `xxxx = yyyy` suffices_by xsimpl
+  (* now let us unabbreviate xxxx and yyyy *)
+  \\ map_every qunabbrev_tac[`xxxx`,`yyyy`] \\ simp[]
+  \\ assume_tac (REWRITE_RULE [valid_runchecker_output_def] runchecker_output_spec_def)
+  \\ fs[all_lines_def]);
+
+val main_whole_prog_spec = Q.store_thm("main_whole_prog_spec",
+  `hasFreeFD fs /\ inFS_fname fs (File fname) /\
+   cl = [pname; fname] /\
+   contents = lines_of (implode (THE (ALOOKUP fs.files (File fname)))) ==>
+   whole_prog_spec ^(fetch_v "main" st) cl fs
+         ((=) (add_stdout fs (runchecker_output_spec contents)))`,
+  disch_then assume_tac
+  \\ simp[whole_prog_spec_def]
+  \\ qmatch_goalsub_abbrev_tac`fs1 = _ with numchars := _`
+  \\ qexists_tac`fs1`
+  \\ simp[Abbr`fs1`,GSYM add_stdo_with_numchars,with_same_numchars]
+  \\ match_mp_tac (MP_CANON (MATCH_MP app_wgframe (UNDISCH main_spec)))
   \\ xsimpl);
 
-val spec = main_spec |> UNDISCH_ALL |> add_basis_proj;
-val name = "main"
-val (semantics_thm,prog_tm) = call_thm st name spec;
+val (sem_thm,prog_tm) = whole_prog_thm (get_ml_prog_state ()) "main" (UNDISCH main_whole_prog_spec);
 
-val entire_program_def = Define`entire_program = ^prog_tm`;
+val main_prog_def = Define `main_prog = ^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 main_semantics =
+  sem_thm |> ONCE_REWRITE_RULE[GSYM main_prog_def]
+  |> DISCH_ALL |> Q.GENL[`cl`,`contents`]
+  |> SIMP_RULE(srw_ss())[AND_IMP_INTRO,GSYM CONJ_ASSOC]
+  |> curry save_thm "main_semantics";
 
 val _ = export_theory();