# HG changeset patch # User Walther Neuper # Date 1574346692 -3600 # Node ID cc83c55e1c1cb8c7295afb4e086e4ca6d2d8ada1 # Parent 190d4d8433ab5b332221c360c36cbcd47ec5ad51 lucin: shift datatype, rename diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/CalcElements/calcelems.sml --- a/src/Tools/isac/CalcElements/calcelems.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/CalcElements/calcelems.sml Thu Nov 21 15:31:32 2019 +0100 @@ -10,8 +10,6 @@ signature CALC_ELEMENT = sig - datatype stacexpr = Expr of term | STac of term - val rep_stacexpr: stacexpr -> term type cas_elem type pbt type ptyps @@ -441,11 +439,6 @@ let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl in overwritel (al, bl') end; -datatype stacexpr = STac of term | Expr of term -fun rep_stacexpr (STac t ) = t - | rep_stacexpr (Expr t) = - error ("rep_stacexpr called with t= " ^ Rule.term2str t); - fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/CalcElements/termC.sml --- a/src/Tools/isac/CalcElements/termC.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/CalcElements/termC.sml Thu Nov 21 15:31:32 2019 +0100 @@ -575,9 +575,10 @@ end (* expects t as Const *) -fun contains_Const_typeless ts t = t +fun contains_Const_typeless ts t = (t |> strip_comb |> fst |> member (fn (t1, t2) => fst (dest_Const t1) = fst (dest_Const t2)) ts +) handle TERM("dest_Const", _) => raise TERM ("contains_Const_typeless", [t]) end \ No newline at end of file diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 15:31:32 2019 +0100 @@ -178,24 +178,15 @@ | scan_dn1 ((pt, p), ctxt, tac) (ist as {eval, act_arg, or, ...}) t = if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t]) - else (* - if Prog_Tac.is t - then - case check_tactic1 t of - Ackn_Tac1 ... - | Reject_Tac1 ... - else - Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval - (subst_atomic (Env.update_opt'' (get_act_env ist, a'(* ?!?!? *))) t)) - - Tactic.from_Prog_Tac vvv etc ... as later change set -*) - (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of - (a', Celem.Expr _) => + else + case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of + (a', Program.Expr _) => +(*--------------------------- eval_Prog_Expr -----*) Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t)) - | (a', Celem.STac stac) => - (case Lucin.associate pt ctxt (tac, stac) of + | (a', Program.Tac stac) => +(*/------------ interprete_Prog_Tac -----*) + case Lucin.associate pt ctxt (tac, stac) of (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*) Lucin.Ass (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) | Lucin.Ass_Weak (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_false (a', v'), ctxt, m) @@ -207,7 +198,8 @@ case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac) | Chead.Notappl _ => Term_Val1 act_arg) - )); +(*------------- interprete_tactic ---//*) + ; fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist @@ -377,8 +369,8 @@ if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t]) else case Lucin.handle_leaf "next " ctxt eval (get_subst ist) t of - (_, Celem.Expr s) => Term_Val2 s - | (a', Celem.STac stac) => + (_, Program.Expr s) => Term_Val2 s + | (a', Program.Tac stac) => let val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac in diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/Interpret/script.sml Thu Nov 21 15:31:32 2019 +0100 @@ -33,7 +33,7 @@ val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool val handle_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*) string -> Rule.theory' -> Rule.rls -> (Env.T * (term option * term)) -> term -> - term option * Celem.stacexpr + term option * Program.leaf (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) @@ -608,23 +608,23 @@ fun handle_leaf call thy srls (E, (a, v)) t = (*WN050916 'upd_env_opt' is a blind copy from previous version*) case Prog_Tac.subst_stacexpr E a v t of - (a', Celem.STac stac) => (* Prog_Tac *) + (a', Program.Tac stac) => (* Prog_Tac *) let val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) stac) in (if (! trace_script) - then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> STac '" ^ Rule.term2str stac ^ "'") + then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'") else (); - (a', Celem.STac stac')) + (a', Program.Tac stac')) end - | (a', Celem.Expr lexpr) => (* Prog_Expr *) + | (a', Program.Expr lexpr) => (* Prog_Expr *) let val lexpr' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) lexpr) in (if (! trace_script) then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'") else (); - (a', Celem.Expr lexpr')) (*lexpr' is the value of the Expr*) + (a', Program.Expr lexpr')) (*lexpr' is the value of the Expr*) end; (*. fetch _all_ tactics from script .*) @@ -643,7 +643,7 @@ val (sc, srls) = (case Specify.get_met metID' of {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1") val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst - in map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o + in map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o (handle_leaf "selrul" thy' srls subst)) (Auto_Prog.stacpbls sc) end; @@ -670,7 +670,7 @@ val (env, (a, v)) = (case get_istate pt (p, p_) of Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2") val alltacs = (*we expect at least 1 stac in a script*) - map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o + map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc) val f = (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/ProgLang/Auto_Prog.thy --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Nov 21 15:31:32 2019 +0100 @@ -83,7 +83,7 @@ | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2) | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2) | scan t = case Prog_Tac.subst_stacexpr [] NONE Rule.e_term t of - (_, Celem.STac _) => [t] | (_, Celem.Expr _) => [] + (_, Program.Tac _) => [t] | (_, Program.Expr _) => [] in (distinct o scan) body end | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Rule.term2str t ^ "'") diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/ProgLang/Prog_Expr.thy --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Nov 21 15:31:32 2019 +0100 @@ -5,7 +5,7 @@ *) theory Prog_Expr - imports Calculate ListC + imports Calculate ListC Program begin text \Abstract: diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/ProgLang/Prog_Tac.thy --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Nov 21 15:31:32 2019 +0100 @@ -4,7 +4,7 @@ *) theory Prog_Tac - imports "~~/src/Tools/isac/CalcElements/CalcElements" + imports Program begin text \Abstract: @@ -59,7 +59,7 @@ sig val dest_spec : term -> Celem.spec val get_stac : 'a -> term -> term option (*rename get_first*) - val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Celem.stacexpr + val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Program.leaf val is: term -> bool (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) @@ -126,59 +126,63 @@ and attach the curried argument of a tactic, if any. CAUTION: (1) currying with #> requires 2 patterns for each tactic (2) the non-curried version must return NONE for a - (3) non-matching patterns become an Celem.Expr by fall-through. + (3) non-matching patterns become an Program.Expr by fall-through. WN060906 quick and dirty fix: due to (2) a is returned, too *) -fun subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite",_) $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite",_) $ _)) = - (a, (*in these cases we hope, that a = SOME _*) - Celem.STac (case a of SOME a' => (subst_atomic E (t $ a')) - | NONE => ((subst_atomic E t) $ v))) - | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)) = - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) - | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _)) = - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) - | subst_stacexpr E _ _ - (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v - (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _)) = - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate", _) $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Calculate", _) $ _)) = - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) - | subst_stacexpr E _ _ - (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Check'_elementwise", _) $ _)) = - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Or'_to'_List", _) $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Or'_to'_List", _))) = (*t $ v*) - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) +fun subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) = + (a, Program.Tac ( + case a of SOME a' => (subst_atomic E (t $ a')) + | NONE => ((subst_atomic E t) $ v))) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) = + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) = + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) = + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) = + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) = + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*) + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Take",_) $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute", _) $ _ $ _)) = - (NONE, Celem.STac (subst_atomic E t)) - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Substitute", _) $ _)) = - (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a') - | NONE => ((subst_atomic E t) $ v))) + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) = + (NONE, Program.Tac (subst_atomic E t)) + | subst_stacexpr E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) = + (a, Program.Tac ( + case a of SOME a' => subst_atomic E (t $ a') + | NONE => ((subst_atomic E t) $ v))) (*now all tactics are matched out and this leaf must be without a tactic*) | subst_stacexpr E a v t = - (a, Celem.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t)); + (a, Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t)); (* check if a term is a Prog_Tac *) diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/ProgLang/Program.thy --- a/src/Tools/isac/ProgLang/Program.thy Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/ProgLang/Program.thy Thu Nov 21 15:31:32 2019 +0100 @@ -34,6 +34,8 @@ \ ML \ signature PROGRAM = sig + datatype leaf = Expr of term | Tac of term + val rep_stacexpr: leaf -> term val prep_program : thm -> term (*ren prepare*) val get_fun_id: term -> string * typ (*ren fun_id*) val formal_args : term -> term list @@ -54,6 +56,11 @@ struct (**) +datatype leaf = Tac of term | Expr of term +fun rep_stacexpr (Tac t ) = t + | rep_stacexpr (Expr t) = + error ("rep_stacexpr called with t= " ^ Rule.term2str t); + (* the lucas-interpreter requires programs in this specific format *) fun prep_program thm = (thm |> Thm.prop_of @@ -83,7 +90,7 @@ handle TERM _ => raise TERM ("body_of", [tm]) -end +(**)end(**) \ ML \ \ ML \ \ diff -r 190d4d8433ab -r cc83c55e1c1c src/Tools/isac/TODO.thy --- a/src/Tools/isac/TODO.thy Thu Nov 21 12:05:56 2019 +0100 +++ b/src/Tools/isac/TODO.thy Thu Nov 21 15:31:32 2019 +0100 @@ -14,6 +14,9 @@ text \ \begin{itemize} \item xxx + \item consistently replace thy by ctxt in lucin; search for + "Isac_Knowledge", Context.theory_name (Rule.Isac""), etc + \item fun mathml.indent: use from LibraryC \item shift show_pt, pr_ctree --> Ctree, improve naming? \item xxx \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here @@ -108,7 +111,7 @@ \item reconsider "fun subst_stacexpr" CAUTION: (1) currying with @@ requires 2 patterns for each tactic (2) the non-curried version must return NONE for a - (3) non-matching patterns become an Celem.Expr by fall-through. + (3) non-matching patterns become an Program.Expr by fall-through. (a, (*in these cases we hope, that a = SOME _*) --> exn ?PROGRAM? rename ?ptac?, prog_tac \item xxx diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Nov 21 15:31:32 2019 +0100 @@ -1295,13 +1295,13 @@ (PolyEq',[abcFormula, degree_2, polynomial, univariate, equation], no_meth) [BOOL equ, REAL z]' - ---> STac 'SubProblem (PolyEq', + ---> Program.Tac 'SubProblem (PolyEq', [abcFormula, degree_2, polynomial, univariate, equation], no_meth) [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]' \end{verbatim} We see the SubProblem with correct arguments from searching next - step (program text !!!--->!!! STac (script tactic) with arguments + step (program text !!!--->!!! Program.Tac (script tactic) with arguments evaluated.) \item Do we have the right Program \ldots difference in the arguments in the arguments\ldots diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Nov 21 15:31:32 2019 +0100 @@ -2379,13 +2379,13 @@ (PolyEq',[abcFormula, degree_2, polynomial, univariate, equation], no_meth) [BOOL equ, REAL z]' - ---> STac 'SubProblem (PolyEq', + ---> Program.Tac 'SubProblem (PolyEq', [abcFormula, degree_2, polynomial, univariate, equation], no_meth) [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]' \end{verbatim} We see the SubProblem with correct arguments from searching next - step (program text !!!--->!!! STac (script tactic) with arguments + step (program text !!!--->!!! Program.Tac (script tactic) with arguments evaluated.) \item Do we have the right Program \ldots difference in the arguments in the arguments\ldots diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 15:31:32 2019 +0100 @@ -83,7 +83,7 @@ (*======= end of scanning tacticals, a leaf =======*) "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) = (xxx, (ist |> path_down [L, R]), e); -val (a', STac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t; +val (a', Program.Tac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t; "----------- re-build: fun locate_input_tactic -------------------------------------------------"; @@ -151,7 +151,7 @@ (*======= end of scanning tacticals, a leaf =======*) "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) = (xxx, (ist |> path_down [R]), e); - val (a', Celem.STac stac) = + val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); val Lucin.Ass (m, v', ctxt) = (*case*) associate pt ctxt (m, stac) (*of*); @@ -328,7 +328,7 @@ (*======= end of scanning tacticals, a leaf =======*) "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t) = (xxx, (ist |> path_down [R]), e); - val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); + val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*); val Aundef = (*case*) or (*of*); val Notappl "norm_equation not applicable" = diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Knowledge/partial_fractions.sml --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Nov 21 15:31:32 2019 +0100 @@ -432,6 +432,6 @@ @@@ istate [" (f_f, 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))"," (zzz, z)"] -@@@ next leaf 'Take f_f' ---> STac 'Take (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))' +@@@ next leaf 'Take f_f' ---> Program.Tac 'Take (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))' *) diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Knowledge/polyeq-1.sml --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu Nov 21 15:31:32 2019 +0100 @@ -236,7 +236,7 @@ ... Ackn_Tac1 ... is correct*) "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body); -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t +val (a', Program.Tac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t val ctxt = get_ctxt pt (p,p_) val p' = lev_on p : pos; (* WAS val NotAss = associate pt d (m, stac) diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Nov 21 15:31:32 2019 +0100 @@ -122,13 +122,13 @@ "~~~~~ fun handle_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t); "~~~~~ fun subst_stacexpr, args:"; val (E, a, v, (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t); -val STac tm = STac (subst_atomic E t); +val Program.Tac tm = Program.Tac (subst_atomic E t); term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}"; (* ------ ^^^ ----- ? "x" ?*) -"~~~~~ to handle_leaf return val:"; val ((a', STac stac)) = ((NONE, STac (subst_atomic E t))); +"~~~~~ to handle_leaf return val:"; val ((a', Program.Tac stac)) = ((NONE, Program.Tac (subst_atomic E t))); val stac' = eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac); term2str stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}"; -"~~~~~ to scan_dn2 return val:"; val ((a', STac stac)) = ((a', STac stac')); +"~~~~~ to scan_dn2 return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac')); val (m,m') = stac2tac_ pt (assoc_thy th) stac; case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *); val (p''''', pt''''', m''''') = (p, pt, m); diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Minisubpbl/200-start-method.sml --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Nov 21 15:31:32 2019 +0100 @@ -146,7 +146,7 @@ (* a leaf has been found *) "~~~~~ fun scan_dn2, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) = (thy, ptp, E, (l @ [Celem.R]), e, a, v); -val (a', STac stac) = handle_leaf "next " th sr (E, (a, v)) t; +val (a', Program.Tac stac) = handle_leaf "next " th sr (E, (a, v)) t; val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac; "~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) = (pt, (Celem.assoc_thy th), stac); diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Nov 21 15:31:32 2019 +0100 @@ -79,7 +79,7 @@ (*======= end of scanning tacticals, a leaf =======*) "~~~~~ fun scan_dn1, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) = (xxx, (ist |> path_down_form ([L, R], a)), e); -val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); +val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); val Ass (Rewrite_Set' _, _, _) = (*case*) associate pt ctxt (m, stac) (*of*); @@ -216,7 +216,7 @@ (*========== a leaf has been found ==========*) "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t) = (xxx, (ist |> path_down [L, R]), e); - val (a', STac stac) = (*case*) Lucin.handle_leaf "next " ctxt eval (get_subst ist) t (*of*); + val (a', Program.Tac stac) = (*case*) Lucin.handle_leaf "next " ctxt eval (get_subst ist) t (*of*); (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy ctxt) stac; "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Minisubpbl/300-init-subpbl.sml --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Nov 21 15:31:32 2019 +0100 @@ -94,24 +94,24 @@ "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) = (xxx, (ist |> path_down [L, R]), e); -val (NONE, STac _) = (*case*) +val (NONE, Program.Tac _) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t); - val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*); + val (a', Program.Tac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*); "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _))) = (E, a, v, t); - (NONE, STac (subst_atomic E t)); (*return value*) -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', STac stac)) - = ((NONE : term option, STac (subst_atomic E t))); + (NONE, Program.Tac (subst_atomic E t)); (*return value*) +"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', Program.Tac stac)) + = ((NONE : term option, Program.Tac (subst_atomic E t))); val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac); - (*return value*) (a', STac stac'); -"~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', STac stac) - = ((a' : term option, STac stac')); + (*return value*) (a', Program.Tac stac'); +"~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', Program.Tac stac) + = ((a' : term option, Program.Tac stac')); val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); (*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 returns e_ctxt" else (); diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Nov 21 15:31:32 2019 +0100 @@ -84,7 +84,7 @@ (*========== a leaf has been found ==========*) "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t) = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body); - val (a', STac stac) = (*case*) + val (a', Program.Tac stac) = (*case*) handle_leaf "next " ctxt eval (get_subst ist) t; val (Check_elementwise "Assumptions", Empty_Tac_) = diff -r 190d4d8433ab -r cc83c55e1c1c test/Tools/isac/Minisubpbl/700-interSteps.sml --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Nov 21 12:05:56 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Nov 21 15:31:32 2019 +0100 @@ -150,7 +150,7 @@ "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t) = (xxx, (ist |> path_down [R]), e); - val (a', STac stac) = + val (a', Program.Tac stac) = (*case*) handle_leaf "next " th sr (get_subst ist) t (*of*); "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (get_subst ist), t); @@ -185,12 +185,12 @@ val SOME a' = (*case*) a (*of*); -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Celem.STac stac) = - ((a, Celem.STac (subst_atomic E (t $ a')))); +"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Program.Tac stac) = + ((a, Program.Tac (subst_atomic E (t $ a')))); val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac) (*------------------------------------------- HERE IS A SECOND subst_atomic ?!?*) ; -"~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Celem.STac stac) = (a', Celem.STac stac); +"~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Program.Tac stac) = (a', Program.Tac stac); val (m,m') = (stac2tac_ : ctree -> theory -> term -> input * T) pt (Celem.assoc_thy th) stac; case m of (**)Rewrite_Inst ([_(*"(''bdv'', x)"*)], ("risolate_bdv_add", _)) => ();