Commit 0f33d0c0 authored by Heiko Becker's avatar Heiko Becker

Tweak conversions to get more performance

parent df68b894
......@@ -8,11 +8,42 @@
let Checker_Rewrites =
[CertificateChecker;validIntervalbounds; validErrorbound;
maxAbsFun; isSupersetInterval; multInterval; subtractInterval;
maxAbsFun; isSupersetInterval; multInterval; subtractInterval; widenInterval; mkInterval;
addInterval; absIntvUpd; min4; max4; machineEpsilon; IVlo; IVhi];;
let DistinctnessAndInjectivity = [distinctness "exp"; injectivity "exp"; distinctness "binop"];;
(*
First get the free variables of the pattern
Then check wether the free variables can be instantiated such that pattern matches thm.
Since term_match may fail, check the returned instantiation on the pattern and check wether this is alpha convertibe (aconv) to the given thm.
If all this succeeds then return true, otherwise false
*)
let matchable pat tm =
try aconv (instantiate(term_match (frees pat) pat tm) pat) tm
with Failure _ -> false;;
(*
test wether matchable pat tm is true.
If this holds true, then apply conv else recurse.
Recursion: If tm is a combination, recurse in the arguments, if tm is an abstraction, recurse into the term, commented out since it is not need in certificate checker
*)
let rec DEPTH_PAT_CONV pat (conv:term->thm) term =
if matchable pat term then conv else
match term with
Comb(s,t) -> COMB2_CONV (DEPTH_PAT_CONV pat conv s)
(DEPTH_PAT_CONV pat conv t)
(* | Abs(x,t) -> ABS_CONV (DEPTH_PAT_CONV pats t conv) *)
| _ -> REFL;;
(*
Subterm rewriting conversion
let REWRITE_SUBTERMS_CONV pats pat ths =
DEPTH_PAT_CONV pats pat (REWRITE_CONV(ADD_CLAUSES::MULT_CLAUSES::ths));;
*)
let DAISY_CONV theRewrites term =
let allRewrites = List.concat [Checker_Rewrites; theRewrites; DistinctnessAndInjectivity] in
let unfolded_defs = REWRITE_CONV allRewrites term in
......@@ -39,3 +70,67 @@ let DAISY_CONV theRewrites term =
)
)
) no_lets;;
let matchable pattern term =
try
aconv (instantiate (term_match (frees term) pattern term) pattern) term
with
|Failure _ -> false;;
let step conv t = time (CONV_RULE conv) t;;
let rec DEPTH_PAT_CONV pattern conv term :thm =
if (matchable pattern term)
then
conv term
else match term with
|Comb (s,t) -> COMB2_CONV (DEPTH_PAT_CONV pattern conv) (DEPTH_PAT_CONV pattern conv) term
|Abs (x,t) -> ABS_CONV (DEPTH_PAT_CONV pattern conv) term
|_ -> REFL term;;
let errsimp_conv = PATH_CONV "rr" (REWRITE_CONV theRewrites);;
let ivsimp_conv = PATH_CONV "rl" (REWRITE_CONV theRewrites);;
let unfold_defs_conv = PATH_CONV "r" (REWRITE_CONV Checker_Rewrites);;
let arith_conv =
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV NUM_REDUCE_CONV THENC TRY_CONV REAL_RAT_RED_CONV)));;
let errorBound_conv =
(DEPTH_PAT_CONV `validErrorbound e E`
(ONCE_REWRITE_CONV [validErrorbound] THENC
DEPTH_CONV BETA_CONV THENC
COND_ELIM_CONV THENC
(*REWRITE_CONV [COND_ELIM_THM] THENC *)
REWRITE_CONV DistinctnessAndInjectivity THENC
(REPEATC (CHANGED_CONV (TRY_CONV (COND_ELIM_CONV THENC arith_conv)))) THENC
REPEATC let_CONV));;
let intervalBound_conv =
(DEPTH_PAT_CONV `validIntervalbounds e E P`
(ONCE_REWRITE_CONV [validIntervalbounds] THENC
DEPTH_CONV BETA_CONV THENC
REWRITE_CONV [COND_ELIM_THM] THENC
REWRITE_CONV DistinctnessAndInjectivity));;
let precond_conv =
(DEPTH_PAT_CONV `thePrecond n`
(ONCE_REWRITE_CONV [thePrecondition] THENC REWRITE_CONV[COND_ELIM_THM]));;
let full_arith_conv = REPEATC (CHANGED_CONV arith_conv);;
let thm = REWRITE_CONV[CertificateChecker] term;;
let thm2 = step errsimp_conv thm;;
let thm3 = step (REPEATC (CHANGED_CONV errorBound_conv)) thm2;;
let thm5 = step ivsimp_conv thm3;;
let thm6 = step (REPEATC (CHANGED_CONV intervalBound_conv)) thm5;;
let thm8 = step unfold_defs_conv thm6;;
let thm9 = step precond_conv thm8;;
let thm10 = step full_arith_conv thm9;;
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