(*
 * Copyright 2018, Data61
 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
 * ABN 41 687 119 230.
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)

(* Preprocess AutoCorres translation of Cogent compiler's output code. *)
theory Tidy
  imports
    "AutoCorres.AutoCorres"
    "Cogent.ML_Old"
begin

(* Each Cogent_Corres rule expects (at most) one guard *)
lemma join_guards:
  "do g1 <- guard G1; g2 <- guard G2; P g1 g2 od
    =
   do g1 <- guard (\<lambda>s. G1 s \<and> G2 s); P g1 g1 od"
  by monad_eq

(* C-parser function epilogue *)
lemma return_exn_simp:
  "do ret <- A;
      _ <- gets (\<lambda>_. x :: c_exntype);
      _ <- gets (\<lambda>_. ());
      gets (\<lambda>_. ret) od = A"
  by simp

(* Cogent function epilogue *)
lemma return_cogent_simp:
  "do a \<leftarrow> A;
      r \<leftarrow> gets (\<lambda>_. a);
      gets (\<lambda>_. r) od = A"
  by simp

lemma simp_unit_return:
  "\<And>A. (do (x::unit) \<leftarrow> A; gets (\<lambda>_. ()) od) = A"
  by simp

(* Compose variant constructor with the gets immediately after it *)
(* TODO: this should be more specific, and only instantiated when variant_init is an actual variant constructor *)
lemma compose_gets_variant_con:
  "do a \<leftarrow> select UNIV;
      b \<leftarrow> gets (\<lambda>_. payload_update (\<lambda>_. payload) (tag_update (\<lambda>_. tag) variant_init));
      c \<leftarrow> gets (\<lambda>_. b);
      A c
   od =
   do
      b \<leftarrow> gets (\<lambda>_. payload_update (\<lambda>_. payload) (tag_update (\<lambda>_. tag) variant_init));
      A b
  od"
  by monad_eq
lemma compose_gets_variant_con_2:
  "do a \<leftarrow> select UNIV;
      b \<leftarrow> gets (\<lambda>_. payload_update (\<lambda>_. payload) (tag_update (\<lambda>_. tag) variant_init));
      gets (\<lambda>_. b)
   od =
      gets (\<lambda>_. payload_update (\<lambda>_. payload) (tag_update (\<lambda>_. tag) variant_init))"
  by monad_eq

(* Cogent compiler adds one assignment at the end of every block; remove it *)
definition "simp_last_bind = id"

lemma simp_last_bind:
  "\<And>A B C. simp_last_bind (do x \<leftarrow> A; y \<leftarrow> B x; C x y od) = do x \<leftarrow> A; simp_last_bind (do y \<leftarrow> B x; C x y od) od"
  "\<And>A. simp_last_bind (do x \<leftarrow> A; gets (\<lambda>_. x) od) = A"
  "\<And>A. simp_last_bind A = A"
  by (simp_all add: simp_last_bind_def)

lemma simp_last_bindI:
  "simp_last_bind A = B \<Longrightarrow> A = B"
  by (simp add: simp_last_bind_def)
lemma simp_last_bind_recI:
  "condition C (simp_last_bind L) R = B \<Longrightarrow> condition C L R = B"
  by (simp add: simp_last_bind_def)

(* Simplify uninitialised variables. *)
lemma unknown_bind_ignore:
  "select UNIV >>= (\<lambda>_. A) = A"
  by monad_eq

(* The True condition will also be instantiated with LET_TRUE and LET_BANG_TRUE per program *)
lemma unknown_bind_if_True:
  "do x \<leftarrow> select UNIV;
      condition (\<lambda>_. True) T (F x) >>= R od
   = condition (\<lambda>_. True) T (F undefined) >>= R"
  by monad_eq

ML \<open>
fun tidy_C_fun_def f ctxt = let
  val fun_term = Syntax.read_term ctxt (f ^ "'")
  (* Guess whether the function is recursive.
   * FIXME: use AutoCorresFunctionInfo instead *)
  val ([fun_def], fun_rec) = (Proof_Context.get_thms ctxt (f ^ "'.simps"), true)
                             handle ERROR _ => (Proof_Context.get_thms ctxt (f ^ "'_def"), false)

  (* Helper theorems for LET_TRUE and LETBANG_TRUE, if they exist *)
  val unknown_bind_more_thms = ["LET_TRUE", "LETBANG_TRUE"]
        |> maps (fn c => case Syntax.read_term ctxt c of
                             c' as Const _ => [Goal.prove ctxt [] []
                                                (@{mk_term "True \<equiv> (?c \<noteq> 0)" (c)} c')
                                                (K (simp_tac (ctxt addsimps (Proof_Context.get_thms ctxt (c ^ "_def"))) 1))]
                           | _ => [])
        |> map (fn thm => Simplifier.rewrite_rule ctxt [thm] @{thm unknown_bind_if_True})

  (* Use a schematic lemma to rewrite AutoCorres function defs.
   * We can assume the Cogent compiler generates all functions with only one argument. *)
  val prop = if fun_rec then @{mk_term "Trueprop (?f m a = ?A)" f} fun_term
                        else @{mk_term "Trueprop (?f a = ?A)" f} fun_term

  fun subst thms = EqSubst.eqsubst_tac ctxt [0] thms 1

  (* clarsimp won't touch the schematic ?A *)
  fun subst' thms = Clasimp.clarsimp_tac (put_simpset HOL_basic_ss ctxt addsimps thms) 1

  val tacs = subst [fun_def] (* get function definition *)
             THEN subst' @{thms bind_assoc}          (* normalise binds *)
             THEN subst' @{thms join_guards}         (* normalise guards *)
             THEN subst' @{thms simp_thms(21-22,25)} (* simplify conj in guards *)
             THEN subst' @{thms guard_True_bind}     (* remove unnecessary guards *)
             THEN subst @{thms return_exn_simp}      (* remove C parser's function epilogue *)
             (* Remove exactly one bind-gets from the end of the program,
              * which is inserted by the Cogent code generator *)
             THEN rtac (if fun_rec then @{thm simp_last_bind_recI} else @{thm simp_last_bindI}) 1
             THEN subst' @{thms simp_last_bind(1-2) simp_unit_return}
             (* Cleanup any remaining @{term simp_last_bind}s *)
             THEN subst' @{thms simp_last_bind(3)}
             (* Compose variant constructor with the gets immediately after it *)
             THEN subst' @{thms compose_gets_variant_con compose_gets_variant_con_2}
             (* Simplify uninitialised variables *)
             THEN subst' (@{thms unknown_bind_ignore unknown_bind_if_True} @ unknown_bind_more_thms)
             THEN rtac @{thm refl} 1 (* final definition *)
  in Goal.prove ctxt (if fun_rec then ["m", "a"] else ["a"]) [] prop (K tacs) end

fun tidy_C_fun_def' f ctxt =
  Utils.define_lemmas (f ^ "'_def'") [tidy_C_fun_def f ctxt] ctxt |> snd
\<close>

end