theory Test1
imports "../thys/Uncomputable"
begin

ML {*
fun timing_wrapper tac st =
let
  val t_start = Timing.start ();
  val res = tac st;
  val t_end = Timing.result t_start;
in
  (tracing (Timing.message t_end); res)
end
*}


datatype abc_inst =
     Inc nat
   | Dec nat nat
   | Goto nat
  
type_synonym abc_prog = "abc_inst list"

datatype recf = 
  z 
| s 
| id nat nat              --"Projection"
| Cn nat recf "recf list" --"Composition"
| Pr nat recf recf        --"Primitive recursion"
| Mn nat recf             --"Minimisation"



fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
  where
  "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"

fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
  where
  "mv_box m n = [Dec m 3, Inc n, Goto 0]"

fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"
  where
  "abc_inst_shift (Inc m) n = Inc m" |
  "abc_inst_shift (Dec m e) n = Dec m (e + n)" |
  "abc_inst_shift (Goto m) n = Goto (m + n)"

fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" 
  where
  "abc_shift [] n = []"
| "abc_shift (x#xs) n = (abc_inst_shift x n) # (abc_shift xs n)" 

fun abc_append :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> abc_inst list" (infixl "[+]" 60)
  where
  "abc_append al bl = al @ abc_shift bl (length al)"

lemma [simp]: 
  "length (pa [+] pb) = length pa + length pb"
by (induct pb) (auto)


text {* The compilation of @{text "z"}-operator. *}
definition rec_ci_z :: "abc_inst list"
  where
   [simp]: "rec_ci_z = [Goto 1]"


text {* The compilation of @{text "s"}-operator. *}
definition rec_ci_s :: "abc_inst list"
  where
  "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"

lemma [simp]:
  "rec_ci_s = [Dec 0 4, Inc 1, Inc 2, Goto 0, Dec 2 7, Inc 0, Goto 4, Inc 1] "
by (simp add: rec_ci_s_def)

text {* The compilation of @{text "id i j"}-operator *}
fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
  where
  "rec_ci_id i j = addition j i (i + 1)"

fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
  where
  "mv_boxes ab bb n = (case n of 
      0 => [] 
    | Suc n => mv_boxes ab bb n [+] mv_box (ab + n) (bb + n))"

fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
  where
  "empty_boxes n = (case n of
      0 => []
    | Suc n => empty_boxes n [+] [Dec n 2, Goto 0])"

fun cn_merge_gs ::
  "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
  where
  "cn_merge_gs [] p = []" |
  "cn_merge_gs (g # gs) p = 
      (let (gprog, gpara, gn) = g in 
         gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"

fun list_max :: "nat list \<Rightarrow> nat"
  where
  "list_max [] = 0"
| "list_max (x#xs) = (let y = list_max xs in
                      if (y < x) then x else y)"

fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"
  where
  "rec_ci z = (rec_ci_z, 1, 2)" |
  "rec_ci s = (rec_ci_s, 1, 3)" |
  "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |
  "rec_ci (Cn n f gs) = 
      (let cied_gs = map rec_ci gs in
       let (fprog, fpara, fn) = rec_ci f in 
       let pstr = list_max (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs)) in
       let qstr = pstr + Suc (length gs) in 
       (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+] 
          mv_boxes pstr 0 (length gs) [+] fprog [+] 
            mv_box fpara pstr [+] empty_boxes (length gs) [+] 
             mv_box pstr n [+] mv_boxes qstr 0 n, n,  qstr + n))" | 
  "rec_ci (Pr n f g) = 
         (let (fprog, fpara, fn) = rec_ci f in 
          let (gprog, gpara, gn) = rec_ci g in 
          let p = list_max [n + 3, fn, gn] in 
          let e = length gprog + 7 in 
           (mv_box n p [+] fprog [+] mv_box n (Suc n) [+] 
               (([Dec p e] [+] gprog [+] 
                 [Inc n, Dec (Suc n) 3, Goto 1]) @
                     [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),
             Suc n, p + 1))" |
  "rec_ci (Mn n f) =
         (let (fprog, fpara, fn) = rec_ci f in 
          let len = length (fprog) in 
            (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
             Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"

definition rec_add :: "recf"
  where
   [simp]: "rec_add \<equiv>  Pr 1 (id 1 0) (Cn 3 s [id 3 2])"

fun constn :: "nat \<Rightarrow> recf" where
  "constn n = (case n of
      0 => z  |
      Suc n => Cn 1 s [constn n])"

ML {*
fun dest_suc_trm @{term "Suc 0"} = raise TERM ("Suc 0", [])
  | dest_suc_trm @{term "Suc (Suc 0)"} = 2
  | dest_suc_trm (@{term "Suc"} $ t) = 1 + dest_suc_trm t
  | dest_suc_trm t = snd (HOLogic.dest_number t)

fun get_thm ctxt (t, n) =
let
  val num = HOLogic.mk_number @{typ "nat"} n
  val goal = Logic.mk_equals (t, num)
  val num_ss = HOL_ss addsimps @{thms semiring_norm}
in
  Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
end

fun nat_number_simproc ss ctrm =
let
  val trm = term_of ctrm
  val ctxt = Simplifier.the_context ss
in
  SOME (get_thm ctxt (trm, dest_suc_trm trm))
  handle TERM _ => NONE
end
*}

simproc_setup nat_number ("Suc n") = {* K nat_number_simproc*}

declare Nat.One_nat_def[simp del]

lemma [simp]: 
  shows "nat_case g f (1::nat) = f (0::nat)"
by (metis One_nat_def nat_case_Suc)

lemma 
  "rec_ci (constn 0) = ([Goto 1], 1, 2)"
apply(tactic {*
  timing_wrapper (asm_full_simp_tac @{simpset} 1)
*})
done

lemma 
  "rec_ci (constn 10) = XXX"
apply(tactic {*
  timing_wrapper (asm_full_simp_tac @{simpset} 1)
*})
oops

lemma 
  "rec_ci (constn 3) = XXX"
apply(tactic {*
  timing_wrapper (asm_full_simp_tac @{simpset} 1)
*})
oops

lemma 
  "rec_ci (rec_add) = XXX"
apply(simp del: abc_append.simps)
apply(simp)
oops

definition rec_mult :: "recf"
  where
  [simp]: "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"

lemma 
  "rec_ci (rec_mult) = XXX"
apply(simp)
oops

fun mopup_a :: "nat \<Rightarrow> instr list"
  where
  "mopup_a 0 = []" |
  "mopup_a (Suc n) = mopup_a n @ 
       [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]"

definition mopup_b :: "instr list"
  where
  "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3),
            (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]"

fun mopup :: "nat \<Rightarrow> instr list"
  where 
  "mopup n = mopup_a n @ shift mopup_b (2*n)"


lemma
  "tcopy |+| mopup 0 = XXX"
apply(simp add: tm_comp.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def mopup_b_def)
apply(simp add: adjust.simps shift.simps)
end