1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -5,43 +5,44 @@
1.4 signature REWRITE =
1.5 sig
1.6 exception NO_REWRITE
1.7 - val calculate_: theory -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
1.8 - val eval__true: theory -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool
1.9 - val eval_prog_expr: theory -> Rule_Set.T -> term -> term
1.10 - val eval_true_: theory -> Rule_Set.T -> term -> bool
1.11 - val eval_true: theory -> term list -> Rule_Set.T -> bool
1.12 - val rew_sub: theory -> int -> Subst.T -> Rule_Def.rew_ord_
1.13 + val calculate_: Proof.context -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
1.14 + val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool
1.15 + val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
1.16 + val eval_true_: Proof.context -> Rule_Set.T -> term -> bool
1.17 + val eval_true: Proof.context -> term list -> Rule_Set.T -> bool
1.18 + val rew_sub: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_
1.19 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
1.20 - val rewrite_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
1.21 + val rewrite_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
1.22 term -> (term * term list) option
1.23 - val rewrite_inst_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
1.24 + val rewrite_inst_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
1.25 -> Subst.T -> thm -> term -> (term * term list) option
1.26 - val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
1.27 - val rewrite_set_inst_: theory -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
1.28 - val rewrite_terms_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
1.29 + val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option
1.30 + val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
1.31 + val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
1.32 -> term -> (term * term list) option
1.33
1.34 - val trace_on: bool Unsynchronized.ref
1.35 val depth: int Unsynchronized.ref
1.36 val lim_deriv: int Unsynchronized.ref
1.37
1.38 \<^isac_test>\<open>
1.39 - val rewrite__: theory -> int -> Subst.T -> Rule_Def.rew_ord_ ->
1.40 + val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ ->
1.41 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
1.42 - val rewrite__set_: theory -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
1.43 - val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.44 - val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.45 - val trace1: int -> string -> unit
1.46 - val trace_eq1 : int -> string -> Rule_Def.rule_set -> theory -> term -> unit;
1.47 - val trace_eq2 : int -> string -> theory -> term -> term -> unit;
1.48 - val trace_in1 : int -> string -> string -> unit;
1.49 - val trace_in2 : int -> string -> theory -> term -> unit;
1.50 - val trace_in3 : int -> string -> theory -> (term * 'a) option -> unit;
1.51 - val trace_in4 : int -> string -> theory -> term list -> term list -> unit;
1.52 - val trace_in5 : int -> string -> theory -> term list -> unit;
1.53 + val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
1.54 + val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
1.55 + val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
1.56 + val trace1: Proof.context -> int -> string -> unit
1.57 + val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit;
1.58 + val trace_eq2 : Proof.context -> int -> string -> term -> term -> unit;
1.59 + val trace_in1 : Proof.context -> int -> string -> string -> unit;
1.60 + val trace_in2 : Proof.context -> int -> string -> term -> unit;
1.61 + val trace_in3 : Proof.context -> int -> string -> (term * 'a) option -> unit;
1.62 + val trace_in4 : Proof.context -> int -> string -> term list -> term list -> unit;
1.63 + val trace_in5 : Proof.context -> int -> string -> term list -> unit;
1.64 \<close>
1.65 end
1.66
1.67 +(* must be global for re-use in other structs *)
1.68 +val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
1.69 (**)
1.70 structure Rewrite(**): REWRITE(**) =
1.71 struct
1.72 @@ -49,65 +50,65 @@
1.73
1.74 exception NO_REWRITE;
1.75
1.76 -val trace_on = Unsynchronized.ref false;
1.77 (* depth of recursion in traces of the rewriter, if trace_on:=true *)
1.78 val depth = Unsynchronized.ref 99999;
1.79 (* no of rewrites exceeding this int -> NO rewrite *)
1.80 val lim_deriv = Unsynchronized.ref 100;
1.81
1.82 -fun trace i str =
1.83 - if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
1.84 -fun trace_eq1 i str rrls thy t =
1.85 - trace i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
1.86 -fun trace_eq2 i str thy t t' =
1.87 - trace i (" " ^ str ^ ": \"" ^
1.88 - UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
1.89 -fun trace1 i str =
1.90 - if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
1.91 -fun trace_in1 i str thmid =
1.92 - trace1 i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
1.93 -fun trace_in2 i str thy t =
1.94 - trace1 i (" " ^ str ^ ": \"" ^ UnparseC.term_in_thy thy t ^ "\"");
1.95 -fun trace_in3 i str thy pairopt =
1.96 - trace1 i (" " ^ str ^ ": " ^ UnparseC.term_in_thy thy ((fst o the) pairopt));
1.97 -fun trace_in4 i str thy ts ts' =
1.98 - if ! trace_on andalso i < ! depth andalso ts <> []
1.99 - then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy ts ^
1.100 - " stored: " ^ UnparseC.terms_in_thy thy ts')
1.101 +fun trace ctxt i str =
1.102 + if Config.get ctxt rewrite_trace andalso i < ! depth then tracing (idt "#" i ^ str) else ()
1.103 +fun trace_eq1 ctxt i str rrls t =
1.104 + trace ctxt i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_ctxt ctxt t)
1.105 +fun trace_eq2 ctxt i str t t' =
1.106 + trace ctxt i (" " ^ str ^ ": \"" ^
1.107 + UnparseC.term_in_ctxt ctxt t ^ "\" > \"" ^ UnparseC.term_in_ctxt ctxt t' ^ "\"");
1.108 +fun trace1 ctxt i str =
1.109 + if Config.get ctxt rewrite_trace andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
1.110 +fun trace_in1 ctxt i str thmid =
1.111 + trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
1.112 +fun trace_in2 ctxt i str t =
1.113 + trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"");
1.114 +fun trace_in3 ctxt i str pairopt =
1.115 + trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));
1.116 +fun trace_in4 ctxt i str ts ts' =
1.117 + if Config.get ctxt rewrite_trace andalso i < ! depth andalso ts <> []
1.118 + then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt ts ^
1.119 + " stored: " ^ UnparseC.terms_in_ctxt ctxt ts')
1.120 else ();
1.121 -fun trace_in5 i str thy p' =
1.122 - if ! trace_on andalso i < ! depth
1.123 - then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
1.124 +fun trace_in5 ctxt i str p' =
1.125 + if Config.get ctxt rewrite_trace andalso i < ! depth
1.126 + then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt p')
1.127 else();
1.128 -fun msg call thy op_ thmC t =
1.129 +fun msg call ctxt op_ thmC t =
1.130 call ^ ": \n" ^
1.131 "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
1.132 - "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
1.133 + "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";
1.134
1.135 -fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.136 +fun rewrite__ ctxt i bdv tless rls put_asm thm ct =
1.137 let
1.138 - val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.139 + val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.140 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
1.141 in if rew then SOME (t', distinct op = asms) else NONE end
1.142 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
1.143 -and rew_sub thy i bdv tless rls put_asm lrd r t =
1.144 +and rew_sub ctxt i bdv tless rls put_asm lrd r t =
1.145 (let
1.146 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.147 - val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.148 + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
1.149 + (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.150 handle Pattern.MATCH => raise NO_REWRITE
1.151 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.152 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.153 - val _ = trace_in2 i "eval asms" thy r';
1.154 + val _ = trace_in2 ctxt i "eval asms" r';
1.155 val (t'', p'') = (*conditional rewriting*)
1.156 - let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
1.157 + let val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls
1.158 in
1.159 if nofalse
1.160 - then (trace_in4 i "asms accepted" thy p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)
1.161 - else (trace_in5 i "asms false" thy p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
1.162 + then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)
1.163 + else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
1.164 end
1.165 in
1.166 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.167 - then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
1.168 + then (trace_eq2 ctxt i "not >" t t'; raise NO_REWRITE)
1.169 else (t'', p'', [], true)
1.170 end
1.171 ) handle NO_REWRITE =>
1.172 @@ -117,17 +118,17 @@
1.173 | Var(n, T) => (Var(n, T), [], lrd, false)
1.174 | Bound i => (Bound i, [], lrd, false)
1.175 | Abs(s, T, body) =>
1.176 - let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
1.177 + let val (t', asms, _ (*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.D]) r body
1.178 in (Abs(s, T, t'), asms, [], rew) end
1.179 | t1 $ t2 =>
1.180 - let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.181 + let val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.182 in
1.183 if rew2 then (t1 $ t2', asm2, lrd, true)
1.184 else
1.185 - let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
1.186 + let val (t1', asm1, lrd, rew1) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
1.187 in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
1.188 end)
1.189 -and eval__true thy i asms bdv rls = (* rewrite asumptions until one evaluates to false*)
1.190 +and eval__true ctxt i asms bdv rls = (* rewrite asumptions until one evaluates to false*)
1.191 if asms = [@{term True}] orelse asms = [] then ([], true)
1.192 else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
1.193 if asms = [@{term False}] then ([], false)
1.194 @@ -135,7 +136,7 @@
1.195 let
1.196 fun chk indets [] = (indets, true) (*return asms<>True until false*)
1.197 | chk indets (a :: asms) =
1.198 - (case rewrite__set_ thy (i + 1) false bdv rls a of
1.199 + (case rewrite__set_ ctxt (i + 1) false bdv rls a of
1.200 NONE => (chk (indets @ [a]) asms)
1.201 | SOME (t, a') =>
1.202 if t = @{term True} then (chk (indets @ a') asms)
1.203 @@ -143,16 +144,16 @@
1.204 (*asm false .. thm not applied ^^^; continue until False vvv*)
1.205 else chk (indets @ [t] @ a') asms);
1.206 in chk [] asms end
1.207 -and rewrite__set_ thy (*1*)_ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
1.208 - raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
1.209 - | rewrite__set_ (*2*)thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
1.210 +and rewrite__set_ ctxt (*1*)_ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
1.211 + raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_ctxt ctxt t ^ "'")
1.212 + | rewrite__set_ (*2*)ctxt i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
1.213 let
1.214 - val _= trace_eq1 i "rls" rrls thy t;
1.215 - val (t', asm, rew) = app_rev thy (i + 1) rrls t
1.216 + val _= trace_eq1 ctxt i "rls" rrls t;
1.217 + val (t', asm, rew) = app_rev ctxt (i + 1) rrls t
1.218 in if rew then SOME (t', distinct op = asm) else NONE end
1.219 - | rewrite__set_ (*3*)thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
1.220 + | rewrite__set_ (*3*)ctxt i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
1.221 let
1.222 - (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
1.223 + (* attention with cp to test/..: unbound ctxt, i, bdv, rls; TODO1803? pull out to rewrite__*)
1.224 datatype switch = Appl | Noap;
1.225 fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
1.226 | rew_once (*2*)ruls asm ct Appl [] =
1.227 @@ -162,90 +163,90 @@
1.228 | rew_once (*3*)ruls asm ct apno (rul :: thms) =
1.229 case rul of
1.230 Rule.Thm (thmid, thm) =>
1.231 - (trace_in1 i "try thm" thmid;
1.232 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.233 + (trace_in1 ctxt i "try thm" thmid;
1.234 + case rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.235 ((#erls o Rule_Set.rep) rls) put_asm thm ct of
1.236 NONE => rew_once ruls asm ct apno thms
1.237 | SOME (ct', asm') =>
1.238 - (trace_in2 i "rewrites to" thy ct';
1.239 + (trace_in2 ctxt i "rewrites to" ct';
1.240 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.241 (* once again try the same rule, e.g. associativity against "()"*)
1.242 - | Rule.Eval (cc as (op_, _)) =>
1.243 - let val _ = trace_in1 i "try calc" op_;
1.244 - in case Eval.adhoc_thm thy cc ct of
1.245 + | Rule.Eval (cc as (op_, _)) =>
1.246 + let val _ = trace_in1 ctxt i "try calc" op_;
1.247 + in case Eval.adhoc_thm (Proof_Context.theory_of ctxt) cc ct of
1.248 NONE => rew_once ruls asm ct apno thms
1.249 | SOME (_, thm') =>
1.250 let
1.251 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.252 + val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.253 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.254 - val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct)
1.255 - val _ = trace_in3 i "calc. to" thy pairopt;
1.256 + val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct)
1.257 + val _ = trace_in3 ctxt i "calc. to" pairopt;
1.258 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.259 end
1.260 | Rule.Cal1 (cc as (op_, _)) =>
1.261 - let val _ = trace_in1 i "try cal1" op_;
1.262 - in case Eval.adhoc_thm1_ thy cc ct of
1.263 + let val _ = trace_in1 ctxt i "try cal1" op_;
1.264 + in case Eval.adhoc_thm1_ (Proof_Context.theory_of ctxt) cc ct of
1.265 NONE => (ct, asm)
1.266 | SOME (_, thm') =>
1.267 let
1.268 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.269 + val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.270 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.271 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
1.272 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.273 - val _ = trace_in3 i "cal1. to" thy pairopt;
1.274 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
1.275 + val _ = trace_in3 ctxt i "cal1. to" pairopt;
1.276 in the pairopt end
1.277 end
1.278 | Rule.Rls_ rls' =>
1.279 - (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
1.280 + (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of
1.281 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.282 | NONE => rew_once ruls asm ct apno thms)
1.283 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
1.284 val ruls = (#rules o Rule_Set.rep) rls;
1.285 - val _ = trace_eq1 i "rls" rls thy ct
1.286 + val _ = trace_eq1 ctxt i "rls" rls ct
1.287 val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.288 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end
1.289 -(*-------------------------------------------------------------*)
1.290 -and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
1.291 +(*--vvv and app_sub are type correct-----------------------------------------------------------*)
1.292 +and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
1.293 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
1.294 fun chk_prepat _ _ [] _ = true
1.295 - | chk_prepat thy erls prepat t =
1.296 + | chk_prepat ctxt erls prepat t =
1.297 let
1.298 fun chk (pres, pat) =
1.299 (let
1.300 val subst: Type.tyenv * Envir.tenv =
1.301 - Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
1.302 + Pattern.match (Proof_Context.theory_of ctxt) (pat, t) (Vartab.empty, Vartab.empty)
1.303 in
1.304 - snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
1.305 + snd (eval__true ctxt (i + 1) (map (Envir.subst_term subst) pres) [] erls)
1.306 end) handle Pattern.MATCH => false
1.307 fun scan_ _ [] = false
1.308 | scan_ f (pp :: pps) =
1.309 if f pp then true else scan_ f pps;
1.310 in scan_ chk prepat end;
1.311 (* apply the normal_form of a rev-set *)
1.312 - fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
1.313 - if chk_prepat thy erls prepat t then normal_form t else NONE
1.314 + fun app_rev' ctxt (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
1.315 + if chk_prepat ctxt erls prepat t then normal_form t else NONE
1.316 | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
1.317 - val opt = app_rev' thy rrls t
1.318 + val opt = app_rev' ctxt rrls t
1.319 in
1.320 case opt of
1.321 SOME (t', asm) => (t', asm, true)
1.322 - | NONE => app_sub thy i rrls t
1.323 + | NONE => app_sub ctxt i rrls t
1.324 end
1.325 -and app_sub thy i rrls t = (* apply an Rrls to subterms*)
1.326 +and app_sub ctxt i rrls t = (* apply an Rrls to subterms*)
1.327 case t of
1.328 Const (s, T) => (Const(s, T), [], false)
1.329 | Free (s, T) => (Free(s, T), [], false)
1.330 | Var (n, T) => (Var(n, T), [], false)
1.331 | Bound i => (Bound i, [], false)
1.332 | Abs (s, T, body) =>
1.333 - let val (t', asm, rew) = app_rev thy i rrls body
1.334 + let val (t', asm, rew) = app_rev ctxt i rrls body
1.335 in (Abs(s, T, t'), asm, rew) end
1.336 | t1 $ t2 =>
1.337 - let val (t2', asm2, rew2) = app_rev thy i rrls t2
1.338 + let val (t2', asm2, rew2) = app_rev ctxt i rrls t2
1.339 in
1.340 if rew2 then (t1 $ t2', asm2, true)
1.341 else
1.342 - let val (t1', asm1, rew1) = app_rev thy i rrls t1
1.343 + let val (t1', asm1, rew1) = app_rev ctxt i rrls t1
1.344 in if rew1 then (t1' $ t2, asm1, true)
1.345 else (t1 $ t2, [], false)
1.346 end
1.347 @@ -282,13 +283,13 @@
1.348 end;
1.349
1.350 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
1.351 -fun calculate_ thy (isa_fn as (id, eval_fn)) t =
1.352 - case Eval.adhoc_thm thy isa_fn t of
1.353 +fun calculate_ ctxt (isa_fn as (id, eval_fn)) t =
1.354 + case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of
1.355 NONE => NONE
1.356 | SOME (thmID, thm) =>
1.357 - (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
1.358 + (let val rew = case rewrite_ ctxt Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
1.359 SOME (rew, _) => rew
1.360 - | NONE => raise ERROR (msg "calculate_" thy id thm t)
1.361 + | NONE => raise ERROR (msg "calculate_" ctxt id thm t)
1.362 in SOME (rew, (thmID, thm)) end)
1.363 handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
1.364