1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 16:53:17 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Apr 22 11:06:48 2020 +0200
1.3 @@ -3,33 +3,38 @@
1.4 *)
1.5
1.6 signature REWRITE =
1.7 - sig
1.8 - val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
1.9 - val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
1.10 - val eval_prog_expr: theory -> Rule_Set.T -> term -> term
1.11 - val eval_true_: theory -> Rule_Set.T -> term -> bool
1.12 - val eval_true: theory -> term list -> Rule_Set.T -> bool
1.13 - val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
1.14 - -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
1.15 - val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
1.16 - term -> (term * term list) option
1.17 - val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
1.18 - -> (term * term) list -> thm -> term -> (term * term list) option
1.19 - val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
1.20 - val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.21 - val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
1.22 - -> term -> (term * term list) option
1.23 +sig
1.24 + val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
1.25 + val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
1.26 + val eval_prog_expr: theory -> Rule_Set.T -> term -> term
1.27 + val eval_true_: theory -> Rule_Set.T -> term -> bool
1.28 + val eval_true: theory -> term list -> Rule_Set.T -> bool
1.29 + val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
1.30 + -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
1.31 + val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
1.32 + term -> (term * term list) option
1.33 + val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
1.34 + -> (term * term) list -> thm -> term -> (term * term list) option
1.35 + val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
1.36 + val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.37 + val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
1.38 + -> term -> (term * term list) option
1.39 +
1.40 + val trace_on: bool Unsynchronized.ref
1.41 + val depth: int Unsynchronized.ref
1.42 + val lim_deriv: int Unsynchronized.ref
1.43 +
1.44 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.45 (* NONE *)
1.46 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.47 - val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
1.48 - Rule_Set.T -> bool -> thm -> term -> (term * term list) option
1.49 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.50 - val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.51 - val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.52 - val trace1: int -> string -> unit
1.53 + val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
1.54 + Rule_Set.T -> bool -> thm -> term -> (term * term list) option
1.55 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.56 + val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.57 + val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.58 + val trace1: int -> string -> unit
1.59 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.60 - end
1.61 +end
1.62
1.63 (**)
1.64 structure Rewrite(**): REWRITE(**) =
1.65 @@ -39,10 +44,16 @@
1.66 exception NO_REWRITE;
1.67 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
1.68
1.69 +val trace_on = Unsynchronized.ref false;
1.70 +(* depth of recursion in traces of the rewriter, if trace_on:=true *)
1.71 +val depth = Unsynchronized.ref 99999;
1.72 +(* no of rewrites exceeding this int -> NO rewrite *)
1.73 +val lim_deriv = Unsynchronized.ref 100;
1.74 +
1.75 fun trace i str =
1.76 - if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" i ^ str) else ()
1.77 + if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
1.78 fun trace1 i str =
1.79 - if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ str) else ()
1.80 + if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
1.81
1.82 fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.83 let
1.84 @@ -58,7 +69,7 @@
1.85 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
1.86 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.87 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.88 - val _ = if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
1.89 + val _ = if ! trace_on andalso i < ! depth andalso p' <> []
1.90 then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
1.91 val (t'', p'') = (*conditional rewriting*)
1.92 let
1.93 @@ -66,20 +77,20 @@
1.94 in
1.95 if nofalse
1.96 then
1.97 - (if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
1.98 + (if ! trace_on andalso i < ! depth andalso p' <> []
1.99 then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
1.100 " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
1.101 else();
1.102 (t',simpl_p')) (* uncond.rew. from above*)
1.103 else
1.104 - (if ! Trace.trace_rewrite andalso i < ! Trace.depth
1.105 + (if ! trace_on andalso i < ! depth
1.106 then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
1.107 else();
1.108 raise STOP_REW_SUB (* don't go into subterms of cond *))
1.109 end
1.110 in
1.111 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.112 - then (if ! Trace.trace_rewrite andalso i < ! Trace.depth
1.113 + then (if ! trace_on andalso i < ! depth
1.114 then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
1.115 else ();
1.116 raise NO_REWRITE)