1.1 --- a/src/Tools/isac/CalcElements/calcelems.sml	Thu Nov 21 12:05:56 2019 +0100
     1.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml	Thu Nov 21 15:31:32 2019 +0100
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  signature CALC_ELEMENT =
     1.6    sig
     1.7 -    datatype stacexpr = Expr of term | STac of term
     1.8 -    val rep_stacexpr: stacexpr -> term
     1.9      type cas_elem
    1.10      type pbt
    1.11      type ptyps
    1.12 @@ -441,11 +439,6 @@
    1.13      let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl
    1.14      in overwritel (al, bl') end;
    1.15  
    1.16 -datatype stacexpr = STac of term | Expr of term
    1.17 -fun rep_stacexpr (STac t ) = t
    1.18 -  | rep_stacexpr (Expr t) = 
    1.19 -    error ("rep_stacexpr called with t= " ^ Rule.term2str t);
    1.20 -
    1.21  fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
    1.22  
    1.23  

     2.1 --- a/src/Tools/isac/CalcElements/termC.sml	Thu Nov 21 12:05:56 2019 +0100
     2.2 +++ b/src/Tools/isac/CalcElements/termC.sml	Thu Nov 21 15:31:32 2019 +0100
     2.3 @@ -575,9 +575,10 @@
     2.4    end
     2.5  
     2.6  (* expects t as Const *)
     2.7 -fun contains_Const_typeless ts t = t
     2.8 +fun contains_Const_typeless ts t = (t
     2.9    |> strip_comb |> fst
    2.10    |> member (fn (t1, t2) => fst (dest_Const t1) = fst (dest_Const t2)) ts
    2.11 +) handle TERM("dest_Const", _) => raise TERM ("contains_Const_typeless", [t])
    2.12  
    2.13  
    2.14  end
    2.15 \ No newline at end of file

     3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Nov 21 12:05:56 2019 +0100
     3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Nov 21 15:31:32 2019 +0100
     3.3 @@ -178,24 +178,15 @@
     3.4  
     3.5    | scan_dn1 ((pt, p), ctxt, tac) (ist as {eval, act_arg, or, ...}) t =
     3.6      if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
     3.7 -    else (*
     3.8 -      if Prog_Tac.is t
     3.9 -      then
    3.10 -        case check_tactic1 t of
    3.11 -          Ackn_Tac1 ...
    3.12 -        | Reject_Tac1 ...
    3.13 -      else
    3.14 -        Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
    3.15 -  		    (subst_atomic (Env.update_opt'' (get_act_env ist, a'(* ?!?!? *))) t))
    3.16 -
    3.17 -            Tactic.from_Prog_Tac vvv etc ... as later change set
    3.18 -*)
    3.19 -      (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
    3.20 -  	     (a', Celem.Expr _) => 
    3.21 +    else
    3.22 +      case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
    3.23 +  	     (a', Program.Expr _) => 
    3.24 +(*--------------------------- eval_Prog_Expr -----*)
    3.25    	       Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
    3.26    		       (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t))
    3.27 -       | (a', Celem.STac stac) =>
    3.28 -           (case Lucin.associate pt ctxt (tac, stac) of
    3.29 +       | (a', Program.Tac stac) =>
    3.30 +(*/------------ interprete_Prog_Tac -----*)
    3.31 +           case Lucin.associate pt ctxt (tac, stac) of
    3.32                (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
    3.33    	           Lucin.Ass      (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m)
    3.34               | Lucin.Ass_Weak (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_false (a', v'), ctxt, m)
    3.35 @@ -207,7 +198,8 @@
    3.36                     case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of
    3.37                        Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac)
    3.38                      | Chead.Notappl _ => Term_Val1 act_arg)
    3.39 -      ));
    3.40 +(*------------- interprete_tactic ---//*)
    3.41 +      ;
    3.42  
    3.43  fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
    3.44    | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
    3.45 @@ -377,8 +369,8 @@
    3.46      if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t])
    3.47      else
    3.48        case Lucin.handle_leaf "next  " ctxt eval (get_subst ist) t of
    3.49 -  	    (_, Celem.Expr s) => Term_Val2 s
    3.50 -      | (a', Celem.STac stac) =>
    3.51 +  	    (_, Program.Expr s) => Term_Val2 s
    3.52 +      | (a', Program.Tac stac) =>
    3.53    	    let
    3.54    	      val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
    3.55          in

     4.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Nov 21 12:05:56 2019 +0100
     4.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Nov 21 15:31:32 2019 +0100
     4.3 @@ -33,7 +33,7 @@
     4.4    val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
     4.5    val handle_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
     4.6      string -> Rule.theory' -> Rule.rls -> (Env.T * (term option * term)) -> term -> 
     4.7 -      term option * Celem.stacexpr
     4.8 +      term option * Program.leaf
     4.9  
    4.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    4.11    (*NONE*)
    4.12 @@ -608,23 +608,23 @@
    4.13  fun handle_leaf call thy srls (E, (a, v)) t =
    4.14        (*WN050916 'upd_env_opt' is a blind copy from previous version*)
    4.15      case Prog_Tac.subst_stacexpr E a v t of
    4.16 -	    (a', Celem.STac stac) => (* Prog_Tac *)
    4.17 +	    (a', Program.Tac stac) => (* Prog_Tac *)
    4.18  	      let val stac' =
    4.19              Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) stac)
    4.20  	      in
    4.21            (if (! trace_script) 
    4.22 -	         then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> STac '" ^ Rule.term2str stac ^ "'")
    4.23 +	         then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
    4.24  	         else ();
    4.25 -	         (a', Celem.STac stac'))
    4.26 +	         (a', Program.Tac stac'))
    4.27  	      end
    4.28 -    | (a', Celem.Expr lexpr) => (* Prog_Expr *)
    4.29 +    | (a', Program.Expr lexpr) => (* Prog_Expr *)
    4.30  	      let val lexpr' =
    4.31              Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
    4.32  	      in
    4.33            (if (! trace_script) 
    4.34  	         then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
    4.35  	         else ();
    4.36 -	         (a', Celem.Expr lexpr')) (*lexpr' is the value of the Expr*)
    4.37 +	         (a', Program.Expr lexpr')) (*lexpr' is the value of the Expr*)
    4.38  	      end;
    4.39  
    4.40  (*. fetch _all_ tactics from script .*)
    4.41 @@ -643,7 +643,7 @@
    4.42          val (sc, srls) = (case Specify.get_met metID' of
    4.43              {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
    4.44          val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
    4.45 -      in map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o
    4.46 +      in map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o
    4.47    	    (handle_leaf "selrul" thy' srls subst)) (Auto_Prog.stacpbls sc)
    4.48    	  end;
    4.49  
    4.50 @@ -670,7 +670,7 @@
    4.51          val (env, (a, v)) = (case get_istate pt (p, p_) of
    4.52              Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
    4.53          val alltacs = (*we expect at least 1 stac in a script*)
    4.54 -          map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o
    4.55 +          map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o
    4.56             (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
    4.57          val f =
    4.58            (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p

     5.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Thu Nov 21 12:05:56 2019 +0100
     5.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Thu Nov 21 15:31:32 2019 +0100
     5.3 @@ -83,7 +83,7 @@
     5.4          | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
     5.5          | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2)
     5.6          | scan t = case Prog_Tac.subst_stacexpr [] NONE Rule.e_term t of
     5.7 -  			  (_, Celem.STac _) => [t] | (_, Celem.Expr _) => []
     5.8 +  			  (_, Program.Tac _) => [t] | (_, Program.Expr _) => []
     5.9      in (distinct o scan) body end
    5.10    | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Rule.term2str t ^ "'")
    5.11  

     6.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Nov 21 12:05:56 2019 +0100
     6.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Nov 21 15:31:32 2019 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  *)
     6.5  
     6.6  theory Prog_Expr
     6.7 -  imports Calculate ListC
     6.8 +  imports Calculate ListC Program
     6.9  begin
    6.10  
    6.11  text \<open>Abstract:

     7.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Nov 21 12:05:56 2019 +0100
     7.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Nov 21 15:31:32 2019 +0100
     7.3 @@ -4,7 +4,7 @@
     7.4   *)
     7.5  
     7.6  theory Prog_Tac
     7.7 -  imports "~~/src/Tools/isac/CalcElements/CalcElements"
     7.8 +  imports Program
     7.9  begin
    7.10  
    7.11  text \<open>Abstract:
    7.12 @@ -59,7 +59,7 @@
    7.13  sig
    7.14    val dest_spec : term -> Celem.spec
    7.15    val get_stac : 'a -> term -> term option (*rename get_first*)
    7.16 -  val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Celem.stacexpr
    7.17 +  val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Program.leaf
    7.18    val is: term -> bool
    7.19  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    7.20    (*NONE*)
    7.21 @@ -126,59 +126,63 @@
    7.22     and attach the curried argument of a tactic, if any.
    7.23  CAUTION: (1) currying with #> requires 2 patterns for each tactic
    7.24           (2) the non-curried version must return NONE for a 
    7.25 -	       (3) non-matching patterns become an Celem.Expr by fall-through.
    7.26 +	       (3) non-matching patterns become an Program.Expr by fall-through.
    7.27  WN060906 quick and dirty fix: due to (2) a is returned, too *)
    7.28 -fun subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite",_) $ _ $ _)) =
    7.29 -    (NONE, Celem.STac (subst_atomic E t))
    7.30 -  | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite",_) $ _)) =
    7.31 -    (a, (*in these cases we hope, that a = SOME _*)
    7.32 -     Celem.STac (case a of SOME a' => (subst_atomic E (t $ a'))
    7.33 -		       | NONE => ((subst_atomic E t) $ v)))
    7.34 -  | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _)) =
    7.35 -    (NONE, Celem.STac (subst_atomic E t))
    7.36 -  | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)) =
    7.37 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
    7.38 -	     | NONE => ((subst_atomic E t) $ v)))
    7.39 -  | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _ $ _)) =
    7.40 -    (NONE, Celem.STac (subst_atomic E t))
    7.41 -  | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _)) =
    7.42 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
    7.43 -	     | NONE => ((subst_atomic E t) $ v)))
    7.44 -  | subst_stacexpr E _ _ 
    7.45 -	      (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
    7.46 -    (NONE, Celem.STac (subst_atomic E t))
    7.47 -  | subst_stacexpr E a v 
    7.48 -	      (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _)) =
    7.49 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
    7.50 -	     | NONE => ((subst_atomic E t) $ v)))
    7.51 -  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate", _) $ _ $ _)) =
    7.52 -    (NONE, Celem.STac (subst_atomic E t))
    7.53 -  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Calculate", _) $ _)) =
    7.54 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
    7.55 -	     | NONE => ((subst_atomic E t) $ v)))
    7.56 -  | subst_stacexpr E _ _ 
    7.57 -	      (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _)) = 
    7.58 -    (NONE, Celem.STac (subst_atomic E t))
    7.59 -  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Check'_elementwise", _) $ _)) = 
    7.60 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
    7.61 -		 | NONE => ((subst_atomic E t) $ v)))
    7.62 -  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Or'_to'_List", _) $ _)) = 
    7.63 -    (NONE, Celem.STac (subst_atomic E t))
    7.64 -  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Or'_to'_List", _))) = (*t $ v*)
    7.65 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
    7.66 -		 | NONE => ((subst_atomic E t) $ v)))
    7.67 +fun subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
    7.68 +    (NONE, Program.Tac (subst_atomic E t))
    7.69 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
    7.70 +    (a, Program.Tac (
    7.71 +      case a of SOME a' => (subst_atomic E (t $ a'))
    7.72 +		          | NONE => ((subst_atomic E t) $ v)))
    7.73 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
    7.74 +    (NONE, Program.Tac (subst_atomic E t))
    7.75 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =
    7.76 +    (a, Program.Tac (
    7.77 +      case a of SOME a' => subst_atomic E (t $ a')
    7.78 +	            | NONE => ((subst_atomic E t) $ v)))
    7.79 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =
    7.80 +    (NONE, Program.Tac (subst_atomic E t))
    7.81 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =
    7.82 +    (a, Program.Tac (
    7.83 +      case a of SOME a' => subst_atomic E (t $ a')
    7.84 +	            | NONE => ((subst_atomic E t) $ v)))
    7.85 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =
    7.86 +    (NONE, Program.Tac (subst_atomic E t))
    7.87 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =
    7.88 +    (a, Program.Tac (
    7.89 +      case a of SOME a' => subst_atomic E (t $ a')
    7.90 +	            | NONE => ((subst_atomic E t) $ v)))
    7.91 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
    7.92 +    (NONE, Program.Tac (subst_atomic E t))
    7.93 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
    7.94 +    (a, Program.Tac (
    7.95 +      case a of SOME a' => subst_atomic E (t $ a')
    7.96 +	            | NONE => ((subst_atomic E t) $ v)))
    7.97 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) = 
    7.98 +    (NONE, Program.Tac (subst_atomic E t))
    7.99 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) = 
   7.100 +    (a, Program.Tac (
   7.101 +      case a of SOME a' => subst_atomic E (t $ a')
   7.102 +		          | NONE => ((subst_atomic E t) $ v)))
   7.103 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) = 
   7.104 +    (NONE, Program.Tac (subst_atomic E t))
   7.105 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*)
   7.106 +    (a, Program.Tac (
   7.107 +      case a of SOME a' => subst_atomic E (t $ a')
   7.108 +		          | NONE => ((subst_atomic E t) $ v)))
   7.109    | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
   7.110 -    (NONE, Celem.STac (subst_atomic E t))
   7.111 -  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Take",_) $ _)) =
   7.112 -    (NONE, Celem.STac (subst_atomic E t))
   7.113 -  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute", _) $ _ $ _)) =
   7.114 -    (NONE, Celem.STac (subst_atomic E t))
   7.115 -  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Substitute", _) $ _)) =
   7.116 -    (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
   7.117 -		 | NONE => ((subst_atomic E t) $ v)))
   7.118 +    (NONE, Program.Tac (subst_atomic E t))
   7.119 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =
   7.120 +    (NONE, Program.Tac (subst_atomic E t))
   7.121 +  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
   7.122 +    (NONE, Program.Tac (subst_atomic E t))
   7.123 +  | subst_stacexpr E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
   7.124 +    (a, Program.Tac (
   7.125 +      case a of SOME a' => subst_atomic E (t $ a')
   7.126 +		          | NONE => ((subst_atomic E t) $ v)))
   7.127    (*now all tactics are matched out and this leaf must be without a tactic*)
   7.128    | subst_stacexpr E a v t = 
   7.129 -    (a, Celem.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));
   7.130 +    (a, Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));
   7.131  
   7.132  
   7.133  (* check if a term is a Prog_Tac *)

     8.1 --- a/src/Tools/isac/ProgLang/Program.thy	Thu Nov 21 12:05:56 2019 +0100
     8.2 +++ b/src/Tools/isac/ProgLang/Program.thy	Thu Nov 21 15:31:32 2019 +0100
     8.3 @@ -34,6 +34,8 @@
     8.4  \<close> ML \<open>
     8.5  signature PROGRAM =
     8.6    sig
     8.7 +    datatype leaf = Expr of term | Tac of term
     8.8 +    val rep_stacexpr: leaf -> term
     8.9      val prep_program : thm -> term        (*ren prepare*)
    8.10      val get_fun_id: term -> string * typ  (*ren fun_id*)
    8.11      val formal_args : term -> term list
    8.12 @@ -54,6 +56,11 @@
    8.13  struct
    8.14  (**)
    8.15  
    8.16 +datatype leaf = Tac of term | Expr of term
    8.17 +fun rep_stacexpr (Tac t ) = t
    8.18 +  | rep_stacexpr (Expr t) = 
    8.19 +    error ("rep_stacexpr called with t= " ^ Rule.term2str t);
    8.20 +
    8.21  (* the lucas-interpreter requires programs in this specific format *)
    8.22  fun prep_program thm = (thm
    8.23    |> Thm.prop_of
    8.24 @@ -83,7 +90,7 @@
    8.25    handle TERM _ => raise TERM ("body_of", [tm])
    8.26  
    8.27  
    8.28 -end
    8.29 +(**)end(**)
    8.30  \<close> ML \<open>
    8.31  \<close> ML \<open>
    8.32  \<close>

     9.1 --- a/src/Tools/isac/TODO.thy	Thu Nov 21 12:05:56 2019 +0100
     9.2 +++ b/src/Tools/isac/TODO.thy	Thu Nov 21 15:31:32 2019 +0100
     9.3 @@ -14,6 +14,9 @@
     9.4  text \<open>
     9.5    \begin{itemize}
     9.6    \item xxx
     9.7 +  \item consistently replace thy by ctxt in lucin; search for 
     9.8 +    "Isac_Knowledge", Context.theory_name (Rule.Isac""), etc
     9.9 +  \item fun mathml.indent: use from LibraryC
    9.10    \item shift show_pt, pr_ctree --> Ctree, improve naming?
    9.11    \item xxx
    9.12    \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
    9.13 @@ -108,7 +111,7 @@
    9.14    \item reconsider "fun subst_stacexpr"
    9.15       CAUTION: (1) currying with @@ requires 2 patterns for each tactic
    9.16                (2) the non-curried version must return NONE for a 
    9.17 -     	      (3) non-matching patterns become an Celem.Expr by fall-through.
    9.18 +     	      (3) non-matching patterns become an Program.Expr by fall-through.
    9.19         (a, (*in these cases we hope, that a = SOME _*) --> exn ?PROGRAM?
    9.20       rename ?ptac?, prog_tac
    9.21    \item xxx

    10.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Nov 21 12:05:56 2019 +0100
    10.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Nov 21 15:31:32 2019 +0100
    10.3 @@ -1295,13 +1295,13 @@
    10.4       (PolyEq',[abcFormula, degree_2, polynomial, 
    10.5                 univariate, equation], no_meth)
    10.6       [BOOL equ, REAL z]' 
    10.7 -       ---> STac 'SubProblem (PolyEq',
    10.8 +       ---> Program.Tac 'SubProblem (PolyEq',
    10.9                [abcFormula, degree_2, polynomial,
   10.10                 univariate, equation], no_meth)
   10.11       [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
   10.12       \end{verbatim}
   10.13           We see the SubProblem with correct arguments from searching next
   10.14 -         step (program text !!!--->!!! STac (script tactic) with arguments
   10.15 +         step (program text !!!--->!!! Program.Tac (script tactic) with arguments
   10.16           evaluated.)
   10.17       \item Do we have the right Program \ldots difference in the
   10.18           arguments in the arguments\ldots

    11.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Thu Nov 21 12:05:56 2019 +0100
    11.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Thu Nov 21 15:31:32 2019 +0100
    11.3 @@ -2379,13 +2379,13 @@
    11.4       (PolyEq',[abcFormula, degree_2, polynomial, 
    11.5                 univariate, equation], no_meth)
    11.6       [BOOL equ, REAL z]' 
    11.7 -       ---> STac 'SubProblem (PolyEq',
    11.8 +       ---> Program.Tac 'SubProblem (PolyEq',
    11.9                [abcFormula, degree_2, polynomial,
   11.10                 univariate, equation], no_meth)
   11.11       [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
   11.12       \end{verbatim}
   11.13           We see the SubProblem with correct arguments from searching next
   11.14 -         step (program text !!!--->!!! STac (script tactic) with arguments
   11.15 +         step (program text !!!--->!!! Program.Tac (script tactic) with arguments
   11.16           evaluated.)
   11.17       \item Do we have the right Program \ldots difference in the
   11.18           arguments in the arguments\ldots

    12.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Thu Nov 21 12:05:56 2019 +0100
    12.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Thu Nov 21 15:31:32 2019 +0100
    12.3 @@ -83,7 +83,7 @@
    12.4      (*======= end of scanning tacticals, a leaf =======*)
    12.5  "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
    12.6    = (xxx, (ist |> path_down [L, R]), e);
    12.7 -val (a', STac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
    12.8 +val (a', Program.Tac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
    12.9  
   12.10  
   12.11  "----------- re-build: fun locate_input_tactic -------------------------------------------------";
   12.12 @@ -151,7 +151,7 @@
   12.13      (*======= end of scanning tacticals, a leaf =======*)
   12.14  "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
   12.15    = (xxx, (ist |> path_down [R]), e);
   12.16 -    val (a', Celem.STac stac) =
   12.17 +    val (a', Program.Tac stac) =
   12.18        (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
   12.19      val Lucin.Ass (m, v', ctxt) =
   12.20        (*case*) associate pt ctxt (m, stac) (*of*);
   12.21 @@ -328,7 +328,7 @@
   12.22      (*======= end of scanning tacticals, a leaf =======*)
   12.23  "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
   12.24    = (xxx, (ist |> path_down [R]), e);
   12.25 -    val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
   12.26 +    val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
   12.27        val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
   12.28        val Aundef = (*case*) or (*of*);
   12.29    val Notappl "norm_equation not applicable" =    

    13.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Nov 21 12:05:56 2019 +0100
    13.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Nov 21 15:31:32 2019 +0100
    13.3 @@ -432,6 +432,6 @@
    13.4  @@@ istate ["
    13.5  (f_f, 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))","
    13.6  (zzz, z)"] 
    13.7 -@@@ next   leaf 'Take f_f' ---> STac 'Take (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))'
    13.8 +@@@ next   leaf 'Take f_f' ---> Program.Tac 'Take (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))'
    13.9  *)
   13.10  

    14.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 21 12:05:56 2019 +0100
    14.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 21 15:31:32 2019 +0100
    14.3 @@ -236,7 +236,7 @@
    14.4        ... Ackn_Tac1 ... is correct*)
    14.5  "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
    14.6       ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
    14.7 -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
    14.8 +val (a', Program.Tac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
    14.9               val ctxt = get_ctxt pt (p,p_)
   14.10               val p' = lev_on p : pos;
   14.11  (* WAS val NotAss = associate pt d (m, stac)

    15.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Thu Nov 21 12:05:56 2019 +0100
    15.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Thu Nov 21 15:31:32 2019 +0100
    15.3 @@ -122,13 +122,13 @@
    15.4  "~~~~~ fun handle_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
    15.5  "~~~~~ fun subst_stacexpr, args:"; val (E, a, v, 
    15.6  	  (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
    15.7 -val STac tm = STac (subst_atomic E t);
    15.8 +val Program.Tac tm = Program.Tac (subst_atomic E t);
    15.9  term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
   15.10  (*                                     ------ ^^^ ----- ? "x" ?*)
   15.11 -"~~~~~ to handle_leaf return val:"; val ((a', STac stac)) = ((NONE, STac (subst_atomic E t)));
   15.12 +"~~~~~ to handle_leaf return val:"; val ((a', Program.Tac stac)) = ((NONE, Program.Tac (subst_atomic E t)));
   15.13  val stac' = eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
   15.14  term2str stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
   15.15 -"~~~~~ to scan_dn2 return val:"; val ((a', STac stac)) = ((a', STac stac'));
   15.16 +"~~~~~ to scan_dn2 return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));
   15.17  val (m,m') = stac2tac_ pt (assoc_thy th) stac;
   15.18  case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
   15.19  val (p''''', pt''''', m''''') = (p, pt, m);

    16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Thu Nov 21 12:05:56 2019 +0100
    16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Thu Nov 21 15:31:32 2019 +0100
    16.3 @@ -146,7 +146,7 @@
    16.4    (* a leaf has been found *)   
    16.5  "~~~~~ fun scan_dn2, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
    16.6    (thy, ptp, E, (l @ [Celem.R]), e, a, v);
    16.7 -val (a', STac stac) = handle_leaf "next  " th sr (E, (a, v)) t;
    16.8 +val (a', Program.Tac stac) = handle_leaf "next  " th sr (E, (a, v)) t;
    16.9  val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
   16.10  "~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
   16.11    (pt, (Celem.assoc_thy th), stac);

    17.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Thu Nov 21 12:05:56 2019 +0100
    17.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Thu Nov 21 15:31:32 2019 +0100
    17.3 @@ -79,7 +79,7 @@
    17.4      (*======= end of scanning tacticals, a leaf =======*)
    17.5  "~~~~~ fun scan_dn1, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
    17.6    (xxx, (ist |> path_down_form ([L, R], a)), e);
    17.7 -val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
    17.8 +val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
    17.9  
   17.10  val Ass (Rewrite_Set' _, _, _) = (*case*)
   17.11             associate pt ctxt (m, stac) (*of*);
   17.12 @@ -216,7 +216,7 @@
   17.13      (*========== a leaf has been found ==========*)   
   17.14  "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
   17.15    = (xxx, (ist |> path_down [L, R]), e);
   17.16 -        val (a', STac stac) = (*case*) Lucin.handle_leaf  "next  " ctxt eval (get_subst ist) t (*of*);
   17.17 +        val (a', Program.Tac stac) = (*case*) Lucin.handle_leaf  "next  " ctxt eval (get_subst ist) t (*of*);
   17.18  
   17.19     (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy ctxt) stac;
   17.20  "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))

    18.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Thu Nov 21 12:05:56 2019 +0100
    18.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Thu Nov 21 15:31:32 2019 +0100
    18.3 @@ -94,24 +94,24 @@
    18.4  "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
    18.5    = (xxx, (ist |> path_down [L, R]), e);
    18.6  
    18.7 -val (NONE, STac _) = (*case*)
    18.8 +val (NONE, Program.Tac _) = (*case*)
    18.9             handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
   18.10  "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
   18.11    = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t);
   18.12  
   18.13 -    val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
   18.14 +    val (a', Program.Tac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
   18.15  "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
   18.16    = (E, a, v, t);
   18.17  
   18.18 -     (NONE, STac (subst_atomic E t)); (*return value*)
   18.19 -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', STac stac))
   18.20 -  = ((NONE : term option, STac (subst_atomic E t)));
   18.21 +     (NONE, Program.Tac (subst_atomic E t)); (*return value*)
   18.22 +"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', Program.Tac stac))
   18.23 +  = ((NONE : term option, Program.Tac (subst_atomic E t)));
   18.24          val stac' =
   18.25              Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac);
   18.26  
   18.27 -                                 (*return value*) (a', STac stac');
   18.28 -"~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', STac stac)
   18.29 -  = ((a' : term option, STac stac'));
   18.30 +                                 (*return value*) (a', Program.Tac stac');
   18.31 +"~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', Program.Tac stac)
   18.32 +  = ((a' : term option, Program.Tac stac'));
   18.33             val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
   18.34  
   18.35  (*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 returns e_ctxt" else ();

    19.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Thu Nov 21 12:05:56 2019 +0100
    19.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Thu Nov 21 15:31:32 2019 +0100
    19.3 @@ -84,7 +84,7 @@
    19.4      (*========== a leaf has been found ==========*)   
    19.5  "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
    19.6    = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
    19.7 -  val (a', STac stac) = (*case*)
    19.8 +  val (a', Program.Tac stac) = (*case*)
    19.9        handle_leaf "next " ctxt eval (get_subst ist) t;
   19.10  
   19.11  	      val (Check_elementwise "Assumptions", Empty_Tac_) =

    20.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml	Thu Nov 21 12:05:56 2019 +0100
    20.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml	Thu Nov 21 15:31:32 2019 +0100
    20.3 @@ -150,7 +150,7 @@
    20.4  "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
    20.5    = (xxx, (ist |> path_down [R]), e);
    20.6  
    20.7 -  val (a', STac stac) =
    20.8 +  val (a', Program.Tac stac) =
    20.9    (*case*) handle_leaf "next  " th sr (get_subst ist) t (*of*);
   20.10  "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
   20.11    = ("next  ", th, sr, (get_subst ist), t);
   20.12 @@ -185,12 +185,12 @@
   20.13  
   20.14      val SOME a' = (*case*) a (*of*);
   20.15  
   20.16 -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Celem.STac stac) =
   20.17 -  ((a, Celem.STac (subst_atomic E (t $ a'))));
   20.18 +"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Program.Tac stac) =
   20.19 +  ((a, Program.Tac (subst_atomic E (t $ a'))));
   20.20    val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac)
   20.21    (*------------------------------------------- HERE IS A SECOND subst_atomic ?!?*)
   20.22  ;
   20.23 -"~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Celem.STac stac) = (a', Celem.STac stac);
   20.24 +"~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Program.Tac stac) = (a', Program.Tac stac);
   20.25    val (m,m') = (stac2tac_ : ctree -> theory -> term -> input * T) pt (Celem.assoc_thy th) stac;
   20.26    case m of
   20.27  (**)Rewrite_Inst ([_(*"(''bdv'', x)"*)], ("risolate_bdv_add", _)) => ();