Commit f63a86a5 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' of gitlab.mpi-sws.org:AVA/icing

parents 4c1fb6a6 8af276e4
......@@ -365,8 +365,8 @@ val greedyRws_def = Define `
(* Simple testcases for optimizeGreedy*)
val test1 = prove (``
optimizeGreedy greedyRws
(Scope Opt (Binop Plus (Wconst 1w) (Binop Plus (Wconst 2w) (Wconst 3w)))) =
(Scope Opt (Binop Plus (Binop Plus (Wconst 3w) (Wconst 2w)) (Wconst 1w)))``,
(Scope Opt (Binop Plus (Binop Plus (Wconst 3w) (Wconst 2w)) (Wconst 1w))) =
(Scope Opt (Binop Plus (Wconst 1w) (Binop Plus (Wconst 2w) (Wconst 3w))))``,
EVAL_TAC);
val test2 = prove (``
......
......@@ -15,11 +15,11 @@ val _ = new_theory "rewriteRulesProofs";
Theorem ASSOCRULE_GEN_cases
`!b1 b2 e11 e12.
(?b3 e21 e22.
(e12 = Binop b3 e21 e22 /\ b3 = b2 /\ b1 = b2) /\
rewriteExp [ASSOCRULE_GEN b2] (Binop b1 e11 e12) =
Binop b1 (Binop b1 e11 e21) e22) \/
(e11 = Binop b2 e21 e22 /\ b1 = b2 /\ b2 = b3) /\
rewriteExp [ASSOCRULE_GEN b1] (Binop b1 (Binop b1 e21 e22) e12) =
(Binop b1 e21 (Binop b1 e22 e12))) \/
rewriteExp [ASSOCRULE_GEN b2] (Binop b1 e11 e12) = Binop b1 e11 e12`
(rpt strip_tac \\ Cases_on `e12` \\ Cases_on `b1 = b2` \\ EVAL_TAC \\ fs[]
(rpt strip_tac \\ Cases_on `e11` \\ Cases_on `b1 = b2` \\ EVAL_TAC \\ fs[]
\\ TOP_CASE_TAC \\ fs[] \\ rveq \\ EVAL_TAC);
(** Correctness proofs for above patterns **)
......@@ -34,20 +34,20 @@ Theorem ASSOCRULE_GEN_correct
\\ fs[] \\ rveq
>- (qpat_x_assum `rewriteExp _ _ = _` (fn thm => fs[thm])
\\ fs[evalExpNonDet_cases] \\ fs[]
\\ rename1 `evalExpNonDet cfg E e1 (Val v1i)`
\\ rename1 `evalExpNonDet cfg E e2 (Val v2i)`
\\ rename1 `evalExpNonDet cfg E e21 (Val v21)`
\\ rename1 `evalExpNonDet cfg E e22 (Val v22)`
\\ qexistsl_tac [`v1i`, `BinVal b v21 v22`]
\\ qexistsl_tac [`BinVal b v21 v22`, `v2i`]
\\ rpt conj_tac
>- drop_sem_rw_tac
>- (qexistsl_tac [`v21`, `v22`] \\ fs[rewritesTo_def]
\\ rpt conj_tac \\ fs[]
\\ drop_sem_rw_tac)
>- drop_sem_rw_tac
\\ fs[rewritesTo_def]
\\ Cases_on `cfg.canOpt` \\ fs[]
\\ rename1 `rwAllValTree insts2 T cfg.opts (BinVal b v1 v22) = SOME r`
\\ last_assum (mp_then Any assume_tac rwAllValTree_comp_left)
\\ first_x_assum (qspecl_then [`b`,`v22`] assume_tac) \\ fs[]
\\ rename1 `rwAllValTree insts2 T cfg.opts (BinVal b v211 v2) = SOME r`
\\ last_assum (mp_then Any assume_tac rwAllValTree_comp_right)
\\ first_x_assum (qspecl_then [`b`,`v211`] assume_tac) \\ fs[]
\\ first_x_assum (mp_then Any assume_tac rwAllValTree_up)
\\ first_x_assum
(qspec_then `(ASSOCRULE_GEN b)::cfg.opts` destruct)
......@@ -56,8 +56,7 @@ Theorem ASSOCRULE_GEN_correct
(mp_then Any assume_tac rwAllValTree_up)
\\ first_x_assum (qspec_then `ASSOCRULE_GEN b ::cfg.opts` destruct)
\\ fs[SUBSET_DEF]
\\ Cases_on `cfg.canOpt` \\ fs[]
\\ qpat_x_assum `rwAllValTree _ _ _ _ = SOME (BinVal b v1 _)`
\\ qpat_x_assum `rwAllValTree _ _ _ _ = SOME (BinVal b v211 _)`
(mp_then Any assume_tac rwAllValTree_chaining)
\\ first_x_assum (qspecl_then [`r`, `insts2`] destruct) \\ fs[]
\\ irule rwAllValTree_chaining
......
......@@ -14,8 +14,8 @@ val _ = new_theory "rewriteRules";
(** A generator for associativity rewrites **)
val ASSOCRULE_GEN_def = Define `
ASSOCRULE_GEN (b:binop) =
(Binop b (Var 0) (Binop b (Var 1) (Var 2)),
Binop b (Binop b (Var 0) (Var 1)) (Var 2))`;
(Binop b (Binop b (Var 0) (Var 1)) (Var 2),
Binop b (Var 0) (Binop b (Var 1) (Var 2)))`;
(**
a + (b + c) -> (a + b) + c
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment