1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Apr 21 16:53:17 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Wed Apr 22 11:06:48 2020 +0200
1.3 @@ -6,7 +6,6 @@
1.4 *)
1.5 theory BaseDefinitions imports Know_Store
1.6 begin
1.7 - ML_file tracing.sml
1.8 ML_file calcelems.sml
1.9 ML_file termC.sml
1.10 ML_file contextC.sml
2.1 --- a/src/Tools/isac/BaseDefinitions/tracing.sml Tue Apr 21 16:53:17 2020 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,39 +0,0 @@
2.4 -(* Title: BaseDefinitions/tracing.sml
2.5 - Author: Walther Neuper
2.6 - (c) due to copyright terms
2.7 -
2.8 -This structure could be dropped due to improved reflection in Isabelle;
2.9 -but ThmC.sym_thm requires still an identifying string thm_id.
2.10 -*)
2.11 -signature TRACING =
2.12 -sig
2.13 -(*/------- to Trace from Celem -------\*)
2.14 - val trace_calc: bool Unsynchronized.ref
2.15 - val trace_rewrite: bool Unsynchronized.ref
2.16 - val depth: int Unsynchronized.ref
2.17 - val lim_deriv: int Unsynchronized.ref
2.18 -(*\------- to Trace from Celem --------/*)
2.19 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.20 - (*NONE*)
2.21 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.22 - (*NONE*)
2.23 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.24 -end
2.25 -
2.26 -(**)
2.27 -structure Trace(**): TRACING(**) =
2.28 -struct
2.29 -(**)
2.30 -
2.31 -(*/------- to Trace from Celem -------\*)
2.32 -(* trace internal steps of isac's numeral calculations *)
2.33 -val trace_calc = Unsynchronized.ref false;
2.34 -(* trace internal steps of isac's rewriter *)
2.35 -val trace_rewrite = Unsynchronized.ref false;
2.36 -(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *)
2.37 -val depth = Unsynchronized.ref 99999;
2.38 -(* no of rewrites exceeding this int -> NO rewrite *)
2.39 -val lim_deriv = Unsynchronized.ref 100;
2.40 -(*\------- to Trace from Celem --------/*)
2.41 -
2.42 -(**)end(**)
3.1 --- a/src/Tools/isac/Build_Isac.thy Tue Apr 21 16:53:17 2020 +0200
3.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 22 11:06:48 2020 +0200
3.3 @@ -150,11 +150,11 @@
3.4 REPLACE BY Know_Store... (has been overlooked)
3.5 calcelems.sml:val rew_ord' = Unsynchronized.ref ...
3.6 KEEP FOR TRACING
3.7 - calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
3.8 - calcelems.sml:val depth = Unsynchronized.ref 99999;
3.9 - calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
3.10 - calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
3.11 - Interpret/script.sml:val trace_LI = Unsynchronized.ref false;
3.12 + rewrite.sml:val Rewrite.trace_on = Unsynchronized.ref false;
3.13 + rewrite.sml:val depth = Unsynchronized.ref 99999;
3.14 + rewrite.sml:val lim_rewrite = Unsynchronized.ref 99999;
3.15 + rewrite.sml:val lim_deriv = Unsynchronized.ref 100;
3.16 + Interpret/rewtools.sml:val LItool.trace = Unsynchronized.ref false;
3.17 KEEP FOR EASIER DEVELOPMENT
3.18 calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
3.19 KEEP FOR DEMOS
4.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue Apr 21 16:53:17 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 22 11:06:48 2020 +0200
4.3 @@ -24,6 +24,8 @@
4.4 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
4.5 val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
4.6 Program.leaf * term option
4.7 +
4.8 + val trace_on: bool Unsynchronized.ref
4.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.10 (*NONE*)
4.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.12 @@ -31,9 +33,6 @@
4.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.14 end
4.15
4.16 -(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
4.17 -val trace_LI = Unsynchronized.ref false; (* TODO: adopt Isabelle's tracing *)
4.18 -
4.19 (**)
4.20 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
4.21 struct
4.22 @@ -41,6 +40,9 @@
4.23 open Ctree
4.24 open Pos
4.25
4.26 +(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
4.27 +val trace_on = Unsynchronized.ref false; (* TODO: adopt Isabelle's tracing *)
4.28 +
4.29 (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
4.30 fun implicit_take (Rule.Prog prog) env =
4.31 (case Prog_Tac.get_first_argument prog of
4.32 @@ -102,7 +104,7 @@
4.33 | Not_Associated;
4.34
4.35 fun trace_msg_3 tac =
4.36 - if (!trace_LI) then
4.37 + if (!trace_on) then
4.38 tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
4.39 "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
4.40 else ();
4.41 @@ -262,7 +264,7 @@
4.42 "formals: " ^ UnparseC.terms formals ^ "\n" ^
4.43 "actuals: " ^ UnparseC.terms actuals
4.44 fun trace_init metID =
4.45 - if (!trace_LI)
4.46 + if (!trace_on)
4.47 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
4.48 else ();
4.49 in
4.50 @@ -330,11 +332,11 @@
4.51
4.52
4.53 fun trace_msg_1 call t stac =
4.54 - if (! trace_LI) then
4.55 + if (! trace_on) then
4.56 tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \<longrightarrow> Tac \"" ^ UnparseC.term stac ^ "\"")
4.57 else ();
4.58 fun trace_msg_2 call t lexpr' =
4.59 - if (! trace_LI) then
4.60 + if (! trace_on) then
4.61 tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"")
4.62 else ();
4.63 (*
5.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Apr 21 16:53:17 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 22 11:06:48 2020 +0200
5.3 @@ -124,6 +124,8 @@
5.4 WN060825 too complicated for the intended use by cancel_, common_nominator_
5.5 and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
5.6 -- replaced below *)
5.7 +
5.8 +
5.9 fun make_deriv thy erls rs ro goal tt =
5.10 let
5.11 datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
5.12 @@ -137,20 +139,20 @@
5.13 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
5.14 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
5.15 if lim < 0
5.16 - then (tracing ("make_deriv exceeds " ^ int2str (! Trace.lim_deriv) ^ "with deriv =\n");
5.17 + then (tracing ("make_deriv exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with deriv =\n");
5.18 tracing (deriv2str rts); rts)
5.19 else
5.20 (case r of
5.21 Rule.Thm (thmid, tm) =>
5.22 - (if not (! Trace.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
5.23 + (if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
5.24 case Rewrite.rewrite_ thy ro erls true tm t of
5.25 NONE => rew_once lim rts t apno rs'
5.26 | SOME (t', a') =>
5.27 - (if ! Trace.trace_rewrite then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
5.28 + (if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
5.29 rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
5.30 | Rule.Eval (c as (op_, _)) =>
5.31 let
5.32 - val _ = if not (! Trace.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
5.33 + val _ = if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"")
5.34 val t = TermC.uminus_to_string t
5.35 in
5.36 case Eval.adhoc_thm thy c t of
5.37 @@ -160,7 +162,7 @@
5.38 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
5.39 SOME ta => ta
5.40 | NONE => error "adhoc_thm: NONE"
5.41 - val _ = if not (! Trace.trace_rewrite) then () else tracing("=== calc. to: " ^ UnparseC.term t')
5.42 + val _ = if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
5.43 val r' = Rule.Thm (thmid, tm)
5.44 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
5.45 handle _ => error "derive_norm, Eval: no rewrite"
5.46 @@ -172,7 +174,7 @@
5.47 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
5.48 | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
5.49 | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
5.50 - in rew_once (! Trace.lim_deriv) [] tt Noap rs end
5.51 + in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
5.52
5.53 (*version for reverse rewrite used before 040214*)
5.54 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
6.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 16:53:17 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Apr 22 11:06:48 2020 +0200
6.3 @@ -3,33 +3,38 @@
6.4 *)
6.5
6.6 signature REWRITE =
6.7 - sig
6.8 - val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
6.9 - val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
6.10 - val eval_prog_expr: theory -> Rule_Set.T -> term -> term
6.11 - val eval_true_: theory -> Rule_Set.T -> term -> bool
6.12 - val eval_true: theory -> term list -> Rule_Set.T -> bool
6.13 - val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
6.14 - -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
6.15 - val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
6.16 - term -> (term * term list) option
6.17 - val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
6.18 - -> (term * term) list -> thm -> term -> (term * term list) option
6.19 - val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
6.20 - val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
6.21 - val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
6.22 - -> term -> (term * term list) option
6.23 +sig
6.24 + val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
6.25 + val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
6.26 + val eval_prog_expr: theory -> Rule_Set.T -> term -> term
6.27 + val eval_true_: theory -> Rule_Set.T -> term -> bool
6.28 + val eval_true: theory -> term list -> Rule_Set.T -> bool
6.29 + val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
6.30 + -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
6.31 + val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
6.32 + term -> (term * term list) option
6.33 + val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
6.34 + -> (term * term) list -> thm -> term -> (term * term list) option
6.35 + val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
6.36 + val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
6.37 + val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
6.38 + -> term -> (term * term list) option
6.39 +
6.40 + val trace_on: bool Unsynchronized.ref
6.41 + val depth: int Unsynchronized.ref
6.42 + val lim_deriv: int Unsynchronized.ref
6.43 +
6.44 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.45 (* NONE *)
6.46 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.47 - val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
6.48 - Rule_Set.T -> bool -> thm -> term -> (term * term list) option
6.49 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
6.50 - val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
6.51 - val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
6.52 - val trace1: int -> string -> unit
6.53 + val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
6.54 + Rule_Set.T -> bool -> thm -> term -> (term * term list) option
6.55 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
6.56 + val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
6.57 + val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
6.58 + val trace1: int -> string -> unit
6.59 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.60 - end
6.61 +end
6.62
6.63 (**)
6.64 structure Rewrite(**): REWRITE(**) =
6.65 @@ -39,10 +44,16 @@
6.66 exception NO_REWRITE;
6.67 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
6.68
6.69 +val trace_on = Unsynchronized.ref false;
6.70 +(* depth of recursion in traces of the rewriter, if trace_on:=true *)
6.71 +val depth = Unsynchronized.ref 99999;
6.72 +(* no of rewrites exceeding this int -> NO rewrite *)
6.73 +val lim_deriv = Unsynchronized.ref 100;
6.74 +
6.75 fun trace i str =
6.76 - if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" i ^ str) else ()
6.77 + if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
6.78 fun trace1 i str =
6.79 - if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ str) else ()
6.80 + if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
6.81
6.82 fun rewrite__ thy i bdv tless rls put_asm thm ct =
6.83 let
6.84 @@ -58,7 +69,7 @@
6.85 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
6.86 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
6.87 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
6.88 - val _ = if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
6.89 + val _ = if ! trace_on andalso i < ! depth andalso p' <> []
6.90 then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
6.91 val (t'', p'') = (*conditional rewriting*)
6.92 let
6.93 @@ -66,20 +77,20 @@
6.94 in
6.95 if nofalse
6.96 then
6.97 - (if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
6.98 + (if ! trace_on andalso i < ! depth andalso p' <> []
6.99 then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
6.100 " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
6.101 else();
6.102 (t',simpl_p')) (* uncond.rew. from above*)
6.103 else
6.104 - (if ! Trace.trace_rewrite andalso i < ! Trace.depth
6.105 + (if ! trace_on andalso i < ! depth
6.106 then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
6.107 else();
6.108 raise STOP_REW_SUB (* don't go into subterms of cond *))
6.109 end
6.110 in
6.111 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
6.112 - then (if ! Trace.trace_rewrite andalso i < ! Trace.depth
6.113 + then (if ! trace_on andalso i < ! depth
6.114 then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
6.115 else ();
6.116 raise NO_REWRITE)
7.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Apr 21 16:53:17 2020 +0200
7.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Wed Apr 22 11:06:48 2020 +0200
7.3 @@ -3,32 +3,34 @@
7.4 *)
7.5
7.6 signature NUMERAL_CALCULATION =
7.7 - sig
7.8 - type float
7.9 - val calc_equ: string -> int * int -> bool
7.10 - val power: int -> int -> int
7.11 - val sign_mult: int -> int -> int
7.12 - val squfact: int -> int
7.13 - val gcd: int -> int -> int
7.14 - val sqrt: int -> int
7.15 - val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
7.16 - val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
7.17 - val norm: term -> term
7.18 - val popt2str: ('a * term) option -> string
7.19 - val numeral: term -> ((int * int) * (int * int)) option
7.20 - val calcul: string -> float -> float -> float
7.21 - val term_of_float: typ -> float -> term
7.22 - val var_op_float: term -> string -> typ -> typ ->float -> term
7.23 - val float_op_var: term -> string -> typ -> typ -> float -> term
7.24 +sig
7.25 + type float
7.26 + val calc_equ: string -> int * int -> bool
7.27 + val power: int -> int -> int
7.28 + val sign_mult: int -> int -> int
7.29 + val squfact: int -> int
7.30 + val gcd: int -> int -> int
7.31 + val sqrt: int -> int
7.32 + val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
7.33 + val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
7.34 + val norm: term -> term
7.35 + val popt2str: ('a * term) option -> string
7.36 + val numeral: term -> ((int * int) * (int * int)) option
7.37 + val calcul: string -> float -> float -> float
7.38 + val term_of_float: typ -> float -> term
7.39 + val var_op_float: term -> string -> typ -> typ ->float -> term
7.40 + val float_op_var: term -> string -> typ -> typ -> float -> term
7.41 + val trace_on: bool Unsynchronized.ref
7.42 +
7.43 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.44 (* NONE *)
7.45 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.46 - val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
7.47 - val mk_rule: term list * term * term -> term
7.48 - val divisors: int -> int list
7.49 - val doubles: int list -> int list
7.50 + val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
7.51 + val mk_rule: term list * term * term -> term
7.52 + val divisors: int -> int list
7.53 + val doubles: int list -> int list
7.54 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.55 - end
7.56 +end
7.57
7.58 (**)
7.59 structure Eval(**): NUMERAL_CALCULATION(**) =
7.60 @@ -37,7 +39,10 @@
7.61
7.62 type float =
7.63 (int * int) (* value: significand * exponent *)
7.64 - * (int * int) (* precision: significand * exponent *)
7.65 + * (int * int); (* precision: significand * exponent *)
7.66 +
7.67 +(* trace internal steps of isac's numeral calculations *)
7.68 +val trace_on = Unsynchronized.ref false;
7.69
7.70 (** calculate integers **)
7.71
7.72 @@ -94,15 +99,15 @@
7.73 ^^^^^^... the selecting operator op_ (variable for eval_binop)
7.74 *)
7.75 fun trace_calc0 str =
7.76 - if ! Trace.trace_calc then writeln ("### " ^ str) else ()
7.77 + if ! trace_on then writeln ("### " ^ str) else ()
7.78 fun trace_calc1 str1 str2 =
7.79 - if ! Trace.trace_calc then writeln (str1 ^ str2) else ()
7.80 + if ! trace_on then writeln (str1 ^ str2) else ()
7.81 fun trace_calc2 str term popt =
7.82 - if ! Trace.trace_calc then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
7.83 + if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
7.84 fun trace_calc3 str term =
7.85 - if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term term) else ()
7.86 + if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
7.87 fun trace_calc4 str t1 t2 =
7.88 - if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
7.89 + if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
7.90
7.91 fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
7.92 if op_ = op0 then
8.1 --- a/src/Tools/isac/TODO.thy Tue Apr 21 16:53:17 2020 +0200
8.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 22 11:06:48 2020 +0200
8.3 @@ -216,7 +216,7 @@
8.4 \item automatically extrac rls from program-code
8.5 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
8.6 \item xxx
8.7 - \item finish output of trace_LI with Check_Postcond (useful for SubProblem)
8.8 + \item finish output of LItool.trace with Check_Postcond (useful for SubProblem)
8.9 \item xxx
8.10 \item replace Rule_Set.empty by Rule_Set.Empty
8.11 latter is more clear, but replacing ***breaks rewriting over all examples***,
9.1 --- a/src/Tools/isac/Test_Code/test-code.sml Tue Apr 21 16:53:17 2020 +0200
9.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Apr 22 11:06:48 2020 +0200
9.3 @@ -9,9 +9,11 @@
9.4 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
9.5 val f2str : Generate.mout -> TermC.as_string
9.6 val TESTg_form : Calc.T -> Generate.mout
9.7 +
9.8 val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
9.9 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
9.10 Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
9.11 +
9.12 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
9.13 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
9.14 Calc.T * Tactic.input * Generate.mout
10.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Apr 21 16:53:17 2020 +0200
10.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Apr 22 11:06:48 2020 +0200
10.3 @@ -652,7 +652,7 @@
10.4 of simplification occurs right here, in the next step.\<close>
10.5
10.6 ML \<open>
10.7 - Trace.trace_rewrite := false;
10.8 + Rewrite.trace_on := false;
10.9 val SOME fract1 =
10.10 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
10.11 (*
10.12 @@ -1242,8 +1242,8 @@
10.13 tree and check if every node implements that what we have wanted.\<close>
10.14
10.15 ML \<open>
10.16 - Trace.trace_rewrite := false; (*true*)
10.17 - trace_LI := false; (*true*)
10.18 + Rewrite.trace_on := false; (*true*)
10.19 + LItool.trace_on := false; (*true*)
10.20 print_depth 9;
10.21
10.22 val fmz =
10.23 @@ -1492,7 +1492,7 @@
10.24 \<close>
10.25
10.26 ML \<open>
10.27 -trace_LI := true;
10.28 +LItool.trace_on := true;
10.29 \<close>
10.30 ML \<open>
10.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
11.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Tue Apr 21 16:53:17 2020 +0200
11.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Wed Apr 22 11:06:48 2020 +0200
11.3 @@ -55,7 +55,7 @@
11.4 \<close>
11.5 ML \<open>
11.6 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t;
11.7 -Celem.Trace.trace_rewrite := false;
11.8 +Rewrite.trace_on := false;
11.9 \<close>
11.10
11.11 section \<open>Note on bound variables\<close>
11.12 @@ -155,13 +155,13 @@
11.13 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
11.14 \<close>
11.15 text \<open>The simplifiers are quite busy when finding the above results. you can
11.16 - watch them at work by setting the switch 'Trace.trace_rewrite:\<close>
11.17 + watch them at work by setting the switch 'Rewrite.trace_on:\<close>
11.18 ML \<open>
11.19 -Celem.Trace.trace_rewrite := false;
11.20 +Celem.Rewrite.trace_on := false;
11.21 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
11.22 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
11.23 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
11.24 -Celem.Trace.trace_rewrite := false;
11.25 +Celem.Rewrite.trace_on := false;
11.26 \<close>
11.27 text \<open>You see what happend when you click the checkbox <Tracing> on the bar
11.28 separating this window from the Output-window.
12.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue Apr 21 16:53:17 2020 +0200
12.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 22 11:06:48 2020 +0200
12.3 @@ -44,8 +44,8 @@
12.4 else error "script.sml fun specific_from_prog diff.behav. 2"
12.5 | _ => error "script.sml fun specific_from_prog diff.behav. 1";
12.6
12.7 -trace_LI := true;
12.8 -trace_LI := false;
12.9 +LItool.trace_on := true;
12.10 +LItool.trace_on := false;
12.11 applyTactic 1 p (hd appltacs);
12.12 val ((pt, p), _) = get_calc 1; show_pt pt;
12.13 val appltacs = specific_from_prog pt p;
13.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Tue Apr 21 16:53:17 2020 +0200
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Wed Apr 22 11:06:48 2020 +0200
13.3 @@ -81,8 +81,8 @@
13.4 if UnparseC.term x1__ = "0" then ()
13.5 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
13.6
13.7 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
13.8 -Trace.trace_rewrite:=false;
13.9 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
13.10 +Rewrite.trace_on:=false;
13.11
13.12 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
13.13 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
14.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Apr 21 16:53:17 2020 +0200
14.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Apr 22 11:06:48 2020 +0200
14.3 @@ -326,8 +326,8 @@
14.4 Iterator 1;
14.5 moveActiveRoot 1;
14.6 autoCalculate 1 CompleteCalc;
14.7 -(* Trace.trace_rewrite := true;
14.8 - trace_LI := false;
14.9 +(* Rewrite.trace_on := true;
14.10 + LItool.trace_on := false;
14.11 *)
14.12 val ((pt,p),_) = get_calc 1; show_pt pt;
14.13
14.14 @@ -346,12 +346,12 @@
14.15 ["diff","after_simplification"]))];
14.16 Iterator 1;
14.17 moveActiveRoot 1;
14.18 -(* Trace.trace_rewrite := true;
14.19 - trace_LI := true;
14.20 +(* Rewrite.trace_on := true;
14.21 + LItool.trace_on := true;
14.22 *)
14.23 autoCalculate 1 CompleteCalc;
14.24 -(* Trace.trace_rewrite := false;
14.25 - trace_LI := false;
14.26 +(* Rewrite.trace_on := false;
14.27 + LItool.trace_on := false;
14.28 *)
14.29 val ((pt,p),_) = get_calc 1; show_pt pt;
14.30 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
15.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Apr 21 16:53:17 2020 +0200
15.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 22 11:06:48 2020 +0200
15.3 @@ -6,7 +6,7 @@
15.4 use"diffapp.sml";
15.5 *)
15.6
15.7 -Trace.trace_rewrite := false;
15.8 +Rewrite.trace_on := false;
15.9 "Contents----------------------------------------------";
15.10 " Specify_Problem (match_itms_oris) ";
15.11 " test specify, fmz <> [] ";
15.12 @@ -671,9 +671,9 @@
15.13 UnparseC.term s;
15.14 val t = str2term
15.15 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
15.16 -Trace.trace_rewrite := false;
15.17 +Rewrite.trace_on := false;
15.18 val SOME (t',_) = rewrite_set_ thy false prog_expr t;
15.19 -Trace.trace_rewrite:=false;
15.20 +Rewrite.trace_on:=false;
15.21 val s' = UnparseC.term t';
15.22 (*=== inhibit exn 110726=============================================================
15.23 if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1.";
16.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Apr 21 16:53:17 2020 +0200
16.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 22 11:06:48 2020 +0200
16.3 @@ -3,7 +3,7 @@
16.4 (c) due to copyright terms
16.5 *)
16.6
16.7 -Trace.trace_rewrite := false;
16.8 +Rewrite.trace_on := false;
16.9 "-----------------------------------------------------------------";
16.10 "table of contents -----------------------------------------------";
16.11 "-----------------------------------------------------------------";
16.12 @@ -360,7 +360,7 @@
16.13 [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
16.14 val t = str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
16.15 "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]");
16.16 -Trace.trace_rewrite := false;
16.17 +Rewrite.trace_on := false;
16.18 val SOME (t',_) = rewrite_set_ thy false prls_triangular t;
16.19 (*found:...
16.20 ## try thm: NTH_CONS
16.21 @@ -372,7 +372,7 @@
16.22 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"]
16.23
16.24 ... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
16.25 -Trace.trace_rewrite:=false;
16.26 +Rewrite.trace_on:=false;
16.27
16.28 "===== case 3: relaxed preconditions for triangular system =====";
16.29 val fmz = ["equalities [L * q_0 = c, \
16.30 @@ -421,9 +421,9 @@
16.31 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
16.32 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
16.33 "solveForVars [c, c_2]", "solution LL"];
16.34 -Trace.trace_rewrite := false;
16.35 +Rewrite.trace_on := false;
16.36 val matches = refine fmz ["2x2", "LINEAR","system"];
16.37 -Trace.trace_rewrite:=false;
16.38 +Rewrite.trace_on:=false;
16.39 (*default_print_depth 11;*) matches; (*default_print_depth 3;*)
16.40 (*brought: 'False "length_ es_ = 2"'*)
16.41
16.42 @@ -653,7 +653,7 @@
16.43 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
16.44 moveActiveRoot 1;
16.45 (*
16.46 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.47 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.48 ##7.27## ordered substs
16.49 c_4 c_2
16.50 c c_2 c_3 c_4 c c_2 1->2: c
16.51 @@ -698,7 +698,7 @@
16.52 ["Biegelinien", "AusMomentenlinie"]))];
16.53 (*
16.54 moveActiveRoot 1;
16.55 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.56 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.57 *)
16.58
16.59 "------- Bsp 7.69";
16.60 @@ -709,7 +709,7 @@
16.61 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
16.62 moveActiveRoot 1;
16.63 (*
16.64 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.65 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.66 ##7.69## ordered subst 2x2
16.67 c_4 c_3
16.68 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
16.69 @@ -729,7 +729,7 @@
16.70 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
16.71 moveActiveRoot 1;
16.72 (*
16.73 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.74 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.75 ##7.70## |subst
16.76 c |
16.77 c c_2 |1:c -> 2:c_2
16.78 @@ -846,7 +846,7 @@
16.79 ["IntegrierenUndKonstanteBestimmen2"] ))];
16.80 moveActiveRoot 1;
16.81 (*
16.82 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.83 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.84 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
16.85 c c_2 |c c_2 |1' |1': c c_2 |
16.86 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
16.87 @@ -868,7 +868,7 @@
16.88 ["Biegelinien", "AusMomentenlinie"]))];
16.89 moveActiveRoot 1;
16.90 (*
16.91 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.92 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.93 *)
16.94
16.95 "------- Bsp 7.72b";
16.96 @@ -881,7 +881,7 @@
16.97 ["IntegrierenUndKonstanteBestimmen2"] ))];
16.98 moveActiveRoot 1;
16.99 (*
16.100 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.101 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.102 ##7.72b## |ord. |subst.singles |ord.triang.
16.103 c_2 | | |c_2
16.104 c c_2 | |1:c_2 -> 2':c |c_2 c
16.105 @@ -902,7 +902,7 @@
16.106 ["Biegelinien", "AusMomentenlinie"]))];
16.107 moveActiveRoot 1;
16.108 (*
16.109 -trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.110 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
16.111 *)
16.112
16.113 "----------- 4x4 systems from Biegelinie -------------------------";
17.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Apr 21 16:53:17 2020 +0200
17.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Apr 22 11:06:48 2020 +0200
17.3 @@ -426,7 +426,7 @@
17.4 exception Empty raised (line 429 of "library.ML") TODO during lucin: *)
17.5
17.6 (*
17.7 -trace_LI := true;
17.8 +LItool.trace_on := true;
17.9
17.10 @@@ program ["simplification","of_rationals","to_partial_fraction"]
17.11 @@@ istate ["
18.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Apr 21 16:53:17 2020 +0200
18.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Apr 22 11:06:48 2020 +0200
18.3 @@ -341,7 +341,7 @@
18.4 if UnparseC.term t' = "x * x ^^^ 2" then ()
18.5 else error "poly.sml Poly.is'_multUnordered doesn't work";
18.6
18.7 -(* 100928 Trace.trace_rewrite shows the first occurring difference in 267b:
18.8 +(* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
18.9 ### rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
18.10 (-48 * x ^^^ 4 + 8))
18.11 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
18.12 @@ -575,12 +575,12 @@
18.13 (*default_print_depth 3;*)
18.14 (*if there is ...
18.15 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
18.16 -... then Trace.trace_rewrite:*)
18.17 +... then Rewrite.trace_on:*)
18.18
18.19 "-----2 ---";
18.20 -Trace.trace_rewrite := false;
18.21 +Rewrite.trace_on := false;
18.22 match_pbl fmz pbt;
18.23 -Trace.trace_rewrite := false;
18.24 +Rewrite.trace_on := false;
18.25 (*... if there is no rewrite, then there is something wrong with prls*)
18.26
18.27 "-----3 ---";
19.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Apr 21 16:53:17 2020 +0200
19.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 22 11:06:48 2020 +0200
19.3 @@ -49,8 +49,8 @@
19.4 "----------- tests on predicates in problems ---------------------";
19.5 "----------- tests on predicates in problems ---------------------";
19.6 "----------- tests on predicates in problems ---------------------";
19.7 -(* Trace.trace_rewrite:=true;
19.8 - Trace.trace_rewrite:=false;
19.9 +(* Rewrite.trace_on:=true;
19.10 + Rewrite.trace_on:=false;
19.11 *)
19.12 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
19.13 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
19.14 @@ -160,7 +160,7 @@
19.15 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
19.16
19.17 (*das rewriting l"asst sich beobachten mit
19.18 -Trace.trace_rewrite := false;
19.19 +Rewrite.trace_on := false;
19.20 *)
19.21
19.22 "------15.11.02 --------------------------";
19.23 @@ -168,7 +168,7 @@
19.24 val bdv = (Thm.term_of o the o (parse thy)) "bdv";
19.25 val a = (Thm.term_of o the o (parse thy)) "a";
19.26
19.27 -Trace.trace_rewrite := false;
19.28 +Rewrite.trace_on := false;
19.29 (* Anwenden einer Regelmenge aus Termorder.ML: *)
19.30 val SOME (t,_) =
19.31 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
20.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Tue Apr 21 16:53:17 2020 +0200
20.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Wed Apr 22 11:06:48 2020 +0200
20.3 @@ -256,9 +256,9 @@
20.4 (* the invisible parentheses are as expected *)
20.5
20.6 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
20.7 -Trace.trace_rewrite:=(*true*)false;
20.8 +Rewrite.trace_on:=(*true*)false;
20.9 rewrite_set_ thy false expand_binoms t;
20.10 -Trace.trace_rewrite:=false;
20.11 +Rewrite.trace_on:=false;
20.12
20.13
20.14 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
21.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue Apr 21 16:53:17 2020 +0200
21.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Apr 22 11:06:48 2020 +0200
21.3 @@ -66,13 +66,13 @@
21.4 "----------- watch order_add_mult -------------------------------";
21.5 "----------- watch order_add_mult -------------------------------";
21.6 "----- with these simple variables it works...";
21.7 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
21.8 -Trace.trace_rewrite:=false;
21.9 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
21.10 +Rewrite.trace_on:=false;
21.11 val t = str2term "((a + d) + c) + b";
21.12 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
21.13 if UnparseC.term t = "a + (b + (c + d))" then ()
21.14 else error "polyminus.sml 1 watch order_add_mult";
21.15 -Trace.trace_rewrite:=false;
21.16 +Rewrite.trace_on:=false;
21.17
21.18 "----- the same stepwise...";
21.19 val od = ord_make_polynomial true (@{theory "Poly"});
21.20 @@ -169,7 +169,7 @@
21.21 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
21.22
21.23 "======= test rewrite_, rewrite_set_";
21.24 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
21.25 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
21.26 val erls = erls_ordne_alphabetisch;
21.27 val t = str2term "b + a";
21.28 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
21.29 @@ -227,8 +227,8 @@
21.30 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
21.31 else error "polyminus.sml: verschoenere 3 + -2 * e ...";
21.32
21.33 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
21.34 -Trace.trace_rewrite:=false;
21.35 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
21.36 +Rewrite.trace_on:=false;
21.37
21.38 "----------- met simplification for_polynomials with_minus -------";
21.39 "----------- met simplification for_polynomials with_minus -------";
21.40 @@ -420,7 +420,7 @@
21.41 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
21.42 val ((pt,p),_) = get_calc 1; show_pt pt;
21.43 "----- 2 ^^^";
21.44 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
21.45 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
21.46 val erls = erls_ordne_alphabetisch;
21.47 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
21.48 val SOME (t',_) =
21.49 @@ -435,7 +435,7 @@
21.50 val SOME (t',_) =
21.51 rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
21.52 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
21.53 -Trace.trace_rewrite := false;
21.54 +Rewrite.trace_on := false;
21.55
21.56
21.57 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
21.58 @@ -577,9 +577,9 @@
21.59 (*"(~ True) = False"*)
21.60 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
21.61 (*"(~ False) = True"*)];
21.62 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
21.63 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
21.64 val SOME (t', _) = rewrite_set_ thy false prls t;
21.65 -Trace.trace_rewrite := false;
21.66 +Rewrite.trace_on := false;
21.67
21.68 "--- does the respective prls rewrite the whole predicate ?";
21.69 val t = str2term
21.70 @@ -587,9 +587,9 @@
21.71 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
21.72 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
21.73 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
21.74 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
21.75 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
21.76 val SOME (t', _) = rewrite_set_ thy false prls t;
21.77 -Trace.trace_rewrite := false;
21.78 +Rewrite.trace_on := false;
21.79 if UnparseC.term t' = "False" then ()
21.80 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
21.81
22.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Apr 21 16:53:17 2020 +0200
22.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Apr 22 11:06:48 2020 +0200
22.3 @@ -336,7 +336,7 @@
22.4 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
22.5 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
22.6 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
22.7 -Trace.trace_rewrite := false (*true false*);
22.8 +Rewrite.trace_on := false (*true false*);
22.9 (* trace stops with ...: (and then jEdit hangs)..
22.10 rewrite_set_ thy false norm_Rational t;
22.11 :
22.12 @@ -438,10 +438,10 @@
22.13 (* required for applying thms in rewriting ^^^^*)
22.14 (* we get details from here..*)
22.15
22.16 -Trace.trace_rewrite := false;
22.17 +Rewrite.trace_on := false;
22.18 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
22.19 -Celem.Trace.trace_rewrite := false;
22.20 -(* Trace.trace_rewrite:
22.21 +Celem.Rewrite.trace_on := false;
22.22 +(* Rewrite.trace_on:
22.23 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
22.24 (* |||||||||||||||||||||||||||||||||||| *)
22.25
22.26 @@ -450,7 +450,7 @@
22.27 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
22.28 val NONE = (*case*) check_frac_sum t (*of*)
22.29
22.30 -(* Trace.trace_rewrite:
22.31 +(* Rewrite.trace_on:
22.32 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
22.33 (* |||||||||||||||||||||||||||| *)
22.34 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
22.35 @@ -481,10 +481,10 @@
22.36 (*AA :: real*)
22.37 (* we get details from here..*)
22.38
22.39 -Celem.Trace.trace_rewrite := false;
22.40 +Celem.Rewrite.trace_on := false;
22.41 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
22.42 -Celem.Trace.trace_rewrite := false;
22.43 -(* Trace.trace_rewrite:
22.44 +Celem.Rewrite.trace_on := false;
22.45 +(* Rewrite.trace_on:
22.46 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
22.47 (* |||||||||||||||||||||||||||||||||||| *)
22.48 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
22.49 @@ -492,7 +492,7 @@
22.50 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
22.51 val NONE = (*case*) check_frac_sum t (*of*)
22.52
22.53 -(* Trace.trace_rewrite:
22.54 +(* Rewrite.trace_on:
22.55 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
22.56 (* |||||||||||||||||||||||||||| *)
22.57 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
22.58 @@ -752,7 +752,7 @@
22.59 (* simpler variant *)
22.60 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty [Rls_ cancel_p, Rls_ add_fractions_p]
22.61 val SOME (t', asm) = rewrite_set_ thy false testrls t;
22.62 -(*Trace.trace_rewrite := false;
22.63 +(*Rewrite.trace_on := false;
22.64 # rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
22.65 ## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
22.66 ## rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
22.67 @@ -949,7 +949,7 @@
22.68 if UnparseC.term t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
22.69 else error "rational.sml 3";
22.70
22.71 -(*Trace.trace_rewrite:=true;*)
22.72 +(*Rewrite.trace_on:=true;*)
22.73 val t = str2term "Not (6*x is_atom)";
22.74 val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';
22.75 "HOL.True";
22.76 @@ -1807,7 +1807,7 @@
22.77 val t = str2term
22.78 ("((a^^^2 - b^^^2)/(2*a*b) + 2*a*b/(a^^^2 - b^^^2)) / ((a^^^2 + b^^^2)/(2*a*b) + 1) / " ^
22.79 "((a^^^2 + b^^^2)^^^2 / (a + b)^^^2)");
22.80 -(* Trace.trace_rewrite := true;
22.81 +(* Rewrite.trace_on := true;
22.82 rewrite_set_ thy false norm_Rational t;
22.83 :
22.84 #### rls: cancel_p on: (2 * (a ^^^ 7 * b) + 4 * (a ^^^ 6 * b ^^^ 2) + 6 * (a ^^^ 5 * b ^^^ 3) +
22.85 @@ -1830,7 +1830,7 @@
22.86 "-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";
22.87 val t = str2term ("(1/x + 1/y + 1/z) / (1/x - 1/y - 1/z) / " ^
22.88 "(2*x^^^2 / (x^^^2 - z^^^2) / (x / (x + z) + x / (x - z)))");
22.89 -(* Trace.trace_rewrite := true;
22.90 +(* Rewrite.trace_on := true;
22.91 rewrite_set_ thy false norm_Rational t;
22.92 :
22.93 #### rls: cancel_p on: (2 * (x ^^^ 6 * (y ^^^ 2 * z)) + 2 * (x ^^^ 6 * (y * z ^^^ 2)) +
22.94 @@ -1860,7 +1860,7 @@
22.95
22.96 anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
22.97
22.98 -"-------- Schalk I, p.70 Nr. 480b: terms are exploding, Trace.trace_rewrite stops at";
22.99 +"-------- Schalk I, p.70 Nr. 480b: terms are exploding, Rewrite.trace_on stops at";
22.100 val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
22.101 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
22.102 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
23.1 --- a/test/Tools/isac/Knowledge/rlang.sml Tue Apr 21 16:53:17 2020 +0200
23.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Apr 22 11:06:48 2020 +0200
23.3 @@ -50,8 +50,8 @@
23.4 }
23.5 *)
23.6
23.7 -(* Trace.trace_rewrite:=true;
23.8 - Trace.trace_rewrite:=false;
23.9 +(* Rewrite.trace_on:=true;
23.10 + Rewrite.trace_on:=false;
23.11 refine fmz ["univariate","equation"];
23.12 *)
23.13 "---- rlang.sml begin-----------------------------------";
23.14 @@ -353,7 +353,7 @@
23.15 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
23.16 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
23.17 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
23.18 -(*Trace.trace_rewrite:=true;
23.19 +(*Rewrite.trace_on:=true;
23.20 *)
23.21 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
23.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
23.23 @@ -1419,10 +1419,10 @@
23.24
23.25
23.26 val t = str2term"(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)";
23.27 -Trace.trace_rewrite := false;
23.28 +Rewrite.trace_on := false;
23.29 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
23.30 UnparseC.term t';
23.31 -Trace.trace_rewrite:=false;
23.32 +Rewrite.trace_on:=false;
23.33
23.34 # rls: norm_Rational on: (a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) = 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)
23.35
23.36 @@ -1635,7 +1635,7 @@
23.37 "------ rlang.sml end---------------------------------";
23.38
23.39 (*------------------------------vvv-Rewrite_Set "rat_eliminate"---------
23.40 -> Trace.trace_rewrite:=true;
23.41 +> Rewrite.trace_on:=true;
23.42 > val t = str2term
23.43 "(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x";
23.44 > val SOME (t',asm) =
23.45 @@ -1643,7 +1643,7 @@
23.46 > UnparseC.term t'; UnparseC.terms asm;
23.47 "(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3)"
23.48 "[\"9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0\",\"x ~= 0\"]"
23.49 -> Trace.trace_rewrite:=false;
23.50 +> Rewrite.trace_on:=false;
23.51 ------------------------------^^^-Rewrite_Set "rat_eliminate"---------*)
23.52
23.53
24.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 16:53:17 2020 +0200
24.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Apr 22 11:06:48 2020 +0200
24.3 @@ -246,8 +246,8 @@
24.4 (writeln o UnparseC.term) t;
24.5 if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
24.6 then () else error "rewrite.sml rewrite_inst_ bdvs";
24.7 -> Trace.trace_rewrite:=true;
24.8 -Trace.trace_rewrite:=false;--------------------------------------------*)
24.9 +> Rewrite.trace_on:=true;
24.10 +Rewrite.trace_on:=false;--------------------------------------------*)
24.11
24.12
24.13 "----------- check diff 2002--2009-3 --------------------";
24.14 @@ -327,7 +327,7 @@
24.15 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
24.16 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
24.17 UnparseC.term t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
24.18 -(*checked visually: Trace.trace_rewrite looks like above for 2009*)
24.19 +(*checked visually: Rewrite.trace_on looks like above for 2009*)
24.20
24.21 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
24.22 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
24.23 @@ -422,9 +422,9 @@
24.24 Const ("HOL.True", _))) => ()
24.25 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
24.26
24.27 -tracing "----- begin rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
24.28 +tracing "----- begin rewrite x^^^2 * x ---"; Rewrite.trace_on := false;
24.29 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
24.30 -tracing "----- end rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
24.31 +tracing "----- end rewrite x^^^2 * x ---"; Rewrite.trace_on := false;
24.32 if UnparseC.term t' = "x * x ^^^ 2" then ()
24.33 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
24.34
24.35 @@ -655,7 +655,7 @@
24.36
24.37 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
24.38
24.39 -(*+*)Trace.trace_rewrite := true;
24.40 +(*+*)Rewrite.trace_on := true;
24.41
24.42 (*this was False; vvvv--- means: indeterminate*)
24.43 val (* SOME (t, a') *)NONE = (*case*)
24.44 @@ -676,7 +676,7 @@
24.45 :
24.46 ### asms accepted: [x \<noteq> 0] stored: []
24.47 : *)
24.48 -Trace.trace_rewrite := false;
24.49 +Rewrite.trace_on := false;
24.50 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
24.51
24.52
25.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Apr 21 16:53:17 2020 +0200
25.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 22 11:06:48 2020 +0200
25.3 @@ -1,5 +1,5 @@
25.4 -(* Trace.trace_rewrite:= true;
25.5 - Trace.trace_rewrite:= false;
25.6 +(* Rewrite.trace_on:= true;
25.7 + Rewrite.trace_on:= false;
25.8
25.9 method "sqrt-equ-test", _NOT_ "square-equation"
25.10 *)
25.11 @@ -546,8 +546,8 @@
25.12 val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
25.13 val SOME (t',asm) = rewrite_set_ thy false rls t;
25.14 UnparseC.term t';
25.15 -> Trace.trace_rewrite:=true;
25.16 - Trace.trace_rewrite:=false;
25.17 +> Rewrite.trace_on:=true;
25.18 + Rewrite.trace_on:=false;
25.19 *)
25.20
25.21 (*me------------
26.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Apr 21 16:53:17 2020 +0200
26.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Apr 22 11:06:48 2020 +0200
26.3 @@ -402,9 +402,9 @@
26.4 "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)
26.5 Ctree.get_assumptions pt p;
26.6 (*it = [] : string list;*)
26.7 -Trace.trace_rewrite := false;
26.8 +Rewrite.trace_on := false;
26.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.10 -Trace.trace_rewrite := false;
26.11 +Rewrite.trace_on := false;
26.12 val asms = Ctree.get_assumptions pt p;
26.13 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
26.14 (str2term "0 <= x",[1]),
27.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Apr 21 16:53:17 2020 +0200
27.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Apr 22 11:06:48 2020 +0200
27.3 @@ -148,7 +148,7 @@
27.4 "----------- check calculate bottom up ------------------";
27.5 "----------- check calculate bottom up ------------------";
27.6 (*-------------- eval_cancel works: *)
27.7 - Trace.trace_rewrite:=false;
27.8 + Rewrite.trace_on := false;
27.9 val thy = @{theory Test};
27.10 val rls = Test_simplify;
27.11 val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
27.12 @@ -166,9 +166,9 @@
27.13 SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
27.14 | _ => error "rewrite_set_ (3+1+2*x)/2 changed";
27.15
27.16 - Trace.trace_rewrite:=false; (*=true3.6.03*)
27.17 + Rewrite.trace_on:=false; (*=true3.6.03*)
27.18
27.19 -(*--- Trace.trace_rewrite before correction of ... --------------------
27.20 +(*--- Rewrite.trace_on before correction of ... --------------------
27.21 val ct = "(-3 + 2 * x + -1) / 2";
27.22 val (ct,_) = the (rewrite_set thy' false rls ct);
27.23 :
27.24 @@ -197,7 +197,7 @@
27.25
27.26
27.27 (*===================*)
27.28 - Trace.trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
27.29 + Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
27.30 val t = (Thm.term_of o the o (parse thy)) "x + (-1 + -3) / 2";
27.31 val SOME (res, []) = rewrite_set_ thy false rls t;
27.32 if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
27.33 @@ -215,7 +215,7 @@
27.34 ### trying calc. 'pow'
27.35 *)
27.36
27.37 - Trace.trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
27.38 + Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
27.39
27.40 "----------- Prog_Expr.pow Power.power_class.power ---------";
27.41 "----------- Prog_Expr.pow Power.power_class.power ---------";
28.1 --- a/test/Tools/isac/ProgLang/listC.sml Tue Apr 21 16:53:17 2020 +0200
28.2 +++ b/test/Tools/isac/ProgLang/listC.sml Wed Apr 22 11:06:48 2020 +0200
28.3 @@ -63,9 +63,9 @@
28.4 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
28.5 val t = str2term "NTH 3 [a,b,c,d,e]";
28.6 atomty t;
28.7 -Trace.trace_rewrite := false;
28.8 +Rewrite.trace_on := false;
28.9 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
28.10 -Trace.trace_rewrite := false;
28.11 +Rewrite.trace_on := false;
28.12 if UnparseC.term t' = "c" then ()
28.13 else error "NTH 3 [a,b,c,d,e] = c ..changed";
28.14
29.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Tue Apr 21 16:53:17 2020 +0200
29.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Wed Apr 22 11:06:48 2020 +0200
29.3 @@ -230,14 +230,14 @@
29.4 if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
29.5 else error "atools.sml diff.behav. in eval_boollist2sum";
29.6
29.7 -Trace.trace_rewrite := false;
29.8 +Rewrite.trace_on := false;
29.9 val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
29.10 [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
29.11 val t = str2t
29.12 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
29.13 case rewrite_set_ thy false srls_ t of SOME _ => ()
29.14 | _ => error "atools.sml diff.rewrite boollist2sum";
29.15 -Trace.trace_rewrite := false;
29.16 +Rewrite.trace_on := false;
29.17
29.18
29.19 "---------fun eval_binop -----------------------------------------------------------------------";