open preamble
open simpLib realTheory realLib RealArith stringTheory

open ml_translatorTheory ml_translatorLib realProgTheory cfTacticsLib ioProgLib

open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
     ErrorBoundsTheory IntervalArithTheory DaisyTactics IntervalValidationTheory
     EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory
     CertificateCheckerTheory daisyParserTheory

val _ = new_theory "trans";

val _ = translation_extends "realProg";

val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);

val check_rec_def = Define `
  check_rec (input:Token list) (num_fun:num)=
  case num_fun of
    | SUC n' =>
      (case dParse input of
         | SOME ((dCmd, P, A, Gamma),NIL) =>
           if CertificateCheckerCmd dCmd A P Gamma
           then "True\n"
           else "False\n"
         | SOME ((dCmd, P, A, Gamma), residual) =>
           if CertificateCheckerCmd dCmd A P Gamma
           then check_rec residual n'
           else "False\n"
         | NONE => pp input(*"parse failure\n"*))
    | _ => "failure num of functions"`;

val check_def = Define `
check (f:real cmd) (P:precond) (A:analysisResult) Gamma (n:num) =
case n of
 | SUC n' => (CertificateCheckerCmd f A P Gamma /\ check f P A Gamma n')
 | _ => 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
          | SOME ((f,P,A, Gamma), residual) =>
            if (check f P A Gamma iters)
                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"`;

val runChecker_def = Define `
  runChecker (input:tvarN) =
    let tokList = lex input in
        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"`;

(* 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 *)

val _ = translate lookup_def;

val _ = translate subspt_eq;

val res = translate parseExp_def;

val parseexp_side_true = prove(
  ``!x. parseexp_side x = T``,
  recInduct parseExp_ind \\ rw []
  \\ once_rewrite_tac [fetch "-" "parseexp_side_def"] \\ rw [])
  |> update_precondition;

val res = translate dParse_def;

val res = translate CertificateCheckerCmd_def;

val invertinterval_side_def = fetch "-" "invertinterval_side_def";

val divideinterval_side_def = fetch "-" "divideinterval_side_def";

val validintervalbounds_side_def = fetch "-" "validintervalbounds_side_def";

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 (
  ``!e absenv P (dVars:num_set).
      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
      validintervalbounds_side e absenv P dVars``,
  recInduct validIntervalbounds_ind
  \\ rw[]
  \\ once_rewrite_tac [validintervalbounds_side_def]
  \\ Cases_on `f` \\ fs []
  \\ rpt (qpat_x_assum `T` kall_tac)
  >- (once_rewrite_tac [GSYM noDivzero_def]
      \\ rpt strip_tac
      \\ rveq
      \\ `valid (FST(absenv e))`
           by (irule validIntervalbounds_validates_iv
               \\ qexistsl_tac [`P`, `validVars`]
               \\ fs[])
      \\ once_rewrite_tac [invertinterval_side_def]
      \\ rw_asm `absenv e = _`
      \\ Cases_on `x2` \\ rename1 `absenv e = ((elo,ehi),err)`
      \\ qpat_x_assum `!v. _` kall_tac
      \\ qpat_x_assum `!intv. _` kall_tac
      \\ fs [IVlo_def, IVhi_def, valid_def, noDivzero_def]
      \\ REAL_ASM_ARITH_TAC)
  >- (once_rewrite_tac [GSYM noDivzero_def]
      \\ rpt strip_tac
      \\ rveq
      \\ once_rewrite_tac [divideinterval_side_def]
      \\ once_rewrite_tac [invertinterval_side_def]
      \\ `valid (FST(absenv e0))`
           by (irule validIntervalbounds_validates_iv
               \\ qexistsl_tac [`P`, `validVars`]
               \\ fs[])
      \\ Cases_on `x4` \\ rename1 `absenv e0 = ((elo,ehi),err)`
      \\ qpat_x_assum `!v. _` kall_tac
      \\ rpt (qpat_x_assum `!intv. _` kall_tac)
      \\ qpat_x_assum `absenv e0 = _` (fn thm => fs [thm])
      \\ fs [IVlo_def, IVhi_def, valid_def, noDivzero_def]
      \\ REAL_ASM_ARITH_TAC));

val precond_validIntervalboundsCmd_true = prove (
  ``!f absenv P (dVars:num_set).
      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
      validintervalboundscmd_side f absenv P dVars``,
  recInduct validIntervalboundsCmd_ind
  \\ rpt strip_tac
  \\ once_rewrite_tac [validintervalboundscmd_side_def]
  \\ rpt strip_tac \\ fs []
  >- (irule precond_validIntervalbounds_true \\ fs [])
  >- (first_x_assum irule
      \\ rw []
      >- (imp_res_tac validIntervalbounds_validates_iv \\ fs [] \\ rfs [])
      >- (first_x_assum match_mp_tac \\ fs []))
  >- (irule precond_validIntervalbounds_true
      \\ fs []));

val precond_validErrorbound_true = prove (``
  !P f expTypes absenv (dVars:num_set).
    (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) /\
    validIntervalbounds f absenv P dVars ==>
    validerrorbound_side f expTypes absenv dVars ``,
  gen_tac
  \\ recInduct validErrorbound_ind
  \\ rpt gen_tac
  \\ fs[AND_IMP_INTRO]
  \\ disch_then ASSUME_TAC
  \\ once_rewrite_tac [validerrorbound_side_def]
  \\ once_rewrite_tac [GSYM noDivzero_def]
  \\ rpt gen_tac \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
  \\ rpt gen_tac
  \\ ntac 2 (disch_then ASSUME_TAC)
  \\ rpt gen_tac
  \\ conj_tac
  >- (rpt strip_tac
      \\ rveq
      \\ fs[]
      \\ first_x_assum irule
      \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
      \\ rw_asm_star `absenv _ = _`
      \\ Cases_on `absenv x15`
      \\ fs [])
  \\ conj_tac
  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ conj_tac
      >- (conj_tac \\ first_x_assum match_mp_tac
          \\ fs [Once validIntervalbounds_def])
      >- (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)
          \\ rveq
          \\ rename1 `absenv (Binop Div e1 e2) = (ivDiv, errDiv)`
          \\ rename1 `absenv e1 = (ive1,err1)`
          \\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
          \\ rename1 `absenv e2 = (ive2,err2)`
          \\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
          \\ rewrite_tac [divideinterval_side_def, widenInterval_def, minAbsFun_def, invertinterval_side_def, IVlo_def, IVhi_def]
          \\ `valid (FST(absenv e1)) /\ valid (FST(absenv e2))`
               by (conj_tac \\ drule validIntervalbounds_validates_iv
                   >- (disch_then match_mp_tac
                       \\ qexists_tac `P`
                       \\ fs [Once validIntervalbounds_def])
                   >- (disch_then match_mp_tac
                       \\ qexists_tac `P`
                       \\ fs [Once validIntervalbounds_def]))
          \\ rw_asm `absenv e1 = _`
          \\ rw_asm `absenv e2 = _`
          \\ qpat_x_assum `!v. _` kall_tac
          \\ `0 <= err2`
               by (drule err_always_positive
                 \\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
                 \\ fs [])
        \\ `e2lo - err2 <> 0 /\ e2hi + err2 <> 0`
             by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
                 \\ conj_tac \\ REAL_ASM_ARITH_TAC)
        \\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
             by (drule validIntervalbounds_noDivzero_real
                 \\ fs [])
        \\ `abs (e2lo - err2) <> 0 /\ abs (e2hi + err2) <> 0`
             by (REAL_ASM_ARITH_TAC)
        \\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) <> 0`
             by (fs [min_def]
                 \\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
                 \\ fs [] \\ REAL_ASM_ARITH_TAC)
        \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
        \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
        \\ REAL_ASM_ARITH_TAC))
  \\ conj_tac
  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ rpt conj_tac \\ first_x_assum match_mp_tac
          \\ fs [Once validIntervalbounds_def])
  \\ rpt strip_tac
  \\ rveq
  \\ fs[]
  \\ first_x_assum irule
  \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
  \\ rw_asm_star `absenv _ = _`
  \\ rw_asm_star `absenv (Downcast _ _) = _`);

val precond_errorbounds_true = prove (``
  !P f expTypes absenv dVars.
    (!v. v IN domain dVars ==> valid (FST (absenv (Var v)))) /\
    validIntervalboundsCmd f absenv P dVars ==>
    validerrorboundcmd_side f expTypes absenv dVars``,
  gen_tac
  \\ recInduct validErrorboundCmd_ind
  \\ rpt strip_tac
  \\ once_rewrite_tac [validerrorboundcmd_side_def]
  \\ Cases_on `f` \\ fs [Once validIntervalboundsCmd_def]
  >- (rpt strip_tac
      >- (irule precond_validErrorbound_true \\ fs[]
          \\ qexists_tac `P` \\ fs [])
      >- (first_x_assum irule
          \\ rpt (conj_tac)
          \\ fs[]
          >- (gen_tac
              \\ Cases_on `v = n` \\ fs[]
              \\ rveq
              \\ rw_sym_asm `env e = _`
              \\ drule validIntervalbounds_validates_iv
              \\ disch_then drule \\ fs[])
          >- (Cases_on `c` \\ fs [Once validIntervalboundsCmd_def])))
  >- (irule precond_validErrorbound_true \\ fs[]
      \\ qexists_tac `P` \\ fs []));

val precond_is_true = prove (
  ``!f absenv P expTypes.
      certificatecheckercmd_side f absenv P expTypes``,
   once_rewrite_tac [certificatecheckercmd_side_def]
   \\ rpt gen_tac
   \\ strip_tac
   \\ conj_tac
   >- (irule precond_validIntervalboundsCmd_true
       \\ fs [])
   >- (strip_tac \\ irule precond_errorbounds_true \\ fs[]
       \\ qexists_tac `P` \\ fs []))
  |> update_precondition;

val res = translate str_of_num_def;

val str_of_num_side_def = fetch "-" "str_of_num_side_def";

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;

(* -- I/O routines 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 * 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`
  >- (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`]
      \\ 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[`STDERR err * 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();