1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 13 13:13:07 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 13 13:27:55 2020 +0200
1.3 @@ -64,7 +64,7 @@
1.4 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.5 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.6 val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
1.7 - then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_thy thy r') else ()
1.8 + then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
1.9 val (t'', p'') = (*conditional rewriting*)
1.10 let
1.11 val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
1.12 @@ -72,20 +72,20 @@
1.13 if nofalse
1.14 then
1.15 (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
1.16 - then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_thy thy p' ^
1.17 - " stored: " ^ UnparseC.terms_thy thy simpl_p')
1.18 + then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
1.19 + " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
1.20 else();
1.21 (t',simpl_p')) (* uncond.rew. from above*)
1.22 else
1.23 (if ! Celem.trace_rewrite andalso i < ! Celem.depth
1.24 - then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_thy thy p')
1.25 + then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
1.26 else();
1.27 raise STOP_REW_SUB (* don't go into subterms of cond *))
1.28 end
1.29 in
1.30 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.31 then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
1.32 - then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_thy thy t ^ "\" > \"" ^ UnparseC.term_thy thy t' ^ "\"")
1.33 + then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
1.34 else ();
1.35 raise NO_REWRITE)
1.36 else (t'', p'', [], true)
1.37 @@ -124,10 +124,10 @@
1.38 else chk (indets @ [t] @ a') asms);
1.39 in chk [] asms end
1.40 and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
1.41 - error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_thy thy t ^ "'")
1.42 + error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
1.43 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
1.44 let
1.45 - val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_thy thy t)
1.46 + val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
1.47 val (t', asm, rew) = app_rev thy (i + 1) rrls t
1.48 in if rew then SOME (t', distinct asm) else NONE end
1.49 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
1.50 @@ -147,7 +147,7 @@
1.51 ((#erls o Rule_Set.rep) rls) put_asm thm ct of
1.52 NONE => rew_once ruls asm ct apno thms
1.53 | SOME (ct', asm') =>
1.54 - (trace1 i (" rewrites to: \"" ^ UnparseC.term_thy thy ct' ^ "\"");
1.55 + (trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
1.56 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.57 (* once again try the same rule, e.g. associativity against "()"*)
1.58 | Rule.Num_Calc (cc as (op_, _)) =>
1.59 @@ -160,8 +160,8 @@
1.60 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.61 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.62 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.63 - ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
1.64 - val _ = trace1 i (" calc. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
1.65 + ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.66 + val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
1.67 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.68 end
1.69 | Rule.Cal1 (cc as (op_, _)) =>
1.70 @@ -174,8 +174,8 @@
1.71 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.72 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.73 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.74 - ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
1.75 - val _ = trace1 i (" cal1. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
1.76 + ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.77 + val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
1.78 in the pairopt end
1.79 end
1.80 | Rule.Rls_ rls' =>
1.81 @@ -184,7 +184,7 @@
1.82 | NONE => rew_once ruls asm ct apno thms)
1.83 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
1.84 val ruls = (#rules o Rule_Set.rep) rls;
1.85 - val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_thy thy ct)
1.86 + val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)
1.87 val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.88 in if ct = ct' then NONE else SOME (ct', distinct asm') end
1.89 (*-------------------------------------------------------------*)