Theory EPAC_Efficient_Checker_MLton

(*
  File:         PAC_Checker_MLton.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory EPAC_Efficient_Checker_MLton
  imports EPAC_Efficient_Checker_Synthesis
begin
local_setup ‹
  let
    val version =
      trim_line (#1 (Isabelle_System.bash_output ("cd $ISAFOL/ && git rev-parse --short HEAD || echo unknown")))
  in
    Local_Theory.define
      ((\<^binding>‹version›, NoSyn),
        ((\<^binding>‹version_def›, []), HOLogic.mk_literal version)) #> #2
  end
›

declare version_def [code]

definition uint32_of_uint64 :: ‹uint64 ⇒ uint32› where
  ‹uint32_of_uint64 n = uint32_of_nat (nat_of_uint64 n)›

lemma [code]: ‹hashcode n = uint32_of_uint64 (n AND 4294967295)› for n :: uint64
  unfolding hashcode_uint64_def uint32_of_uint64_def by auto

(*TODO this is a copy paste because of the order of the merge *)
code_printing code_module Uint64 ⇀ (SML) ‹(* Test that words can handle numbers between 0 and 63 *)
val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6"));

structure Uint64 : sig
  eqtype uint64;
  val zero : uint64;
  val one : uint64;
  val fromInt : IntInf.int -> uint64;
  val toInt : uint64 -> IntInf.int;
  val toFixedInt : uint64 -> Int.int;
  val toLarge : uint64 -> LargeWord.word;
  val fromLarge : LargeWord.word -> uint64
  val fromFixedInt : Int.int -> uint64
  val toWord32: uint64 -> Word32.word
  val plus : uint64 -> uint64 -> uint64;
  val minus : uint64 -> uint64 -> uint64;
  val times : uint64 -> uint64 -> uint64;
  val divide : uint64 -> uint64 -> uint64;
  val modulus : uint64 -> uint64 -> uint64;
  val negate : uint64 -> uint64;
  val less_eq : uint64 -> uint64 -> bool;
  val less : uint64 -> uint64 -> bool;
  val notb : uint64 -> uint64;
  val andb : uint64 -> uint64 -> uint64;
  val orb : uint64 -> uint64 -> uint64;
  val xorb : uint64 -> uint64 -> uint64;
  val shiftl : uint64 -> IntInf.int -> uint64;
  val shiftr : uint64 -> IntInf.int -> uint64;
  val shiftr_signed : uint64 -> IntInf.int -> uint64;
  val set_bit : uint64 -> IntInf.int -> bool -> uint64;
  val test_bit : uint64 -> IntInf.int -> bool;
end = struct

type uint64 = Word64.word;

val zero = (0wx0 : uint64);

val one = (0wx1 : uint64);

fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);

fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);

fun toFixedInt x = Word64.toInt x;

fun fromLarge x = Word64.fromLarge x;

fun fromFixedInt x = Word64.fromInt x;

fun toLarge x = Word64.toLarge x;

fun toWord32 x = Word32.fromLarge x

fun plus x y = Word64.+(x, y);

fun minus x y = Word64.-(x, y);

fun negate x = Word64.~(x);

fun times x y = Word64.*(x, y);

fun divide x y = Word64.div(x, y);

fun modulus x y = Word64.mod(x, y);

fun less_eq x y = Word64.<=(x, y);

fun less x y = Word64.<(x, y);

fun set_bit x n b =
  let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word64.orb (x, mask)
     else Word64.andb (x, Word64.notb mask)
  end

fun shiftl x n =
  Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0

val notb = Word64.notb

fun andb x y = Word64.andb(x, y);

fun orb x y = Word64.orb(x, y);

fun xorb x y = Word64.xorb(x, y);

end (*struct Uint64*)
›

code_printing constant arl_get_u' ⇀ (SML) "(fn/ ()/ =>/ Array.sub/ ((fn/ (a,b)/ =>/ a) ((_)),/ Word64.toInt (Uint64.toLarge ((_)))))"

definition uint32_of_uint64' where
  [symmetric, code]: "uint32_of_uint64' = uint32_of_uint64"
code_printing constant uint32_of_uint64' ⇀ (SML) "Uint64.toWord32 ((_))"
thm hashcode_literal_def[unfolded hashcode_list_def]

definition string_nth where
  ‹string_nth s x = literal.explode s ! x›

definition string_nth' where
  ‹string_nth' s x = literal.explode s ! nat x›

lemma [code]: ‹string_nth s x = string_nth' s (int x)›
  unfolding string_nth_def string_nth'_def
  by auto

definition string_size :: ‹String.literal⇒nat› where
  ‹string_size s = size s›

definition string_size' where
  [symmetric,code]: ‹string_size' = string_size›

lemma [code]: ‹size = string_size›
  unfolding string_size_def ..

code_printing constant string_nth' ⇀ (SML) "(String.sub/ ((_),/ IntInf.toInt ((integer'_of'_int ((_))))))"
code_printing constant string_size' ⇀ (SML) "nat'_of'_integer ((IntInf.fromInt ((String.size ((_))))))"

function hashcode_eff where 
  [simp del]: ‹hashcode_eff s h i = (if i ≥ size s then h else hashcode_eff s (h * 33 + hashcode (s ! i)) (i+1))›
  by auto
termination
  by (relation ‹measure (λ(s,h,i). size s -i)›)
    auto

definition hashcode_eff' where
  ‹hashcode_eff' s h i = hashcode_eff (String.explode s) h i›

lemma hashcode_eff'_code[code]:
   ‹hashcode_eff' s h i = (if i ≥ size s then h else hashcode_eff' s (h * 33 + hashcode (string_nth s i)) (i+1))›
  unfolding hashcode_eff'_def string_nth_def  hashcode_eff.simps[symmetric] size_literal.rep_eq
  ..

lemma [simp]: ‹length s ≤ i ⟹ hashcode_eff s h i = h›
  by (subst hashcode_eff.simps)
   auto
lemma [simp]: ‹hashcode_eff (a # s) h (Suc i) = hashcode_eff (s) h (i)›
  apply (induction "s" h "i" rule: hashcode_eff.induct)
  subgoal
    apply (subst (2) hashcode_eff.simps)
    apply (subst (1) hashcode_eff.simps)
    apply auto
    done
  done


lemma hashcode_eff_def[unfolded hashcode_eff'_def[symmetric], code]:
  ‹hashcode s = hashcode_eff (String.explode s)5381 0› for s::String.literal
proof -
  have H: ‹length (literal.explode s) = size s›
    by (simp add: size_literal.rep_eq)
  have [simp]: ‹foldl (λh xa. h * 33 + hashcode ((xs @ [x]) ! xa)) 5381 [0..<length xs] =
    foldl (λh x. h * 33 + hashcode (xs ! x)) 5381 [0..<length xs]› for xs x
    by (rule foldl_cong) auto
  have ‹foldl (λh x. h * 33 + hashcode x) 5381 (s) =
    foldl (λh x. h * 33 + hashcode (s ! x)) 5381
     [0..<length (s)]› for s
    by (induction s rule: rev_induct) auto
  then have 0: ‹hashcode s = foldl (λh x. h * 33 + hashcode (string_nth s x)) 5381 [0..<size s]›
    unfolding string_nth_def
    unfolding hashcode_literal_def[unfolded hashcode_list_def] size_literal.rep_eq
    by blast

  have upt: ‹¬ Suc (length s) ≤ i ⟹ [i..<Suc (length s)] = i # [Suc i..<Suc (length s)]› for i s
    by (meson leI upt_rec)

  have [simp]: ‹foldl (λh x. h * 33 + hashcode ((a # s) ! x)) h [Suc i..<Suc (length s)] =
    foldl (λh x. h * 33 + hashcode (s ! x)) h [i..<(length s)]› for a s i h
  proof -
    have ‹foldl (λh x. h * 33 + hashcode ((a # s) ! x)) h [Suc i..<Suc (length s)] = 
      foldl (λh x. h * 33 + hashcode ((a # s) ! x)) h (map Suc [i..<(length s)])›
      using map_Suc_upt by presburger
    also have ‹… = foldl (λaa x. aa * 33 + hashcode (s ! x)) h [i..<length s]›
      unfolding foldl_map by (rule foldl_cong) auto
    finally show ?thesis .
  qed
   
  have H': ‹foldl (λh x. h * 33 + hashcode (s ! x)) h [i..<length s] =
    hashcode_eff s h i› for i h s
    unfolding string_nth_def H[symmetric]
    supply [simp del] = upt.simps
    apply (induction ‹s› arbitrary: h)
    subgoal
      by (subst hashcode_eff.simps)
       auto
    subgoal
      by (subst hashcode_eff.simps)
       (auto simp: upt)
    done
  show ?thesis
    unfolding 0 H[symmetric] string_nth_def H'
    ..
qed

export_code "hashcode :: String.literal ⇒ _" 
  in SML_imp module_name PAC_Checker
(*make array_blit compatible with unsafe*)
code_printing code_module "array_blit" ⇀ (SML)
    ‹
   fun array_blit src si dst di len = (
      src=dst andalso raise Fail ("array_blit: Same arrays");
      ArraySlice.copy {
        di = IntInf.toInt di,
        src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)),
        dst = dst})

    fun array_nth_oo v a i () = if IntInf.toInt i >= Array.length a then v 
       else Array.sub(a,IntInf.toInt i) handle Overflow => v
    fun array_upd_oo f i x a () = 
      if IntInf.toInt i >= Array.length a then f ()
      else
        (Array.update(a,IntInf.toInt i,x); a) handle Overflow => f ()

›

text ‹This is a hack for performance. There is no need to recheck that that a char is valid when
  working on chars coming from strings... It is not that important in most cases, but in our case
  the preformance difference is really large.›


definition unsafe_asciis_of_literal :: ‹_› where
  ‹unsafe_asciis_of_literal xs = String.asciis_of_literal xs›

definition unsafe_asciis_of_literal' :: ‹_› where
  [simp, symmetric, code]: ‹unsafe_asciis_of_literal' = unsafe_asciis_of_literal›

code_printing
  constant unsafe_asciis_of_literal' ⇀
    (SML) "!(List.map (fn c => let val k = Char.ord c in IntInf.fromInt k end) /o String.explode)"

text ‹
  Now comes the big and ugly and unsafe hack.

  Basically, we try to avoid the conversion to IntInf when calculating the hash. The performance
  gain is roughly 40\%, which is a LOT and definitively something we need to do. We are aware that the
  SML semantic encourages compilers to optimise conversions, but this does not happen here,
  corroborating our early observation on the verified SAT solver IsaSAT.x
›
definition raw_explode where
  [simp]: ‹raw_explode = String.explode›
code_printing
  constant raw_explode ⇀
    (SML) "String.explode"

lemmas [code] =
  hashcode_literal_def[unfolded String.explode_code
    unsafe_asciis_of_literal_def[symmetric]]

definition uint32_of_char where
  [symmetric, code_unfold]: ‹uint32_of_char x = uint32_of_int (int_of_char x)›


code_printing
  constant uint32_of_char ⇀
    (SML) "!(Word32.fromInt /o (Char.ord))"

lemma [code]: ‹hashcode s = hashcode_literal' s›
  unfolding hashcode_literal_def hashcode_list_def
  apply (auto simp: unsafe_asciis_of_literal_def hashcode_list_def
     String.asciis_of_literal_def hashcode_literal_def hashcode_literal'_def)
  done

export_code
    full_checker_l_s2_impl int_of_integer Del CL nat_of_integer String.implode remap_polys_l2_with_err_s_impl
    PAC_update_impl PAC_empty_impl the_error is_cfailed is_cfound
    fully_normalize_poly_impl empty_shared_vars_int_impl
    PAC_checker_l_s_impl PAC_checker_l_step_s_impl version
  in SML_imp module_name PAC_Checker
  file_prefix "checker"


compile_generated_files _
  external_files
    ‹code/parser.sml›
    ‹code/pasteque.sml›
    ‹code/pasteque.mlb›
  where ‹fn dir =>
  let

    val exec = Generated_Files.execute (Path.append dir (Path.basic "code"));
    val _ = exec ‹Copy files›
      ("cp checker.ML " ^ ((File.bash_path \<^path>‹$ISAFOL›) ^ "/PAC_Checker2/code/checker.ML"));
    val _ =
        exec ‹Compilation›
          (File.bash_path \<^path>‹$ISABELLE_MLTON› ^ " " ^
            "-const 'MLton.safe false' -verbose 1 -default-type int64 -output pasteque " ^
            "-codegen native -inline 700 -cc-opt -O3 pasteque.mlb");
    in () end› 

end