1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 24 18:29:33 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 24 19:02:19 2022 +0200
     1.3 @@ -18,20 +18,10 @@
     1.4  
     1.5    val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
     1.6      string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
     1.7 -(** )
     1.8 -  val get_eval: string -> Pos.pos -> Ctree.ctree ->
     1.9 -    string * ThyC.id * (Eval.ml_fun)
    1.10 -( *original*)
    1.11 -  val get_eval: string -> Pos.pos ->Ctree.ctree ->
    1.12 -    string * ThyC.id * (string * Rule_Def.eval_fn)
    1.13 -(**)
    1.14 +  val get_eval: string -> Pos.pos -> Ctree.ctree -> string * ThyC.id * Eval.ml
    1.15  
    1.16  \<^isac_test>\<open>
    1.17 -(**)
    1.18 -  val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.eval_ml_from_prog list
    1.19 -(*original* )
    1.20 -  val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.eval_ml_from_prog list
    1.21 -( **)
    1.22 +  val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
    1.23  \<close>
    1.24  end
    1.25  
    1.26 @@ -81,7 +71,7 @@
    1.27  	    in
    1.28  	      case opt of
    1.29  	        SOME isa_fn => ("OK", thy', isa_fn)
    1.30 -	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.ml_fun_empty))
    1.31 +	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval.ml_fun_empty))
    1.32  	    end
    1.33      else 
    1.34  		  let
    1.35 @@ -90,7 +80,7 @@
    1.36  		  in
    1.37  		    case assoc (scr_isa_fns, scrop) of
    1.38  		      SOME isa_fn => ("OK",thy',isa_fn)
    1.39 -		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.ml_fun_empty))
    1.40 +		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval.ml_fun_empty))
    1.41  		  end
    1.42    end;
    1.43  

     2.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 24 18:29:33 2022 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 24 19:02:19 2022 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  signature REWRITE =
     2.5  sig
     2.6    exception NO_REWRITE
     2.7 -  val calculate_: Proof.context -> string * Eval_Def.ml_fun -> term -> (term * (string * thm)) option
     2.8 +  val calculate_: Proof.context -> string * Eval.ml_fun -> term -> (term * (string * thm)) option
     2.9    val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool
    2.10    val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
    2.11    val eval_true_: Proof.context -> Rule_Set.T -> term -> bool

     3.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Aug 24 18:29:33 2022 +0200
     3.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Aug 24 19:02:19 2022 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4      val subpbl: string -> string list -> term
     3.5      val stacpbls: term -> term list
     3.6      val op_of_calc: term -> string
     3.7 -    val get_calcs: theory -> term -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
     3.8 +    val get_calcs: theory -> term -> Eval_Def.ml_from_prog list
     3.9      val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
    3.10      val gen: theory -> term -> Rule_Set.T -> term
    3.11  \<^isac_test>\<open>

     4.1 --- a/src/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 18:29:33 2022 +0200
     4.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 19:02:19 2022 +0200
     4.3 @@ -9,6 +9,7 @@
     4.4  sig
     4.5    type ml
     4.6    type ml_fun
     4.7 +  val ml_fun_empty: ml_fun
     4.8    type ml_from_prog
     4.9  
    4.10    val is_num: term -> bool
    4.11 @@ -39,6 +40,7 @@
    4.12  
    4.13  type ml = Eval_Def.ml
    4.14  type ml_fun = Eval_Def.ml_fun
    4.15 +val ml_fun_empty =  Eval_Def.ml_fun_empty
    4.16  type ml_from_prog = Eval_Def.ml_from_prog
    4.17  
    4.18  val is_num = can HOLogic.dest_number;
    4.19 @@ -119,7 +121,7 @@
    4.20  fun trace_calc4 ctxt str t1 t2 =
    4.21    if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
    4.22  
    4.23 -fun get_pair (*1*)ctxt  op_ (ef: Eval_Def.ml_fun) (t as (Const (op0, _) $ arg)) =   (* unary fns *)
    4.24 +fun get_pair (*1*)ctxt  op_ (ef: ml_fun) (t as (Const (op0, _) $ arg)) =   (* unary fns *)
    4.25      if op_ = op0 then 
    4.26        let val popt = ef op_ t ctxt  
    4.27        in case popt of SOME _ => popt | NONE => get_pair ctxt  op_ ef arg end

     5.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Wed Aug 24 18:29:33 2022 +0200
     5.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Wed Aug 24 19:02:19 2022 +0200
     5.3 @@ -14,6 +14,6 @@
     5.4      else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
     5.5  \<close>
     5.6  
     5.7 -setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Eval_Def.ml_fun_empty))]\<close>
     5.8 +setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Eval.ml_fun_empty))]\<close>
     5.9  
    5.10  end

     6.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Wed Aug 24 18:29:33 2022 +0200
     6.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Wed Aug 24 19:02:19 2022 +0200
     6.3 @@ -9,8 +9,8 @@
     6.4  sig
     6.5    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
     6.6    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
     6.7 -  val get_calcs: theory -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
     6.8 -  val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory
     6.9 +  val get_calcs: theory -> Eval.ml_from_prog list
    6.10 +  val add_calcs: Eval.ml_from_prog list -> theory -> theory
    6.11    (*etc*)
    6.12  end;                               
    6.13  
    6.14 @@ -28,7 +28,7 @@
    6.15  
    6.16    val calc_eq = rls_eq
    6.17    structure Data = Theory_Data (
    6.18 -    type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
    6.19 +    type T = Eval.ml_from_prog list;
    6.20      val empty = [];
    6.21      val extend = I;
    6.22      val merge = merge calc_eq;

     7.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 18:29:33 2022 +0200
     7.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 24 19:02:19 2022 +0200
     7.3 @@ -49,10 +49,10 @@
     7.4  val t = TermC.str2term "((1+2)*4/3) \<up> 2";
     7.5  val thy = @{theory};
     7.6  val ctxt = Proof_Context.init_global @{theory}
     7.7 -val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.ml_fun;
     7.8 -val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.ml_fun;
     7.9 -val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.ml_fun;
    7.10 -val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.ml_fun;
    7.11 +val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun;
    7.12 +val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun;
    7.13 +val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun;
    7.14 +val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval.ml_fun;
    7.15  
    7.16  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
    7.17  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;