1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Feb 08 17:00:37 2020 +0100
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Sun Feb 09 12:48:18 2020 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4    val scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val
     1.5    val go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val
     1.6    val scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val
     1.7 -  val check_tac: Calc.T * Proof.context -> Istate.pstate -> term option * term -> expr_val;
     1.8 +  val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
     1.9  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.10    val check_Let_up: Istate.pstate -> term -> term * term
    1.11    val compare_step: Generate.taci list * Ctree.pos' list * (Calc.T) -> term -> string * Chead.calcstate'
    1.12 @@ -56,7 +56,7 @@
    1.13    val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
    1.14    val scan_to_tactic1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.T -> expr_val1
    1.15  
    1.16 -  val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
    1.17 +  val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
    1.18  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.19  end
    1.20  
    1.21 @@ -104,7 +104,7 @@
    1.22      term;           (* value of Prog_Expr, for updating environment               *)
    1.23  
    1.24  (* check if a prog_tac found in a program is applicable_in *)
    1.25 -fun check_tac ((pt, p), ctxt) ist (form_arg, prog_tac) =
    1.26 +fun check_tac ((pt, p), ctxt) ist (prog_tac, form_arg) =
    1.27    let
    1.28      val (m, m') = LItool.stac2tac_(*..see TODO.thy*)pt (Proof_Context.theory_of ctxt) prog_tac
    1.29    in
    1.30 @@ -157,13 +157,11 @@
    1.31      | (*Accept_Tac*) goback => goback)
    1.32  
    1.33    | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
    1.34 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
    1.35 -      eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
    1.36 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
    1.37      then scan_dn cc (ist |> path_down_form ([L, R], a)) e
    1.38      else Term_Val act_arg
    1.39    | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
    1.40 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
    1.41 -      eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
    1.42 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
    1.43      then scan_dn cc (ist |> path_down [R]) e
    1.44      else Term_Val act_arg
    1.45  
    1.46 @@ -177,8 +175,7 @@
    1.47      | _ => scan_dn cc (ist |> path_down [R]) e2)
    1.48  
    1.49    |  scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
    1.50 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
    1.51 -      eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
    1.52 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
    1.53      then scan_dn cc (ist |> path_down [L, R]) e1
    1.54      else scan_dn cc (ist |> path_down [R]) e2
    1.55  
    1.56 @@ -189,7 +186,7 @@
    1.57        case LItool.check_leaf "next  " ctxt eval (get_subst ist) t of
    1.58    	    (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
    1.59        | (Program.Tac prog_tac, form_arg) =>
    1.60 -          check_tac cc ist (form_arg, prog_tac)
    1.61 +          check_tac cc ist (prog_tac, form_arg)
    1.62  
    1.63  fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = 
    1.64      if path = [R] (*root of the program body*)
    1.65 @@ -239,8 +236,7 @@
    1.66  
    1.67    | scan_up (pcc as (_, cc as (_, ctxt)))  (ist as {eval, ...})
    1.68        (Const ("Tactical.While"(*1*), _) $ c $ e $ _) = 
    1.69 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
    1.70 -      eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
    1.71 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
    1.72      then
    1.73        case scan_dn cc (ist |> path_down [L, R]) e of
    1.74    	     Accept_Tac ict => Accept_Tac ict
    1.75 @@ -250,8 +246,7 @@
    1.76        go_scan_up pcc (ist (*|> set_found*))
    1.77    | scan_up  (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
    1.78        (Const ("Tactical.While"(*2*), _) $ c $ e) = 
    1.79 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
    1.80 -      eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
    1.81 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
    1.82      then
    1.83        case scan_dn cc (ist |> path_down [R]) e of
    1.84    	    Accept_Tac ict => Accept_Tac ict
    1.85 @@ -318,7 +313,7 @@
    1.86  
    1.87  (** check a Prog_Tac: is it associated to Tactic ? **)
    1.88  
    1.89 -fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (form_arg, prog_tac) =
    1.90 +fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (prog_tac, form_arg) =
    1.91    case LItool.associate pt ctxt (tac, prog_tac) of
    1.92       (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
    1.93        LItool.Ass      (m, v', ctxt)
    1.94 @@ -369,14 +364,12 @@
    1.95  
    1.96    | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
    1.97        (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
    1.98 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval
    1.99 -      (subst_atomic (ist |> get_act_env |> Env.update' a) c)
   1.100 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
   1.101      then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
   1.102      else Term_Val1 act_arg
   1.103    | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
   1.104        (Const ("Tactical.While"(*2*),_) $ c $ e) =
   1.105 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
   1.106 -      eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
   1.107 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
   1.108      then scan_dn1 cct (ist |> path_down [R]) e
   1.109      else Term_Val1 act_arg
   1.110  
   1.111 @@ -398,8 +391,7 @@
   1.112       | goback => goback)
   1.113  
   1.114    | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
   1.115 -    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt)
   1.116 -      eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
   1.117 +    if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
   1.118      then scan_dn1 cct (ist |> path_down [L, R]) e1
   1.119      else scan_dn1 cct (ist |> path_down [R]) e2
   1.120  
   1.121 @@ -411,7 +403,7 @@
   1.122    	      Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
   1.123    		      (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
   1.124        | (Program.Tac prog_tac, form_arg) =>
   1.125 -          check_tac1 cct ist (form_arg, prog_tac)
   1.126 +          check_tac1 cct ist (prog_tac, form_arg)
   1.127  
   1.128  fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
   1.129      if 1 < length path

     2.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Sat Feb 08 17:00:37 2020 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Sun Feb 09 12:48:18 2020 +0100
     2.3 @@ -145,7 +145,7 @@
     2.4  subsection \<open>CAS-commands\<close>
     2.5  ML \<open>
     2.6  (* for starting a new example, e.g. "Sort {|| 1, 3, 2 ||}" after <NEW> on WorkSheet;
     2.7 -   associate above input with dataformat of pbt (without "#Given", etc):
     2.8 +   combine this input with dataformat of pbt (without "#Given", etc):
     2.9  *)
    2.10  fun argl2dtss [t] =
    2.11      [(@{term "unsorted"}, [t]),
    2.12 @@ -153,7 +153,7 @@
    2.13       ]
    2.14    | argl2dtss _ = error "InsSort.thy: wrong argument for argl2dtss"
    2.15  \<close>
    2.16 -(* associate input with other data required for formal specification *)
    2.17 +(* combine input with other data required for formal specification *)
    2.18  setup \<open>KEStore_Elems.add_cas
    2.19    [ ( @{term "Sort"},  
    2.20        (("InsSort", ["insertion","SORT","Programming"], ["no_met"]), argl2dtss)

     3.1 --- a/src/Tools/isac/TODO.thy	Sat Feb 08 17:00:37 2020 +0100
     3.2 +++ b/src/Tools/isac/TODO.thy	Sun Feb 09 12:48:18 2020 +0100
     3.3 @@ -31,27 +31,19 @@
     3.4    \item xxx          
     3.5    \item xxx
     3.6    \item xxx          
     3.7 -  \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
     3.8    \item xxx
     3.9 -  \item switch args
    3.10 -    check_tac cc ist (form_arg, prog_tac) to
    3.11 -    check_tac cc ist (prog_tac, form_arg)
    3.12 -  + in check_tac1
    3.13    \item xxx
    3.14 -  \item rm test/..--- check Scripts ---
    3.15    \item xxx
    3.16    \item reformat + rename "fun eval_leaf"+"fun get_stac"
    3.17          (*1*)(*2*)
    3.18          ?consistency with subst term?
    3.19    \item Tactic.Rewrite*': drop "bool"
    3.20    \item xxx
    3.21 -  \item exception PROG analogous to TERM
    3.22    \item xxx
    3.23    \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Tactical
    3.24      then shift into common descendant
    3.25      rename get_stac --> ?ptac?
    3.26    \item xxx
    3.27 -  \item separate code required in both, ProgLang & Interpret (e.g?)
    3.28    \item xxx
    3.29    \item /-------------------------------------------------------------------
    3.30    \item check occurences of KEStore_Elems.add_rlss [("list_rls",
    3.31 @@ -173,6 +165,20 @@
    3.32          .. see \<open>Separate ..\<close>
    3.33    \end{itemize}
    3.34  \<close>
    3.35 +subsection \<open>Postponed, questionable\<close>
    3.36 +text \<open>
    3.37 +  \begin{itemize}
    3.38 +  \item xxx          
    3.39 +  \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
    3.40 +  \item xxx
    3.41 +  \item exception PROG analogous to TERM
    3.42 +  \item xxx
    3.43 +  \item xxx          
    3.44 +  \item xxx          
    3.45 +  \item xxx
    3.46 +  \item xxx          
    3.47 +  \end{itemize}
    3.48 +\<close>
    3.49  
    3.50  section \<open>Separated tasks\<close>
    3.51  text \<open>

     4.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Feb 08 17:00:37 2020 +0100
     4.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Sun Feb 09 12:48:18 2020 +0100
     4.3 @@ -399,9 +399,9 @@
     4.4        val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);
     4.5  
     4.6  val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
     4.7 -          check_tac cc ist (form_arg, prog_tac)  (*return from xxx*);
     4.8 +          check_tac cc ist (prog_tac, form_arg)  (*return from xxx*);
     4.9  "~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
    4.10 -  = (check_tac cc ist (form_arg, prog_tac));
    4.11 +  = (check_tac cc ist (prog_tac, form_arg));
    4.12  
    4.13      Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)  (*return from find_next_step*);
    4.14  "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))

     5.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Sat Feb 08 17:00:37 2020 +0100
     5.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Sun Feb 09 12:48:18 2020 +0100
     5.3 @@ -12,7 +12,6 @@
     5.4  "----------- integrate by ruleset -----------------------";
     5.5  "----------- rewrite 3rd integration in 7.27 ------------";
     5.6  "----------- check probem type --------------------------";
     5.7 -"----------- check Scripts ------------------------------";
     5.8  "----------- me method [diff,integration] ---------------";
     5.9  "----------- autoCalculate [diff,integration] -----------";
    5.10  "----------- me method [diff,integration,named] ---------";
    5.11 @@ -371,25 +370,6 @@
    5.12  	 | _ => error "integrate.sml: Integrate.Integrate ???";
    5.13  
    5.14  
    5.15 -"----------- check Scripts ------------------------------";
    5.16 -"----------- check Scripts ------------------------------";
    5.17 -"----------- check Scripts ------------------------------";
    5.18 -val str = 
    5.19 -"Program IntegrationScript (f_f::real) (v_v::real) =               \
    5.20 -\  (let t_t = Take (Integral f_f D v_v)                                 \
    5.21 -\   in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) (t_t::real))";
    5.22 -val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    5.23 -atomty sc;
    5.24 -
    5.25 -val str = 
    5.26 -"Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
    5.27 -\  (let t_t = Take (F_F v_v = Integral f_f D v_v)                         \
    5.28 -\   in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) t_t)";
    5.29 -val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    5.30 -atomty sc;
    5.31 -show_mets();
    5.32 -
    5.33 -
    5.34  "----------- me method [diff,integration] ---------------";
    5.35  "----------- me method [diff,integration] ---------------";
    5.36  "----------- me method [diff,integration] ---------------";