1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Oct 30 16:46:05 2019 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Oct 31 10:41:42 2019 +0100
1.3 @@ -56,9 +56,9 @@
1.4 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
1.5 val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
1.6 val setTheory : Celem.calcID -> Rule.thyID -> XML.tree
1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
1.9 (* NONE *)
1.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.12 end
1.13
1.14 (**)
2.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Wed Oct 30 16:46:05 2019 +0100
2.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Thu Oct 31 10:41:42 2019 +0100
2.3 @@ -110,11 +110,11 @@
2.4 val pats2str' : pat list -> string
2.5 val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
2.6 thydata ptyp list
2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
2.9 val knowthys: unit -> theory list
2.10 val e_pbt: pbt
2.11 val e_met: met
2.12 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.13 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.14
2.15 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
2.16 val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->
3.1 --- a/src/Tools/isac/CalcElements/contextC.sml Wed Oct 30 16:46:05 2019 +0100
3.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Thu Oct 31 10:41:42 2019 +0100
3.3 @@ -14,9 +14,9 @@
3.4 val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
3.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.6 (*NONE*)
3.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
3.9 val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
3.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.12 end
3.13
3.14 (* survey on handling contexts:
4.1 --- a/src/Tools/isac/CalcElements/libraryC.sml Wed Oct 30 16:46:05 2019 +0100
4.2 +++ b/src/Tools/isac/CalcElements/libraryC.sml Thu Oct 31 10:41:42 2019 +0100
4.3 @@ -77,10 +77,10 @@
4.4 val ~~~ : 'a list * 'b list -> ('a * 'b) list
4.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.6 (* NONE *)
4.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
4.9 val enumerate_strings: string list -> string list
4.10 val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
4.11 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.12 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.13
4.14
4.15 (*///------------------------------>>> thy ------------------------------------------------\\\*)
5.1 --- a/src/Tools/isac/CalcElements/rule.sml Wed Oct 30 16:46:05 2019 +0100
5.2 +++ b/src/Tools/isac/CalcElements/rule.sml Thu Oct 31 10:41:42 2019 +0100
5.3 @@ -110,11 +110,11 @@
5.4 val terms2str': term list -> string (* shift up to Unparse *)
5.5 val thm2str: thm -> string
5.6 val thms2str : thm list -> string
5.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
5.9 val string_of_thm': theory -> thm -> string (* shift up to Unparse *)
5.10 val string_of_thm: thm -> string (* shift up to Unparse *)
5.11 val errpats2str : errpat list -> string
5.12 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.13 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.14
5.15 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
5.16
6.1 --- a/src/Tools/isac/CalcElements/termC.sml Wed Oct 30 16:46:05 2019 +0100
6.2 +++ b/src/Tools/isac/CalcElements/termC.sml Thu Oct 31 10:41:42 2019 +0100
6.3 @@ -85,10 +85,10 @@
6.4 val atomty_thy: Rule.thyID -> term -> unit
6.5 val free2var: term -> term
6.6 val contains_one_of: thm * (string * typ) list -> bool
6.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
6.9 val atomt: term -> unit
6.10 val typ_a2real: term -> term
6.11 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.12 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.13 end
6.14
6.15 (**)
7.1 --- a/src/Tools/isac/Interpret/Interpret.thy Wed Oct 30 16:46:05 2019 +0100
7.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Oct 31 10:41:42 2019 +0100
7.3 @@ -18,7 +18,7 @@
7.4 Istate.AppUndef_: Istate.appy_ (*end =...*);
7.5 Istate.Skip_
7.6 \<close> ML \<open>
7.7 -Aundef: asap (*or = ... NOT : Istate TODO*)
7.8 +Istate.Aundef: Istate.asap (*or = ... NOT : Istate TODO*)
7.9 \<close> ML \<open>
7.10 \<close> ML \<open>
7.11 \<close> ML \<open>
8.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Oct 30 16:46:05 2019 +0100
8.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Oct 31 10:41:42 2019 +0100
8.3 @@ -24,7 +24,7 @@
8.4
8.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.6 (* NONE *)
8.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
8.9 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
8.10 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
8.11 val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option
8.12 @@ -32,7 +32,7 @@
8.13 'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
8.14 val get_fillpats :
8.15 'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list
8.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.18
8.19 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
8.20 val e_icalhd : icalhd
9.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 16:46:05 2019 +0100
9.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Oct 31 10:41:42 2019 +0100
9.3 @@ -40,13 +40,12 @@
9.4 | NasApp of Istate.pstate * Proof.context * Tactic.T
9.5 | NasNap of term * Env.T;
9.6 val assoc2str : assoc -> string
9.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
9.9 datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T
9.10 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
9.11 val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy
9.12 val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy
9.13 val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy
9.14 - datatype asap = Aundef | AssOnly | AssGen;
9.15 val go : Celem.loc_ -> term -> term
9.16 val go_up: Celem.loc_ -> term -> term
9.17 val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy
9.18 @@ -54,11 +53,11 @@
9.19 val check_Let_up : Celem.loc_ -> term -> term * term
9.20 val check_Seq_up: Celem.loc_ -> term -> term
9.21 (* intermediate arg list ---------------------------------------------------------------------\*)
9.22 - val assy : Proof.context * Rule.rls * Ctree.state * asap -> Istate.pstate * Tactic.T -> term -> assoc
9.23 + val assy : Proof.context * Rule.rls * Ctree.state * Istate.asap -> Istate.pstate * Tactic.T -> term -> assoc
9.24 val astep_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> assoc
9.25 val ass_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> term -> assoc
9.26 (* intermediate arg list ---------------------------------------------------------------------/*)
9.27 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.28 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.29 end
9.30
9.31 (**)
9.32 @@ -175,12 +174,10 @@
9.33 val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy th) stac
9.34 in
9.35 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
9.36 - Tactic.Subproblem _ => Appy (m', (
9.37 - get_env ist, get_path ist, get_rls ist, a', Lucin.tac_2res m', Istate.AppUndef_, false))
9.38 + Tactic.Subproblem _ => Appy (m', ist |> upd_subst_reset (a', Lucin.tac_2res m'))
9.39 | _ =>
9.40 (case Applicable.applicable_in p pt m of
9.41 - Chead.Appl m' => (Appy (m', (
9.42 - get_env ist, get_path ist, get_rls ist, a', Lucin.tac_2res m', Istate.AppUndef_, false)))
9.43 + Chead.Appl m' => (Appy (m', ist |> upd_subst_reset (a', Lucin.tac_2res m')))
9.44 | _ => Napp (get_env ist))
9.45 end
9.46
9.47 @@ -282,7 +279,7 @@
9.48 fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate ist) =
9.49 if 0 = length (get_path ist)
9.50 then appy thy ptp (trans_scan_down2 ist) (Program.body_of prog)
9.51 - else nstep_up thy ptp sc (trans_scan_down2 ist) Skip_
9.52 + else nstep_up thy ptp sc (trans_scan_up2 ist) Skip_
9.53 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";
9.54
9.55 (* decide for the next applicable Prog_Tac in the program *)
9.56 @@ -292,7 +289,7 @@
9.57 (case par_pbl_det pt p of
9.58 (true, p', _) =>
9.59 let
9.60 - val (_,pblID,_) = get_obj g_spec pt p';
9.61 + val (_, pblID, _) = get_obj g_spec pt p';
9.62 in
9.63 (Tactic.Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
9.64 (Istate.e_istate, ctxt), (v, Telem.Safe))
9.65 @@ -301,8 +298,8 @@
9.66 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe)))
9.67 | Napp _ =>
9.68 (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
9.69 - | Appy (m', scrst as (_,_,_,_,v,_,_)) =>
9.70 - (m', (Istate.Pstate scrst, ctxt), (v, Telem.Safe))) (* found next tac *)
9.71 + | Appy (m', ist) =>
9.72 + (m', (Pstate ist, ctxt), (get_act ist, Telem.Safe))) (* found next tac *)
9.73 | determine_next_tactic _ _ _ (is, _) =
9.74 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
9.75
9.76 @@ -328,14 +325,6 @@
9.77 | assoc2str (NasNap _) = "NasNap"
9.78 | assoc2str (NasApp _) = "NasApp";
9.79
9.80 -datatype asap = (* arg. of assy _only_ for distinction w.r.t. Or *)
9.81 - Aundef (* undefined: set only by (topmost) Or *)
9.82 -| AssOnly (* do not execute appl stacs - there could be an associated
9.83 - in parallel Or-branch *)
9.84 -| AssGen; (* no Ass(Weak) found within Or, thus
9.85 - search for _applicable_ stacs, execute and generate pt *)
9.86 -(*this constructions doesnt allow arbitrary nesting of Or !!! *)
9.87 -
9.88 (*WN161112 blanks between list elements left as is until istate is introduced here*)
9.89 fun assy (ya as (_, _, cstate, asap)) (ist, tac) (Const ("HOL.Let", _) $ e $ (Abs (id, T, body))) =
9.90 (case assy ya (ist |> path_down [L, R], tac) e of
9.91 @@ -501,10 +490,10 @@
9.92 val _ = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*)
9.93 in
9.94 (case execute_progr_2 Rule.e_rls tac cstate (progr, Rule.e_rls) (istate, ctxt) of
9.95 - Assoc (is as (_,_,_,_,_,_,strong_ass), ctxt, tac') =>
9.96 - if strong_ass
9.97 - then Safe_Step (Istate.Pstate is, ctxt, tac')
9.98 - else Unsafe_Step (Istate.Pstate is, ctxt, tac')
9.99 + Assoc (ist, ctxt, tac') =>
9.100 + if get_assoc ist
9.101 + then Safe_Step (Istate.Pstate ist, ctxt, tac')
9.102 + else Unsafe_Step (Istate.Pstate ist, ctxt, tac')
9.103 | NasApp _ => Not_Locatable (Tactic.tac_2str tac ^ " not locatable")
9.104 | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
9.105 end
10.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Oct 30 16:46:05 2019 +0100
10.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 31 10:41:42 2019 +0100
10.3 @@ -45,12 +45,12 @@
10.4 val guh2theID : Celem.guh -> Celem.theID
10.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.6 (* NONE *)
10.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
10.9 val trtas2str : (term * Rule.rule * (term * term list)) list -> string
10.10 val eq_Thm : Rule.rule * Rule.rule -> bool
10.11 val deriv2str : (term * Rule.rule * (term * term list)) list -> string
10.12 val deriv_of_thm'' : Celem.thm'' -> string
10.13 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.14 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.15
10.16 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
10.17 val deri2str : (Rule.rule * (term * term list)) list -> string
11.1 --- a/src/Tools/isac/Interpret/script.sml Wed Oct 30 16:46:05 2019 +0100
11.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Oct 31 10:41:42 2019 +0100
11.3 @@ -38,10 +38,10 @@
11.4
11.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.6 (*NONE*)
11.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
11.9 val is_spec_pos : Ctree.pos_ -> bool
11.10 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
11.11 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.12 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.13
11.14 end
11.15
12.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Oct 30 16:46:05 2019 +0100
12.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Thu Oct 31 10:41:42 2019 +0100
12.3 @@ -21,5 +21,8 @@
12.4 ML \<open>
12.5 \<close> ML \<open>
12.6 \<close> ML \<open>
12.7 +\<close> ML \<open>
12.8 +\<close> ML \<open>
12.9 +\<close> ML \<open>
12.10 \<close>
12.11 end
13.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Oct 30 16:46:05 2019 +0100
13.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Thu Oct 31 10:41:42 2019 +0100
13.3 @@ -39,12 +39,12 @@
13.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.5 val cappend_parent : CTbasic.ctree -> int list -> Istate.T * Proof.context -> term ->
13.6 Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
13.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
13.9 val update_loc' : CTbasic.ctree -> CTbasic.pos ->
13.10 (Istate.T * Proof.context) option * (Istate.T * Proof.context) option -> CTbasic.ctree
13.11 val append_problem : int list -> Istate.T * Proof.context -> Selem.fmz ->
13.12 Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree
13.13 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.14 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.15 end
13.16 (**)
13.17 structure CTaccess(**): CALC_TREE_ACCESS(**) =
14.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Oct 30 16:46:05 2019 +0100
14.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Thu Oct 31 10:41:42 2019 +0100
14.3 @@ -112,7 +112,7 @@
14.4 val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
14.5 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
14.6
14.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
14.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
14.9 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
14.10 val pr_short : pos -> ppobj -> string
14.11 val g_ctxt : ppobj -> Proof.context
14.12 @@ -126,7 +126,7 @@
14.13 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
14.14 val get_trace : ctree -> int list -> int list -> int list list
14.15 val branch2str : branch -> string
14.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.18
14.19 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
14.20 (* NONE *)
15.1 --- a/src/Tools/isac/MathEngBasic/ctree-navi.sml Wed Oct 30 16:46:05 2019 +0100
15.2 +++ b/src/Tools/isac/MathEngBasic/ctree-navi.sml Thu Oct 31 10:41:42 2019 +0100
15.3 @@ -28,9 +28,9 @@
15.4
15.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.6 (* NONE *)
15.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
15.9 (* NONE *)
15.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
15.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
15.12
15.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
15.14 (* NONE *)
16.1 --- a/src/Tools/isac/MathEngBasic/ctree.sml Wed Oct 30 16:46:05 2019 +0100
16.2 +++ b/src/Tools/isac/MathEngBasic/ctree.sml Thu Oct 31 10:41:42 2019 +0100
16.3 @@ -15,9 +15,9 @@
16.4 open CTnavi
16.5 open CTaccess
16.6 end;
16.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
16.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
16.9 open Ctree;
16.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
16.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
16.12
16.13 (* policy for "open" structures:
16.14 --------------------------------
17.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Wed Oct 30 16:46:05 2019 +0100
17.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Thu Oct 31 10:41:42 2019 +0100
17.3 @@ -5,10 +5,11 @@
17.4 signature INTERPRETER_STATE =
17.5 sig
17.6
17.7 + datatype asap = Aundef | AssOnly | AssGen;
17.8 datatype appy_ = AppUndef_ | Napp_ | Skip_
17.9 type pstate
17.10 val e_scrstate: pstate
17.11 - val scrstate2str: Rule.subst * Celem.loc_ * Rule.rls * term option * term * appy_ * bool -> string
17.12 + val scrstate2str: pstate -> string
17.13
17.14 datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
17.15 val istate2str: T -> string
17.16 @@ -49,6 +50,7 @@
17.17 val upd_subst: Env.T -> (term * term) -> pstate -> pstate
17.18 val upd_subst_true: (term option * term) -> pstate -> pstate
17.19 val upd_subst_false: (term option * term) -> pstate -> pstate
17.20 + val upd_subst_reset: (term option * term) -> pstate -> pstate
17.21
17.22 end
17.23
17.24 @@ -59,6 +61,17 @@
17.25
17.26 open Celem
17.27
17.28 +datatype asap = (* arg. of assy _only_ for distinction w.r.t. Or *)
17.29 + Aundef (* undefined: set only by (topmost) Or *)
17.30 +| AssOnly (* do not execute appl stacs - there could be an associated
17.31 + in parallel Or-branch *)
17.32 +| AssGen; (* no Ass(Weak) found within Or, thus
17.33 + search for _applicable_ stacs, execute and generate pt *)
17.34 +(*this constructions doesnt allow arbitrary nesting of Or !!! *)
17.35 +fun asap2str Aundef = "Aundef"
17.36 + | asap2str AssOnly = "AssOnly"
17.37 + | asap2str AssGen = "AssGen"
17.38 +
17.39 datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
17.40 (*Appy is only (final) returnvalue, not argument during search *)
17.41 AppUndef_
17.42 @@ -71,30 +84,32 @@
17.43 | appy_2str Skip_ = "Skip_"
17.44
17.45 type pstate = (* state for script interpreter *)
17.46 - Env.T(*stack*) (* used to instantiate tac for checking associate
17.47 - 12.03.noticed: e_ not updated during execution ?!? *)
17.48 - * Celem.loc_ (* location of tac in script *)
17.49 - * Rule.rls (* for evaluating Prog_Expr *)
17.50 - * term option (*id FORMal ARGument of curried functions *)
17.51 - * term (*vl ACTual ARGument (value) for execution of Tactic.T
17.52 - updated also after a derivation by 'new_val' *)
17.53 - * appy_ (* estimation of how result will be obtained *)
17.54 - * bool; (* true = strongly .., false = weakly associated:
17.55 - only used during ass_dn/up *)
17.56 + Env.T(*stack*) (* used to instantiate tac for checking associate
17.57 + 12.03.noticed: e_ not updated during execution ?!? *)
17.58 + * Celem.loc_ (* location of tac in script *)
17.59 + * Rule.rls (* for evaluating Prog_Expr *)
17.60 + * term option (*id FORMal ARGument of curried functions *)
17.61 + * term (*vl ACTual ARGument (value) for execution of Tactic.T
17.62 + updated also after a derivation by 'new_val' *)
17.63 + * asap (* flag for scanning Or *)
17.64 + * appy_ (* estimation of how result will be obtained *)
17.65 + * bool; (* true = strongly .., false = weakly associated:
17.66 + only used during ass_dn/up *)
17.67 val e_scrstate =
17.68 - ([]: Env.T, []:Celem.loc_, Rule.e_rls, NONE, Rule.e_term, AppUndef_, false) : pstate
17.69 + ([]: Env.T, []:Celem.loc_, Rule.e_rls, NONE, Rule.e_term, Aundef, AppUndef_, false) : pstate
17.70 fun topt2str NONE = "NONE"
17.71 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
17.72 -fun scrstate2str (env, loc_, rls, topt, t, safe, bool) = (* for tests only *)
17.73 +fun scrstate2str (env, loc_, rls, topt, t, asap, safe, bool) = (* for tests only *)
17.74 "(" ^ Env.env2str env ^ ", " ^ Celem.loc_2str loc_ ^ ", " ^ Rule.id_rls rls ^ ", " ^
17.75 - topt2str topt ^ ", \n" ^ Rule.term2str t ^ ", " ^ appy_2str safe ^ ", " ^ bool2str bool ^ ")";
17.76 + topt2str topt ^ ", \n" ^ Rule.term2str t ^ ", " ^ asap2str asap ^ ", " ^ appy_2str safe ^ ", " ^
17.77 + bool2str bool ^ ")";
17.78
17.79 (* for handling type T see fun from_pblobj_or_detail', +? *)
17.80 datatype T = (*interpreter state*)
17.81 Uistate (*undefined in modspec, in '_deriv'ation*)
17.82 | Pstate of pstate (*for script interpreter*)
17.83 | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
17.84 -val e_istate = (Pstate ([], [], Rule.e_rls, NONE, Rule.e_term, AppUndef_, false));
17.85 +val e_istate = Pstate e_scrstate;
17.86
17.87 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
17.88 fun istate2str Uistate = "Uistate"
17.89 @@ -109,65 +124,67 @@
17.90 | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
17.91 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
17.92
17.93 -fun get_path (_, path, _, _,_, _, _) = path
17.94 -fun get_path_up (ist as (_, path, _, _, _, _, _)) =
17.95 +fun get_path (_, path, _, _, _, _, _, _) = path
17.96 +fun get_path_up (ist as (_, path, _, _, _, _, _, _)) =
17.97 if length path > 1 then drop_last path else raise ERROR ("get_path_up [] with " ^ scrstate2str ist)
17.98 -fun get_act (_, _, _, _, act_arg, _, _) = act_arg
17.99 -fun get_rls (_, _, rls, _, _, _, _) = rls
17.100 -fun get_env (env, _, _, _, _, _, _) = env
17.101 -fun get_act_env (env, _, _, _, act_arg, _, _) = (act_arg, env)
17.102 -fun get_assoc (_, _, _, _, _, _, ass) = ass
17.103 -fun get_subst (env, _, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
17.104 +fun get_act (_, _, _, _, act_arg, _, _, _) = act_arg
17.105 +fun get_rls (_, _, rls, _, _, _, _, _) = rls
17.106 +fun get_env (env, _, _, _, _, _, _, _) = env
17.107 +fun get_act_env (env, _, _, _, act_arg, _, _, _) = (act_arg, env)
17.108 +fun get_assoc (_, _, _, _, _, _, _, ass) = ass
17.109 +fun get_subst (env, _, _, form_arg, act_arg, _, _, _) = (env, (form_arg, act_arg))
17.110
17.111 -fun trans_scan_down2 (env, _, rls, _, act_arg, _, _) =
17.112 - (env, [R], rls, NONE, act_arg, AppUndef_, false)
17.113 -fun trans_scan_up2 (env, path, rls, form_arg, act_arg, _, _) =
17.114 - (env, path, rls, form_arg, act_arg, AppUndef_, false)
17.115 -fun trans_ass (_, _, _, _,_, _, ass) (env, path, rls, form_arg, act_arg, safe, _) =
17.116 - (env, path, rls, form_arg, act_arg, safe, ass)
17.117 -fun trans_env_act (env, _, _, _, act_arg, _, _) (_, path, rls, form_arg, _, safe, ass) =
17.118 - (env, path, rls, form_arg, act_arg, safe, ass)
17.119 +fun trans_scan_down2 (env, _, rls, _, act_arg, asap, _, _) =
17.120 + (env, [R], rls, NONE, act_arg, asap, AppUndef_, false)
17.121 +fun trans_scan_up2 (env, path, rls, form_arg, act_arg, asap, _, _) =
17.122 + (env, path, rls, form_arg, act_arg, asap, AppUndef_, false)
17.123 +fun trans_ass (_, _, _, _, _, _, _, ass) (env, path, rls, form_arg, act_arg, asap, safe, _) =
17.124 + (env, path, rls, form_arg, act_arg, asap, safe, ass)
17.125 +fun trans_env_act (env, _, _, _, act_arg, _, _, _) (_, path, rls, form_arg, _, asap, safe, ass) =
17.126 + (env, path, rls, form_arg, act_arg, asap, safe, ass)
17.127
17.128 -fun path_down path (env, p, rls, form_arg, act_arg, safe, ass) =
17.129 - (env, p @ path, rls, form_arg, act_arg, safe, ass)
17.130 -fun path_down_form (path, form_arg) (env, p, rls, _, act_arg, safe, ass) =
17.131 - (env, p @ path, rls, SOME form_arg, act_arg, safe, ass)
17.132 -fun path_up (env, path, rls, form_arg, act_arg, safe, ass) =
17.133 - (env, drop_last path, rls, form_arg, act_arg, safe, ass)
17.134 -fun path_up_down path (env, p, rls, form_arg, act_arg, safe, ass) =
17.135 - (env, (drop_last p) @ path, rls, form_arg, act_arg, safe, ass)
17.136 +fun path_down path (env, p, rls, form_arg, act_arg, asap, safe, ass) =
17.137 + (env, p @ path, rls, form_arg, act_arg, asap, safe, ass)
17.138 +fun path_down_form (path, form_arg) (env, p, rls, _, act_arg, asap, safe, ass) =
17.139 + (env, p @ path, rls, SOME form_arg, act_arg, asap, safe, ass)
17.140 +fun path_up (env, path, rls, form_arg, act_arg, asap, safe, ass) =
17.141 + (env, drop_last path, rls, form_arg, act_arg, asap, safe, ass)
17.142 +fun path_up_down path (env, p, rls, form_arg, act_arg, asap, safe, ass) =
17.143 + (env, (drop_last p) @ path, rls, form_arg, act_arg, asap, safe, ass)
17.144
17.145 -fun upd_form form (env, path, rls, _, act_arg, safe, ass) =
17.146 - (env, path, rls, SOME form, act_arg, safe, ass)
17.147 -fun upd_path path (env, _, rls, form_arg, act_arg, safe, ass) =
17.148 - (env, path, rls, form_arg, act_arg, safe, ass)
17.149 -fun upd_rls rls (env, path, _, form_arg, act_arg, safe, ass) =
17.150 - (env, path, rls, form_arg, act_arg, safe, ass)
17.151 -fun upd_act act (env, path, rls, form_arg, _, safe, ass) =
17.152 - (env, path, rls, form_arg, act, safe, ass)
17.153 -fun upd_appy app (env, path, rls, form_arg, act_arg, _, ass) =
17.154 - (env, path, rls, form_arg, act_arg, app, ass)
17.155 +fun upd_form form (env, path, rls, _, act_arg, asap, safe, ass) =
17.156 + (env, path, rls, SOME form, act_arg, asap, safe, ass)
17.157 +fun upd_path path (env, _, rls, form_arg, act_arg, asap, safe, ass) =
17.158 + (env, path, rls, form_arg, act_arg, asap, safe, ass)
17.159 +fun upd_rls rls (env, path, _, form_arg, act_arg, asap, safe, ass) =
17.160 + (env, path, rls, form_arg, act_arg, asap, safe, ass)
17.161 +fun upd_act act (env, path, rls, form_arg, _, asap, safe, ass) =
17.162 + (env, path, rls, form_arg, act, asap, safe, ass)
17.163 +fun upd_appy app (env, path, rls, form_arg, act_arg, asap, _, ass) =
17.164 + (env, path, rls, form_arg, act_arg, asap, app, ass)
17.165
17.166 -fun upd_env env (_, path, rls, form_arg, act_arg, safe, ass) =
17.167 - (env, path, rls, form_arg, act_arg, safe, ass)
17.168 -fun upd_env_true env (_, path, rls, form_arg, act_arg, safe, _) =
17.169 - (env, path, rls, form_arg, act_arg, safe, true)
17.170 -fun upd_env' form (env, path, rls, form_arg, act_arg, safe, ass) =
17.171 - (Env.upd_env env (form, act_arg), path, rls, form_arg, act_arg, safe, ass)
17.172 -fun upd_env'' (env, (form, act)) (_, path, rls, _, _, safe, ass) =
17.173 - (Env.upd_env env (form, act), path, rls, SOME form, act, safe, ass)
17.174 +fun upd_env env (_, path, rls, form_arg, act_arg, asap, safe, ass) =
17.175 + (env, path, rls, form_arg, act_arg, asap, safe, ass)
17.176 +fun upd_env_true env (_, path, rls, form_arg, act_arg, asap, safe, _) =
17.177 + (env, path, rls, form_arg, act_arg, asap, safe, true)
17.178 +fun upd_env' form (env, path, rls, form_arg, act_arg, asap, safe, ass) =
17.179 + (Env.upd_env env (form, act_arg), path, rls, form_arg, act_arg,asap, safe, ass)
17.180 +fun upd_env'' (env, (form, act)) (_, path, rls, _, _, asap, safe, ass) =
17.181 + (Env.upd_env env (form, act), path, rls, SOME form, act, asap, safe, ass)
17.182
17.183 -fun upd_form_env (form_arg, env) (_, path, rls, _, act_arg, safe, ass) =
17.184 - (env, path, rls, SOME form_arg, act_arg, safe, ass)
17.185 -fun upd_act_env (act_arg, env) (_, path, rls, form_arg, _, safe, ass) =
17.186 - (env, path, rls, form_arg, act_arg, safe, ass)
17.187 +fun upd_form_env (form_arg, env) (_, path, rls, _, act_arg, asap, safe, ass) =
17.188 + (env, path, rls, SOME form_arg, act_arg, asap, safe, ass)
17.189 +fun upd_act_env (act_arg, env) (_, path, rls, form_arg, _, asap, safe, ass) =
17.190 + (env, path, rls, form_arg, act_arg, asap, safe, ass)
17.191
17.192 -fun upd_subst env (form_arg, act_arg) (_, path, rls, _, _, safe, ass) =
17.193 - (env, path, rls, SOME form_arg, act_arg, safe, ass)
17.194 -fun upd_subst_true (form_arg, act_arg) (env, path, rls, _, _, safe, _) =
17.195 - (env, path, rls, form_arg, act_arg, safe, true)
17.196 -fun upd_subst_false (form_arg, act_arg) (env, path, rls, _, _, safe, _) =
17.197 - (env, path, rls, form_arg, act_arg, safe, false)
17.198 +fun upd_subst env (form_arg, act_arg) (_, path, rls, _, _, asap, safe, ass) =
17.199 + (env, path, rls, SOME form_arg, act_arg, asap, safe, ass)
17.200 +fun upd_subst_true (form_arg, act_arg) (env, path, rls, _, _, asap, safe, _) =
17.201 + (env, path, rls, form_arg, act_arg, asap, safe, true)
17.202 +fun upd_subst_false (form_arg, act_arg) (env, path, rls, _, _, asap, safe, _) =
17.203 + (env, path, rls, form_arg, act_arg, asap, safe, false)
17.204 +fun upd_subst_reset (form_arg, act_arg) (env, path, rls, _, _, _, _, _) =
17.205 + (env, path, rls, form_arg, act_arg, Aundef, AppUndef_, false)
17.206
17.207 (**)end(**)
17.208
18.1 --- a/src/Tools/isac/MathEngBasic/model.sml Wed Oct 30 16:46:05 2019 +0100
18.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Thu Oct 31 10:41:42 2019 +0100
18.3 @@ -51,9 +51,9 @@
18.4 val penv2str_ : Proof.context -> penv -> string (* NONE *)
18.5 type preori
18.6 val preoris2str : preori list -> string
18.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
18.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
18.9 (* NONE *)
18.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
18.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
18.12
18.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
18.14 val untouched : itm list -> bool
19.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Wed Oct 30 16:46:05 2019 +0100
19.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Thu Oct 31 10:41:42 2019 +0100
19.3 @@ -20,9 +20,9 @@
19.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
19.5 val pres2str : (bool * term) list -> string
19.6 val refined : match list -> Celem.pblID
19.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
19.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
19.9 (*NONE*)
19.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19.12
19.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
19.14 val pblID_of_match : match -> Celem.pblID
20.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Wed Oct 30 16:46:05 2019 +0100
20.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Thu Oct 31 10:41:42 2019 +0100
20.3 @@ -33,9 +33,9 @@
20.4 val e_sube : Rule.cterm' list
20.5 val e_subs : string list
20.6 val subte2subst : term list -> (term * term) list
20.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
20.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
20.9 (* NONE *)
20.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20.12
20.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
20.14 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
21.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Oct 30 16:46:05 2019 +0100
21.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Oct 31 10:41:42 2019 +0100
21.3 @@ -112,9 +112,9 @@
21.4 val rule2tac : theory -> (term * term) list -> Rule.rule -> input (* for rewtools.sml *)
21.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
21.6 (* NONE *)
21.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
21.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
21.9 (* NONE *)
21.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21.12
21.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
21.14 (* NONE *)
22.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Oct 30 16:46:05 2019 +0100
22.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Oct 31 10:41:42 2019 +0100
22.3 @@ -28,14 +28,14 @@
22.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22.5 val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Telem.safe * Ctree.ctree
22.6 val f2str : Generate.mout -> Rule.cterm'
22.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
22.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
22.9 type nxt_
22.10 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
22.11 val loc_solve_ : string * Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_
22.12 val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
22.13 val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
22.14 val TESTg_form : Ctree.state -> Generate.mout
22.15 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22.16 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22.17
22.18 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
22.19 (* NONE *)
23.1 --- a/src/Tools/isac/MathEngine/solve.sml Wed Oct 30 16:46:05 2019 +0100
23.2 +++ b/src/Tools/isac/MathEngine/solve.sml Thu Oct 31 10:41:42 2019 +0100
23.3 @@ -23,9 +23,9 @@
23.4 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
23.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
23.6 val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout
23.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
23.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
23.9 (*NONE*)
23.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
23.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
23.12
23.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
23.14 (* NONE *)
24.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Oct 30 16:46:05 2019 +0100
24.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Oct 31 10:41:42 2019 +0100
24.3 @@ -36,7 +36,7 @@
24.4 val prep_rls: theory -> Rule.rls -> Rule.rls (*ren insert*)
24.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24.6 (* NONE *)
24.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
24.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
24.9 val subst_typ: string -> typ -> term list -> (typ * typ) list
24.10 val is_calc: term -> bool
24.11 val rule2stac: theory -> Rule.rule -> term
24.12 @@ -44,7 +44,7 @@
24.13 val #> : term list -> term
24.14 val rules2scr_Rls : theory -> Rule.rule list -> term
24.15 val rules2scr_Seq : theory -> Rule.rule list -> term
24.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24.18 end
24.19 (**)
24.20 structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =
25.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 30 16:46:05 2019 +0100
25.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Oct 31 10:41:42 2019 +0100
25.3 @@ -63,9 +63,9 @@
25.4 val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Celem.stacexpr
25.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25.6 (*NONE*)
25.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
25.9 (*NONE*)
25.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25.12 end
25.13 \<close> ML \<open>
25.14 (**)
26.1 --- a/src/Tools/isac/ProgLang/Program.thy Wed Oct 30 16:46:05 2019 +0100
26.2 +++ b/src/Tools/isac/ProgLang/Program.thy Thu Oct 31 10:41:42 2019 +0100
26.3 @@ -40,9 +40,9 @@
26.4 val body_of : term -> term (*ren body*)
26.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26.6 (* NONE *)
26.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
26.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
26.9 (* NONE *)
26.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
26.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
26.12 end
26.13 \<close> ML \<open>
26.14 \<close> ML \<open>
27.1 --- a/src/Tools/isac/ProgLang/calculate.sml Wed Oct 30 16:46:05 2019 +0100
27.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Thu Oct 31 10:41:42 2019 +0100
27.3 @@ -22,12 +22,12 @@
27.4 val float_op_var: term -> string -> typ -> typ -> float -> term
27.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
27.6 (* NONE *)
27.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
27.9 val get_pair: theory -> string -> Rule.eval_fn -> term -> (string * term) option
27.10 val mk_rule: term list * term * term -> term
27.11 val divisors: int -> int list
27.12 val doubles: int list -> int list
27.13 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27.14 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27.15 end
27.16
27.17 (**)
28.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Wed Oct 30 16:46:05 2019 +0100
28.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 31 10:41:42 2019 +0100
28.3 @@ -23,7 +23,7 @@
28.4 -> term -> (term * term list) option
28.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
28.6 (* NONE *)
28.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
28.9 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
28.10 Rule.rls -> bool -> thm -> term -> (term * term list) option
28.11 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
28.12 @@ -31,7 +31,7 @@
28.13 val app_sub: theory -> int -> Rule.rls -> term -> term * term list * bool
28.14 val mk_thm: theory -> string -> thm
28.15 val trace1: int -> string -> unit
28.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28.18 end
28.19
28.20 (**)
29.1 --- a/src/Tools/isac/Specify/Input_Descript.thy Wed Oct 30 16:46:05 2019 +0100
29.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy Thu Oct 31 10:41:42 2019 +0100
29.3 @@ -71,9 +71,9 @@
29.4 val pbl_ids: Proof.context -> term -> term -> term list
29.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
29.6 (* NONE *)
29.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
29.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
29.9 (* NONE *)
29.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29.12 end
29.13 \<close> ML \<open>
29.14 (**)
30.1 --- a/src/Tools/isac/Specify/appl.sml Wed Oct 30 16:46:05 2019 +0100
30.2 +++ b/src/Tools/isac/Specify/appl.sml Thu Oct 31 10:41:42 2019 +0100
30.3 @@ -10,9 +10,9 @@
30.4 val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> Chead.appl
30.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
30.6 val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T
30.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
30.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
30.9 val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
30.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30.12 end
30.13
30.14 (**)
31.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Oct 30 16:46:05 2019 +0100
31.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu Oct 31 10:41:42 2019 +0100
31.3 @@ -106,7 +106,7 @@
31.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
31.5 val e_calcstate : Ctree.state * Generate.taci list
31.6 val e_calcstate' : calcstate'
31.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
31.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
31.9 val posterms2str : (pos' * term * 'a) list -> string
31.10 val postermtacs2str : (pos' * term * Tactic.input option) list -> string
31.11 val vals_of_oris : Model.ori list -> term list
31.12 @@ -124,7 +124,7 @@
31.13 Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
31.14 val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
31.15 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
31.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31.18
31.19 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
31.20 val variants_in : term list -> int
32.1 --- a/src/Tools/isac/Specify/generate.sml Wed Oct 30 16:46:05 2019 +0100
32.2 +++ b/src/Tools/isac/Specify/generate.sml Thu Oct 31 10:41:42 2019 +0100
32.3 @@ -31,9 +31,9 @@
32.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
32.5 val tacis2str : taci list -> string
32.6 val mout2str : mout -> string
32.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
32.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
32.9 (* NONE *)
32.10 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32.11 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32.12
32.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
32.14 (* NONE *)
33.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed Oct 30 16:46:05 2019 +0100
33.2 +++ b/src/Tools/isac/Specify/ptyps.sml Thu Oct 31 10:41:42 2019 +0100
33.3 @@ -55,7 +55,7 @@
33.4 val e_errpat : Rule.errpat
33.5 val show_pblguhs : unit -> unit
33.6 val sort_pblguhs : unit -> unit
33.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
33.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
33.9 val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b
33.10 val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
33.11 val coll_variants: ('a * ''b) list -> ('a list * ''b) list
33.12 @@ -63,7 +63,7 @@
33.13 val max: int list -> int
33.14 val replace_0: int -> int list -> int list
33.15 val split_did: term -> term * term
33.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
33.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
33.18
33.19 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
33.20 val e_fillpat : string * term * string
34.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Oct 30 16:46:05 2019 +0100
34.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Oct 31 10:41:42 2019 +0100
34.3 @@ -161,7 +161,7 @@
34.4 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
34.5 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
34.6 andalso istate2str (get_istate pt p)
34.7 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, AppUndef_, true)"
34.8 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, Aundef, AppUndef_, true)"
34.9 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
34.10 (*-------------------------------------------------------------------------*)
34.11
34.12 @@ -181,11 +181,11 @@
34.13 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)
34.14 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);
34.15 if istate2str istate
34.16 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
34.17 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
34.18 then () else error "from locatetac return --- changed 1";
34.19
34.20 if istate2str (get_istate (fst cstate) (snd cstate))
34.21 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
34.22 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
34.23 then () else error "from locatetac return --- changed 2";
34.24 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
34.25
34.26 @@ -207,7 +207,7 @@
34.27 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
34.28 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
34.29 (*+*)if istate2str istate
34.30 -(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
34.31 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
34.32 then case m of Rewrite_Set_Inst' _ => ()
34.33 else error "from locate_input_tactic return --- changed";
34.34
34.35 @@ -232,7 +232,7 @@
34.36 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
34.37 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
34.38 (*+*)if pos' = ([1], Res) andalso istate2str istate
34.39 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
34.40 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
34.41 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
34.42
34.43 val pIopt = get_pblID (pt,ip);
34.44 @@ -242,9 +242,9 @@
34.45 (*val (pt',c',p') =*) Generate.generate tacis (pt,[],p);
34.46 (*//------------------------------------- final test -----------------------------------------\\*)
34.47 val ("ok", [], ptp as (pt, p)) = xxxx;
34.48 -
34.49 +
34.50 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
34.51 -(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
34.52 +(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
34.53 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
34.54
34.55 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
35.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 16:46:05 2019 +0100
35.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Oct 31 10:41:42 2019 +0100
35.3 @@ -54,17 +54,17 @@
35.4 val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
35.5 val d = e_rls (*FIXME: get simplifier from domID*);
35.6 "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
35.7 - (scr as Prog (h $ body),d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt)) =
35.8 + (scr as Prog (h $ body),d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) =
35.9 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
35.10 val thy = assoc_thy thy';
35.11 l = [] orelse ((*init.in solve..Apply_Method...*)
35.12 (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
35.13 -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,S,b),ss),
35.14 +"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,asap,S,b),ss),
35.15 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
35.16 - ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
35.17 + ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]), body);
35.18 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
35.19 -"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
35.20 - (ya, ((E , l@[L,R], rls,a,v,S,b),ss), e);
35.21 +"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,asap,S,b), (m,_,pt,(p,p_),c)::ss), t) =
35.22 + (ya, ((E , l@[L,R], rls,a,v,asap,S,b),ss), e);
35.23 val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t;
35.24 (* val ctxt = get_ctxt pt (p,p_)
35.25 exception PTREE "get_obj: pos = [0] does not exist" raised
35.26 @@ -115,37 +115,37 @@
35.27
35.28 (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
35.29 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
35.30 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
35.31 +"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
35.32 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
35.33 (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
35.34
35.35 (** )val xxxxx_xx = ( **)
35.36 - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,S,b), m) (Program.body_of sc);
35.37 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
35.38 - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,S,b), m), (Program.body_of sc));
35.39 + assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,asap,S,b), m) (Program.body_of sc);
35.40 +"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,asap,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
35.41 + = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,asap,S,b), m), (Program.body_of sc));
35.42
35.43 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), tac) e (*of*);
35.44 -"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a))
35.45 - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), tac), e);
35.46 + (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac) e (*of*);
35.47 +"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a))
35.48 + = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac), e);
35.49
35.50 - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,S,b),ss) e1 (*of*);
35.51 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e))
35.52 - = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,S,b),ss), e1);
35.53 + (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss) e1 (*of*);
35.54 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e))
35.55 + = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss), e1);
35.56
35.57 - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e (*of*);
35.58 + (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*);
35.59 (*======= end of scanning tacticals, a leaf =======*)
35.60 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,S,_), m), t)
35.61 - = (ya, ((E, l @ [Celem.R], rls,a,v,S,b),ss), e);
35.62 +"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
35.63 + = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e);
35.64 val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
35.65 val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
35.66 (* 1st ContextC.insert_assumptions asms' ctxt *)
35.67
35.68 -(*NEW*) Assoc ((E,l,rls,a',v',S,true), ctxt, m) (*return value*);
35.69 +(*NEW*) Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m) (*return value*);
35.70 "~~~~~ from assy to execute_progr_2 return val:"; val (xxxxx_xx)
35.71 - = (Assoc ((E,l,rls,a',v',S,true), ctxt, m)); (*return value*)
35.72 + = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); (*return value*)
35.73
35.74 -"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac')
35.75 - = (Assoc ((E,l,rls,a',v',S,true), ctxt, m));
35.76 +"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac')
35.77 + = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m));
35.78 (*if*) strong_ass; (*then*)
35.79
35.80 "~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (istate, ctxt, tac)
35.81 @@ -159,7 +159,7 @@
35.82 (*NEW*) val (p'', _, _,pt') =
35.83 (*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m
35.84 (*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
35.85 -(*NEW*) (Istate.Pstate (E,l,rls,a',v',S,true), ctxt) (p', p_) pt;
35.86 +(*NEW*) (Istate.Pstate (E,l,rls,a',v',asap,S,true), ctxt) (p', p_) pt;
35.87 (*NEW*) (*in*)
35.88 (*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
35.89 (*NEW*) [(*ctree NOT cut*)], (pt', p'')));
35.90 @@ -277,58 +277,58 @@
35.91 val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
35.92
35.93 (*case*) execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*);
35.94 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
35.95 +"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
35.96 = (srls, tac, cstate ,(progr, Rule.e_rls), (istate, ctxt));
35.97 (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
35.98
35.99 - astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,S,b), m);
35.100 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss))
35.101 - = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,S,b), m));
35.102 + astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,asap,S,b), m);
35.103 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,asap,S,b),ss))
35.104 + = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,asap,S,b), m));
35.105 (*if*) 1 < length l (*then*);
35.106 val up = drop_last l; (* = [R, L, R, L, R]*)
35.107
35.108 - ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
35.109 + ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
35.110 "~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Try"(*2*),_) $ _))
35.111 - = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
35.112 + = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
35.113
35.114 astep_up ysa iss;
35.115 -"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)))
35.116 +"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)))
35.117 = (ysa, iss);
35.118 (*if*) 1 < length l (*then*);
35.119 val up = drop_last l; (* = [R, L, R, L]*)
35.120
35.121 - ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
35.122 -"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,S,b),ss),
35.123 + ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
35.124 +"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss),
35.125 (Const ("Tactical.Seq"(*3*),_) $ _ ))
35.126 - = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
35.127 + = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
35.128 val up = drop_last l;
35.129 val Const ("Tactical.Seq",_) $ _ $ e2 = (*case*) go up sc (*of*);
35.130
35.131 - (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,S,b),ss) e2 (*of*);
35.132 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2))
35.133 - = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,S,b),ss), e2);
35.134 - val NasApp ((E,_,_,_,v,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,S,b),ss) e1 (*of*);
35.135 + (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss) e2 (*of*);
35.136 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2))
35.137 + = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss), e2);
35.138 + val NasApp ((E,_,_,_,v,_,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,asap,S,b),ss) e1 (*of*);
35.139
35.140 - assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e2;
35.141 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e))
35.142 - = (ya, ((E, l @ [Celem.R], rls,a,v,S,b),ss), e2);
35.143 + assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e2;
35.144 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e))
35.145 + = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e2);
35.146
35.147 - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e (*of*);
35.148 + (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*);
35.149 (*======= end of scanning tacticals, a leaf =======*)
35.150 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,S,_), m), t)
35.151 - = (ya, ((E, l @ [Celem.R], rls,a,v,S,b),ss), e);
35.152 +"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
35.153 + = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e);
35.154 val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
35.155 val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
35.156 val Aundef = (*case*) ap (*of*);
35.157 val Appl m' = (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
35.158 - val is = (E,l,rls,a',Lucin.tac_2res m',S,false(*FIXXXME.WN0?*));
35.159 + val is = (E,l,rls,a',Lucin.tac_2res m',asap,S,false(*FIXXXME.WN0?*));
35.160 NasApp (is, ctxt, m) (* return value *);
35.161
35.162 val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
35.163 t, (res, asm)) = m;
35.164 if scrstate2str is =
35.165 "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], e_rls, SOMEt_t, \n" ^
35.166 - "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, AppUndef_, false)"
35.167 + "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)"
35.168 andalso
35.169 term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
35.170 andalso
35.171 @@ -337,6 +337,7 @@
35.172 terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
35.173 then () else error "locate_input_tactic Helpless, but applicable CHANGED";
35.174
35.175 +
35.176 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
35.177 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
35.178 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
36.1 --- a/test/Tools/isac/Interpret/script.sml Wed Oct 30 16:46:05 2019 +0100
36.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Oct 31 10:41:42 2019 +0100
36.3 @@ -416,7 +416,7 @@
36.4 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, assoc_thy thy, meth, metID);
36.5 val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
36.6 if scrstate2str st =
36.7 - "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, AppUndef_, true)"
36.8 + "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, Aundef, AppUndef_, true)"
36.9 then () else error "init_pstate changed for Biegelinie";
36.10
36.11 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
37.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Oct 30 16:46:05 2019 +0100
37.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Oct 31 10:41:42 2019 +0100
37.3 @@ -487,9 +487,10 @@
37.4 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
37.5 val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
37.6 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
37.7 +
37.8 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
37.9 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
37.10 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
37.11 -(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
37.12 l = [] = false;
37.13 nstep_up thy ptp sc ist Skip_ (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
37.14 BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
38.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Oct 30 16:46:05 2019 +0100
38.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Oct 31 10:41:42 2019 +0100
38.3 @@ -58,7 +58,7 @@
38.4 val {srls, pre, prls, ...} = get_met mI;
38.5 val pres = check_preconds thy prls pre meth |> map snd;
38.6 val ctxt = ctxt |> insert_assumptions pres;
38.7 -val (is'''' as Pstate (env'''',_,_,_,_,_,_), _, sc'''') = init_pstate srls ctxt meth mI;
38.8 +val (is'''' as Pstate (env'''',_,_,_,_,_,_,_), _, sc'''') = init_pstate srls ctxt meth mI;
38.9 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI)
38.10 val actuals = itms2args thy metID itms
38.11 val scr as Prog sc = (#scr o get_met) metID
38.12 @@ -131,7 +131,7 @@
38.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
38.14 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
38.15 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
38.16 - (Istate.Pstate (E,l,rls,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
38.17 + (Istate.Pstate (E,l,rls,a,v,asap,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
38.18 l = [] (* = true*);
38.19 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
38.20 (thy, ptp, E, [Celem.R], body, NONE, v);
39.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Oct 30 16:46:05 2019 +0100
39.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Oct 31 10:41:42 2019 +0100
39.3 @@ -53,28 +53,28 @@
39.4 val srls = get_simplifier cstate;
39.5
39.6 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
39.7 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
39.8 +"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
39.9 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
39.10 (*if*)l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
39.11
39.12 (*val Assoc (pstate, steps) = in isabisacREP*)
39.13 (*ERROR assy: call by ([3], Pbl) in isabisac*)
39.14 - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,S,b), m) (Program.body_of sc);
39.15 + assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,asap,S,b), m) (Program.body_of sc);
39.16
39.17 (* checked all arguments of assy for equality: isabisac -- isabisacREP *)
39.18 -"~~~~~ fun assy [1], args:"; val (ya, ((E,l,rls,a,v,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
39.19 - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],rls,a,v,S,b), m), (Program.body_of sc));
39.20 +"~~~~~ fun assy [1], args:"; val (ya, ((E,l,rls,a,v,asap,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
39.21 + = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],rls,a,v,asap,S,b), m), (Program.body_of sc));
39.22
39.23 -(*val Assoc (pstate, steps) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), tac) e;
39.24 -"~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss),
39.25 +(*val Assoc (pstate, steps) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac) e;
39.26 +"~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,asap,S,b),ss),
39.27 (Const ("Tactical.Seq"(*1*),_) $e1 $ e2 $ a)) =
39.28 - (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac), e);
39.29 + (ya, ((E , l @ [Celem.L, Celem.R], a,v,asap,S,b), tac), e);
39.30
39.31 (*val Assoc (pstate, steps) = in isabisacREP*)
39.32 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
39.33 - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls, SOME a,v,S,b),ss) e1 (*of*);
39.34 -"~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =
39.35 - ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
39.36 + (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls, SOME a,v,asap,S,b),ss) e1 (*of*);
39.37 +"~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =
39.38 + ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,asap,S,b),ss), e1);
39.39
39.40 term2str e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
39.41 term2str e1 = "Try (Rewrite_Set norm_equation)" (*in isabisacREP*);
39.42 @@ -82,10 +82,10 @@
39.43
39.44 (*val Assoc (pstate, steps) = in isabisacREP*)
39.45 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
39.46 -assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e ;
39.47 +assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e ;
39.48 (*======= end of scanning tacticals, a leaf =======*)
39.49 -"~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t) =
39.50 - (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
39.51 +"~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,asap,S,_), m), t) =
39.52 + (ya, ((E, l @ [Celem.R], a,v,asap,S,b),ss), e);
39.53 val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr (E, (a, v)) t (*of*);
39.54
39.55 (*val Ass (m,v') = in isabisacREP*)
39.56 @@ -114,7 +114,7 @@
39.57 (* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
39.58 go: no [L,L,R] *)
39.59 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)),
39.60 - (Pstate (E,l,rls,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
39.61 + (Pstate (E,l,rls,a,v,asap,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
39.62 (*if*) l = [] = false;
39.63
39.64 (* isabisac17: nstep_up thy ptp sc E l Skip_ a v ERROR go: no [L,L,R] *)
39.65 @@ -170,12 +170,12 @@
39.66 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
39.67
39.68 (*val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
39.69 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,rls,a,v,s,_), ctxt))
39.70 +"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,rls,a,v,asap,s,_), ctxt))
39.71 = ((thy', srls), (pt, pos), sc, is);
39.72
39.73 - (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,rls,a,v,s,false)) (*of*);
39.74 + (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,rls,a,v,asap,s,false)) (*of*);
39.75 "~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate (ist as (E, l, rls,a, v, _, _))))
39.76 - = (thy, ptp, sc, (Istate.Pstate (E,l,rls,a,v,s,false)));
39.77 + = (thy, ptp, sc, (Istate.Pstate (E,l,rls,a,v,asap,s,false)));
39.78 (*if*) l = [] (*else*);
39.79
39.80 nstep_up thy ptp sc ist Skip_;
40.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Oct 30 16:46:05 2019 +0100
40.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Oct 31 10:41:42 2019 +0100
40.3 @@ -43,44 +43,44 @@
40.4 val srls = get_simplifier cstate;
40.5
40.6 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
40.7 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
40.8 +"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
40.9 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
40.10 (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)
40.11 (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
40.12 (*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
40.13 - (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
40.14 -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss))
40.15 - = ((ctxt,srls,scr, (pt, p)), ((E,l,a,v,S,b), m));
40.16 + (astep_up (thy',srls,scr,d) ((E,l,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]) );*)
40.17 +"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,asap,S,b),ss))
40.18 + = ((ctxt,srls,scr, (pt, p)), ((E,l,a,v,asap,S,b), m));
40.19 (*if*) 1 < length l (*true*);
40.20 val up = drop_last l;
40.21
40.22 - ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
40.23 + ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
40.24 "~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Tactical.Try",_) $ e)) =
40.25 - (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
40.26 + (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
40.27 astep_up ysa iss;
40.28 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)) = (ysa, iss);
40.29 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
40.30 (*if*) 1 < length l; (*then*)
40.31 val up = drop_last l;
40.32
40.33 - ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
40.34 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
40.35 + ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
40.36 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
40.37
40.38 astep_up ysa iss (*2*: comes from e2*);
40.39 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)) = (ysa, iss);
40.40 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
40.41 (*if*) 1 < length l; (*then*)
40.42 val up = drop_last l;
40.43
40.44 - ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
40.45 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
40.46 + ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
40.47 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
40.48
40.49 astep_up ysa iss (*all has been done in (*2*) below*);
40.50 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)) = (ysa, iss);
40.51 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
40.52 (*if*) 1 < length l; (*then*)
40.53 val up = drop_last l;
40.54
40.55 - ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
40.56 -"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,S,b),ss), (Const ("HOL.Let",_) $ _))
40.57 - = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
40.58 + ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
40.59 +"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ _))
40.60 + = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
40.61 val l = drop_last l; (*comes from e, goes to Abs*)
40.62 val (i, T, body) =
40.63 (case go l sc of
40.64 @@ -89,14 +89,14 @@
40.65 val i = TermC.mk_Free (i, T);
40.66 val E = Env.upd_env E (i, v);
40.67
40.68 - (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], rls,a,v,S,b),ss) body (*of*);
40.69 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
40.70 - = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], rls,a,v,S,b),ss), body);
40.71 + (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss) body (*of*);
40.72 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
40.73 + = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss), body);
40.74
40.75 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), ss) e (*of*);
40.76 + (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss) e (*of*);
40.77 (*======= end of scanning tacticals, a leaf =======*)
40.78 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,S,_), m), t)
40.79 - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), ss), e);
40.80 +"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
40.81 + = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss), e);
40.82
40.83 (*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
40.84 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
41.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Oct 30 16:46:05 2019 +0100
41.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Oct 31 10:41:42 2019 +0100
41.3 @@ -55,7 +55,7 @@
41.4 val thy' = get_obj g_domID pt p;
41.5 val thy = assoc_thy thy';
41.6 val srls = Lucin.get_simplifier (pt, pos)
41.7 - val (is as Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI;
41.8 + val (is as Pstate (env,_,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI;
41.9 (*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
41.10
41.11 (*+*)val (pt, p) = case locatetac tac (pt, pos) of
41.12 @@ -74,7 +74,7 @@
41.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
41.14 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
41.15 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
41.16 - (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
41.17 + (Pstate (ist as (E,l,rls,a,v,asap,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
41.18
41.19 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
41.20
42.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Oct 30 16:46:05 2019 +0100
42.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Oct 31 10:41:42 2019 +0100
42.3 @@ -56,7 +56,7 @@
42.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
42.5 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
42.6 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
42.7 -(Pstate (E,l,rls,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
42.8 +(Pstate (E,l,rls,a,v,asap,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
42.9 val ctxt = get_ctxt pt pos
42.10 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
42.11 l; (*= [R, R, D, L, R]*)
43.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Oct 30 16:46:05 2019 +0100
43.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Oct 31 10:41:42 2019 +0100
43.3 @@ -123,7 +123,7 @@
43.4 (* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
43.5 ;
43.6 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
43.7 - (Istate.Pstate (ist as (E,l,rls,a,v,s,_)), ctxt)) = ((thy', srls), (pt, pos), sc, is);
43.8 + (Istate.Pstate (ist as (E,l,rls,a,v,asap,s,_)), ctxt)) = ((thy', srls), (pt, pos), sc, is);
43.9 (*if*) l = [] (* = true *);
43.10
43.11 appy thy ptp ist body;