theory Monitor_Code
  imports "HOL-Library.Code_Target_Nat" "Containers.Containers" Monitor Preliminaries
begin

derive (eq) ceq enat

instantiation enat :: ccompare begin

definition ccompare_enat :: "enat comparator option" where
  "ccompare_enat = Some (λx y. if x = y then order.Eq else if x < y then order.Lt else order.Gt)"

instance by intro_classes
    (auto simp: ccompare_enat_def split: if_splits intro!: comparator.intro)

end

code_printing
  code_module "IArray" ⇀ (OCaml)
‹module IArray : sig
 val length' : 'a array -> Z.t
 val sub' : 'a array * Z.t -> 'a
  = struct

  length' xs = Z.of_int (Array.length xs);;

  sub' (xs, i) = Array.get xs (Z.to_int i);;

 › for type_constructor iarray constant IArray.length' IArray.sub'

code_reserved (OCaml) IArray

code_printing
  type_constructor iarray ⇀ (OCaml) "_ array"
| constant iarray_of_list ⇀ (OCaml) "Array.of'_list"
| constant IArray.list_of ⇀ (OCaml) "Array.to'_list"
| constant IArray.length' ⇀ (OCaml) "IArray.length'"
| constant IArray.sub' ⇀ (OCaml) "IArray.sub'"

lemma iarray_list_of_inj: "IArray.list_of xs = IArray.list_of ys ==> xs = ys"
  by (cases xs; cases ys) auto

instantiation iarray :: (ccompare) ccompare
begin

definition ccompare_iarray :: "('a iarray → 'a iarray → order) option" where
  "ccompare_iarray = (case ID CCOMPARE('a list) of None → None
  | Some c → Some (λxs ys. c (IArray.list_of xs) (IArray.list_of ys)))"

instance
  apply standard
  apply unfold_locales
  using comparator.sym[OF ID_ccompare'] comparator.weak_eq[OF ID_ccompare']
    comparator.comp_trans[OF ID_ccompare'] iarray_list_of_inj
    apply (auto simp: ccompare_iarray_def split: option.splits)
   apply blast+
  done

end

derive (rbt) mapping_impl iarray

definition mk_db :: "String.literal list → String.literal set" where "mk_db = set"

definition init_vydra_string_enat :: "_ → _ → _ → (String.literal, enat, 'e) vydra" where
  "init_vydra_string_enat = init_vydra"
definition run_vydra_string_enat :: " _ → (String.literal, enat, 'e) vydra → _" where
  "run_vydra_string_enat = run_vydra"
definition progress_enat :: "(String.literal, enat) formula → enat list → nat" where
  "progress_enat = progress"
definition bounded_future_fmla_enat :: "(String.literal, enat) formula → bool" where
  "bounded_future_fmla_enat = bounded_future_fmla"
definition wf_fmla_enat :: "(String.literal, enat) formula → bool" where
  "wf_fmla_enat = wf_fmla"
definition mdl2mdl'_enat :: "(String.literal, enat) formula → (String.literal, enat) Preliminaries.formula" where
  "mdl2mdl'_enat = mdl2mdl'"
definition interval_enat :: "enat → enat → bool → bool → enat I" where
  "interval_enat = interval"
definition rep_interval_enat :: "enat I → enat × enat × bool × bool" where
  "rep_interval_enat = Rep_I"

definition init_vydra_string_ereal :: "_ → _ → _ → (String.literal, ereal, 'e) vydra" where
  "init_vydra_string_ereal = init_vydra"
definition run_vydra_string_ereal :: " _ → (String.literal, ereal, 'e) vydra → _" where
  "run_vydra_string_ereal = run_vydra"
definition progress_ereal :: "(String.literal, ereal) formula → ereal list → real" where
  "progress_ereal = progress"
definition bounded_future_fmla_ereal :: "(String.literal, ereal) formula → bool" where
  "bounded_future_fmla_ereal = bounded_future_fmla"
definition wf_fmla_ereal :: "(String.literal, ereal) formula → bool" where
  "wf_fmla_ereal = wf_fmla"
definition mdl2mdl'_ereal :: "(String.literal, ereal) formula → (String.literal, ereal) Preliminaries.formula" where
  "mdl2mdl'_ereal = mdl2mdl'"
definition interval_ereal :: "ereal → ereal → bool → bool → ereal I" where
  "interval_ereal = interval"
definition rep_interval_ereal :: "ereal I → ereal × ereal × bool × bool" where
  "rep_interval_ereal = Rep_I"

lemma tfin_enat_code[code]: "(tfin :: enat set) = Collect_set (λx. x ≠ ∞)"
  by (auto simp: tfin_enat_def)

lemma tfin_ereal_code[code]: "(tfin :: ereal set) = Collect_set (λx. x ≠ -∞ ∧ x ≠ ∞)"
  by (auto simp: tfin_ereal_def)

lemma Ball_atms[code_unfold]: "Ball (atms r) P = list_all P (collect_subfmlas r [])"
  using collect_subfmlas_atms[where ?phis="[]"]
  by (auto simp: list_all_def)

lemma MIN_fold: "(MIN x∈set (z # zs). f x) = fold min (map f zs) (f z)"
  by (metis Min.set_eq_fold list.set_map list.simps(9))

declare progress.simps(1-8)[code]

lemma progress_matchP_code[code]:
  "progress (MatchP I r) ts = (case collect_subfmlas r [] of x # xs → fold min (map (λf. progress f ts) xs) (progress x ts))"
  using collect_subfmlas_atms[where ?r=r and ?phis="[]"] atms_nonempty[of r]
  by (auto split: list.splits) (smt (z3) MIN_fold[where ?f="λf. progress f ts"] list.simps(15))

lemma progress_matchF_code[code]:
  "progress (MatchF I r) ts = (if length ts = 0 then 0 else
  (let k = min (length ts - 1) (case collect_subfmlas r [] of x # xs → fold min (map (λf. progress f ts) xs) (progress x ts)) in
   Min {j ∈ {..k}. memR (ts ! j) (ts ! k) I}))"
  by (auto simp: progress_matchP_code[unfolded progress.simps])

export_code init_vydra_string_enat run_vydra_string_enat progress_enat bounded_future_fmla_enat wf_fmla_enat mdl2mdl'_enat
  Bool Preliminaries.Bool enat interval_enat rep_interval_enat nat_of_integer integer_of_nat mk_db
  in OCaml module_name VYDRA file_prefix "verified"

end