1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 26 14:16:35 2021 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 27 18:09:22 2021 +0200
1.3 @@ -25,12 +25,20 @@
1.4 val lim_deriv: int Unsynchronized.ref
1.5
1.6 \<^isac_test>\<open>
1.7 + exception NO_REWRITE
1.8 val rewrite__: theory -> int -> (term * term) list -> Rule_Def.rew_ord_ ->
1.9 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
1.10 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.11 val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.12 val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.13 val trace1: int -> string -> unit
1.14 + val trace_eq1 : int -> string -> Rule_Def.rule_set -> theory -> term -> unit;
1.15 + val trace_eq2 : int -> string -> theory -> term -> term -> unit;
1.16 + val trace_in1 : int -> string -> string -> unit;
1.17 + val trace_in2 : int -> string -> theory -> term -> unit;
1.18 + val trace_in3 : int -> string -> theory -> (term * 'a) option -> unit;
1.19 + val trace_in4 : int -> string -> theory -> term list -> term list -> unit;
1.20 + val trace_in5 : int -> string -> theory -> term list -> unit;
1.21 \<close>
1.22 end
1.23
1.24 @@ -40,7 +48,6 @@
1.25 (**)
1.26
1.27 exception NO_REWRITE;
1.28 -exception STOP_REW_SUB; (*WN050820 quick and dirty*)
1.29
1.30 val trace_on = Unsynchronized.ref false;
1.31 (* depth of recursion in traces of the rewriter, if trace_on:=true *)
1.32 @@ -50,68 +57,74 @@
1.33
1.34 fun trace i str =
1.35 if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
1.36 -fun trace1 i str =
1.37 +fun trace_eq1 i str rrls thy t =
1.38 + trace i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
1.39 +fun trace_eq2 i str thy t t' =
1.40 + trace i (" " ^ str ^ ": \"" ^
1.41 + UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
1.42 +
1.43 +fun trace1 i str =
1.44 if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
1.45 +fun trace_in1 i str thmid =
1.46 + trace1 i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
1.47 +fun trace_in2 i str thy t =
1.48 + trace1 i (" " ^ str ^ ": \"" ^ UnparseC.term_in_thy thy t ^ "\"");
1.49 +fun trace_in3 i str thy pairopt =
1.50 + trace1 i (" " ^ str ^ ": " ^ UnparseC.term_in_thy thy ((fst o the) pairopt));
1.51 +fun trace_in4 i str thy ts ts' =
1.52 + if ! trace_on andalso i < ! depth andalso ts <> []
1.53 + then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy ts ^
1.54 + " stored: " ^ UnparseC.terms_in_thy thy ts')
1.55 + else ();
1.56 +fun trace_in5 i str thy p' =
1.57 + if ! trace_on andalso i < ! depth
1.58 + then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
1.59 + else();
1.60
1.61 fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.62 let
1.63 - val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.64 + val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.65 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
1.66 in if rew then SOME (t', distinct op = asms) else NONE end
1.67 - (* one rewrite (possibly conditional, ordered) EXOR exn Pattern.MATCH EXOR go into subterms *)
1.68 + (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
1.69 and rew_sub thy i bdv tless rls put_asm lrd r t =
1.70 (let
1.71 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.72 - (*?alternative Unify.matchers:
1.73 - http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
1.74 - val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
1.75 + val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.76 + handle Pattern.MATCH => raise NO_REWRITE
1.77 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.78 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.79 - val _ = if ! trace_on andalso i < ! depth andalso p' <> []
1.80 - then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
1.81 - val (t'', p'') = (*conditional rewriting*)
1.82 - let
1.83 - val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
1.84 + val _ = trace_in2 i "eval asms" thy r';
1.85 + val (t'', p'') = (*conditional rewriting*)
1.86 + let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
1.87 in
1.88 if nofalse
1.89 - then
1.90 - (if ! trace_on andalso i < ! depth andalso p' <> []
1.91 - then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
1.92 - " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
1.93 - else();
1.94 - (t',simpl_p')) (* uncond.rew. from above*)
1.95 - else
1.96 - (if ! trace_on andalso i < ! depth
1.97 - then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
1.98 - else();
1.99 - raise STOP_REW_SUB (* don't go into subterms of cond *))
1.100 + then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
1.101 + else (trace_in5 i "asms false" thy p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
1.102 end
1.103 - in
1.104 - if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.105 - then (if ! trace_on andalso i < ! depth
1.106 - then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
1.107 - else ();
1.108 - raise NO_REWRITE)
1.109 - else (t'', p'', [], true)
1.110 - end
1.111 - ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
1.112 - (case t of
1.113 - Const(s,T) => (Const(s,T),[],lrd,false)
1.114 - | Free(s,T) => (Free(s,T),[],lrd,false)
1.115 - | Var(n,T) => (Var(n,T),[],lrd,false)
1.116 - | Bound i => (Bound i,[],lrd,false)
1.117 - | Abs(s,T,body) =>
1.118 - let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
1.119 - in (Abs(s, T, t'), asms, [], rew) end
1.120 - | t1 $ t2 =>
1.121 - let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.122 - in
1.123 - if rew2 then (t1 $ t2', asm2, lrd, true)
1.124 - else
1.125 - let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
1.126 - in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
1.127 - end)
1.128 -and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
1.129 + in
1.130 + if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.131 + then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
1.132 + else (t'', p'', [], true)
1.133 + end
1.134 + ) handle NO_REWRITE =>
1.135 + (case t of
1.136 + Const(s, T) => (Const(s, T), [], lrd, false)
1.137 + | Free(s, T) => (Free(s, T), [], lrd, false)
1.138 + | Var(n, T) => (Var(n, T), [], lrd, false)
1.139 + | Bound i => (Bound i, [], lrd, false)
1.140 + | Abs(s, T, body) =>
1.141 + let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
1.142 + in (Abs(s, T, t'), asms, [], rew) end
1.143 + | t1 $ t2 =>
1.144 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.145 + in
1.146 + if rew2 then (t1 $ t2', asm2, lrd, true)
1.147 + else
1.148 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
1.149 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
1.150 + end)
1.151 +and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false*)
1.152 if asms = [@{term True}] orelse asms = [] then ([], true)
1.153 else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
1.154 if asms = [@{term False}] then ([], false)
1.155 @@ -127,18 +140,18 @@
1.156 (*asm false .. thm not applied ^^^; continue until False vvv*)
1.157 else chk (indets @ [t] @ a') asms);
1.158 in chk [] asms end
1.159 -and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
1.160 +and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
1.161 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
1.162 - | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
1.163 + | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
1.164 let
1.165 - val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
1.166 + val _= trace_eq1 i "rls" rrls thy t;
1.167 val (t', asm, rew) = app_rev thy (i + 1) rrls t
1.168 in if rew then SOME (t', distinct op = asm) else NONE end
1.169 - | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
1.170 + | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
1.171 let
1.172 (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
1.173 datatype switch = Appl | Noap;
1.174 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
1.175 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
1.176 | rew_once ruls asm ct Appl [] =
1.177 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
1.178 | Rule_Set.Sequence _ => (ct, asm)
1.179 @@ -146,16 +159,16 @@
1.180 | rew_once ruls asm ct apno (rul :: thms) =
1.181 case rul of
1.182 Rule.Thm (thmid, thm) =>
1.183 - (trace1 i (" try thm: \"" ^ thmid ^ "\"");
1.184 + (trace_in1 i "try thm" thmid;
1.185 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.186 ((#erls o Rule_Set.rep) rls) put_asm thm ct of
1.187 NONE => rew_once ruls asm ct apno thms
1.188 | SOME (ct', asm') =>
1.189 - (trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
1.190 + (trace_in2 i "rewrites to" thy ct';
1.191 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.192 (* once again try the same rule, e.g. associativity against "()"*)
1.193 | Rule.Eval (cc as (op_, _)) =>
1.194 - let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
1.195 + let val _= trace_in1 i "try calc" op_;
1.196 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
1.197 in case Eval.adhoc_thm thy cc ct of
1.198 NONE => rew_once ruls asm ct apno thms
1.199 @@ -165,11 +178,11 @@
1.200 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.201 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
1.202 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.203 - val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
1.204 + val _ = trace_in3 i "calc. to" thy pairopt;
1.205 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.206 end
1.207 | Rule.Cal1 (cc as (op_, _)) =>
1.208 - let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
1.209 + let val _= trace_in1 i "try cal1" op_;
1.210 val ct = TermC.uminus_to_string ct
1.211 in case Eval.adhoc_thm1_ thy cc ct of
1.212 NONE => (ct, asm)
1.213 @@ -179,7 +192,7 @@
1.214 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.215 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
1.216 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.217 - val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
1.218 + val _ = trace_in3 i "cal1. to" thy pairopt;
1.219 in the pairopt end
1.220 end
1.221 | Rule.Rls_ rls' =>
1.222 @@ -188,11 +201,11 @@
1.223 | NONE => rew_once ruls asm ct apno thms)
1.224 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
1.225 val ruls = (#rules o Rule_Set.rep) rls;
1.226 - val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)
1.227 + val _ = trace_eq1 i "rls" rls thy ct
1.228 val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.229 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end
1.230 (*-------------------------------------------------------------*)
1.231 -and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
1.232 +and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
1.233 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
1.234 fun chk_prepat _ _ [] _ = true
1.235 | chk_prepat thy erls prepat t =
1.236 @@ -203,7 +216,7 @@
1.237 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
1.238 in
1.239 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
1.240 - end) handle _ (*TODO Pattern.MATCH*) => false
1.241 + end) handle STOP_REW_SUB => false
1.242 fun scan_ _ [] = false
1.243 | scan_ f (pp :: pps) =
1.244 if f pp then true else scan_ f pps;
1.245 @@ -218,7 +231,7 @@
1.246 SOME (t', asm) => (t', asm, true)
1.247 | NONE => app_sub thy i rrls t
1.248 end
1.249 -and app_sub thy i rrls t = (* apply an Rrls to subterms *)
1.250 +and app_sub thy i rrls t = (* apply an Rrls to subterms*)
1.251 case t of
1.252 Const (s, T) => (Const(s, T), [], false)
1.253 | Free (s, T) => (Free(s, T), [], false)
1.254 @@ -291,4 +304,4 @@
1.255 SOME (Const ("HOL.True",_),_) => true
1.256 | _ => false;
1.257
1.258 -end
1.259 \ No newline at end of file
1.260 +end