# HG changeset patch # User Christian Urban # Date 1362136590 0 # Node ID 17d80924af53d0bf2ca6809af75103f969d7adf7 # Parent c7975ab7c52e59a40b2e39f9902c099982f64fa3 added a test to make the simplifier be fast enough to do actual compilations diff -r c7975ab7c52e -r 17d80924af53 Tests/Test1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tests/Test1.thy Fri Mar 01 11:16:30 2013 +0000 @@ -0,0 +1,216 @@ +theory Test1 +imports Main +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 \ nat \ nat \ 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 \ nat \ abc_prog" + where + "mv_box m n = [Dec m 3, Inc n, Goto 0]" + +fun abc_inst_shift :: "abc_inst \ nat \ 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 \ nat \ 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 \ abc_inst list \ 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 \ (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 \ nat \ abc_inst list" + where + "rec_ci_id i j = addition j i (i + 1)" + +fun mv_boxes :: "nat \ nat \ nat \ 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 \ 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 \ nat \ nat) list \ nat \ 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 \ 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 \ abc_inst list \ nat \ 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 (\ (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 \ Pr 1 (id 1 0) (Cn 3 s [id 3 2])" + +fun constn :: "nat \ 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) = XXX" +apply(tactic {* + timing_wrapper (asm_full_simp_tac @{simpset} 1) +*}) +oops + +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 + +end \ No newline at end of file