1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 28 19:39:06 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 29 09:03:01 2020 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  ML_file unparseC.sml
     1.5  ML_file "rule-def.sml"
     1.6  ML_file "thmC-def.sml"
     1.7 -ML_file "exec-def.sml"       (*rename identifiers by use of struct.id*)
     1.8 +ML_file "eval-def.sml"       (*rename identifiers by use of struct.id*)
     1.9  ML_file "rewrite-order.sml"  (*rename identifiers by use of struct.id*)
    1.10  ML_file rule.sml
    1.11  ML_file "error-pattern-def.sml"
    1.12 @@ -61,8 +61,8 @@
    1.13  sig
    1.14    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    1.15    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    1.16 -  val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
    1.17 -  val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
    1.18 +  val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
    1.19 +  val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
    1.20    val get_cas: theory -> CAS_Def.T list
    1.21    val add_cas: CAS_Def.T list -> theory -> theory
    1.22    val get_ptyps: theory -> Probl_Def.store
    1.23 @@ -90,13 +90,13 @@
    1.24    fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
    1.25  
    1.26    structure Data = Theory_Data (
    1.27 -    type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
    1.28 +    type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
    1.29      val empty = [];
    1.30      val extend = I;
    1.31 -    val merge = merge Exec_Def.calc_eq;
    1.32 +    val merge = merge Eval_Def.calc_eq;
    1.33      );                                                              
    1.34    fun get_calcs thy = Data.get thy
    1.35 -  fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
    1.36 +  fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
    1.37  
    1.38    structure Data = Theory_Data (
    1.39      type T = (term * (Spec.T * (term list -> (term * term list) list))) list;

     2.1 --- a/src/Tools/isac/BaseDefinitions/cas-def.sml	Tue Apr 28 19:39:06 2020 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/cas-def.sml	Wed Apr 29 09:03:01 2020 +0200
     2.3 @@ -2,7 +2,9 @@
     2.4     Author: Walther Neuper
     2.5     (c) due to copyright terms
     2.6  
     2.7 -          *)
     2.8 +Here is a minimum of code required for Know_Store.thy.
     2.9 +For main code see structure CAS_Cmd.
    2.10 +*)
    2.11  signature COMPUTER_ALGEBRA_SYSTEM__COMMAND_DEF =
    2.12  sig
    2.13    type T

     3.1 --- a/src/Tools/isac/BaseDefinitions/error-pattern-def.sml	Tue Apr 28 19:39:06 2020 +0200
     3.2 +++ b/src/Tools/isac/BaseDefinitions/error-pattern-def.sml	Wed Apr 29 09:03:01 2020 +0200
     3.3 @@ -1,6 +1,9 @@
     3.4  (* Title:  BaseDefinitions/error-pattern-def.sml
     3.5     Author: Walther Neuper
     3.6     (c) due to copyright terms
     3.7 +
     3.8 +Here is a minimum of code required for theory Know_Store,
     3.9 +further code see structure Error_Pattern.
    3.10  *)
    3.11  signature ERROR_PATTERN_DEFINITION =
    3.12  sig

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/isac/BaseDefinitions/eval-def.sml	Wed Apr 29 09:03:01 2020 +0200
     4.3 @@ -0,0 +1,50 @@
     4.4 +(* Title:  BaseDefinitions/eval-def.sml
     4.5 +   Author: Walther Neuper
     4.6 +   (c) due to copyright terms
     4.7 +
     4.8 +Here is a minimum of code required for Know_Store.thy.
     4.9 +For main code see structure Eval.
    4.10 +*)
    4.11 +signature EVALUATE__DEFINITION =
    4.12 +sig
    4.13 +  eqtype calID
    4.14 +  eqtype prog_calcID
    4.15 +  type cal
    4.16 +  type calc_elem
    4.17 +  val calc_eq: calc_elem * calc_elem -> bool
    4.18 +  type eval_fn
    4.19 +  val e_evalfn: Rule_Def.eval_fn
    4.20 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    4.21 +  (*NONE*)
    4.22 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    4.23 +  (*NONE*)
    4.24 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.25 +end
    4.26 +
    4.27 +(**)
    4.28 +structure Eval_Def(**): EVALUATE__DEFINITION(**) =
    4.29 +struct
    4.30 +(**)
    4.31 +
    4.32 +type calID = Rule_Def.calID
    4.33 +type prog_calcID = string;
    4.34 +(* op in isa-term "Const(op,_)" *)
    4.35 +type cal = Rule_Def.calID * Rule_Def.eval_fn;
    4.36 +type calc_elem =  (* fun calculate_ fetches the evaluation-function via this list *)
    4.37 +  prog_calcID *   (* a simple identifier used in programs                    *)
    4.38 +  (Rule_Def.calID *        (* a long identifier used in Const                         *)
    4.39 +    Rule_Def.eval_fn)      (* an ML function                                          *)
    4.40 +fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
    4.41 +  if pi1 = pi2
    4.42 +  then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
    4.43 +  else false
    4.44 +
    4.45 +(* eval function calling sml code during rewriting.
    4.46 +Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
    4.47 +  see "fun rule2stac": instead of 
    4.48 +    Eval: calID * eval_fn -> rule
    4.49 +  would be better
    4.50 +    Eval: prog_calcID * (calID * eval_fn)) -> rule*)
    4.51 +type eval_fn = Rule_Def.eval_fn
    4.52 +fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
    4.53 +end

     5.1 --- a/src/Tools/isac/BaseDefinitions/exec-def.sml	Tue Apr 28 19:39:06 2020 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,49 +0,0 @@
     5.4 -(* Title:  BaseDefinitions/exec-def.sml
     5.5 -   Author: Walther Neuper
     5.6 -   (c) due to copyright terms
     5.7 -
     5.8 -TODO: use "Exec_Def" for renaming identifiers
     5.9 -*)
    5.10 -signature EXECUTE_DEFINITION =
    5.11 -sig
    5.12 -  eqtype calID
    5.13 -  eqtype prog_calcID
    5.14 -  type cal
    5.15 -  type calc_elem
    5.16 -  val calc_eq: calc_elem * calc_elem -> bool
    5.17 -  type eval_fn
    5.18 -  val e_evalfn: Rule_Def.eval_fn
    5.19 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    5.20 -  (*NONE*)
    5.21 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    5.22 -  (*NONE*)
    5.23 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.24 -end
    5.25 -
    5.26 -(**)
    5.27 -structure Exec_Def(**): EXECUTE_DEFINITION(**) =
    5.28 -struct
    5.29 -(**)
    5.30 -
    5.31 -type calID = Rule_Def.calID
    5.32 -type prog_calcID = string;
    5.33 -(* op in isa-term "Const(op,_)" *)
    5.34 -type cal = Rule_Def.calID * Rule_Def.eval_fn;
    5.35 -type calc_elem =  (* fun calculate_ fetches the evaluation-function via this list *)
    5.36 -  prog_calcID *   (* a simple identifier used in programs                    *)
    5.37 -  (Rule_Def.calID *        (* a long identifier used in Const                         *)
    5.38 -    Rule_Def.eval_fn)      (* an ML function                                          *)
    5.39 -fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
    5.40 -  if pi1 = pi2
    5.41 -  then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
    5.42 -  else false
    5.43 -
    5.44 -(* eval function calling sml code during rewriting.
    5.45 -Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
    5.46 -  see "fun rule2stac": instead of 
    5.47 -    Eval: calID * eval_fn -> rule
    5.48 -  would be better
    5.49 -    Eval: prog_calcID * (calID * eval_fn)) -> rule*)
    5.50 -type eval_fn = Rule_Def.eval_fn
    5.51 -fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
    5.52 -end

     6.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml	Tue Apr 28 19:39:06 2020 +0200
     6.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml	Wed Apr 29 09:03:01 2020 +0200
     6.3 @@ -2,7 +2,8 @@
     6.4     Author: Walther Neuper
     6.5     (c) due to copyright terms
     6.6  
     6.7 -Will be enhanced by Method later.
     6.8 +Here is a minimum of code required for Know_Store.thy.
     6.9 +For main code see structure Method.
    6.10  *)
    6.11  signature METHOD_DEFINITION =
    6.12  sig

     7.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml	Tue Apr 28 19:39:06 2020 +0200
     7.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml	Wed Apr 29 09:03:01 2020 +0200
     7.3 @@ -2,7 +2,8 @@
     7.4     Author: Walther Neuper
     7.5     (c) due to copyright terms
     7.6  
     7.7 -Will be enhanced by Problem later.
     7.8 +Here is a minimum of code required for Know_Store.thy.
     7.9 +For main code see structure Problem.
    7.10  *)
    7.11  signature PROBLEM_DEFINITION =
    7.12  sig

     8.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Tue Apr 28 19:39:06 2020 +0200
     8.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Apr 29 09:03:01 2020 +0200
     8.3 @@ -2,8 +2,8 @@
     8.4     Author: Walther Neuper
     8.5     (c) due to copyright terms
     8.6  
     8.7 -A minimum of code for a mutual recursive datatype definition
     8.8 -awaiting individual specification later.
     8.9 +Here is a minimum of code required for Know_Store.thy.
    8.10 +For main code see structure Rule.
    8.11  *)
    8.12  signature RULE_DEFINITION =
    8.13  sig

     9.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Tue Apr 28 19:39:06 2020 +0200
     9.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Apr 29 09:03:01 2020 +0200
     9.3 @@ -96,7 +96,7 @@
     9.4  	    preconds = union (op =) pc1 pc2,	    
     9.5  	    erls = merge (merge_ids er1 er2) er1 er2,
     9.6  	    srls = merge (merge_ids sr1 sr2) sr1 sr2,
     9.7 -	    calc = union Exec_Def.calc_eq ca1 ca2,
     9.8 +	    calc = union Eval_Def.calc_eq ca1 ca2,
     9.9  		  rules = union Rule.equal rs1 rs2,
    9.10        errpatts = union (op =) eps1 eps2}
    9.11    | merge id
    9.12 @@ -109,7 +109,7 @@
    9.13  	    preconds = union (op =) pc1 pc2,	    
    9.14  	    erls = merge (merge_ids er1 er2) er1 er2,
    9.15  	    srls = merge (merge_ids sr1 sr2) sr1 sr2,
    9.16 -	    calc = union Exec_Def.calc_eq ca1 ca2,
    9.17 +	    calc = union Eval_Def.calc_eq ca1 ca2,
    9.18  		  rules = union Rule.equal rs1 rs2,
    9.19        errpatts = union (op =) eps1 eps2}
    9.20    | merge id _ _ = error ("merge: \"" ^ id ^ 

    10.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml	Tue Apr 28 19:39:06 2020 +0200
    10.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml	Wed Apr 29 09:03:01 2020 +0200
    10.3 @@ -3,6 +3,8 @@
    10.4     (c) due to copyright terms
    10.5  
    10.6  Probably this structure can be dropped due to improved reflection in Isabelle.
    10.7 +Here is a minimum of code required for theory Know_Store,
    10.8 +further code see structure ThmC.
    10.9  *)
   10.10  signature THEOREM_ISAC_DEF =
   10.11  sig

    11.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml	Tue Apr 28 19:39:06 2020 +0200
    11.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Apr 29 09:03:01 2020 +0200
    11.3 @@ -2,7 +2,10 @@
    11.4     Author: Walther Neuper
    11.5     (c) due to copyright terms
    11.6  
    11.7 -Legacy for HTML representation of theory data in Isac's Java front end.
    11.8 +Here is a minimum of code required for Know_Store.thy.
    11.9 +For main code see structure Thy_Write and structure Thy_Present.
   11.10 +
   11.11 +The latter is legacy for HTML representation of theory data in Isac's Java front end.
   11.12  *)
   11.13  signature THEORY_DATA_STORE_WRITE =
   11.14  sig

    12.1 --- a/src/Tools/isac/Build_Isac.thy	Tue Apr 28 19:39:06 2020 +0200
    12.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Apr 29 09:03:01 2020 +0200
    12.3 @@ -19,7 +19,7 @@
    12.4        ML_file unparseC.sml                                                                                                  
    12.5        ML_file "rule-def.sml"
    12.6        ML_file thmC.sml
    12.7 -      ML_file "exec-def.sml"
    12.8 +      ML_file "eval-def.sml"
    12.9        ML_file "rewrite-order.sml"
   12.10        ML_file rule.sml
   12.11        ML_file "error-fill-def.sml"

    13.1 --- a/src/Tools/isac/Interpret/thy-read.sml	Tue Apr 28 19:39:06 2020 +0200
    13.2 +++ b/src/Tools/isac/Interpret/thy-read.sml	Wed Apr 29 09:03:01 2020 +0200
    13.3 @@ -9,7 +9,7 @@
    13.4  sig
    13.5    val thy_containing_thm : string -> string * string
    13.6    val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
    13.7 -  val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
    13.8 +  val thy_containing_cal : ThyC.id -> Eval_Def.prog_calcID -> string * string
    13.9  
   13.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   13.11    (*  NONE *)

    14.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 28 19:39:06 2020 +0200
    14.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 29 09:03:01 2020 +0200
    14.3 @@ -4,7 +4,7 @@
    14.4  
    14.5  signature REWRITE =
    14.6  sig
    14.7 -  val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
    14.8 +  val calculate_: theory -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
    14.9    val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
   14.10    val eval_prog_expr: theory -> Rule_Set.T -> term -> term
   14.11    val eval_true_: theory -> Rule_Set.T -> term -> bool

    15.1 --- a/src/Tools/isac/MathEngine/step.sml	Tue Apr 28 19:39:06 2020 +0200
    15.2 +++ b/src/Tools/isac/MathEngine/step.sml	Wed Apr 29 09:03:01 2020 +0200
    15.3 @@ -17,9 +17,9 @@
    15.4    val do_next: Pos.pos' -> Chead.calcstate -> string * Chead.calcstate'
    15.5    val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'
    15.6  (*val by_term   = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate'
    15.7 -TODO --------------------------------------"----------> ??????   Calc.T 
    15.8 -                = Step_Specify.by_tactic ? depending on PIDE, see TODO.thy*)
    15.9 -
   15.10 +  TODO ------------------------------------"----------> ??????   Calc.T 
   15.11 +                = Step_Specify.by_tactic ? depending on PIDE, see TODO.thy
   15.12 +*)
   15.13  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   15.14    (*NONE*)                                                     
   15.15  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    16.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Tue Apr 28 19:39:06 2020 +0200
    16.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Apr 29 09:03:01 2020 +0200
    16.3 @@ -32,7 +32,7 @@
    16.4      val subpbl: string -> string list -> term
    16.5      val stacpbls: term -> term list
    16.6      val op_of_calc: term -> string
    16.7 -    val get_calcs: theory -> term -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
    16.8 +    val get_calcs: theory -> term -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
    16.9      val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
   16.10      val gen: theory -> term -> Rule_Set.T -> term
   16.11  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    17.1 --- a/src/Tools/isac/ProgLang/evaluate.sml	Tue Apr 28 19:39:06 2020 +0200
    17.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml	Wed Apr 29 09:03:01 2020 +0200
    17.3 @@ -1,8 +1,11 @@
    17.4  (* calculate values for function constants
    17.5     (c) Walther Neuper 000106
    17.6 +
    17.7 +Some formula transformations cannot be done by rewriting;
    17.8 +these are done by structure Eval, which works tightly intertwined with structure Rewrite.
    17.9  *)
   17.10  
   17.11 -signature NUMERAL_CALCULATION =
   17.12 +signature EVALUATE =
   17.13  sig
   17.14    type float
   17.15    val calc_equ: string -> int * int -> bool
   17.16 @@ -11,8 +14,8 @@
   17.17    val squfact: int -> int
   17.18    val gcd: int -> int -> int
   17.19    val sqrt: int -> int
   17.20 -  val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
   17.21 -  val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
   17.22 +  val adhoc_thm: theory -> string * Eval_Def.eval_fn -> term -> (string * thm) option
   17.23 +  val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option
   17.24    val norm: term -> term
   17.25    val popt2str: ('a * term) option -> string
   17.26    val numeral: term -> ((int * int) * (int * int)) option
   17.27 @@ -25,7 +28,7 @@
   17.28  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   17.29    (* NONE *)
   17.30  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   17.31 -  val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
   17.32 +  val get_pair: theory -> string -> Eval_Def.eval_fn -> term -> (string * term) option
   17.33    val mk_rule: term list * term * term -> term
   17.34    val divisors: int -> int list
   17.35    val doubles: int list -> int list
   17.36 @@ -33,7 +36,7 @@
   17.37  end
   17.38  
   17.39  (**)
   17.40 -structure Eval(**): NUMERAL_CALCULATION(**) =
   17.41 +structure Eval(**): EVALUATE(**) =
   17.42  struct
   17.43  (**)
   17.44  
   17.45 @@ -109,7 +112,7 @@
   17.46  fun trace_calc4 str t1 t2 =
   17.47    if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
   17.48  
   17.49 -fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) =                (* unary fns *)
   17.50 +fun get_pair thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) =                (* unary fns *)
   17.51      if op_ = op0 then 
   17.52        let val popt = ef op_ t thy 
   17.53        in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end

    18.1 --- a/src/Tools/isac/Specify/appl.sml	Tue Apr 28 19:39:06 2020 +0200
    18.2 +++ b/src/Tools/isac/Specify/appl.sml	Wed Apr 29 09:03:01 2020 +0200
    18.3 @@ -62,7 +62,7 @@
    18.4  	    in
    18.5  	      case opt of
    18.6  	        SOME isa_fn => ("OK", thy', isa_fn)
    18.7 -	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn))
    18.8 +	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
    18.9  	    end
   18.10      else 
   18.11  		  let
   18.12 @@ -71,7 +71,7 @@
   18.13  		  in
   18.14  		    case assoc (scr_isa_fns, scrop) of
   18.15  		      SOME isa_fn => ("OK",thy',isa_fn)
   18.16 -		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn))
   18.17 +		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
   18.18  		  end
   18.19    end;
   18.20  

    19.1 --- a/src/Tools/isac/TODO.thy	Tue Apr 28 19:39:06 2020 +0200
    19.2 +++ b/src/Tools/isac/TODO.thy	Wed Apr 29 09:03:01 2020 +0200
    19.3 @@ -31,11 +31,7 @@
    19.4    \item xxx
    19.5    \item replace src/ Erls Rule_Set.Empty
    19.6    \item xxx
    19.7 -  \item rename exec-def.sml -> eval_def.sml
    19.8 -               evaluate.sml _> evaluate.sml (struct Eval -> Evaluate?!?)
    19.9    \item xxx
   19.10 -  \item rename Know_Store -> Know_Store KNOWLEDGE_STORE + file.sml
   19.11 -               Build_Thydata -> Build_Knowledge
   19.12    \item xxx
   19.13    \item rename ptyps.sml -> specify-etc.sml
   19.14          rename Specify -> Specify_Etc
   19.15 @@ -60,7 +56,7 @@
   19.16    \item xxx
   19.17    \item xxx
   19.18    \item xxx
   19.19 -  \item use "Exec_Def" for renaming identifiers
   19.20 +  \item use "Eval_Def" for renaming identifiers
   19.21    \item xxx
   19.22    \item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
   19.23    \item xxx

    20.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Tue Apr 28 19:39:06 2020 +0200
    20.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Wed Apr 29 09:03:01 2020 +0200
    20.3 @@ -14,6 +14,6 @@
    20.4      else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
    20.5  \<close>
    20.6  
    20.7 -setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Exec_Def.e_evalfn))]\<close>
    20.8 +setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Eval_Def.e_evalfn))]\<close>
    20.9  
   20.10  end

    21.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Tue Apr 28 19:39:06 2020 +0200
    21.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Wed Apr 29 09:03:01 2020 +0200
    21.3 @@ -9,8 +9,8 @@
    21.4  sig
    21.5    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    21.6    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    21.7 -  val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
    21.8 -  val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
    21.9 +  val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
   21.10 +  val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
   21.11    (*etc*)
   21.12  end;                               
   21.13  
   21.14 @@ -30,7 +30,7 @@
   21.15  
   21.16    val calc_eq = rls_eq
   21.17    structure Data = Theory_Data (
   21.18 -    type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
   21.19 +    type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
   21.20      val empty = [];
   21.21      val extend = I;
   21.22      val merge = merge calc_eq;

    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/test/Tools/isac/BaseDefinitions/eval-def.sml	Wed Apr 29 09:03:01 2020 +0200
    22.3 @@ -0,0 +1,17 @@
    22.4 +(* Title:  "BaseDefinitions/eval-def.sml"
    22.5 +   Author: Walther Neuper
    22.6 +   (c) due to copyright terms
    22.7 +*)
    22.8 +
    22.9 +"-----------------------------------------------------------------------------------------------";
   22.10 +"table of contents -----------------------------------------------------------------------------";
   22.11 +"-----------------------------------------------------------------------------------------------";
   22.12 +"----------- TODO ------------------------------------------------------------------------------";
   22.13 +"-----------------------------------------------------------------------------------------------";
   22.14 +"-----------------------------------------------------------------------------------------------";
   22.15 +"-----------------------------------------------------------------------------------------------";
   22.16 +
   22.17 +
   22.18 +"----------- TODO ------------------------------------------------------------------------------";
   22.19 +"----------- TODO ------------------------------------------------------------------------------";
   22.20 +"----------- TODO ------------------------------------------------------------------------------";

    23.1 --- a/test/Tools/isac/BaseDefinitions/exec-def.sml	Tue Apr 28 19:39:06 2020 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,17 +0,0 @@
    23.4 -(* Title:  "BaseDefinitions/exec-def.sml"
    23.5 -   Author: Walther Neuper
    23.6 -   (c) due to copyright terms
    23.7 -*)
    23.8 -
    23.9 -"-----------------------------------------------------------------------------------------------";
   23.10 -"table of contents -----------------------------------------------------------------------------";
   23.11 -"-----------------------------------------------------------------------------------------------";
   23.12 -"----------- TODO ------------------------------------------------------------------------------";
   23.13 -"-----------------------------------------------------------------------------------------------";
   23.14 -"-----------------------------------------------------------------------------------------------";
   23.15 -"-----------------------------------------------------------------------------------------------";
   23.16 -
   23.17 -
   23.18 -"----------- TODO ------------------------------------------------------------------------------";
   23.19 -"----------- TODO ------------------------------------------------------------------------------";
   23.20 -"----------- TODO ------------------------------------------------------------------------------";

    24.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Apr 28 19:39:06 2020 +0200
    24.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Apr 29 09:03:01 2020 +0200
    24.3 @@ -45,10 +45,10 @@
    24.4  (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
    24.5  val t = str2term "((1+2)*4/3)^^^2";
    24.6  val thy = @{theory};
    24.7 -val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Exec_Def.eval_fn;
    24.8 -val plus =   ("Groups.plus_class.plus",eval_binop "#add_") : string * Exec_Def.eval_fn;
    24.9 -val divide = ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") : string * Exec_Def.eval_fn;
   24.10 -val pow =    ("Prog_Expr.pow"  ,eval_binop "#power_") : string * Exec_Def.eval_fn;
   24.11 +val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
   24.12 +val plus =   ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
   24.13 +val divide = ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
   24.14 +val pow =    ("Prog_Expr.pow"  ,eval_binop "#power_") : string * Eval_Def.eval_fn;
   24.15  
   24.16  "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
   24.17  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;

    25.1 --- a/test/Tools/isac/Test_Isac.thy	Tue Apr 28 19:39:06 2020 +0200
    25.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Apr 29 09:03:01 2020 +0200
    25.3 @@ -100,7 +100,6 @@
    25.4    open Error_Pattern;
    25.5    open Error_Pattern_Def;
    25.6    open In_Chead;
    25.7 -  open Rtools;
    25.8    open Chead;                  pt_extract;
    25.9    open Generate;               (* NONE *)
   25.10    open Ctree;                  append_problem;
   25.11 @@ -126,10 +125,9 @@
   25.12    open Rewrite;
   25.13    open Eval;                   get_pair;
   25.14    open TermC;                  atomt;
   25.15 -  open Celem;
   25.16    open Rule;
   25.17    open Rule_Set;               Sequence;
   25.18 -  open Exec_Def
   25.19 +  open Eval_Def
   25.20    open ThyC
   25.21    open ThmC_Def
   25.22    open ThmC
   25.23 @@ -180,7 +178,7 @@
   25.24    ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
   25.25    ML_file "BaseDefinitions/libraryC.sml"
   25.26    ML_file "BaseDefinitions/rule-def.sml"
   25.27 -  ML_file "BaseDefinitions/exec-def.sml"
   25.28 +  ML_file "BaseDefinitions/eval-def.sml"
   25.29    ML_file "BaseDefinitions/rewrite-order.sml"
   25.30    ML_file "BaseDefinitions/theoryC.sml"
   25.31    ML_file "BaseDefinitions/rule.sml"
   25.32 @@ -250,7 +248,6 @@
   25.33  
   25.34    ML_file "Interpret/istate.sml"
   25.35    ML_file "Interpret/sub-problem.sml"
   25.36 -  ML_file "Interpret/rewtools.sml"
   25.37    ML_file "Interpret/error-pattern.sml"
   25.38    ML_file "Interpret/li-tool.sml"
   25.39    ML_file "Interpret/lucas-interpreter.sml"
   25.40 @@ -263,6 +260,7 @@
   25.41    ML_file "MathEngine/messages.sml"
   25.42    ML_file "MathEngine/states.sml"
   25.43  
   25.44 +  ML_file "BridgeLibisabelle/thy-present.sml"
   25.45    ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
   25.46    ML_file "BridgeLibisabelle/datatypes.sml"        (*TODO/part.*)
   25.47    ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)

    26.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue Apr 28 19:39:06 2020 +0200
    26.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed Apr 29 09:03:01 2020 +0200
    26.3 @@ -125,10 +125,9 @@
    26.4    open Rewrite;
    26.5    open Eval;                   get_pair;
    26.6    open TermC;                  atomt;
    26.7 -  open Celem;
    26.8    open Rule;
    26.9    open Rule_Set;               Sequence;
   26.10 -  open Exec_Def
   26.11 +  open Eval_Def
   26.12    open ThyC
   26.13    open ThmC_Def
   26.14    open ThmC
   26.15 @@ -179,7 +178,7 @@
   26.16    ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
   26.17    ML_file "BaseDefinitions/libraryC.sml"
   26.18    ML_file "BaseDefinitions/rule-def.sml"
   26.19 -  ML_file "BaseDefinitions/exec-def.sml"
   26.20 +  ML_file "BaseDefinitions/eval-def.sml"
   26.21    ML_file "BaseDefinitions/rewrite-order.sml"
   26.22    ML_file "BaseDefinitions/theoryC.sml"
   26.23    ML_file "BaseDefinitions/rule.sml"

    27.1 --- a/test/Tools/isac/Test_Some.thy	Tue Apr 28 19:39:06 2020 +0200
    27.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Apr 29 09:03:01 2020 +0200
    27.3 @@ -48,7 +48,7 @@
    27.4    open Celem;
    27.5    open Rule;
    27.6    open Rule_Set
    27.7 -  open Exec_Def
    27.8 +  open Eval_Def
    27.9    open ThyC
   27.10    open ThmC_Def
   27.11    open ThmC