1.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Tue Apr 21 16:53:17 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Wed Apr 22 11:06:48 2020 +0200
     1.3 @@ -3,32 +3,34 @@
     1.4  *)
     1.5  
     1.6  signature NUMERAL_CALCULATION =
     1.7 -  sig
     1.8 -    type float
     1.9 -    val calc_equ: string -> int * int -> bool
    1.10 -    val power: int -> int -> int
    1.11 -    val sign_mult: int -> int -> int
    1.12 -    val squfact: int -> int
    1.13 -    val gcd: int -> int -> int
    1.14 -    val sqrt: int -> int
    1.15 -    val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
    1.16 -    val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
    1.17 -    val norm: term -> term
    1.18 -    val popt2str: ('a * term) option -> string
    1.19 -    val numeral: term -> ((int * int) * (int * int)) option
    1.20 -    val calcul: string -> float -> float -> float
    1.21 -    val term_of_float: typ -> float -> term
    1.22 -    val var_op_float: term -> string -> typ -> typ ->float -> term
    1.23 -    val float_op_var: term -> string -> typ -> typ -> float -> term
    1.24 +sig
    1.25 +  type float
    1.26 +  val calc_equ: string -> int * int -> bool
    1.27 +  val power: int -> int -> int
    1.28 +  val sign_mult: int -> int -> int
    1.29 +  val squfact: int -> int
    1.30 +  val gcd: int -> int -> int
    1.31 +  val sqrt: int -> int
    1.32 +  val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
    1.33 +  val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
    1.34 +  val norm: term -> term
    1.35 +  val popt2str: ('a * term) option -> string
    1.36 +  val numeral: term -> ((int * int) * (int * int)) option
    1.37 +  val calcul: string -> float -> float -> float
    1.38 +  val term_of_float: typ -> float -> term
    1.39 +  val var_op_float: term -> string -> typ -> typ ->float -> term
    1.40 +  val float_op_var: term -> string -> typ -> typ -> float -> term
    1.41 +  val trace_on: bool Unsynchronized.ref
    1.42 +
    1.43  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.44    (* NONE *)
    1.45  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.46 -    val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
    1.47 -    val mk_rule: term list * term * term -> term
    1.48 -    val divisors: int -> int list
    1.49 -    val doubles: int list -> int list
    1.50 +  val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
    1.51 +  val mk_rule: term list * term * term -> term
    1.52 +  val divisors: int -> int list
    1.53 +  val doubles: int list -> int list
    1.54  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.55 -  end
    1.56 +end
    1.57  
    1.58  (**)
    1.59  structure Eval(**): NUMERAL_CALCULATION(**) =
    1.60 @@ -37,7 +39,10 @@
    1.61  
    1.62  type float =
    1.63    (int * int)   (* value:     significand * exponent *)
    1.64 -  * (int * int) (* precision: significand * exponent *)
    1.65 +  * (int * int); (* precision: significand * exponent *)
    1.66 +
    1.67 +(* trace internal steps of isac's numeral calculations *)
    1.68 +val trace_on = Unsynchronized.ref false;
    1.69  
    1.70  (** calculate integers **)
    1.71  
    1.72 @@ -94,15 +99,15 @@
    1.73              ^^^^^^... the selecting operator op_ (variable for eval_binop)
    1.74  *)
    1.75  fun trace_calc0 str =
    1.76 -  if ! Trace.trace_calc then writeln ("### " ^ str) else ()
    1.77 +  if ! trace_on then writeln ("### " ^ str) else ()
    1.78  fun trace_calc1 str1 str2 =
    1.79 -  if ! Trace.trace_calc then writeln (str1 ^ str2) else ()
    1.80 +  if ! trace_on then writeln (str1 ^ str2) else ()
    1.81  fun trace_calc2 str term popt =
    1.82 -  if ! Trace.trace_calc then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
    1.83 +  if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
    1.84  fun trace_calc3 str term =
    1.85 -  if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term term) else ()
    1.86 +  if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
    1.87  fun trace_calc4 str t1 t2 =
    1.88 -  if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
    1.89 +  if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
    1.90  
    1.91  fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) =                (* unary fns *)
    1.92      if op_ = op0 then