Commit 25363795 authored by Heiko Becker's avatar Heiko Becker

Add cond conv

parent 86741753
......@@ -134,3 +134,144 @@ let thm8 = step unfold_defs_conv thm6;;
let thm9 = step precond_conv thm8;;
let thm10 = step full_arith_conv thm9;;
(* New stuff begins here *)
let test t = match t with |Comb(s,t) -> if (rator s = `COND`) then print_term s else print_term s;;
(test `COND c s t`);;
let rec ONCE_COND_CONDMANIP_CONV conv term =
match term with
|Abs (x,t) -> REFL term
|Var (x,t) -> REFL term
|Const (c,t) -> REFL term
|Comb(s,t) ->
if is_cond (term)
then (COMB2_CONV (COMB2_CONV (COMB2_CONV ALL_CONV conv) ALL_CONV) ALL_CONV) term
else
try CHANGED_CONV (COMB2_CONV (ONCE_COND_CONV conv) (ALL_CONV)) term with
|Failure _ ->
let _ = printf("Right-Hand") in
try (CHANGED_CONV (COMB2_CONV (ALL_CONV) (ONCE_COND_CONV conv))) term with Failure _ -> REFL term;;
let rec ONCE_COND_CONV conv term =
match term with
|Abs (x,t) -> REFL term
|Var (x,t) -> REFL term
|Const (c,t) -> REFL term
|Comb(s,t) ->
if is_cond (term)
then conv term
else
try CHANGED_CONV (COMB2_CONV (ONCE_COND_CONV conv) (ALL_CONV)) term with
|Failure _ ->
let _ = printf("Right-Hand") in
try (CHANGED_CONV (COMB2_CONV (ALL_CONV) (ONCE_COND_CONV conv))) term with Failure _ -> REFL term;;
let ONCE_COND_MANIP_CONV conv = ONCE_COND_CONV (COMB2_CONV (COMB2_CONV (COMB2_CONV ALL_CONV conv) ALL_CONV) ALL_CONV);;
(ONCE_COND_CONDMANIP_CONV (REWRITE_CONV [ASSUME `(a:num) = b`]) THENC ONCE_COND_CONV (PURE_REWRITE_CONV[COND_CLAUSES])) `if (a:num) = b then a else b`;;
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);;
(* Now for conversion not for thm **)
let errsimp_conv = PATH_CONV "r" (REWRITE_CONV theRewrites);;
let ivsimp_conv = PATH_CONV "l" (REWRITE_CONV theRewrites);;
let unfold_defs_conv = 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
(*ONCE_REWRITE_CONV [COND_ELIM_THM] THENC *)
REWRITE_CONV DistinctnessAndInjectivity THENC
(REPEATC let_CONV)));;
(* (REPEATC
(CHANGED_CONV (
(TRY_CONV (COND_ELIM_CONV THENC REWRITE_CONV DistinctnessAndInjectivity 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 `thePrecondition 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 errorBound_conv thm2;;
let thm4 = step errorBound_conv thm3;;
let thm5 = step errorBound_conv thm4;;
let thm6 = step errorBound_conv thm5;;
let thm7 = step errorBound_conv thm6;;
(** A test :Only 4.5 seconds! **)
let thm3_2 = step (REPEATC (CHANGED_CONV errorBound_conv)) thm2;;
let thm5 = step ivsimp_conv thm3_2;;
let thm6 = step (REPEATC (CHANGED_CONV intervalBound_conv)) thm5;;
let thm7 = step unfold_defs_conv thm6;;
let thm8 = step precond_conv thm7;;
let thm9 = step (DEPTH_PAT_CONV `if c then s else t` (REPEATC (CHANGED_CONV (DEPTH_CONV COND_ELIM_CONV THENC arith_conv)))) thm8;;
let thm10 = step (DEPTH_CONV (let_CONV)) thm9;;
let thm11 = step (REWRITE_CONV[FST; SND]) thm10;;
let thm12 = step full_arith_conv thm11;;
let DAISY_CONV =
REWRITE_CONV[CertificateChecker] THENC
errsimp_conv THENC
(REPEATC (CHANGED_CONV errorBound_conv)) THENC
ivsimp_conv THENC
(REPEATC (CHANGED_CONV intervalBound_conv)) THENC
unfold_defs_conv THENC
precond_conv THENC
(DEPTH_PAT_CONV `if c then s else t` (REPEATC (CHANGED_CONV (DEPTH_CONV COND_ELIM_CONV THENC arith_conv)))) THENC
(DEPTH_CONV let_CONV) THENC
REWRITE_CONV[FST; SND] THENC
full_arith_conv;;
let theThm = time DAISY_CONV term;;
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