transScript.sml 18.6 KB
Newer Older
1 2
open simpLib realTheory realLib RealArith stringTheory;
open ml_translatorTheory ml_translatorLib cfTacticsLib basis basisProgTheory;
3
open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
4
     MachineTypeTheory
Heiko Becker's avatar
Heiko Becker committed
5
     ErrorBoundsTheory IntervalArithTheory FloverTactics IntervalValidationTheory
6
     EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory
Heiko Becker's avatar
Heiko Becker committed
7
     CertificateCheckerTheory floverParserTheory;
8
open preamble;
Magnus Myreen's avatar
Magnus Myreen committed
9 10 11

val _ = new_theory "trans";

12
val _ = translation_extends "basisProg";
Magnus Myreen's avatar
Magnus Myreen committed
13

14 15 16 17
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);

18 19 20 21 22 23 24 25 26 27 28 29
(* TODO: move this to RatProgTheory *)
val _ = add_type_inv ``REAL_TYPE`` ``:(int # num)``;

(* translation of real_div *)
val _ = (next_ml_names := ["real_div"]);
val res = translate realTheory.real_div;
val real_div_side = prove(
  let val tm = hyp res |> hd |> rand val v = rand tm
  in mk_eq(tm,``^v <> 0``) end,EVAL_TAC)
  |> update_precondition;
(* / translation of real_div *)

30 31 32 33
val check_rec_def = Define `
  check_rec (input:Token list) (num_fun:num)=
  case num_fun of
    | SUC n' =>
34
      (case dParse input of
35 36
         | SOME ((dCmd, P, A, Gamma),NIL) =>
           if CertificateCheckerCmd dCmd A P Gamma
37 38
           then "True\n"
           else "False\n"
39 40
         | SOME ((dCmd, P, A, Gamma), residual) =>
           if CertificateCheckerCmd dCmd A P Gamma
41 42 43 44 45
           then check_rec residual n'
           else "False\n"
         | NONE => pp input(*"parse failure\n"*))
    | _ => "failure num of functions"`;

46
val check_def = Define `
47
check (f:real cmd) (P:precond) (A:analysisResult) Gamma (n:num) =
48
case n of
49
 | SUC n' => (CertificateCheckerCmd f A P Gamma /\ check f P A Gamma n')
50 51 52 53 54 55 56
 | _ => T`

val check_all_def = Define `
  check_all (num_fun:num) (iters:num) (input:Token list) =
    case num_fun of
      | SUC n =>
        (case (dParse input) of
57 58
          | SOME ((f,P,A, Gamma), residual) =>
            if (check f P A Gamma iters)
59 60 61 62 63 64 65
                then case residual of
                      | a:: b => check_all n iters residual
                      | NIL => "True\n"
                else "False\n"
          | NONE => "Failure: Parse\n")
      | _ => "Failure: Number of Functions in certificate\n"`;

66
val runChecker_def = Define `
Heiko Becker's avatar
Heiko Becker committed
67 68 69 70
  runChecker (input:mlstring list) =
    let inp = concat input in
    let tokList = lex (explode inp) in
      implode (case tokList of
71 72
            (* FIRST: number of iterations, SECOND: number of functions *)
          | DCONST n :: DCONST m :: tokRest => check_all m n tokRest
Heiko Becker's avatar
Heiko Becker committed
73
          | _ => "failure no num of functions")`;
74

Magnus Myreen's avatar
Magnus Myreen committed
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
(* for recursive translation *)

fun def_of_const tm = let
  val res = dest_thy_const tm handle HOL_ERR _ =>
              failwith ("Unable to translate: " ^ term_to_string tm)
  val name = (#Name res)
  fun def_from_thy thy name =
    DB.fetch thy (name ^ "_pmatch") handle HOL_ERR _ =>
    DB.fetch thy (name ^ "_def") handle HOL_ERR _ =>
    DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ =>
    DB.fetch thy name
  val def = def_from_thy "termination" name handle HOL_ERR _ =>
            def_from_thy (#Thy res) name handle HOL_ERR _ =>
            failwith ("Unable to find definition of " ^ name)
  val def = def |> CONV_RULE (DEPTH_CONV BETA_CONV)
  in def end

val _ = (find_def_for_const := def_of_const);

(* / for recursive translation *)

96
val _ = translate lookup_def;
97

98
val _ = translate subspt_eq;
Heiko Becker's avatar
Heiko Becker committed
99

100
val res = translate parseExp_def;
Heiko Becker's avatar
Heiko Becker committed
101

102 103 104 105 106
val parseexp_side_true = prove(
  ``!x. parseexp_side x = T``,
  recInduct parseExp_ind \\ rw []
  \\ once_rewrite_tac [fetch "-" "parseexp_side_def"] \\ rw [])
  |> update_precondition;
Heiko Becker's avatar
Heiko Becker committed
107

108
val res = translate dParse_def;
109

110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
(* improve function definitions a little *)

val const_1_over_2_pow_11_def = Define `
  const_1_over_2_pow_11 = 1 / 2 pow 11`

val const_1_over_2_pow_24_def = Define `
  const_1_over_2_pow_24 = 1 / 2 pow 24`

val const_1_over_2_pow_53_def = Define `
  const_1_over_2_pow_53 = 1 / 2 pow 53`

val const_1_over_2_pow_11_eq = EVAL ``const_1_over_2_pow_11``;
val const_1_over_2_pow_24_eq = EVAL ``const_1_over_2_pow_24``;
val const_1_over_2_pow_53_eq = EVAL ``const_1_over_2_pow_53``;

val _ = translate const_1_over_2_pow_11_eq;
val _ = translate const_1_over_2_pow_24_eq;
val _ = translate const_1_over_2_pow_53_eq;

129
val _ = translate (MachineTypeTheory.mTypeToR_def
130 131 132 133
  |> REWRITE_RULE [GSYM const_1_over_2_pow_11_def,
                   GSYM const_1_over_2_pow_24_def,
                   GSYM const_1_over_2_pow_53_def]);

134 135 136 137 138 139 140 141
(* val isMorePrecise_eq = prove( *)
(*   ``isMorePrecise m1 m2 = *)
(*     case m1 of *)
(*     | REAL => T *)
(*     | M64 => (case m2 of REAL => F | _ => T) *)
(*     | M32 => (case m2 of REAL => F | M64 => F | _ => T) *)
(*     | M16 => (case m2 of M16 => T | _ => F)``, *)
(*   Cases_on `m1` \\ Cases_on `m2` \\ EVAL_TAC); *)
142

143
(* val _ = translate isMorePrecise_eq; *)
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167

fun LET_CONV var_name body =
  (UNBETA_CONV body THENC
   RATOR_CONV (ALPHA_CONV (mk_var(var_name, type_of body))) THENC
   REWR_CONV (GSYM LET_THM));

val absIntvUpd_eq =
  IntervalArithTheory.absIntvUpd_def
  |> SPEC_ALL
  |> CONV_RULE (RAND_CONV (LET_CONV "lo1" ``IVlo iv1`` THENC
                           LET_CONV "lo2" ``IVlo iv2`` THENC
                           LET_CONV "hi1" ``IVhi iv1`` THENC
                           LET_CONV "hi2" ``IVhi iv2``));

val addInterval_eq =
  IntervalArithTheory.addInterval_def
  |> REWRITE_RULE [absIntvUpd_eq]
val _ = translate addInterval_eq

val multInterval_eq =
  IntervalArithTheory.multInterval_def
  |> REWRITE_RULE [absIntvUpd_eq]
val _ = translate multInterval_eq

168 169 170
val maxValueREAL_def =
  let val tm = EVAL ``maxValue REAL`` |> concl |> rand in
  Define `maxValueREAL = ^tm` end |> translate;
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186

val maxValueM16_def =
  let val tm = EVAL ``maxValue M16`` |> concl |> rand in
  Define `maxValueM16 = ^tm` end |> translate;

val maxValueM32_def =
  let val tm = EVAL ``maxValue M32`` |> concl |> rand in
  Define `maxValueM32 = ^tm` end |> translate;

val maxValueM64_def =
  let val tm = EVAL ``maxValue M64`` |> concl |> rand in
  Define `maxValueM64 = ^tm` end |> translate;

val maxValue_eq = prove(
  ``maxValue m =
    case m of
187
    | REAL => maxValueREAL
188 189
    | M16 => maxValueM16
    | M32 => maxValueM32
190 191
    | M64 => maxValueM64
    | F w f => &(2 ** (w  1)  1) * &(2 ** maxExponent m)``,
192 193 194
  Cases_on `m` \\ EVAL_TAC)
  |> translate;

195 196 197
val minValue_posREAL_def =
  let val tm = EVAL ``minValue_pos REAL`` |> concl |> rand in
  Define `minValue_posREAL = ^tm` end |> translate;
198

199 200 201
val minValue_posM16_def =
  let val tm = EVAL ``minValue_pos M16`` |> concl |> rand in
  Define `minValue_posM16 = ^tm` end |> translate;
202

203 204 205
val minValue_posM32_def =
  let val tm = EVAL ``minValue_pos M32`` |> concl |> rand in
  Define `minValue_posM32 = ^tm` end |> translate;
206

207 208 209
val minValue_posM64_def =
  let val tm = EVAL ``minValue_pos M64`` |> concl |> rand in
  Define `minValue_posM64 = ^tm` end |> translate;
210

211 212
val minValue_pos_eq = prove(
  ``minValue_pos m =
213
    case m of
214 215 216 217 218
    | REAL => minValue_posREAL
    | M16 => minValue_posM16
    | M32 => minValue_posM32
    | M64 => minValue_posM64
    | F w f => 0``,
219 220 221
  Cases_on `m` \\ EVAL_TAC)
  |> translate;

Heiko Becker's avatar
Heiko Becker committed
222
val res = translate CertificateCheckerCmd_def;
223

224 225 226 227 228 229
val invertinterval_side_def = fetch "-" "invertinterval_side_def";

val divideinterval_side_def = fetch "-" "divideinterval_side_def";

val validintervalbounds_side_def = fetch "-" "validintervalbounds_side_def";

Heiko Becker's avatar
Heiko Becker committed
230 231 232 233 234 235 236 237 238
val validintervalboundscmd_side_def = fetch "-" "validintervalboundscmd_side_def";

val validerrorbound_side_def = fetch "-" "validerrorbound_side_def";

val validerrorboundcmd_side_def = fetch "-" "validerrorboundcmd_side_def";

val certificatecheckercmd_side_def = fetch "-" "certificatecheckercmd_side_def";

val precond_validIntervalbounds_true = prove (
239 240 241
  ``!e A P (dVars:num_set).
      (!v. v IN (domain dVars) ==>
        ?iv err.
Heiko Becker's avatar
Heiko Becker committed
242
          FloverMapTree_find (Var v) A = SOME (iv, err) /\
243 244
          valid iv) ==>
      validintervalbounds_side e A P dVars``,
245 246 247
  recInduct validIntervalbounds_ind
  \\ rw[]
  \\ once_rewrite_tac [validintervalbounds_side_def]
248 249 250
  \\ Cases_on `f` \\ fs []
  \\ rpt (qpat_x_assum `T` kall_tac)
  >- (once_rewrite_tac [GSYM noDivzero_def]
251 252
      \\ rpt strip_tac
      \\ rveq
Heiko Becker's avatar
Heiko Becker committed
253
      \\ rename1 `FloverMapTree_find e absenv = SOME (iv_e, err_e)`
254 255 256 257
      \\ `valid iv_e`
           by (drule validIntervalbounds_validates_iv
               \\ disch_then (qspecl_then [`e`, `P`] destruct)
               \\ fs[] \\ rveq \\ fs[])
258
      \\ once_rewrite_tac [invertinterval_side_def]
259 260
      \\ rpt (qpat_x_assum `!v. _` kall_tac)
      \\ fs [valid_def, noDivzero_def]
261
      \\ REAL_ASM_ARITH_TAC)
262
  >- (once_rewrite_tac [GSYM noDivzero_def]
263 264
      \\ rpt strip_tac
      \\ rveq
265 266
      \\ once_rewrite_tac [divideinterval_side_def]
      \\ once_rewrite_tac [invertinterval_side_def]
Heiko Becker's avatar
Heiko Becker committed
267
      \\ rename1 `FloverMapTree_find e0 absenv = SOME (iv_e, err_e)`
268 269 270 271 272 273 274
      \\ `valid iv_e`
           by (drule validIntervalbounds_validates_iv
               \\ disch_then (qspecl_then [`e0`, `P`] destruct)
               \\ fs[] \\ rveq \\ fs[])
      \\ once_rewrite_tac [invertinterval_side_def]
      \\ rpt (qpat_x_assum `!v. _` kall_tac)
      \\ fs [valid_def, noDivzero_def]
275
      \\ REAL_ASM_ARITH_TAC));
276

Heiko Becker's avatar
Heiko Becker committed
277
val precond_validIntervalboundsCmd_true = prove (
278 279 280
  ``!f A P (dVars:num_set).
      (!v. v IN (domain dVars) ==>
        ?iv err.
Heiko Becker's avatar
Heiko Becker committed
281
          FloverMapTree_find (Var v) A = SOME (iv, err) /\
282 283
          valid iv) ==>
      validintervalboundscmd_side f A P dVars``,
284 285
  recInduct validIntervalboundsCmd_ind
  \\ rpt strip_tac
286 287
  \\ once_rewrite_tac [validintervalboundscmd_side_def]
  \\ rpt strip_tac \\ fs []
288 289
  >- (irule precond_validIntervalbounds_true \\ fs [])
  >- (first_x_assum irule
290 291 292
      \\ rw []
      >- (imp_res_tac validIntervalbounds_validates_iv \\ fs [] \\ rfs [])
      >- (first_x_assum match_mp_tac \\ fs []))
293
  >- (irule precond_validIntervalbounds_true
294
      \\ fs []));
295

296
val precond_validErrorbound_true = prove (``
297 298 299
  !P f expTypes A (dVars:num_set).
      (!v. v IN (domain dVars) ==>
        ?iv err.
Heiko Becker's avatar
Heiko Becker committed
300
          FloverMapTree_find (Var v) A = SOME (iv, err) /\
301 302 303
          valid iv) /\
    validIntervalbounds f A P dVars ==>
    validerrorbound_side f expTypes A dVars ``,
304 305 306 307 308 309
  gen_tac
  \\ recInduct validErrorbound_ind
  \\ rpt gen_tac
  \\ fs[AND_IMP_INTRO]
  \\ disch_then ASSUME_TAC
  \\ once_rewrite_tac [validerrorbound_side_def]
310
  \\ once_rewrite_tac [GSYM noDivzero_def]
311
  \\ rpt gen_tac \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
312
  \\ rpt gen_tac
313 314 315
  \\ disch_then ASSUME_TAC
  \\ rpt gen_tac
  \\ rpt (disch_then assume_tac)
316 317
  \\ rpt gen_tac
  \\ conj_tac
318
  >- (rpt strip_tac
319 320 321
      \\ rveq
      \\ fs[]
      \\ first_x_assum irule
Heiko Becker's avatar
Heiko Becker committed
322
      \\ Flover_compute ``validIntervalbounds``)
323
  \\ conj_tac
324 325
  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ conj_tac
326
      >- (conj_tac \\ rpt strip_tac \\ first_x_assum match_mp_tac
327
          \\ fs [Once validIntervalbounds_def])
328 329 330 331 332 333 334 335 336
      \\ disch_then assume_tac
      \\ rpt gen_tac
      \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ rpt gen_tac
      \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ rpt (disch_then ASSUME_TAC)
      \\ ntac 2 (rpt gen_tac \\ rpt (disch_then assume_tac))
      \\ rveq
      \\ rename1 `Binop Div e1 e2`
Heiko Becker's avatar
Heiko Becker committed
337 338
      \\ rename1 `FloverMapTree_find e1 A = SOME (iv_e1, err1)`
      \\ rename1 `FloverMapTree_find e2 A = SOME (iv_e2, err2)`
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
      \\ rewrite_tac [divideinterval_side_def, widenInterval_def,
                  minAbsFun_def, invertinterval_side_def, IVlo_def,
                  IVhi_def]
      \\ `valid iv_e1 /\ valid iv_e2`
           by (conj_tac \\ drule validIntervalbounds_validates_iv
               >- (disch_then (qspecl_then [`e1`, `P`] destruct)
                   \\ fs [Once validIntervalbounds_def] \\ rveq \\ fs[])
               \\ disch_then (qspecl_then [`e2`, `P`] destruct)
               \\ fs [Once validIntervalbounds_def] \\ rveq \\ fs[])
      \\ qpat_x_assum `!v. _` kall_tac
      \\ `0 <= err2`
           by (drule err_always_positive
               \\ disch_then (fn thm => qspecl_then [`iv_e2`, `err2`] match_mp_tac thm)
               \\ fs [])
      \\ `FST iv_e2 - err2 <> 0 /\ SND iv_e2 + err2 <> 0`
         by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
             \\ conj_tac \\ REAL_ASM_ARITH_TAC)
      \\ `noDivzero (SND iv_e2) (FST iv_e2)`
         by (drule validIntervalbounds_noDivzero_real
             \\ fs [])
      \\ `abs (FST iv_e2 - err2) <> 0 /\ abs (SND iv_e2 + err2) <> 0`
         by (REAL_ASM_ARITH_TAC)
      \\ `min (abs (FST iv_e2 - err2)) (abs (SND iv_e2 + err2)) <> 0`
         by (fs [min_def]
             \\ Cases_on `abs (FST iv_e2 - err2) <= abs (SND iv_e2 + err2)`
             \\ fs [] \\ REAL_ASM_ARITH_TAC)
      \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
      \\ REAL_ASM_ARITH_TAC)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
367
  \\ conj_tac
368 369
  >- (rpt strip_tac
      \\ rveq
Heiko Becker's avatar
Heiko Becker committed
370
      \\ Flover_compute ``validIntervalbounds``
371
      \\ first_x_assum irule \\ fs[])
372
  \\ rpt strip_tac
Heiko Becker's avatar
Heiko Becker committed
373
  \\ rveq \\ Flover_compute ``validIntervalbounds``
374
  \\ first_x_assum irule \\ fs[]);
375 376

val precond_errorbounds_true = prove (``
377 378 379
  !P f expTypes A dVars.
    (!v. v IN (domain dVars) ==>
      ?iv err.
Heiko Becker's avatar
Heiko Becker committed
380
        FloverMapTree_find (Var v) A = SOME (iv, err) /\
381 382 383
        valid iv) /\
    validIntervalboundsCmd f A P dVars ==>
    validerrorboundcmd_side f expTypes A dVars``,
384 385 386 387
  gen_tac
  \\ recInduct validErrorboundCmd_ind
  \\ rpt strip_tac
  \\ once_rewrite_tac [validerrorboundcmd_side_def]
388
  \\ Cases_on `f` \\ fs [Once validIntervalboundsCmd_def]
389
  >- (rpt strip_tac
390 391
      >- (irule precond_validErrorbound_true \\ fs[]
          \\ qexists_tac `P` \\ fs [])
392 393 394 395 396 397 398 399 400 401 402
      \\ first_x_assum irule
      \\ rpt (conj_tac)
      \\ fs[]
      >- (gen_tac
          \\ Cases_on `v = n` \\ fs[]
          \\ rveq
          \\ drule validIntervalbounds_validates_iv
          \\ disch_then drule \\ fs[])
      \\ Cases_on `c` \\ fs [Once validIntervalboundsCmd_def])
  \\ irule precond_validErrorbound_true \\ fs[]
  \\ qexists_tac `P` \\ fs []);
403

404
val precond_is_true = prove (
405 406
  ``!f absenv P expTypes.
      certificatecheckercmd_side f absenv P expTypes``,
407
   once_rewrite_tac [certificatecheckercmd_side_def]
408
   \\ rpt gen_tac
409
   \\ strip_tac
410
   \\ conj_tac
411
   >- (irule precond_validIntervalboundsCmd_true
412
       \\ fs [])
413
   >- (strip_tac \\ irule precond_errorbounds_true \\ fs[]
414 415
       \\ qexists_tac `P` \\ fs []))
  |> update_precondition;
Heiko Becker's avatar
Heiko Becker committed
416

417 418 419
val res = translate str_of_num_def;

val str_of_num_side_def = fetch "-" "str_of_num_side_def";
420

421 422 423 424 425 426 427 428 429
val str_of_num_side_true = prove (``!a. str_of_num_side a``,
recInduct str_of_num_ind
\\ rpt strip_tac \\ simp [str_of_num_side_def]
\\ rpt strip_tac
\\ `n MOD 10 < 10` by (match_mp_tac MOD_LESS \\ fs [])
\\ match_mp_tac LESS_TRANS
\\ qexists_tac `10 + 48` \\ fs []) |> update_precondition;

val res = translate runChecker_def;
430

Heiko Becker's avatar
Heiko Becker committed
431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
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]);

446
(* -- I/O routines from here onwards -- *)
447 448 449

val main = process_topdecs`
  fun main u =
Heiko Becker's avatar
Heiko Becker committed
450 451 452 453 454 455 456
    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;
457

Heiko Becker's avatar
Heiko Becker committed
458
(* val res = ml_prog_update(ml_progLib.add_prog main I) *)
459 460
val st = get_ml_prog_state()

Heiko Becker's avatar
Heiko Becker committed
461 462 463 464
(* Specification of the runchecker function:
   Running the checker on an input file inp appends the result of running
   the function to STDOUT *)

465
val main_spec = Q.store_thm("main_spec",
Heiko Becker's avatar
Heiko Becker committed
466 467 468 469 470 471 472 473 474 475 476 477
  `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)`, *)
478
  xcf "main" st
Heiko Becker's avatar
Heiko Becker committed
479
  \\ xlet_auto
480
  >- (xcon \\ xsimpl \\ EVAL_TAC)
Heiko Becker's avatar
Heiko Becker committed
481 482
  \\ xlet_auto
  >- (xsimpl \\ qexistsl_tac [`STDIO fs`, `cl`]
483
      \\ xsimpl)
Heiko Becker's avatar
Heiko Becker committed
484 485 486 487 488 489 490 491 492
  \\ 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])`
493
  >- (xapp \\ instantiate \\ xsimpl)
Heiko Becker's avatar
Heiko Becker committed
494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520
  \\ 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)))
521 522
  \\ xsimpl);

Heiko Becker's avatar
Heiko Becker committed
523
val (sem_thm,prog_tm) = whole_prog_thm (get_ml_prog_state ()) "main" (UNDISCH main_whole_prog_spec);
524

Heiko Becker's avatar
Heiko Becker committed
525
val main_prog_def = Define `main_prog = ^prog_tm`;
526

Heiko Becker's avatar
Heiko Becker committed
527 528 529 530 531
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";
532

Magnus Myreen's avatar
Magnus Myreen committed
533
val _ = export_theory();