1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 24 12:37:07 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 24 17:21:14 2022 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4  fun check_kestore_rls (rls', (thyID, rls)) =
     1.5    "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
     1.6  
     1.7 -fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
     1.8 +fun check_kestore_calc ((id, (c, _)) : Rule_Def.eval_ml_from_prog)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
     1.9  
    1.10  (* we avoid term_to_string''' defined later *)
    1.11  fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =

     2.1 --- a/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Aug 24 12:37:07 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Aug 24 17:21:14 2022 +0200
     2.3 @@ -7,15 +7,25 @@
     2.4  *)
     2.5  signature EVALUATE__DEFINITION =
     2.6  sig
     2.7 +(*eqtype const_id*)
     2.8    eqtype calID
     2.9 +(*type ml*)
    2.10 +  type cal
    2.11 +(*eqtype.prog_id*)
    2.12    eqtype prog_calcID
    2.13 -  type cal
    2.14 +(*type ml_from_prog*)
    2.15    type calc_elem
    2.16 +(*val equal*)
    2.17    val calc_eq: calc_elem * calc_elem -> bool
    2.18 +(*type ml_fun*)
    2.19    type eval_fn = Rule_Def.eval_fn
    2.20 +(*val ml_fun_empty*)
    2.21    val e_evalfn: Rule_Def.eval_fn
    2.22 +(*val to_store*)
    2.23    val set_data: eval_fn -> theory -> theory
    2.24 +(*val from_store*)
    2.25    val the_data: theory -> eval_fn
    2.26 +(**)
    2.27  end
    2.28  
    2.29  (**)
    2.30 @@ -23,13 +33,13 @@
    2.31  struct
    2.32  (**)
    2.33  
    2.34 -type calID = Rule_Def.calID
    2.35 +type calID = Rule_Def.eval_const_id
    2.36  type prog_calcID = string;
    2.37  (* op in isa-term "Const(op,_)" *)
    2.38 -type cal = Rule_Def.calID * Rule_Def.eval_fn;
    2.39 +type cal = Rule_Def.eval_const_id * Rule_Def.eval_fn;
    2.40  type calc_elem =  (* fun calculate_ fetches the evaluation-function via this list *)
    2.41    prog_calcID *   (* a simple identifier used in programs                    *)
    2.42 -  (Rule_Def.calID *        (* a long identifier used in Const                         *)
    2.43 +  (Rule_Def.eval_const_id *        (* a long identifier used in Const                         *)
    2.44      Rule_Def.eval_fn)      (* an ML function                                          *)
    2.45  fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
    2.46    if pi1 = pi2

     3.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml	Wed Aug 24 12:37:07 2022 +0200
     3.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml	Wed Aug 24 17:21:14 2022 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4    crls       : Rule_Set.T,        (* DEL: for check_elementwise                               *)
     3.5    nrls       : Rule_Set.T,        (* for rewriting by Tactic.Rewrite                          *)
     3.6    errpats    : Error_Pattern_Def.T list, (* error patterns expected in this method            *)
     3.7 -  calc       : Rule_Def.calc list,(* ?DEL                                                     *)
     3.8 +  calc       : Rule_Def.eval_ml_from_prog list,(* ?DEL                                                     *)
     3.9    scr        : Rule.program,      (* filled in MethodC.prep_input                             *)
    3.10    prls       : Rule_Set.T,        (* for evaluation of preconditions in "#Where" on "#Given"  *)
    3.11    ppc        : Model_Pattern.T,   (* contains "#Given", "#Where", "#Find", "#Relate"

     4.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 24 12:37:07 2022 +0200
     4.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 24 17:21:14 2022 +0200
     4.3 @@ -7,8 +7,11 @@
     4.4  *)
     4.5  signature RULE_DEFINITION =
     4.6  sig
     4.7 -  type calc
     4.8 -  eqtype calID
     4.9 +  eqtype eval_const_id
    4.10 +(*eqtype calID*)
    4.11 +  type eval_ml_from_prog
    4.12 +(*type calc*)
    4.13 +
    4.14    eqtype errpatID
    4.15  
    4.16    type rew_ord_id = string
    4.17 @@ -19,11 +22,11 @@
    4.18  
    4.19    datatype rule_set =
    4.20         Empty
    4.21 -     | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
    4.22 +     | Repeat of {calc: eval_ml_from_prog list, erls: rule_set, errpatts: errpatID list, id: string,
    4.23         preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
    4.24 -     | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
    4.25 +     | Sequence of {calc: eval_ml_from_prog list, erls: rule_set, errpatts: errpatID list, id: string,
    4.26         preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
    4.27 -     | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
    4.28 +     | Rrls of {calc: eval_ml_from_prog list, erls: rule_set, errpatts: errpatID list, id: string,
    4.29         prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program}
    4.30    and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule
    4.31       | Rls_ of rule_set | Thm of string * thm
    4.32 @@ -50,10 +53,10 @@
    4.33  type rew_ord_function = LibraryC.subst -> term * term -> bool;
    4.34  type rew_ord_T = rew_ord_id * rew_ord_function;
    4.35  
    4.36 -type calID = string;
    4.37 -type cal = calID * eval_fn;
    4.38 +type eval_const_id = string;
    4.39 +type cal = eval_const_id * eval_fn;
    4.40  type prog_calcID = string;
    4.41 -type calc = (prog_calcID * cal);
    4.42 +type eval_ml_from_prog = (prog_calcID * cal);
    4.43  
    4.44  (* error patterns and fill patterns *)
    4.45  type errpatID = string
    4.46 @@ -114,20 +117,20 @@
    4.47       rew_ord: rew_ord_T,(* for rules                                                  *)                                             
    4.48       erls: rule_set,  (* for the conditions in rules                                  *)
    4.49       srls: rule_set,  (* for evaluation of Prog_Expr                                  *)
    4.50 -     calc: calc list, (* for calculation in program, set by prep_rls'                 *)
    4.51 +     calc: eval_ml_from_prog list, (* for calculation in program, set by prep_rls'                 *)
    4.52       rules: rule list,
    4.53       errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy              *)
    4.54       scr: program}    (* DEPRECATED: intersteps are created on the fly now            *)
    4.55    | Sequence of       (* a sequence of rules to be tried only once                    *)
    4.56      {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set,
    4.57 -     calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
    4.58 +     calc: eval_ml_from_prog list, rules: rule list, errpatts: errpatID list, scr: program}
    4.59    | Rrls of           (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
    4.60      {id: string,      (* for trace_rewrite                                            *)
    4.61       prepat:          (* a guard which guarantees a redex                             *)
    4.62         (term list *   (* preconds, eval with subst from pattern below                 *)
    4.63  		     term)        (* pattern matched with current (sub)term                       *)
    4.64  		   list,          (* meta-conjunction in guarding is or                           *)
    4.65 -     rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
    4.66 +     rew_ord: rew_ord_T, erls: rule_set, calc: eval_ml_from_prog list, errpatts: errpatID list, scr: program}
    4.67  
    4.68  fun program_to_string Empty_Prog = "Empty_Prog"
    4.69    | program_to_string (Prog s) = "Prog " ^ UnparseC.term s

     5.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Aug 24 12:37:07 2022 +0200
     5.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Aug 24 17:21:14 2022 +0200
     5.3 @@ -10,7 +10,7 @@
     5.4    eqtype id
     5.5  
     5.6    val id: T -> string
     5.7 -  val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
     5.8 +  val rep: T -> {calc: Rule_Def.eval_ml_from_prog list, erls: T, errpats: Rule_Def.errpatID list, id: string,
     5.9      preconds: term list, rew_ord: Rewrite_Ord.T, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
    5.10    val to_string: T -> string
    5.11  

     6.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml	Wed Aug 24 12:37:07 2022 +0200
     6.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml	Wed Aug 24 17:21:14 2022 +0200
     6.3 @@ -37,8 +37,8 @@
     6.4  datatype program = datatype Rule_Def.program;
     6.5  type is_as_string = string;
     6.6  
     6.7 -type calc = Rule_Def.calc
     6.8 -type calID = Rule_Def.calID;
     6.9 +type calc = Rule_Def.eval_ml_from_prog
    6.10 +type calID = Rule_Def.eval_const_id;
    6.11  type eval_fn = Rule_Def.eval_fn;
    6.12  
    6.13  fun set_id Rule_Def.Empty = "empty"

     7.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Aug 24 12:37:07 2022 +0200
     7.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Aug 24 17:21:14 2022 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4  sig
     7.5    type authors
     7.6    datatype thydata
     7.7 -    = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
     7.8 +    = Hcal of {calc: Rule_Def.eval_ml_from_prog, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
     7.9      | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rewrite_Ord.function}
    7.10      | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
    7.11      | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
    7.12 @@ -54,7 +54,7 @@
    7.13  | Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
    7.14     thm: thm} (* here no sym_thm, thus no thmID required *)
    7.15  | Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
    7.16 -| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
    7.17 +| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.eval_ml_from_prog}
    7.18  | Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
    7.19      ord: (subst -> (term * term) -> bool)};
    7.20  fun the2str (Html {guh, ...}) = guh

     8.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 24 12:37:07 2022 +0200
     8.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 24 17:21:14 2022 +0200
     8.3 @@ -21,7 +21,7 @@
     8.4    val get_eval: string -> Pos.pos ->Ctree.ctree ->
     8.5      string * ThyC.id * (string * Rule_Def.eval_fn)
     8.6  \<^isac_test>\<open>
     8.7 -  val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
     8.8 +  val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.eval_ml_from_prog list
     8.9  \<close>
    8.10  end
    8.11  

     9.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Wed Aug 24 12:37:07 2022 +0200
     9.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Wed Aug 24 17:21:14 2022 +0200
     9.3 @@ -41,7 +41,7 @@
     9.4  
     9.5  (* a subset of MethodC.T record's fields *)
     9.6  type input = 
     9.7 -  {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
     9.8 +  {calc: Rule_Def.eval_ml_from_prog list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
     9.9      prls: Rule_Set.T, rew_ord': Rewrite_Ord.id, rls': Rule_Set.T, srls: Rule_Set.T}
    9.10  
    9.11  fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)

    10.1 --- a/src/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 12:37:07 2022 +0200
    10.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 17:21:14 2022 +0200
    10.3 @@ -7,6 +7,9 @@
    10.4  
    10.5  signature EVALUATE =
    10.6  sig
    10.7 +(*type ml*)
    10.8 +(*type ml_from_prog*)
    10.9 +
   10.10    val is_num: term -> bool
   10.11    val calc_equ: string -> int * int -> bool
   10.12    val power: int -> int -> int
   10.13 @@ -15,7 +18,7 @@
   10.14    val gcd: int -> int -> int
   10.15    val sqrt: int -> int
   10.16    val cancel_int: int * int -> int * (int * int)
   10.17 -  val adhoc_thm: Proof.context -> string * Eval_Def.eval_fn -> term -> (string * thm) option
   10.18 +  val adhoc_thm: Proof.context -> Eval_Def.cal -> term -> (string * thm) option
   10.19    val adhoc_thm1_: Proof.context -> Eval_Def.cal -> term -> (string * thm) option
   10.20    val norm: term -> term
   10.21    val popt2str: ('a * term) option -> string
   10.22 @@ -33,6 +36,9 @@
   10.23  struct
   10.24  (**)
   10.25  
   10.26 +(*type ml = Eval_Def.ml*)
   10.27 +(*type ml_from_prog = Eval_Def.ml_from_prog*)
   10.28 +
   10.29  val is_num = can HOLogic.dest_number;
   10.30  
   10.31  (* trace internal steps of isac's numeral calculations *)