1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Jun 21 16:18:27 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Jun 21 20:06:12 2021 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  theory Know_Store
     1.6    imports Complex_Main
     1.7 -  keywords "rule_set_knowledge" :: thy_decl
     1.8 +  keywords "rule_set_knowledge" "calculation" :: thy_decl
     1.9  begin
    1.10  
    1.11  setup \<open>
    1.12 @@ -193,6 +193,25 @@
    1.13        thy |> Context.theory_map
    1.14          (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
    1.15  
    1.16 +val calc_name =
    1.17 +  Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
    1.18 +  Scan.ahead Parse.name -- Parse.const;
    1.19 +
    1.20 +val _ =
    1.21 +  Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
    1.22 +    "prepare ISAC calculation and register it to Knowledge Store"
    1.23 +    (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
    1.24 +      Toplevel.theory (fn thy =>
    1.25 +        let
    1.26 +          val ctxt = Proof_Context.init_global thy;
    1.27 +          val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
    1.28 +          val eval_ml =
    1.29 +            ML_Context.expression (Input.pos_of source)
    1.30 +              (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
    1.31 +            |> Context.theory_map;
    1.32 +          val eval = Eval_Def.the_data (eval_ml thy);
    1.33 +        in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
    1.34 +
    1.35  in end;
    1.36  \<close>
    1.37  

     2.1 --- a/src/Tools/isac/BaseDefinitions/eval-def.sml	Mon Jun 21 16:18:27 2021 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/eval-def.sml	Mon Jun 21 20:06:12 2021 +0200
     2.3 @@ -12,8 +12,10 @@
     2.4    type cal
     2.5    type calc_elem
     2.6    val calc_eq: calc_elem * calc_elem -> bool
     2.7 -  type eval_fn
     2.8 +  type eval_fn = Rule_Def.eval_fn
     2.9    val e_evalfn: Rule_Def.eval_fn
    2.10 +  val set_data: eval_fn -> theory -> theory
    2.11 +  val the_data: theory -> eval_fn
    2.12  end
    2.13  
    2.14  (**)
    2.15 @@ -42,4 +44,19 @@
    2.16      Eval: prog_calcID * (calID * eval_fn)) -> rule*)
    2.17  type eval_fn = Rule_Def.eval_fn
    2.18  fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
    2.19 +
    2.20 +
    2.21 +(* theory data for Isar command 'calculation' *)
    2.22 +
    2.23 +structure Data = Theory_Data
    2.24 +(
    2.25 +  type T = eval_fn option;
    2.26 +  val empty = NONE;
    2.27 +  val extend = I;
    2.28 +  fun merge _ = NONE;
    2.29 +);
    2.30 +
    2.31 +val set_data = Data.put o SOME;
    2.32 +val the_data = the o Data.get;
    2.33 +
    2.34  end

     3.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 16:18:27 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 20:06:12 2021 +0200
     3.3 @@ -24,22 +24,21 @@
     3.4  
     3.5  subsection \<open>setup for ML-functions\<close>
     3.6  text \<open>required by "eval_binop" below\<close>
     3.7 -setup \<open>KEStore_Elems.add_calcs
     3.8 -  [ ("occurs_in", (\<^const_name>\<open>occurs_in\<close>, Prog_Expr.eval_occurs_in "#occurs_in_")),
     3.9 -    ("some_occur_in", (\<^const_name>\<open>some_occur_in\<close>, Prog_Expr.eval_some_occur_in "#some_occur_in_")),
    3.10 -    ("is_atom", (\<^const_name>\<open>is_atom\<close>, Prog_Expr.eval_is_atom "#is_atom_")),
    3.11 -    ("is_even", (\<^const_name>\<open>is_even\<close>, Prog_Expr.eval_is_even "#is_even_")),
    3.12 -    ("is_const", (\<^const_name>\<open>is_const\<close>, Prog_Expr.eval_const "#is_const_")),
    3.13 -    ("le", (\<^const_name>\<open>less\<close>, Prog_Expr.eval_equ "#less_")),
    3.14 -    ("leq", (\<^const_name>\<open>less_eq\<close>, Prog_Expr.eval_equ "#less_equal_")),
    3.15 -    ("ident", (\<^const_name>\<open>ident\<close>, Prog_Expr.eval_ident "#ident_")),
    3.16 -    ("equal", (\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")),
    3.17 -    ("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    3.18 -    ("MINUS", (\<^const_name>\<open>minus\<close>, (**)eval_binop "#sub_")),
    3.19 -    ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    3.20 -    ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    3.21 -    ("POWER",(\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")),
    3.22 -    ("boollist2sum", (\<^const_name>\<open>boollist2sum\<close>, Prog_Expr.eval_boollist2sum ""))]\<close>
    3.23 +calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
    3.24 +calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
    3.25 +calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
    3.26 +calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
    3.27 +calculation is_const = \<open>Prog_Expr.eval_const "#is_const_"\<close>
    3.28 +calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close>
    3.29 +calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
    3.30 +calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
    3.31 +calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
    3.32 +calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
    3.33 +calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
    3.34 +calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
    3.35 +calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
    3.36 +calculation POWER (powr) = \<open>(**)eval_binop "#power_"\<close>
    3.37 +calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
    3.38  
    3.39  subsection \<open>rewrite-order for rule-sets\<close>
    3.40  ML \<open>

     4.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Jun 21 16:18:27 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Jun 21 20:06:12 2021 +0200
     4.3 @@ -99,8 +99,9 @@
     4.4  	  HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
     4.5    | eval_primed _ _ _ _ = NONE;
     4.6  \<close>
     4.7 -setup \<open>KEStore_Elems.add_calcs
     4.8 -  [("primed", (\<^const_name>\<open>primed\<close>, eval_primed "#primed"))]\<close>
     4.9 +
    4.10 +calculation primed = \<open>eval_primed "#primed"\<close>
    4.11 +
    4.12  ML \<open>
    4.13  (** rulesets **)
    4.14  

     5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 16:18:27 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 20:06:12 2021 +0200
     5.3 @@ -76,8 +76,8 @@
     5.4  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
     5.5    | eval_occur_exactly_in _ _ _ _ = NONE;
     5.6  \<close>
     5.7 -setup \<open>KEStore_Elems.add_calcs
     5.8 -  [("occur_exactly_in", (\<^const_name>\<open>occur_exactly_in\<close>, eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
     5.9 +calculation occur_exactly_in = \<open>eval_occur_exactly_in "#eval_occur_exactly_in_"\<close>
    5.10 +
    5.11  ML \<open>
    5.12  (** rewrite order 'ord_simplify_System' **)
    5.13  

     6.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 16:18:27 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 20:06:12 2021 +0200
     6.3 @@ -103,8 +103,9 @@
     6.4    | eval_is_f_x _ _ _ _ = NONE;
     6.5  \<close>
     6.6  setup \<open>KEStore_Elems.add_calcs
     6.7 -  [("add_new_c", ("Integrate.add_new_c" (* FIXME proper const!? *), eval_add_new_c "add_new_c_")),
     6.8 -    ("is_f_x", (\<^const_name>\<open>is_f_x\<close>, eval_is_f_x "is_f_idextifier_"))]\<close>
     6.9 +  [("add_new_c", ("Integrate.add_new_c" (* FIXME proper const!? *), eval_add_new_c "add_new_c_"))]\<close>
    6.10 +calculation is_f_x = \<open>eval_is_f_x "is_f_idextifier_"\<close>
    6.11 +
    6.12  ML \<open>
    6.13  (** rulesets **)
    6.14  

     7.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Mon Jun 21 16:18:27 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Jun 21 20:06:12 2021 +0200
     7.3 @@ -634,14 +634,13 @@
     7.4  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
     7.5    | eval_is_multUnordered _ _ _ _ = NONE; 
     7.6  \<close>
     7.7 -setup \<open>KEStore_Elems.add_calcs
     7.8 -  [("is_polyrat_in", (\<^const_name>\<open>is_polyrat_in\<close>, eval_is_polyrat_in "#eval_is_polyrat_in")),
     7.9 -    ("is_expanded_in", (\<^const_name>\<open>is_expanded_in\<close>, eval_is_expanded_in "")),
    7.10 -    ("is_poly_in", (\<^const_name>\<open>is_poly_in\<close>, eval_is_poly_in "")),
    7.11 -    ("has_degree_in", (\<^const_name>\<open>has_degree_in\<close>, eval_has_degree_in "")),
    7.12 -    ("is_polyexp", (\<^const_name>\<open>is_polyexp\<close>, eval_is_polyexp "")),
    7.13 -    ("is_multUnordered", (\<^const_name>\<open>is_multUnordered\<close>, eval_is_multUnordered"")),
    7.14 -    ("is_addUnordered", (\<^const_name>\<open>is_addUnordered\<close>, eval_is_addUnordered ""))]\<close>
    7.15 +calculation is_polyrat_in = \<open>eval_is_polyrat_in "#eval_is_polyrat_in"\<close>
    7.16 +calculation is_expanded_in = \<open>eval_is_expanded_in ""\<close>
    7.17 +calculation is_poly_in = \<open>eval_is_poly_in ""\<close>
    7.18 +calculation has_degree_in = \<open>eval_has_degree_in ""\<close>
    7.19 +calculation is_polyexp = \<open>eval_is_polyexp ""\<close>
    7.20 +calculation is_multUnordered = \<open>eval_is_multUnordered ""\<close>
    7.21 +calculation is_addUnordered = \<open>eval_is_addUnordered ""\<close>
    7.22  
    7.23  subsection \<open>rule-sets\<close>
    7.24  subsubsection \<open>without specific order\<close>

     8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Jun 21 16:18:27 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Jun 21 20:06:12 2021 +0200
     8.3 @@ -73,8 +73,7 @@
     8.4      else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
     8.5    | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
     8.6  \<close>
     8.7 -setup \<open>KEStore_Elems.add_calcs
     8.8 -  [("is_ratequation_in", (\<^const_name>\<open>is_ratequation_in\<close>, eval_is_ratequation_in ""))]\<close>
     8.9 +calculation is_ratequation_in = \<open>eval_is_ratequation_in ""\<close>
    8.10  
    8.11  subsection \<open>rule-sets\<close>
    8.12  ML \<open>

     9.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jun 21 16:18:27 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jun 21 20:06:12 2021 +0200
     9.3 @@ -458,8 +458,7 @@
     9.4  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
     9.5    | eval_is_expanded _ _ _ _ = NONE;
     9.6  \<close>
     9.7 -setup \<open>KEStore_Elems.add_calcs
     9.8 -  [("is_expanded", (\<^const_name>\<open>is_expanded\<close>, eval_is_expanded ""))]\<close>
     9.9 +calculation is_expanded = \<open>eval_is_expanded ""\<close>
    9.10  ML \<open>
    9.11  val rational_erls = 
    9.12    Rule_Set.merge "rational_erls" calculate_Rational 

    10.1 --- a/src/Tools/isac/Knowledge/Root.thy	Mon Jun 21 16:18:27 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Mon Jun 21 20:06:12 2021 +0200
    10.3 @@ -79,9 +79,8 @@
    10.4  > val SOME ni = int_of_str n1;
    10.5  *)
    10.6  \<close>
    10.7 -setup \<open>KEStore_Elems.add_calcs
    10.8 -  [("SQRT", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))
    10.9 -    (*different types for 'sqrt 4' --- 'Calculate SQRT'*)]\<close>
   10.10 +calculation SQRT (sqrt) = \<open>eval_sqrt "#sqrt_"\<close>
   10.11 +    (*different types for 'sqrt 4' --- 'Calculate SQRT'*)
   10.12  ML \<open>
   10.13  local (* Vers. 7.10.99.A *)
   10.14  

    11.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Jun 21 16:18:27 2021 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Jun 21 20:06:12 2021 +0200
    11.3 @@ -169,10 +169,9 @@
    11.4      else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    11.5    | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
    11.6  \<close>
    11.7 -setup \<open>KEStore_Elems.add_calcs
    11.8 -  [("is_rootTerm_in", (\<^const_name>\<open>is_rootTerm_in\<close>, eval_is_rootTerm_in"")),
    11.9 -    ("is_sqrtTerm_in", (\<^const_name>\<open>is_sqrtTerm_in\<close>, eval_is_sqrtTerm_in"")),
   11.10 -    ("is_normSqrtTerm_in", (\<^const_name>\<open>is_normSqrtTerm_in\<close>, eval_is_normSqrtTerm_in""))]\<close>
   11.11 +calculation is_rootTerm_in = \<open>eval_is_rootTerm_in ""\<close>
   11.12 +calculation is_sqrtTerm_in = \<open>eval_is_sqrtTerm_in ""\<close>
   11.13 +calculation is_normSqrtTerm_in = \<open>eval_is_normSqrtTerm_in ""\<close>
   11.14  
   11.15  subsection \<open>rule-sets\<close>
   11.16  ML \<open>

    12.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jun 21 16:18:27 2021 +0200
    12.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jun 21 20:06:12 2021 +0200
    12.3 @@ -61,8 +61,7 @@
    12.4      else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    12.5    | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
    12.6  \<close>
    12.7 -setup \<open>KEStore_Elems.add_calcs
    12.8 -  [("is_rootRatAddTerm_in", (\<^const_name>\<open>is_rootRatAddTerm_in\<close>, eval_is_rootRatAddTerm_in""))]\<close>
    12.9 +calculation is_rootRatAddTerm_in = \<open>eval_is_rootRatAddTerm_in ""\<close>
   12.10  
   12.11  subsection \<open>rule-sets\<close>
   12.12  ML \<open>

    13.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Jun 21 16:18:27 2021 +0200
    13.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon Jun 21 20:06:12 2021 +0200
    13.3 @@ -272,12 +272,10 @@
    13.4  	    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    13.5  	| eval_precond_rootpbl _ _ _ _ = NONE;
    13.6  \<close>
    13.7 -setup \<open>KEStore_Elems.add_calcs
    13.8 -  [("contains_root", (\<^const_name>\<open>contains_root\<close>, eval_contains_root"#contains_root_")),
    13.9 -    ("Test.precond_rootmet", (\<^const_name>\<open>Test.precond_rootmet\<close>, eval_precond_rootmet"#Test.precond_rootmet_")),
   13.10 -    ("Test.precond_rootpbl", (\<^const_name>\<open>Test.precond_rootpbl\<close>,
   13.11 -        eval_precond_rootpbl"#Test.precond_rootpbl_"))]
   13.12 -\<close>
   13.13 +calculation contains_root = \<open>eval_contains_root "#contains_root_"\<close>
   13.14 +calculation Test.precond_rootmet = \<open>eval_precond_rootmet "#Test.precond_rootmet_"\<close>
   13.15 +calculation Test.precond_rootpbl = \<open>eval_precond_rootpbl "#Test.precond_rootpbl_"\<close>
   13.16 +
   13.17  ML \<open>
   13.18  (*8.4.03  aus Poly.ML--------------------------------vvv---
   13.19    make_polynomial  ---> make_poly

    14.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 16:18:27 2021 +0200
    14.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 20:06:12 2021 +0200
    14.3 @@ -535,12 +535,12 @@
    14.4  subsection \<open>setup for rule-sets and ML-functions\<close>
    14.5  
    14.6  rule_set_knowledge prog_expr = prog_expr
    14.7 -setup \<open>KEStore_Elems.add_calcs
    14.8 -  [("matches", (\<^const_name>\<open>matches\<close>, Prog_Expr.eval_matches "#matches_")),
    14.9 -    ("matchsub", (\<^const_name>\<open>matchsub\<close>, Prog_Expr.eval_matchsub "#matchsub_")),
   14.10 -    ("Vars", (\<^const_name>\<open>Vars\<close>, Prog_Expr.eval_var "#Vars_")),
   14.11 -    ("lhs", (\<^const_name>\<open>lhs\<close>, Prog_Expr.eval_lhs "")),
   14.12 -    ("rhs", (\<^const_name>\<open>rhs\<close>, Prog_Expr.eval_rhs ""))]\<close>
   14.13 +
   14.14 +calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
   14.15 +calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
   14.16 +calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
   14.17 +calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
   14.18 +calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
   14.19  (*\\------------------------- from Tools .thy-------------------------------------------------//*)
   14.20  ML \<open>
   14.21  \<close> ML \<open>