1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 01 10:24:13 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 01 12:42:39 2020 +0200
1.3 @@ -27,14 +27,14 @@
1.4 val pattern2xml :
1.5 int ->
1.6 (string * (Term.term * Term.term)) list -> Term.term list -> string
1.7 - val pos'2xml : int -> string * (int list * Ctree.pos_) -> string
1.8 - val pos'calchead2xml : int -> Ctree.pos' * Ctree.ocalhd -> Celem.xml
1.9 - val pos_2xml : int -> Ctree.pos_ -> string
1.10 - val posform2xml : int -> Ctree.pos' * Term.term -> Celem.xml
1.11 - val posformhead2xml : int -> Ctree.pos' * Ctree.ptform -> string
1.12 - val posformheads2xml : int -> (Ctree.pos' * Ctree.ptform) list -> Celem.xml
1.13 - val posforms2xml : int -> (Ctree.pos' * Term.term) list -> Celem.xml
1.14 - val posterms2xml : int -> (Ctree.pos' * term) list -> Celem.xml
1.15 + val pos'2xml : int -> string * (int list * Pos.pos_) -> string
1.16 + val pos'calchead2xml : int -> Pos.pos' * Ctree.ocalhd -> Celem.xml
1.17 + val pos_2xml : int -> Pos.pos_ -> string
1.18 + val posform2xml : int -> Pos.pos' * Term.term -> Celem.xml
1.19 + val posformhead2xml : int -> Pos.pos' * Ctree.ptform -> string
1.20 + val posformheads2xml : int -> (Pos.pos' * Ctree.ptform) list -> Celem.xml
1.21 + val posforms2xml : int -> (Pos.pos' * Term.term) list -> Celem.xml
1.22 + val posterms2xml : int -> (Pos.pos' * term) list -> Celem.xml
1.23 val precond2xml : int -> bool * Term.term -> Celem.xml
1.24 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
1.25 val rls2xml : int -> Rule.thyID * Rule.rls -> Celem.xml
1.26 @@ -414,7 +414,7 @@
1.27 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
1.28 xml_of_spec spec])
1.29
1.30 -fun xml_of_posmodspec ((p: Ctree.pos', (b, p_, head, gfr, pre, spec): Ctree.ocalhd)) =
1.31 +fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): Ctree.ocalhd)) =
1.32 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
1.33 xml_of_pos "POSITION" p,
1.34 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
1.35 @@ -569,7 +569,7 @@
1.36 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
1.37 | xml_of_tac (Tactic.Specify_Problem ct) =
1.38 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
1.39 - | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.tac2str tac);
1.40 + | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);
1.41
1.42 fun xml_to_tac
1.43 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Wed Apr 01 10:24:13 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Wed Apr 01 12:42:39 2020 +0200
2.3 @@ -27,7 +27,7 @@
2.4 XML.Elem (("DELCALC", []),
2.5 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])
2.6
2.7 -fun iteratorOK2xml (calcid : Celem.calcID) (p : Ctree.pos')=
2.8 +fun iteratorOK2xml (calcid : Celem.calcID) (p : Pos.pos')=
2.9 XML.Elem (("CALCITERATOR", []),
2.10 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.11 xml_of_pos "POSITION" p])
2.12 @@ -100,14 +100,14 @@
2.13 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.14 XML.Elem (("FORMHEADS", []), map xml_of_posterm fs)])
2.15
2.16 -fun appendformulaOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
2.17 +fun appendformulaOK2xml (calcid : Celem.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
2.18 xml_of_calcchanged calcid "APPENDFORMULA" old del new
2.19 fun appendformulaERROR2xml (calcid : Celem.calcID) e =
2.20 XML.Elem (("APPENDFORMULA", []), [
2.21 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.22 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
2.23
2.24 -fun replaceformulaOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
2.25 +fun replaceformulaOK2xml (calcid : Celem.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
2.26 xml_of_calcchanged calcid "REPLACEFORMULA" old del new
2.27 fun replaceformulaERROR2xml (calcid : Celem.calcID) e =
2.28 XML.Elem (("REPLACEFORMULA", []), [
2.29 @@ -139,14 +139,14 @@
2.30 DELETED: last pos' of the succesional sequence of formulae prob. deleted
2.31 GENERATED: the pos' of the new active formula
2.32 .*)
2.33 -fun autocalculateOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
2.34 +fun autocalculateOK2xml (calcid : Celem.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
2.35 xml_of_calcchanged calcid "AUTOCALC" old del new
2.36 fun autocalculateERROR2xml (calcid : Celem.calcID) e =
2.37 XML.Elem (("AUTOCALC", []), [
2.38 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.39 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
2.40
2.41 -fun interStepsOK (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
2.42 +fun interStepsOK (calcid : Celem.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
2.43 xml_of_calcchanged calcid "INTERSTEPS" old del new
2.44 fun interStepsERROR (calcid : Celem.calcID) e =
2.45 XML.Elem (("INTERSTEPS", []), [
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 01 10:24:13 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 01 12:42:39 2020 +0200
3.3 @@ -13,45 +13,45 @@
3.4 sig
3.5 val appendFormula : Celem.calcID -> Rule.cterm' -> XML.tree (*unit future*)
3.6 val autoCalculate : Celem.calcID -> Solve.auto -> XML.tree (*unit future*)
3.7 - val applyTactic : Celem.calcID -> Ctree.pos' -> Tactic.input -> XML.tree
3.8 + val applyTactic : Celem.calcID -> Pos.pos' -> Tactic.input -> XML.tree
3.9 val CalcTree : Selem.fmz list -> XML.tree
3.10 - val checkContext : Celem.calcID -> Ctree.pos' -> Celem.guh -> XML.tree
3.11 + val checkContext : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
3.12 val DEconstrCalcTree : Celem.calcID -> XML.tree
3.13 - val fetchApplicableTactics : Celem.calcID -> int -> Ctree.pos' -> XML.tree
3.14 + val fetchApplicableTactics : Celem.calcID -> int -> Pos.pos' -> XML.tree
3.15 val fetchProposedTactic : Celem.calcID -> XML.tree
3.16 val findFillpatterns : Celem.calcID -> Rule.errpatID -> XML.tree
3.17 - val getAccumulatedAsms : Celem.calcID -> Ctree.pos' -> XML.tree
3.18 + val getAccumulatedAsms : Celem.calcID -> Pos.pos' -> XML.tree
3.19 val getActiveFormula : Celem.calcID -> XML.tree
3.20 - val getAssumptions : Celem.calcID -> Ctree.pos' -> XML.tree
3.21 - val getFormulaeFromTo : Celem.calcID -> Ctree.pos' -> Ctree.pos' -> int -> bool -> XML.tree
3.22 - val getTactic : Celem.calcID -> Ctree.pos' -> XML.tree
3.23 - val initContext : Celem.calcID -> Celem.ketype -> Ctree.pos' -> XML.tree
3.24 + val getAssumptions : Celem.calcID -> Pos.pos' -> XML.tree
3.25 + val getFormulaeFromTo : Celem.calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
3.26 + val getTactic : Celem.calcID -> Pos.pos' -> XML.tree
3.27 + val initContext : Celem.calcID -> Celem.ketype -> Pos.pos' -> XML.tree
3.28 val inputFillFormula: Celem.calcID -> string -> XML.tree
3.29 - val interSteps : Celem.calcID -> Ctree.pos' -> XML.tree
3.30 + val interSteps : Celem.calcID -> Pos.pos' -> XML.tree
3.31 val Iterator : Celem.calcID -> XML.tree
3.32 val IteratorTEST : Celem.calcID -> Celem.iterID
3.33 val modelProblem : Celem.calcID -> XML.tree
3.34 val modifyCalcHead : Celem.calcID -> In_Chead.icalhd -> XML.tree
3.35 val moveActiveCalcHead : Celem.calcID -> XML.tree
3.36 val moveActiveDown : Celem.calcID -> XML.tree
3.37 - val moveActiveFormula : Celem.calcID -> Ctree.pos' -> XML.tree
3.38 + val moveActiveFormula : Celem.calcID -> Pos.pos' -> XML.tree
3.39 val moveActiveLevelDown : Celem.calcID -> XML.tree
3.40 val moveActiveLevelUp : Celem.calcID -> XML.tree
3.41 val moveActiveRoot : Celem.calcID -> XML.tree
3.42 val moveActiveRootTEST : Celem.calcID -> XML.tree
3.43 val moveActiveUp : Celem.calcID -> XML.tree
3.44 - val moveCalcHead : Celem.calcID -> Ctree.pos' -> XML.tree
3.45 - val moveDown : Celem.calcID -> Ctree.pos' -> XML.tree
3.46 - val moveLevelDown : Celem.calcID -> Ctree.pos' -> XML.tree
3.47 - val moveLevelUp : Celem.calcID -> Ctree.pos' -> XML.tree
3.48 + val moveCalcHead : Celem.calcID -> Pos.pos' -> XML.tree
3.49 + val moveDown : Celem.calcID -> Pos.pos' -> XML.tree
3.50 + val moveLevelDown : Celem.calcID -> Pos.pos' -> XML.tree
3.51 + val moveLevelUp : Celem.calcID -> Pos.pos' -> XML.tree
3.52 val moveRoot : Celem.calcID -> XML.tree
3.53 - val moveUp : Celem.calcID -> Ctree.pos' -> XML.tree
3.54 - val refFormula : Celem.calcID -> Ctree.pos' -> XML.tree
3.55 - val refineProblem : Celem.calcID -> Ctree.pos' -> Celem.guh -> XML.tree
3.56 + val moveUp : Celem.calcID -> Pos.pos' -> XML.tree
3.57 + val refFormula : Celem.calcID -> Pos.pos' -> XML.tree
3.58 + val refineProblem : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
3.59 val replaceFormula : Celem.calcID -> Rule.cterm' -> XML.tree
3.60 val requestFillformula : Celem.calcID -> Rule.errpatID * Celem.fillpatID -> XML.tree
3.61 val resetCalcHead : Celem.calcID -> XML.tree
3.62 - val setContext : Celem.calcID -> Ctree.pos' -> Celem.guh -> XML.tree
3.63 + val setContext : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
3.64 val setMethod : Celem.calcID -> Celem.metID -> XML.tree
3.65 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
3.66 val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
3.67 @@ -345,7 +345,7 @@
3.68 | ("failure", _) => sysERROR2xml cI "failure"
3.69 | ("not-applicable", _) => (*the rule comes from anywhere..*)
3.70 (case Applicable.applicable_in ip pt tac of
3.71 - Applicable.Notappl e => message2xml cI ("'" ^ Tactic.tac2str tac ^ "' not-applicable")
3.72 + Applicable.Notappl e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")
3.73 | Applicable.Appl m =>
3.74 let
3.75 val ctxt = get_ctxt pt pold
3.76 @@ -584,7 +584,7 @@
3.77 in
3.78 if Tactic.is_rewtac tac
3.79 then contextthyOK2xml cI (Rtools.context_thy (pt, pos) tac)
3.80 - else message2xml cI ("no thy-context at tac '" ^ Tactic.tac2str tac ^ "'")
3.81 + else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
3.82 end
3.83 else if is_curr_endof_calc pt pos
3.84 then
3.85 @@ -594,7 +594,7 @@
3.86 in
3.87 if Tactic.is_rewtac tac
3.88 then contextthyOK2xml cI (Rtools.context_thy ptp tac)
3.89 - else message2xml cI ("no thy-context at tac '" ^ Tactic.tac2str tac ^ "'")
3.90 + else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
3.91 end
3.92 | (msg, _) => message2xml cI msg
3.93 else message2xml cI "no thy-context at this position"
4.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 01 10:24:13 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 01 12:42:39 2020 +0200
4.3 @@ -181,7 +181,7 @@
4.4
4.5
4.6 (**. write pbls from hierarchy to files.**)
4.7 -fun pbl2file (path: Celem.filepath) (pos: Ctree.pos) (id:Celem.metID) (pbl as {guh,...}) =
4.8 +fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Celem.metID) (pbl as {guh,...}) =
4.9 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos);
4.10 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
4.11 );
4.12 @@ -254,12 +254,12 @@
4.13 *)
4.14
4.15 (*.write the files using an int-key (pos') as filename.*)
4.16 -fun met2file (path: Celem.filepath) (pos: Ctree.pos) (id: Celem.metID) met =
4.17 +fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Celem.metID) met =
4.18 (writeln ("### met2file: id = " ^ strs2str id);
4.19 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
4.20
4.21 (*.write the files using the guh as filename.*)
4.22 -fun met2file (path: Celem.filepath) (pos: Ctree.pos) (id: Celem.metID) (met as {guh,...}) =
4.23 +fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Celem.metID) (met as {guh,...}) =
4.24 (writeln ("### met2file: id = " ^ strs2str id);
4.25 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
4.26
5.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 01 10:24:13 2020 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 01 12:42:39 2020 +0200
5.3 @@ -175,7 +175,7 @@
5.4 error ("thydata2xml: not implemented for "^ strs2str' theID);
5.5
5.6 (* analoguous to 'fun met2file' *)
5.7 -fun thydata2file (path : Celem.filepath) (pos : Ctree.pos) (theID : Celem.theID) thydata =
5.8 +fun thydata2file (path : Celem.filepath) (pos : Pos.pos) (theID : Celem.theID) thydata =
5.9 (writeln ("### thes2file: id = " ^ strs2str theID);
5.10 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
5.11
6.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 10:24:13 2020 +0200
6.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 12:42:39 2020 +0200
6.3 @@ -202,8 +202,10 @@
6.4
6.5 fun check_kestore_calc ((id, (c, _)) : Rule.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
6.6
6.7 +(* we avoid term_to_string''' defined later *)
6.8 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
6.9 - "(" ^ (Rule.term_to_string''' @{theory} t) ^ ", " ^ (Celem.spec2str s) ^ ")";
6.10 + "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
6.11 + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
6.12
6.13 fun count_kestore_ptyps [] = 0
6.14 | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =
7.1 --- a/src/Tools/isac/CalcElements/contextC.sml Wed Apr 01 10:24:13 2020 +0200
7.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Wed Apr 01 12:42:39 2020 +0200
7.3 @@ -5,8 +5,8 @@
7.4 (* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
7.5 signature CONTEXT_C =
7.6 sig
7.7 - val e_ctxt : Proof.context
7.8 - val is_e_ctxt : Proof.context -> bool
7.9 + val empty : Proof.context
7.10 + val is_empty : Proof.context -> bool
7.11 val isac_ctxt : 'a -> Proof.context
7.12 val declare_constraints: term -> Proof.context -> Proof.context
7.13 val initialise : string -> term list -> Proof.context
7.14 @@ -28,9 +28,9 @@
7.15 structure ContextC(**) : CONTEXT_C(**) =
7.16 struct
7.17
7.18 -val e_ctxt = Proof_Context.init_global @{theory "Pure"};
7.19 +val empty = Proof_Context.init_global @{theory "Pure"};
7.20 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
7.21 -fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
7.22 +fun is_empty ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
7.23 fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx)
7.24
7.25 val declare_constraints = Variable.declare_constraints
8.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 10:24:13 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 12:42:39 2020 +0200
8.3 @@ -10,7 +10,7 @@
8.4 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
8.5 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
8.6 Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
8.7 - val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))
8.8 + val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
8.9 val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
8.10 val check_for :
8.11 term * term ->
8.12 @@ -64,11 +64,11 @@
8.13 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
8.14 (Tactic.Rewrite (id, thm),
8.15 Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, rule2thm'' r, t, (t', a)),
8.16 - (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
8.17 + (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
8.18 | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
8.19 (Tactic.Rewrite_Set (rule2rls' r),
8.20 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
8.21 - (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
8.22 + (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
8.23 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)
8.24
8.25 (* fo = ifo excluded already in inform *)
8.26 @@ -155,7 +155,7 @@
8.27 val some = map (get_fillform subst (thm, form) errpatID) fillpats
8.28 in some |> filter is_some |> map the end
8.29
8.30 -fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =
8.31 +fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =
8.32 let
8.33 val f_curr = Ctree.get_curr_formula (pt, pos);
8.34 val pp = Ctree.par_pblobj pt p
9.1 --- a/src/Tools/isac/Interpret/istate.sml Wed Apr 01 10:24:13 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/istate.sml Wed Apr 01 12:42:39 2020 +0200
9.3 @@ -12,7 +12,7 @@
9.4 val pstate2str: pstate -> string
9.5
9.6 datatype T = datatype Istate_Def.T
9.7 - val e_istate: T
9.8 + val empty: T
9.9 val string_of: T -> string
9.10 val string_of': T -> string
9.11 val istates2str: T option * T option -> string
9.12 @@ -70,7 +70,7 @@
9.13 val pstate2str = Istate_Def.pstate2str
9.14
9.15 datatype T = datatype Istate_Def.T
9.16 -val e_istate = Istate_Def.e_istate
9.17 +val empty = Istate_Def.empty
9.18 fun the_pstate (Pstate pst) = pst
9.19 | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
9.20
10.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 10:24:13 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 12:42:39 2020 +0200
10.3 @@ -18,7 +18,7 @@
10.4 Istate.T * Proof.context * Program.T
10.5
10.6 val get_simplifier : Calc.T -> Rule.rls
10.7 - val resume_prog : Rule.theory' (*..for lookup in KEStore*) -> Ctree.pos' -> Ctree.ctree ->
10.8 + val resume_prog : Rule.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
10.9 (Istate.T * Proof.context) * Program.T
10.10
10.11 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
10.12 @@ -113,6 +113,11 @@
10.13 associate is the ONLY code within by_tactic, which handles Tactic.T individually;
10.14 thus it does ContextC.insert_assumptions in case of Rewrite*.
10.15 *)
10.16 +fun trace_msg_3 tac =
10.17 + if (!trace_LI)
10.18 + then tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n"
10.19 + ^ "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
10.20 + else ();
10.21 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
10.22 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
10.23 (case stac of
10.24 @@ -239,12 +244,8 @@
10.25 then Associated (tac, f, ctxt)
10.26 else Not_Associated
10.27 | _ => raise ERROR ("associate: uncovered case"))
10.28 - | associate _ _ (m, _) =
10.29 - (if (!trace_LI)
10.30 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
10.31 - ^ "@@@ tac_ = " ^ Tactic.string_of m)
10.32 - else ();
10.33 - Not_Associated);
10.34 + | associate _ _ (tac, _) =
10.35 + (trace_msg_3 tac; Not_Associated);
10.36
10.37 (* create the initial interpreter state
10.38 from the items of the guard and the formal arguments of the partial_function.
10.39 @@ -290,7 +291,7 @@
10.40 "actuals: " ^ Rule.terms2str actuals
10.41 fun trace_init metID =
10.42 if (!trace_LI)
10.43 - then tracing("@@@ program " ^ strs2str metID)
10.44 + then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
10.45 else ();
10.46 in
10.47 fun init_pstate srls ctxt itms metID =
10.48 @@ -358,11 +359,11 @@
10.49 *)
10.50 fun trace_msg_1 call t stac =
10.51 if (! trace_LI) then
10.52 - tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
10.53 + tracing ("@@@ " ^ call ^ " leaf \"" ^ Rule.term2str t ^ "\" \<longrightarrow> Tac \"" ^ Rule.term2str stac ^ "\"")
10.54 else ();
10.55 fun trace_msg_2 call t lexpr' =
10.56 if (! trace_LI) then
10.57 - tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
10.58 + tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' \<longrightarrow> Expr \"" ^ Rule.term2str lexpr' ^ "\"")
10.59 else ();
10.60
10.61 fun check_leaf call ctxt srls (E, (a, v)) t =
11.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 10:24:13 2020 +0200
11.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 12:42:39 2020 +0200
11.3 @@ -46,7 +46,7 @@
11.4 val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
11.5 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.6 val check_Let_up: Istate.pstate -> term -> term * term
11.7 - val compare_step: Generate.taci list * Ctree.pos' list * (Calc.T) -> term -> string * Chead.calcstate'
11.8 + val compare_step: Generate.taci list * Pos.pos' list * (Calc.T) -> term -> string * Chead.calcstate'
11.9
11.10 val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
11.11 val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
11.12 @@ -668,8 +668,8 @@
11.13 val ptp as (pt, (p, _)) = Chead.all_modspec ptp (*<--------------------*)
11.14 val mI = Ctree.get_obj Ctree.g_metID pt p
11.15 in
11.16 - by_tactic (Tactic.Apply_Method' (mI, NONE, e_istate, ContextC.e_ctxt))
11.17 - (e_istate, ContextC.e_ctxt) ptp
11.18 + by_tactic (Tactic.Apply_Method' (mI, NONE, empty, ContextC.empty))
11.19 + (empty, ContextC.empty) ptp
11.20 end
11.21 | _ => msg_cs';
11.22 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
12.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 01 10:24:13 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 01 12:42:39 2020 +0200
12.3 @@ -32,7 +32,7 @@
12.4 val no_thycontext : Celem.guh -> bool
12.5 val subs_from : Istate.T -> 'a -> Celem.guh -> Selem.subs
12.6 val guh2rewtac : Celem.guh -> Selem.subs -> Tactic.input
12.7 - val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Tactic.input
12.8 + val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
12.9 val context_thy : Calc.T -> Tactic.input -> contthy
12.10 val distinct_Thm : Rule.rule list -> Rule.rule list
12.11 val eq_Thms : string list -> Rule.rule -> bool
12.12 @@ -337,7 +337,7 @@
12.13
12.14 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
12.15 pass other tacs unchanged.*)
12.16 -fun get_tac_checked pt ((p, _) : Ctree.pos') = Ctree.get_obj Ctree.g_tac pt p;
12.17 +fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;
12.18
12.19 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
12.20 fun deriv_of_thm'' (thmID, _) =
12.21 @@ -426,7 +426,7 @@
12.22 bdvs = subst, applto = f, result = res, asms = asm}
12.23 | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
12.24 | context_thy (_, p) tac =
12.25 - error ("context_thy: not for tac " ^ Tactic.tac2str tac ^ " at " ^ Pos.pos'2str p)
12.26 + error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)
12.27
12.28 (* get all theorems in a rule set (recursivley containing rule sets) *)
12.29 fun thm_of_rule Rule.Erule = []
12.30 @@ -492,7 +492,7 @@
12.31 | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set_Inst (subs, rls')) =
12.32 filter_appl_rews thy (Selem.subs2subst thy subs) f (assoc_rls rls')
12.33 | atomic_appl_tacs _ _ _ _ tac =
12.34 - (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Tactic.tac2str tac ^ "'"); []);
12.35 + (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Tactic.input_to_string tac ^ "'"); []);
12.36
12.37 (* filenames not only for thydata, but also for thy's etc *)
12.38 fun theID2filename theID = Celem.theID2guh theID ^ ".xml"
13.1 --- a/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 10:24:13 2020 +0200
13.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 12:42:39 2020 +0200
13.3 @@ -26,7 +26,7 @@
13.4 val p' = lev_dn_ (p, Res);
13.5 val pt = update_metID pt (par_pblobj pt p) Celem.e_metID;
13.6 in
13.7 - ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.e_ctxt)))], [], (pt,p')))
13.8 + ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.empty)))], [], (pt,p')))
13.9 end
13.10 | by_tactic (Tactic.End_Proof'') ptp = ("end-proof", ([], [], ptp))
13.11 | by_tactic (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
13.12 @@ -41,7 +41,7 @@
13.13 let
13.14 val ctxt = get_ctxt pt po
13.15 val ((p, p_), ps, _, pt) =
13.16 - Generate.generate1 m (Istate.e_istate, ctxt) (pt, (p, p_))
13.17 + Generate.generate1 m (Istate.empty, ctxt) (pt, (p, p_))
13.18 in ("no-method-specified", (*Free_Solve*)
13.19 ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
13.20 end
14.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Apr 01 10:24:13 2020 +0200
14.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Apr 01 12:42:39 2020 +0200
14.3 @@ -12,14 +12,12 @@
14.4 ML_file mstools.sml
14.5 ML_file "specification-elems.sml"
14.6 ML_file "istate-def.sml"
14.7 - ML_file "tactic-def.sml"
14.8 - ML_file tactic.sml (*TODO shift BEHIND ctree*)
14.9 + ML_file tactic.sml
14.10 ML_file position.sml
14.11 ML_file "ctree-basic.sml"
14.12 ML_file "ctree-access.sml"
14.13 ML_file "ctree-navi.sml"
14.14 ML_file ctree.sml
14.15 -(*ML_file tactic.sml*)
14.16 ML_file calculation.sml
14.17
14.18 ML \<open>
15.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 01 10:24:13 2020 +0200
15.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 01 12:42:39 2020 +0200
15.3 @@ -6,36 +6,36 @@
15.4 sig
15.5
15.6 val get_last_formula: CTbasic.state -> term
15.7 - val update_branch : CTbasic.ctree -> CTbasic.pos -> CTbasic.branch -> CTbasic.ctree
15.8 - val update_domID : CTbasic.ctree -> CTbasic.pos -> Rule.domID -> CTbasic.ctree
15.9 - val update_met : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
15.10 - val update_metppc : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
15.11 - val update_metID : CTbasic.ctree -> CTbasic.pos -> Celem.metID -> CTbasic.ctree
15.12 - val update_pbl : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
15.13 - val update_pblppc : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
15.14 - val update_pblID : CTbasic.ctree -> CTbasic.pos -> Celem.pblID -> CTbasic.ctree
15.15 - val update_oris : CTbasic.ctree -> CTbasic.pos -> Model.ori list -> CTbasic.ctree
15.16 - val update_orispec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
15.17 - val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
15.18 - val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic.input -> CTbasic.ctree
15.19 + val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree
15.20 + val update_domID : CTbasic.ctree -> Pos.pos -> Rule.domID -> CTbasic.ctree
15.21 + val update_met : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
15.22 + val update_metppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
15.23 + val update_metID : CTbasic.ctree -> Pos.pos -> Celem.metID -> CTbasic.ctree
15.24 + val update_pbl : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
15.25 + val update_pblppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
15.26 + val update_pblID : CTbasic.ctree -> Pos.pos -> Celem.pblID -> CTbasic.ctree
15.27 + val update_oris : CTbasic.ctree -> Pos.pos -> Model.ori list -> CTbasic.ctree
15.28 + val update_orispec : CTbasic.ctree -> Pos.pos -> Celem.spec -> CTbasic.ctree
15.29 + val update_spec : CTbasic.ctree -> Pos.pos -> Celem.spec -> CTbasic.ctree
15.30 + val update_tac : CTbasic.ctree -> Pos.pos -> Tactic.input -> CTbasic.ctree
15.31
15.32 (* original write access *)
15.33 - val cappend_form : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
15.34 - CTbasic.ctree * CTbasic.pos' list
15.35 - val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
15.36 + val cappend_form : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->
15.37 + CTbasic.ctree * Pos.pos' list
15.38 + val cappend_problem : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
15.39 Selem.fmz -> Model.ori list * Celem.spec * term * Proof.context
15.40 - -> CTbasic.ctree * CTbasic.pos' list
15.41 + -> CTbasic.ctree * Pos.pos' list
15.42 val cupdate_problem: CTbasic.ctree -> Pos.pos -> Celem.spec * Model.itm list * Model.itm list * Proof.context
15.43 -> CTbasic.ctree * Pos.pos' list
15.44 val append_atomic : (* for solve.sml *)
15.45 - CTbasic.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
15.46 + Pos.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
15.47 term -> Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
15.48 - val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
15.49 - Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
15.50 - val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
15.51 + val cappend_atomic : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->
15.52 + Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * Pos.pos' list
15.53 + val append_result : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
15.54 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
15.55
15.56 - val update_loc' : CTbasic.ctree -> CTbasic.pos ->
15.57 + val update_loc' : CTbasic.ctree -> Pos.pos ->
15.58 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
15.59 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.60 (*NONE*)
16.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 01 10:24:13 2020 +0200
16.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 01 12:42:39 2020 +0200
16.3 @@ -14,9 +14,6 @@
16.4 type con
16.5 eqtype cellID
16.6
16.7 - type pos
16.8 - type pos'
16.9 - type pos_
16.10 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
16.11 datatype ostate = Complete | Incomplete | Inconsistent
16.12 datatype ppobj =
16.13 @@ -44,18 +41,18 @@
16.14
16.15 (** basic functions **)
16.16 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
16.17 - val existpt' : pos' -> ctree -> bool (* for interface.sml *)
16.18 - val is_interpos : pos' -> bool (* for interface.sml *)
16.19 - val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
16.20 - val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
16.21 + val existpt' : Pos.pos' -> ctree -> bool (* for interface.sml *)
16.22 + val is_interpos : Pos.pos' -> bool (* for interface.sml *)
16.23 + val lev_pred' : ctree -> Pos.pos' -> Pos.pos' (* for interface.sml *)
16.24 + val ins_chn : ctree list -> ctree -> Pos.pos -> ctree (* for solve.sml *)
16.25 val children : ctree -> ctree list (* for solve.sml *)
16.26 - val get_nd : ctree -> pos -> ctree (* for solve.sml *)
16.27 + val get_nd : ctree -> Pos.pos -> ctree (* for solve.sml *)
16.28 val just_created_ : ppobj -> bool (* for mathengine.sml *)
16.29 val just_created : state -> bool (* for mathengine.sml *)
16.30 val e_origin : Model.ori list * Celem.spec * term (* for mathengine.sml *)
16.31
16.32 val is_pblobj : ppobj -> bool
16.33 - val is_pblobj' : ctree -> pos -> bool
16.34 + val is_pblobj' : ctree -> Pos.pos -> bool
16.35 val is_pblnd : ctree -> bool
16.36
16.37 val g_spec : ppobj -> Celem.spec
16.38 @@ -69,28 +66,28 @@
16.39 val g_domID : ppobj -> Rule.domID (* for appl.sml TODO: replace by thyID *)
16.40
16.41 val g_origin : ppobj -> Model.ori list * Celem.spec * term (* for script.sml *)
16.42 - val get_loc : ctree -> pos' -> Istate_Def.T * Proof.context (* for script.sml *)
16.43 - val get_istate_LI : ctree -> pos' -> Istate_Def.T (* for script.sml *)
16.44 - val get_ctxt_LI: ctree -> pos' -> Proof.context
16.45 - val get_ctxt : ctree -> pos' -> Proof.context (*DEPRECATED*)
16.46 - val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
16.47 + val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context (* for script.sml *)
16.48 + val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T (* for script.sml *)
16.49 + val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context
16.50 + val get_ctxt : ctree -> Pos.pos' -> Proof.context (*DEPRECATED*)
16.51 + val get_obj : (ppobj -> 'a) -> ctree -> Pos.pos -> 'a
16.52 val get_curr_formula : state -> term
16.53 - val get_assumptions : ctree -> pos' -> term list (* for appl.sml *)
16.54 + val get_assumptions : ctree -> Pos.pos' -> term list (* for appl.sml *)
16.55
16.56 val new_val : term -> Istate_Def.T -> Istate_Def.T
16.57 (* for calchead.sml *)
16.58 type cid = cellID list
16.59 - type ocalhd = bool * pos_ * term * Model.itm list * (bool * term) list * Celem.spec
16.60 + type ocalhd = bool * Pos.pos_ * term * Model.itm list * (bool * term) list * Celem.spec
16.61 datatype ptform = Form of term | ModSpec of ocalhd
16.62 val get_somespec' : Celem.spec -> Celem.spec -> Celem.spec
16.63 exception PTREE of string;
16.64
16.65 - val parent_node : ctree -> pos -> bool * pos * Rule.rls (* for appl.sml *)
16.66 + val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule.rls (* for appl.sml *)
16.67 val rootthy : ctree -> theory (* for script.sml *)
16.68 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
16.69 - val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
16.70 - val existpt : pos -> ctree -> bool (* also for tests *)
16.71 - val cut_tree : ctree -> pos * 'a -> ctree * pos' list (* also for tests *)
16.72 + val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
16.73 + val existpt : Pos.pos -> ctree -> bool (* also for tests *)
16.74 + val cut_tree : ctree -> Pos.pos * 'a -> ctree * Pos.pos' list (* also for tests *)
16.75 val insert_pt : ppobj -> ctree -> int list -> ctree
16.76 (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
16.77 val g_branch : ppobj -> branch
16.78 @@ -100,22 +97,22 @@
16.79 val g_res : ppobj -> term
16.80 val g_res' : ctree -> term
16.81 (*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
16.82 - val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
16.83 - val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
16.84 + val lev_dn : CTbasic.Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
16.85 + val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
16.86 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
16.87
16.88 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
16.89 - val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
16.90 - val pr_short : pos -> ppobj -> string
16.91 + val pr_ctree : (Pos.pos -> ppobj -> string) -> ctree -> string
16.92 + val pr_short : Pos.pos -> ppobj -> string
16.93 val g_ctxt : ppobj -> Proof.context
16.94 val g_fmz : ppobj -> Selem.fmz
16.95 - val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
16.96 - val get_allps : (pos * pos_) list -> Pos.posel list -> ctree list -> pos' list
16.97 - val get_allpos' : pos * Pos.posel -> ctree -> pos' list
16.98 - val get_allpos's : pos * Pos.posel -> ctree list -> (pos * pos_) list
16.99 - val cut_bottom : pos * Pos.posel -> ctree -> (ctree * pos' list) * bool
16.100 - val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
16.101 - val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
16.102 + val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list
16.103 + val get_allps : (Pos.pos * Pos.pos_) list -> Pos.posel list -> ctree list -> Pos.pos' list
16.104 + val get_allpos' : Pos.pos * Pos.posel -> ctree -> Pos.pos' list
16.105 + val get_allpos's : Pos.pos * Pos.posel -> ctree list -> (Pos.pos * Pos.pos_) list
16.106 + val cut_bottom : Pos.pos * Pos.posel -> ctree -> (ctree * Pos.pos' list) * bool
16.107 + val cut_level : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
16.108 + val cut_level_'_ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
16.109 val get_trace : ctree -> int list -> int list -> int list list
16.110 val branch2str : branch -> string
16.111 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
16.112 @@ -156,7 +153,7 @@
16.113
16.114
16.115 type iist = Istate_Def.T option * Istate_Def.T option;
16.116 -(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
16.117 +(*val e_iist = (empty, empty); --- sinnlos f"ur NICHT-equality-type*)
16.118
16.119
16.120 fun new_val v (Istate_Def.Pstate pst) =
16.121 @@ -202,7 +199,7 @@
16.122 (Istate_Def.T * (* script interpreter state *)
16.123 Proof.context) (* context for provers, type inference *)
16.124 option, (* both for interpreter location on Res *)
16.125 - (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc *)
16.126 + (*(NONE,NONE) <==> empty ! see update_loc, get_loc *)
16.127 branch: branch, (* only rudimentary *)
16.128 result: Selem.result, (* result and assumptions *)
16.129 ostate: ostate} (* Complete <=> result is OK *)
16.130 @@ -465,16 +462,16 @@
16.131 result = (Rule.e_term, []), ostate = Incomplete};
16.132
16.133
16.134 -fun get_loc EmptyPtree _ = (Istate_Def.e_istate, ContextC.e_ctxt)
16.135 +fun get_loc EmptyPtree _ = (Istate_Def.empty, ContextC.empty)
16.136 | get_loc pt (p, Res) =
16.137 (case get_obj g_loc pt p of
16.138 (SOME i, NONE) => i
16.139 - | (NONE , NONE) => (Istate_Def.e_istate, ContextC.e_ctxt)
16.140 + | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
16.141 | (_ , SOME i) => i)
16.142 | get_loc pt (p, _) =
16.143 (case get_obj g_loc pt p of
16.144 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
16.145 - | (NONE , NONE) => (Istate_Def.e_istate, ContextC.e_ctxt)
16.146 + | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
16.147 | (SOME i, _) => i);
16.148 fun get_istate_LI pt p = get_loc pt p |> #1;
16.149 fun get_ctxt_LI pt p = get_loc pt p |> #2;
17.1 --- a/src/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 01 10:24:13 2020 +0200
17.2 +++ b/src/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 01 12:42:39 2020 +0200
17.3 @@ -4,18 +4,18 @@
17.4 *)
17.5 signature CALC_TREE_NAVIGATION =
17.6 sig
17.7 - val last_onlev : CTbasic.ctree -> CTbasic.pos -> bool
17.8 - val exist_lev_on' : CTbasic.ctree -> CTbasic.pos' -> bool (* for interface.sml *)
17.9 - val is_curr_endof_calc : CTbasic.ctree -> CTbasic.pos' -> bool (* for interface.sml *)
17.10 + val last_onlev : CTbasic.ctree -> Pos.pos -> bool
17.11 + val exist_lev_on' : CTbasic.ctree -> Pos.pos' -> bool (* for interface.sml *)
17.12 + val is_curr_endof_calc : CTbasic.ctree -> Pos.pos' -> bool (* for interface.sml *)
17.13
17.14 - val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-basic.sml *)
17.15 + val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-basic.sml *)
17.16
17.17 - val lev_on' : CTbasic.ctree -> CTbasic.pos' -> CTbasic.pos' (* for interface.sml *)
17.18 - val move_dn : CTbasic.pos -> CTbasic.ctree -> CTbasic.pos' -> CTbasic.pos'
17.19 - val move_up : CTbasic.pos -> CTbasic.ctree -> CTbasic.pos' -> CTbasic.pos'(* or interface.sml *)
17.20 - val movelevel_dn : CTbasic.pos -> CTbasic.ctree -> CTbasic.pos' -> CTbasic.pos'(*nterface.sml *)
17.21 - val movelevel_up : CTbasic.pos -> CTbasic.ctree -> CTbasic.pos' -> CTbasic.pos'(*nterface.sml *)
17.22 - val movecalchd_up : CTbasic.ctree -> CTbasic.pos' -> CTbasic.pos' (* for interface.sml *)
17.23 + val lev_on' : CTbasic.ctree -> Pos.pos' -> Pos.pos' (* for interface.sml *)
17.24 + val move_dn : Pos.pos -> CTbasic.ctree -> Pos.pos' -> Pos.pos'
17.25 + val move_up : Pos.pos -> CTbasic.ctree -> Pos.pos' -> Pos.pos'(* or interface.sml *)
17.26 + val movelevel_dn : Pos.pos -> CTbasic.ctree -> Pos.pos' -> Pos.pos'(*nterface.sml *)
17.27 + val movelevel_up : Pos.pos -> CTbasic.ctree -> Pos.pos' -> Pos.pos'(*nterface.sml *)
17.28 + val movecalchd_up : CTbasic.ctree -> Pos.pos' -> Pos.pos' (* for interface.sml *)
17.29
17.30 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
17.31 (* NONE *)
18.1 --- a/src/Tools/isac/MathEngBasic/ctree.sml Wed Apr 01 10:24:13 2020 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/ctree.sml Wed Apr 01 12:42:39 2020 +0200
18.3 @@ -18,7 +18,7 @@
18.4 open CTnavi
18.5 open CTaccess
18.6
18.7 -fun get_pblID (pt, (p, _): pos') =
18.8 +fun get_pblID (pt, (p, _)) =
18.9 let val p' = par_pblobj pt p
18.10 val (_, pI, _) = get_obj g_spec pt p'
18.11 val (_, (_, oI, _), _) = get_obj g_origin pt p'
19.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Wed Apr 01 10:24:13 2020 +0200
19.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Wed Apr 01 12:42:39 2020 +0200
19.3 @@ -15,7 +15,7 @@
19.4 val pstate2str': pstate -> string
19.5
19.6 datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
19.7 - val e_istate: T
19.8 + val empty: T
19.9 val string_of: T -> string
19.10 val string_of': T -> string
19.11 val istates2str: T option * T option -> string
19.12 @@ -72,7 +72,7 @@
19.13 Uistate (*undefined in modspec, in '_deriv'ation*)
19.14 | Pstate of pstate (*for script interpreter*)
19.15 | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
19.16 -val e_istate = Pstate e_pstate;
19.17 +val empty = Pstate e_pstate;
19.18
19.19 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ", (" ^ Rule.term2str t ^ ", " ^ Rule.terms2str a ^ "))";
19.20 fun string_of Uistate = "Uistate"
20.1 --- a/src/Tools/isac/MathEngBasic/tactic-def.sml Wed Apr 01 10:24:13 2020 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,409 +0,0 @@
20.4 -(* Title: Tactics; tac_ for interaction with frontend, input for internal use.
20.5 - Author: Walther Neuper 170121
20.6 - (c) due to copyright terms
20.7 -
20.8 -regular expression for search:
20.9 -
20.10 -Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
20.11 -
20.12 -*)
20.13 -signature TACTIC_DEF =
20.14 -sig
20.15 - datatype T =
20.16 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
20.17 - | Add_Relation' of Rule.cterm' * Model.itm list
20.18 - | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
20.19 -
20.20 - | Begin_Sequ' | Begin_Trans' of term
20.21 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
20.22 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
20.23 - | End_Sequ' | End_Trans' of Selem.result
20.24 - | End_Ruleset' of term | End_Intersect' of term | End_Proof''
20.25 -
20.26 - | CAScmd' of term
20.27 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
20.28 - | Check_Postcond' of Celem.pblID * term
20.29 - | Check_elementwise' of term * Rule.cterm' * Selem.result
20.30 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
20.31 -
20.32 - | Derive' of Rule.rls
20.33 - | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
20.34 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
20.35 - | End_Detail' of Selem.result
20.36 -
20.37 - | Empty_Tac_
20.38 - | Free_Solve'
20.39 -
20.40 - | Init_Proof' of Rule.cterm' list * Celem.spec
20.41 - | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
20.42 - | Or_to_List' of term * term
20.43 - | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
20.44 - | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
20.45 -
20.46 - | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
20.47 - | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
20.48 - | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
20.49 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
20.50 -
20.51 - | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
20.52 - | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
20.53 - | Specify_Theory' of Rule.domID
20.54 - | Subproblem' of
20.55 - Celem.spec * Model.ori list *
20.56 - term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
20.57 - Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
20.58 - (*Istate.T * ? *)
20.59 - Proof.context * (* derived from prog. in ??? *)
20.60 - term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
20.61 - | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
20.62 - | Tac_ of theory * string * string * string
20.63 - | Take' of term
20.64 - val string_of : T -> string
20.65 -
20.66 - datatype input =
20.67 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
20.68 - | Apply_Assumption of Rule.cterm' list
20.69 - | Apply_Method of Celem.metID
20.70 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
20.71 - | Begin_Sequ | Begin_Trans
20.72 - | Split_And | Split_Or | Split_Intersect
20.73 - | Conclude_And | Conclude_Or | Collect_Trues
20.74 - | End_Sequ | End_Trans
20.75 - | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
20.76 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
20.77 - | CAScmd of Rule.cterm'
20.78 - | Calculate of string
20.79 - | Check_Postcond of Celem.pblID
20.80 - | Check_elementwise of Rule.cterm'
20.81 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
20.82 -
20.83 - | Derive of Rule.rls'
20.84 - | Detail_Set of Rule.rls'
20.85 - | Detail_Set_Inst of Selem.subs * Rule.rls'
20.86 - | End_Detail
20.87 -
20.88 - | Empty_Tac
20.89 - | Free_Solve
20.90 -
20.91 - | Init_Proof of Rule.cterm' list * Celem.spec
20.92 - | Model_Problem
20.93 - | Or_to_List
20.94 - | Refine_Problem of Celem.pblID
20.95 - | Refine_Tacitly of Celem.pblID
20.96 -
20.97 - | Rewrite of Celem.thm''
20.98 - | Rewrite_Inst of Selem.subs * Celem.thm''
20.99 - | Rewrite_Set of Rule.rls'
20.100 - | Rewrite_Set_Inst of Selem.subs * Rule.rls'
20.101 -
20.102 - | Specify_Method of Celem.metID
20.103 - | Specify_Problem of Celem.pblID
20.104 - | Specify_Theory of Rule.domID
20.105 - | Subproblem of Rule.domID * Celem.pblID
20.106 -
20.107 - | Substitute of Selem.sube
20.108 - | Tac of string
20.109 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
20.110 - val tac2str : input -> string
20.111 - val tac2IDstr : input -> string
20.112 - val is_empty : input -> bool
20.113 -end
20.114 -
20.115 -(**)
20.116 -structure Tactic_Def(**): TACTIC_DEF(**) =
20.117 -struct
20.118 -(**)
20.119 -
20.120 -(* tactics for user at front-end.
20.121 - input propagates the construction of the calc-tree;
20.122 - there are
20.123 - (a) 'specsteps' for the specify-phase, and others for the solve-phase
20.124 - (b) those of the solve-phase are 'initac's and others;
20.125 - initacs start with a formula different from the preceding formula.
20.126 - see 'type tac_' for the internal representation of tactics
20.127 -*)
20.128 -datatype input =
20.129 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
20.130 - | Apply_Assumption of Rule.cterm' list
20.131 - | Apply_Method of Celem.metID
20.132 - (* creates an "istate" in PblObj.env; in case of "implicit_take"
20.133 - creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
20.134 - a "SOME istate" at fst of "loc".
20.135 - As each step (in the solve-phase) has a resulting formula (at the front-end)
20.136 - Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
20.137 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
20.138 - | Begin_Sequ | Begin_Trans
20.139 - | Split_And | Split_Or | Split_Intersect
20.140 - | Conclude_And | Conclude_Or | Collect_Trues
20.141 - | End_Sequ | End_Trans
20.142 - | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
20.143 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
20.144 - | CAScmd of Rule.cterm'
20.145 - | Calculate of string
20.146 - | Check_Postcond of Celem.pblID
20.147 - | Check_elementwise of Rule.cterm'
20.148 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
20.149 -
20.150 - | Derive of Rule.rls' (* WN0509 drop *)
20.151 - | Detail_Set of Rule.rls' (* WN0509 drop *)
20.152 - | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
20.153 - | End_Detail (* WN0509 drop *)
20.154 -
20.155 - | Empty_Tac
20.156 - | Free_Solve
20.157 -
20.158 - | Init_Proof of Rule.cterm' list * Celem.spec
20.159 - | Model_Problem
20.160 - | Or_to_List
20.161 - | Refine_Problem of Celem.pblID
20.162 - | Refine_Tacitly of Celem.pblID
20.163 -
20.164 - (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
20.165 - because there all the thms are present with both (thmID, thm)
20.166 - (where user-views can show both or only one of (thmID, thm)),
20.167 - and thm is created from ThmID by assoc_thm'' when entering isabisac *)
20.168 - | Rewrite of Celem.thm''
20.169 - | Rewrite_Inst of Selem.subs * Celem.thm''
20.170 - | Rewrite_Set of Rule.rls'
20.171 - | Rewrite_Set_Inst of Selem.subs * Rule.rls'
20.172 -
20.173 - | Specify_Method of Celem.metID
20.174 - | Specify_Problem of Celem.pblID
20.175 - | Specify_Theory of Rule.domID
20.176 - | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
20.177 -
20.178 - | Substitute of Selem.sube
20.179 - | Tac of string (* WN0509 drop *)
20.180 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
20.181 -
20.182 -fun tac2str ma = case ma of
20.183 - Init_Proof (ppc, spec) =>
20.184 - "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
20.185 - | Model_Problem => "Model_Problem "
20.186 - | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
20.187 - | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
20.188 - | Add_Given cterm' => "Add_Given " ^ cterm'
20.189 - | Del_Given cterm' => "Del_Given " ^ cterm'
20.190 - | Add_Find cterm' => "Add_Find " ^ cterm'
20.191 - | Del_Find cterm' => "Del_Find " ^ cterm'
20.192 - | Add_Relation cterm' => "Add_Relation " ^ cterm'
20.193 - | Del_Relation cterm' => "Del_Relation " ^ cterm'
20.194 -
20.195 - | Specify_Theory domID => "Specify_Theory " ^ quote domID
20.196 - | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
20.197 - | Specify_Method metID => "Specify_Method " ^ strs2str metID
20.198 - | Apply_Method metID => "Apply_Method " ^ strs2str metID
20.199 - | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
20.200 - | Free_Solve => "Free_Solve"
20.201 -
20.202 - | Rewrite_Inst (subs, (id, thm)) =>
20.203 - "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
20.204 - | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
20.205 - | Rewrite_Set_Inst (subs, rls) =>
20.206 - "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
20.207 - | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
20.208 - | Detail_Set rls => "Detail_Set " ^ quote rls
20.209 - | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
20.210 - | End_Detail => "End_Detail"
20.211 - | Derive rls' => "Derive " ^ rls'
20.212 - | Calculate op_ => "Calculate " ^ op_
20.213 - | Substitute sube => "Substitute " ^ Selem.sube2str sube
20.214 - | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
20.215 -
20.216 - | Take cterm' => "Take " ^ quote cterm'
20.217 - | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
20.218 - | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
20.219 - | End_Subproblem => "End_Subproblem"
20.220 - | CAScmd cterm' => "CAScmd " ^ quote cterm'
20.221 -
20.222 - | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
20.223 - | Or_to_List => "Or_to_List "
20.224 - | Collect_Trues => "Collect_Trues"
20.225 -
20.226 - | Empty_Tac => "Empty_Tac"
20.227 - | Tac string => "Tac " ^ string
20.228 - | End_Proof' => "input End_Proof'"
20.229 - | _ => "tac2str not impl. for ?!";
20.230 -
20.231 -fun is_empty input = case input of Empty_Tac => true | _ => false
20.232 -
20.233 -(* tactics for for internal use, compare "input" for user at the front-end.
20.234 - tac_ contains results from check in 'fun applicable_in'.
20.235 - This is useful for costly results, e.g. from rewriting;
20.236 - however, these results might be changed by Scripts like
20.237 - " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
20.238 - " eq = (Rewrite_Set equival_trans False) eq;" ^
20.239 - TODO.WN120106 ANALOGOUSLY TO Substitute':
20.240 - So tac_ contains the term t the result was calculated from
20.241 - in order to compare t with t' possibly changed by "Expr "
20.242 - and re-calculate result if t<>t'
20.243 - TODO.WN161219: replace *every* cterm' by term
20.244 -*)
20.245 - datatype T =
20.246 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
20.247 - | Add_Relation' of Rule.cterm' * Model.itm list
20.248 - | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
20.249 - * tactic Apply_Method metID
20.250 - * formula term *)
20.251 - Celem.metID * (* key for KEStore *)
20.252 - term option * (* the first formula of Calc.T. TODO: rm option *)
20.253 - Istate_Def.T * (* for the newly started program *)
20.254 - Proof.context (* for the newly started program *)
20.255 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
20.256 - | Begin_Sequ' | Begin_Trans' of term
20.257 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
20.258 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
20.259 - | End_Sequ' | End_Trans' of Selem.result
20.260 - | End_Ruleset' of term | End_Intersect' of term | End_Proof''
20.261 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
20.262 - | CAScmd' of term
20.263 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
20.264 - | Check_Postcond' of Celem.pblID *
20.265 - term (* returnvalue of program in solve *)
20.266 - | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
20.267 - term * (* (1) the current formula: [x=1,x=...] *)
20.268 - string * (* (2) the pred from Check_elementwise *)
20.269 - Selem.result (* (3) composed from (1) and (2): {x. pred} *)
20.270 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
20.271 -
20.272 - | Derive' of Rule.rls
20.273 - | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
20.274 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
20.275 - | End_Detail' of Selem.result
20.276 -
20.277 - | Empty_Tac_
20.278 - | Free_Solve'
20.279 -
20.280 - | Init_Proof' of Rule.cterm' list * Celem.spec
20.281 - | Model_Problem' of (* first step in specifying *)
20.282 - Celem.pblID * (* key into KEStore *)
20.283 - Model.itm list * (* the 'untouched' pbl *)
20.284 - Model.itm list (* the casually completed met *)
20.285 - | Or_to_List' of term * term
20.286 - | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
20.287 - | Refine_Tacitly' of
20.288 - Celem.pblID * (* input *)
20.289 - Celem.pblID * (* the refined from applicable_in *)
20.290 - Rule.domID * (* from new pbt?! filled in specify *)
20.291 - Celem.metID * (* from new pbt?! filled in specify *)
20.292 - Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
20.293 - | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
20.294 - | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
20.295 - | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
20.296 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
20.297 -
20.298 - | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
20.299 - | Specify_Problem' of Celem.pblID *
20.300 - (bool * (* matches *)
20.301 - (Model.itm list * (* ppc *)
20.302 - (bool * term) list)) (* preconditions marked true/false *)
20.303 - | Specify_Theory' of Rule.domID
20.304 - | Subproblem' of
20.305 - Celem.spec *
20.306 - (Model.ori list) * (* filled in associate Subproblem' *)
20.307 - term * (* filled -"-, headline of calc-head *)
20.308 - Selem.fmz_ * (* string list from arguments *)
20.309 - Proof.context * (* for specify-phase *)
20.310 - term (* Subproblem (thyID, pbl) OR cascmd *)
20.311 - | Substitute' of
20.312 - Rule.rew_ord_ * (* for re-calculation *)
20.313 - Rule.rls * (* for re-calculation *)
20.314 - Selem.subte * (* the 'substitution': terms of type bool *)
20.315 - term * (* to be substituted into *)
20.316 - term (* resulting from the substitution *)
20.317 - | Tac_ of theory * string * string * string
20.318 - | Take' of term
20.319 -
20.320 -fun string_of ma = case ma of
20.321 - Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
20.322 - | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
20.323 - | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
20.324 - strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
20.325 - | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
20.326 - | Add_Given' _ => "Add_Given' "(*^cterm'*)
20.327 - | Del_Given' _ => "Del_Given' "(*^cterm'*)
20.328 - | Add_Find' _ => "Add_Find' "(*^cterm'*)
20.329 - | Del_Find' _ => "Del_Find' "(*^cterm'*)
20.330 - | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
20.331 - | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
20.332 -
20.333 - | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
20.334 - | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
20.335 - spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
20.336 - | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
20.337 - Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
20.338 -
20.339 - | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
20.340 - | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
20.341 - (spair2str (strs2str pblID, Rule.term2str scval))
20.342 -
20.343 - | Free_Solve' => "Free_Solve'"
20.344 -
20.345 - | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
20.346 - | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
20.347 - | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
20.348 - | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
20.349 - "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
20.350 - | End_Detail' _ => "End_Detail' xxx"
20.351 - | Detail_Set' _ => "Detail_Set' xxx"
20.352 - | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
20.353 -
20.354 - | Derive' rls => "Derive' " ^ Rule.id_rls rls
20.355 - | Calculate' _ => "Calculate' "
20.356 - | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
20.357 -
20.358 - | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
20.359 - | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
20.360 - "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
20.361 - | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
20.362 -
20.363 - | Empty_Tac_ => "Empty_Tac_"
20.364 - | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
20.365 - | _ => "string_of not impl. for arg";
20.366 -
20.367 -fun tac2IDstr ma = case ma of
20.368 - Model_Problem => "Model_Problem"
20.369 - | Refine_Tacitly _ => "Refine_Tacitly"
20.370 - | Refine_Problem _ => "Refine_Problem"
20.371 - | Add_Given _ => "Add_Given"
20.372 - | Del_Given _ => "Del_Given"
20.373 - | Add_Find _ => "Add_Find"
20.374 - | Del_Find _ => "Del_Find"
20.375 - | Add_Relation _ => "Add_Relation"
20.376 - | Del_Relation _ => "Del_Relation"
20.377 -
20.378 - | Specify_Theory _ => "Specify_Theory"
20.379 - | Specify_Problem _ => "Specify_Problem"
20.380 - | Specify_Method _ => "Specify_Method"
20.381 - | Apply_Method _ => "Apply_Method"
20.382 - | Check_Postcond _ => "Check_Postcond"
20.383 - | Free_Solve => "Free_Solve"
20.384 -
20.385 - | Rewrite_Inst _ => "Rewrite_Inst"
20.386 - | Rewrite _ => "Rewrite"
20.387 - | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
20.388 - | Rewrite_Set _ => "Rewrite_Set"
20.389 - | Detail_Set _ => "Detail_Set"
20.390 - | Detail_Set_Inst _ => "Detail_Set_Inst"
20.391 - | Derive _ => "Derive "
20.392 - | Calculate _ => "Calculate "
20.393 - | Substitute _ => "Substitute"
20.394 - | Apply_Assumption _ => "Apply_Assumption"
20.395 -
20.396 - | Take _ => "Take"
20.397 - | Take_Inst _ => "Take_Inst"
20.398 - | Subproblem _ => "Subproblem"
20.399 - | End_Subproblem => "End_Subproblem"
20.400 - | CAScmd _ => "CAScmd"
20.401 -
20.402 - | Check_elementwise _ => "Check_elementwise"
20.403 - | Or_to_List => "Or_to_List "
20.404 - | Collect_Trues => "Collect_Trues"
20.405 -
20.406 - | Empty_Tac => "Empty_Tac"
20.407 - | Tac _ => "Tac "
20.408 - | End_Proof' => "End_Proof'"
20.409 - | _ => "tac2str not impl. for ?!";
20.410 -
20.411 -
20.412 -(**)end(**)
21.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 10:24:13 2020 +0200
21.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 12:42:39 2020 +0200
21.3 @@ -9,15 +9,105 @@
21.4 *)
21.5 signature TACTIC =
21.6 sig
21.7 - datatype T = datatype Tactic_Def.T
21.8 + datatype T =
21.9 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
21.10 + | Add_Relation' of Rule.cterm' * Model.itm list
21.11 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
21.12 +
21.13 + | Begin_Sequ' | Begin_Trans' of term
21.14 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
21.15 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
21.16 + | End_Sequ' | End_Trans' of Selem.result
21.17 + | End_Ruleset' of term | End_Intersect' of term | End_Proof''
21.18 +
21.19 + | CAScmd' of term
21.20 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
21.21 + | Check_Postcond' of Celem.pblID * term
21.22 + | Check_elementwise' of term * Rule.cterm' * Selem.result
21.23 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
21.24 +
21.25 + | Derive' of Rule.rls
21.26 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
21.27 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
21.28 + | End_Detail' of Selem.result
21.29 +
21.30 + | Empty_Tac_
21.31 + | Free_Solve'
21.32 +
21.33 + | Init_Proof' of Rule.cterm' list * Celem.spec
21.34 + | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
21.35 + | Or_to_List' of term * term
21.36 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
21.37 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
21.38 +
21.39 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
21.40 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
21.41 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
21.42 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
21.43 +
21.44 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
21.45 + | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
21.46 + | Specify_Theory' of Rule.domID
21.47 + | Subproblem' of
21.48 + Celem.spec * Model.ori list *
21.49 + term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
21.50 + Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
21.51 + (*Istate.T * ? *)
21.52 + Proof.context * (* derived from prog. in ??? *)
21.53 + term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
21.54 + | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
21.55 + | Tac_ of theory * string * string * string
21.56 + | Take' of term
21.57 val string_of: T -> string
21.58
21.59 - datatype input = datatype Tactic_Def.input
21.60 - val tac2str : input -> string
21.61 + datatype input =
21.62 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
21.63 + | Apply_Assumption of Rule.cterm' list
21.64 + | Apply_Method of Celem.metID
21.65 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
21.66 + | Begin_Sequ | Begin_Trans
21.67 + | Split_And | Split_Or | Split_Intersect
21.68 + | Conclude_And | Conclude_Or | Collect_Trues
21.69 + | End_Sequ | End_Trans
21.70 + | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
21.71 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
21.72 + | CAScmd of Rule.cterm'
21.73 + | Calculate of string
21.74 + | Check_Postcond of Celem.pblID
21.75 + | Check_elementwise of Rule.cterm'
21.76 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
21.77 +
21.78 + | Derive of Rule.rls'
21.79 + | Detail_Set of Rule.rls'
21.80 + | Detail_Set_Inst of Selem.subs * Rule.rls'
21.81 + | End_Detail
21.82 +
21.83 + | Empty_Tac
21.84 + | Free_Solve
21.85 +
21.86 + | Init_Proof of Rule.cterm' list * Celem.spec
21.87 + | Model_Problem
21.88 + | Or_to_List
21.89 + | Refine_Problem of Celem.pblID
21.90 + | Refine_Tacitly of Celem.pblID
21.91 +
21.92 + | Rewrite of Celem.thm''
21.93 + | Rewrite_Inst of Selem.subs * Celem.thm''
21.94 + | Rewrite_Set of Rule.rls'
21.95 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
21.96 +
21.97 + | Specify_Method of Celem.metID
21.98 + | Specify_Problem of Celem.pblID
21.99 + | Specify_Theory of Rule.domID
21.100 + | Subproblem of Rule.domID * Celem.pblID
21.101 +
21.102 + | Substitute of Selem.sube
21.103 + | Tac of string
21.104 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
21.105 + val input_to_string : input -> string
21.106 val tac2IDstr : input -> string
21.107 val is_empty : input -> bool
21.108
21.109 -(*//-------------------------------------------------------------- only AFTER ctree.sml required *)
21.110 val eq_tac : input * input -> bool
21.111 val is_rewtac : input -> bool
21.112 val is_rewset : input -> bool
21.113 @@ -45,11 +135,162 @@
21.114 struct
21.115 (**)
21.116
21.117 -datatype input = datatype Tactic_Def.input
21.118 +(* tactics for user at front-end.
21.119 + input propagates the construction of the calc-tree;
21.120 + there are
21.121 + (a) 'specsteps' for the specify-phase, and others for the solve-phase
21.122 + (b) those of the solve-phase are 'initac's and others;
21.123 + initacs start with a formula different from the preceding formula.
21.124 + see 'type tac_' for the internal representation of tactics
21.125 +*)
21.126 +datatype input =
21.127 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
21.128 + | Apply_Assumption of Rule.cterm' list
21.129 + | Apply_Method of Celem.metID
21.130 + (* creates an "istate" in PblObj.env; in case of "implicit_take"
21.131 + creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
21.132 + a "SOME istate" at fst of "loc".
21.133 + As each step (in the solve-phase) has a resulting formula (at the front-end)
21.134 + Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
21.135 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
21.136 + | Begin_Sequ | Begin_Trans
21.137 + | Split_And | Split_Or | Split_Intersect
21.138 + | Conclude_And | Conclude_Or | Collect_Trues
21.139 + | End_Sequ | End_Trans
21.140 + | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
21.141 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
21.142 + | CAScmd of Rule.cterm'
21.143 + | Calculate of string
21.144 + | Check_Postcond of Celem.pblID
21.145 + | Check_elementwise of Rule.cterm'
21.146 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
21.147
21.148 -val tac2str = Tactic_Def.tac2str
21.149 -val tac2IDstr = Tactic_Def.tac2IDstr
21.150 -val is_empty = Tactic_Def.is_empty
21.151 + | Derive of Rule.rls' (* WN0509 drop *)
21.152 + | Detail_Set of Rule.rls' (* WN0509 drop *)
21.153 + | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
21.154 + | End_Detail (* WN0509 drop *)
21.155 +
21.156 + | Empty_Tac
21.157 + | Free_Solve
21.158 +
21.159 + | Init_Proof of Rule.cterm' list * Celem.spec
21.160 + | Model_Problem
21.161 + | Or_to_List
21.162 + | Refine_Problem of Celem.pblID
21.163 + | Refine_Tacitly of Celem.pblID
21.164 +
21.165 + (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
21.166 + because there all the thms are present with both (thmID, thm)
21.167 + (where user-views can show both or only one of (thmID, thm)),
21.168 + and thm is created from ThmID by assoc_thm'' when entering isabisac *)
21.169 + | Rewrite of Celem.thm''
21.170 + | Rewrite_Inst of Selem.subs * Celem.thm''
21.171 + | Rewrite_Set of Rule.rls'
21.172 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
21.173 +
21.174 + | Specify_Method of Celem.metID
21.175 + | Specify_Problem of Celem.pblID
21.176 + | Specify_Theory of Rule.domID
21.177 + | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
21.178 +
21.179 + | Substitute of Selem.sube
21.180 + | Tac of string (* WN0509 drop *)
21.181 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
21.182 +
21.183 +fun input_to_string ma = case ma of
21.184 + Init_Proof (ppc, spec) =>
21.185 + "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
21.186 + | Model_Problem => "Model_Problem "
21.187 + | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
21.188 + | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
21.189 + | Add_Given cterm' => "Add_Given " ^ cterm'
21.190 + | Del_Given cterm' => "Del_Given " ^ cterm'
21.191 + | Add_Find cterm' => "Add_Find " ^ cterm'
21.192 + | Del_Find cterm' => "Del_Find " ^ cterm'
21.193 + | Add_Relation cterm' => "Add_Relation " ^ cterm'
21.194 + | Del_Relation cterm' => "Del_Relation " ^ cterm'
21.195 +
21.196 + | Specify_Theory domID => "Specify_Theory " ^ quote domID
21.197 + | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
21.198 + | Specify_Method metID => "Specify_Method " ^ strs2str metID
21.199 + | Apply_Method metID => "Apply_Method " ^ strs2str metID
21.200 + | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
21.201 + | Free_Solve => "Free_Solve"
21.202 +
21.203 + | Rewrite_Inst (subs, (id, thm)) =>
21.204 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
21.205 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
21.206 + | Rewrite_Set_Inst (subs, rls) =>
21.207 + "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
21.208 + | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
21.209 + | Detail_Set rls => "Detail_Set " ^ quote rls
21.210 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
21.211 + | End_Detail => "End_Detail"
21.212 + | Derive rls' => "Derive " ^ rls'
21.213 + | Calculate op_ => "Calculate " ^ op_
21.214 + | Substitute sube => "Substitute " ^ Selem.sube2str sube
21.215 + | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
21.216 +
21.217 + | Take cterm' => "Take " ^ quote cterm'
21.218 + | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
21.219 + | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
21.220 + | End_Subproblem => "End_Subproblem"
21.221 + | CAScmd cterm' => "CAScmd " ^ quote cterm'
21.222 +
21.223 + | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
21.224 + | Or_to_List => "Or_to_List "
21.225 + | Collect_Trues => "Collect_Trues"
21.226 +
21.227 + | Empty_Tac => "Empty_Tac"
21.228 + | Tac string => "Tac " ^ string
21.229 + | End_Proof' => "input End_Proof'"
21.230 + | _ => "input_to_string not impl. for ?!";
21.231 +
21.232 +fun tac2IDstr ma = case ma of
21.233 + Model_Problem => "Model_Problem"
21.234 + | Refine_Tacitly _ => "Refine_Tacitly"
21.235 + | Refine_Problem _ => "Refine_Problem"
21.236 + | Add_Given _ => "Add_Given"
21.237 + | Del_Given _ => "Del_Given"
21.238 + | Add_Find _ => "Add_Find"
21.239 + | Del_Find _ => "Del_Find"
21.240 + | Add_Relation _ => "Add_Relation"
21.241 + | Del_Relation _ => "Del_Relation"
21.242 +
21.243 + | Specify_Theory _ => "Specify_Theory"
21.244 + | Specify_Problem _ => "Specify_Problem"
21.245 + | Specify_Method _ => "Specify_Method"
21.246 + | Apply_Method _ => "Apply_Method"
21.247 + | Check_Postcond _ => "Check_Postcond"
21.248 + | Free_Solve => "Free_Solve"
21.249 +
21.250 + | Rewrite_Inst _ => "Rewrite_Inst"
21.251 + | Rewrite _ => "Rewrite"
21.252 + | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
21.253 + | Rewrite_Set _ => "Rewrite_Set"
21.254 + | Detail_Set _ => "Detail_Set"
21.255 + | Detail_Set_Inst _ => "Detail_Set_Inst"
21.256 + | Derive _ => "Derive "
21.257 + | Calculate _ => "Calculate "
21.258 + | Substitute _ => "Substitute"
21.259 + | Apply_Assumption _ => "Apply_Assumption"
21.260 +
21.261 + | Take _ => "Take"
21.262 + | Take_Inst _ => "Take_Inst"
21.263 + | Subproblem _ => "Subproblem"
21.264 + | End_Subproblem => "End_Subproblem"
21.265 + | CAScmd _ => "CAScmd"
21.266 +
21.267 + | Check_elementwise _ => "Check_elementwise"
21.268 + | Or_to_List => "Or_to_List "
21.269 + | Collect_Trues => "Collect_Trues"
21.270 +
21.271 + | Empty_Tac => "Empty_Tac"
21.272 + | Tac _ => "Tac "
21.273 + | End_Proof' => "End_Proof'"
21.274 + | _ => "input_to_string not impl. for ?!";
21.275 +
21.276 +fun is_empty input = case input of Empty_Tac => true | _ => false
21.277
21.278 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
21.279 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
21.280 @@ -68,7 +309,7 @@
21.281
21.282 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
21.283 | rls_of (Rewrite_Set rls) = rls
21.284 - | rls_of input = error ("rls_of: called with input \"" ^ Tactic_Def.tac2IDstr input ^ "\"");
21.285 + | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
21.286
21.287 fun rule2tac thy _ (Rule.Num_Calc (opID, _)) = Calculate (assoc_calc thy opID)
21.288 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
21.289 @@ -80,9 +321,139 @@
21.290 | rule2tac _ _ rule =
21.291 error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
21.292
21.293 - datatype T = datatype Tactic_Def.T
21.294 +(* tactics for for internal use, compare "input" for user at the front-end.
21.295 + tac_ contains results from check in 'fun applicable_in'.
21.296 + This is useful for costly results, e.g. from rewriting;
21.297 + however, these results might be changed by Scripts like
21.298 + " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
21.299 + " eq = (Rewrite_Set equival_trans False) eq;" ^
21.300 + TODO.WN120106 ANALOGOUSLY TO Substitute':
21.301 + So tac_ contains the term t the result was calculated from
21.302 + in order to compare t with t' possibly changed by "Expr "
21.303 + and re-calculate result if t<>t'
21.304 + TODO.WN161219: replace *every* cterm' by term
21.305 +*)
21.306 + datatype T =
21.307 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
21.308 + | Add_Relation' of Rule.cterm' * Model.itm list
21.309 + | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
21.310 + * tactic Apply_Method metID
21.311 + * formula term *)
21.312 + Celem.metID * (* key for KEStore *)
21.313 + term option * (* the first formula of Calc.T. TODO: rm option *)
21.314 + Istate_Def.T * (* for the newly started program *)
21.315 + Proof.context (* for the newly started program *)
21.316 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
21.317 + | Begin_Sequ' | Begin_Trans' of term
21.318 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
21.319 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
21.320 + | End_Sequ' | End_Trans' of Selem.result
21.321 + | End_Ruleset' of term | End_Intersect' of term | End_Proof''
21.322 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
21.323 + | CAScmd' of term
21.324 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
21.325 + | Check_Postcond' of Celem.pblID *
21.326 + term (* returnvalue of program in solve *)
21.327 + | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
21.328 + term * (* (1) the current formula: [x=1,x=...] *)
21.329 + string * (* (2) the pred from Check_elementwise *)
21.330 + Selem.result (* (3) composed from (1) and (2): {x. pred} *)
21.331 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
21.332
21.333 -val string_of = Tactic_Def.string_of
21.334 + | Derive' of Rule.rls
21.335 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
21.336 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
21.337 + | End_Detail' of Selem.result
21.338 +
21.339 + | Empty_Tac_
21.340 + | Free_Solve'
21.341 +
21.342 + | Init_Proof' of Rule.cterm' list * Celem.spec
21.343 + | Model_Problem' of (* first step in specifying *)
21.344 + Celem.pblID * (* key into KEStore *)
21.345 + Model.itm list * (* the 'untouched' pbl *)
21.346 + Model.itm list (* the casually completed met *)
21.347 + | Or_to_List' of term * term
21.348 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
21.349 + | Refine_Tacitly' of
21.350 + Celem.pblID * (* input *)
21.351 + Celem.pblID * (* the refined from applicable_in *)
21.352 + Rule.domID * (* from new pbt?! filled in specify *)
21.353 + Celem.metID * (* from new pbt?! filled in specify *)
21.354 + Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
21.355 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
21.356 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
21.357 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
21.358 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
21.359 +
21.360 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
21.361 + | Specify_Problem' of Celem.pblID *
21.362 + (bool * (* matches *)
21.363 + (Model.itm list * (* ppc *)
21.364 + (bool * term) list)) (* preconditions marked true/false *)
21.365 + | Specify_Theory' of Rule.domID
21.366 + | Subproblem' of
21.367 + Celem.spec *
21.368 + (Model.ori list) * (* filled in associate Subproblem' *)
21.369 + term * (* filled -"-, headline of calc-head *)
21.370 + Selem.fmz_ * (* string list from arguments *)
21.371 + Proof.context * (* for specify-phase *)
21.372 + term (* Subproblem (thyID, pbl) OR cascmd *)
21.373 + | Substitute' of
21.374 + Rule.rew_ord_ * (* for re-calculation *)
21.375 + Rule.rls * (* for re-calculation *)
21.376 + Selem.subte * (* the 'substitution': terms of type bool *)
21.377 + term * (* to be substituted into *)
21.378 + term (* resulting from the substitution *)
21.379 + | Tac_ of theory * string * string * string
21.380 + | Take' of term
21.381 +
21.382 +fun string_of ma = case ma of
21.383 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
21.384 + | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
21.385 + | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
21.386 + strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
21.387 + | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
21.388 + | Add_Given' _ => "Add_Given' "(*^cterm'*)
21.389 + | Del_Given' _ => "Del_Given' "(*^cterm'*)
21.390 + | Add_Find' _ => "Add_Find' "(*^cterm'*)
21.391 + | Del_Find' _ => "Del_Find' "(*^cterm'*)
21.392 + | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
21.393 + | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
21.394 +
21.395 + | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
21.396 + | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
21.397 + spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
21.398 + | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
21.399 + Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
21.400 +
21.401 + | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
21.402 + | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
21.403 + (spair2str (strs2str pblID, Rule.term2str scval))
21.404 +
21.405 + | Free_Solve' => "Free_Solve'"
21.406 +
21.407 + | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
21.408 + | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
21.409 + | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
21.410 + | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
21.411 + "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
21.412 + | End_Detail' _ => "End_Detail' xxx"
21.413 + | Detail_Set' _ => "Detail_Set' xxx"
21.414 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
21.415 +
21.416 + | Derive' rls => "Derive' " ^ Rule.id_rls rls
21.417 + | Calculate' _ => "Calculate' "
21.418 + | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
21.419 +
21.420 + | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
21.421 + | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
21.422 + "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
21.423 + | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
21.424 +
21.425 + | Empty_Tac_ => "Empty_Tac_"
21.426 + | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
21.427 + | _ => "string_of not impl. for arg";
21.428
21.429 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
21.430 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
21.431 @@ -116,7 +487,7 @@
21.432 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
21.433 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
21.434 | input_from_T Empty_Tac_ = Empty_Tac
21.435 - | input_from_T m = raise ERROR (": not impl. for "^(Tactic_Def.string_of m));
21.436 + | input_from_T m = raise ERROR (": not impl. for "^(string_of m));
21.437
21.438 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
21.439 | res (Rewrite' (_, _, _, _, _, _, res)) = res
21.440 @@ -128,7 +499,7 @@
21.441 | res (Take' t) = (t, [])
21.442 | res (Substitute' (_, _, _, _, t)) = (t, [])
21.443 | res (Or_to_List' (_, t)) = (t, [])
21.444 - | res m = raise ERROR ("result: not impl.for " ^ Tactic_Def.string_of m)
21.445 + | res m = raise ERROR ("result: not impl.for " ^ string_of m)
21.446
21.447 (*fun result m = (fst o res) m; TODO*)
21.448 fun result tac = (fst o res) tac;
22.1 --- a/src/Tools/isac/MathEngine/detail-step.sml Wed Apr 01 10:24:13 2020 +0200
22.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Wed Apr 01 12:42:39 2020 +0200
22.3 @@ -7,8 +7,8 @@
22.4
22.5 signature DETAIL_STEP =
22.6 sig
22.7 - val go : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
22.8 - val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
22.9 + val go : Ctree.ctree -> Pos.pos' -> string * Ctree.ctree * Pos.pos'
22.10 + val detailrls : Ctree.ctree -> Pos.pos' -> string * Ctree.ctree * Pos.pos'
22.11 end
22.12
22.13 (**)
22.14 @@ -21,7 +21,7 @@
22.15 (* aux.fun for detailrls with Rrls, reverse rewriting *)
22.16 fun rul_terms_2nds _ nds _ [] = nds
22.17 | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
22.18 - (append_atomic [] (NONE(*guessed*), (Istate.e_istate, ContextC.e_ctxt)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
22.19 + (append_atomic [] (NONE(*guessed*), (Istate.empty, ContextC.empty)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
22.20 (rul_terms_2nds thy nds t' rts);
22.21
22.22 (* detail steps done internally by Rewrite_Set* into Ctree
23.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Apr 01 10:24:13 2020 +0200
23.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Apr 01 12:42:39 2020 +0200
23.3 @@ -7,8 +7,8 @@
23.4
23.5 signature FETCH_TACTICS =
23.6 sig
23.7 - val from_prog : Ctree.ctree -> Ctree.pos' -> Tactic.input list
23.8 - val specific_from_prog : Ctree.ctree -> Ctree.pos' -> Tactic.input list
23.9 + val from_prog : Ctree.ctree -> Pos.pos' -> Tactic.input list
23.10 + val specific_from_prog : Ctree.ctree -> Pos.pos' -> Tactic.input list
23.11 end
23.12
23.13 (**)
24.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 01 10:24:13 2020 +0200
24.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 01 12:42:39 2020 +0200
24.3 @@ -7,17 +7,17 @@
24.4
24.5 signature MATH_ENGINE =
24.6 sig
24.7 - val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list ->
24.8 - Solve.auto -> string * Ctree.pos' list * (Calc.T)
24.9 + val autocalc : Pos.pos' list -> Pos.pos' -> (Calc.T) * Generate.taci list ->
24.10 + Solve.auto -> string * Pos.pos' list * (Calc.T)
24.11
24.12 - val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
24.13 - val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
24.14 - val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list
24.15 - val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24.16 + val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
24.17 + val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list
24.18 + val context_met : Celem.metID -> Ctree.ctree -> Pos.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list
24.19 + val context_pbl : Celem.pblID -> Ctree.ctree -> Pos.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24.20 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.21 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.22 val set_theory : Rule.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.23 - val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24.24 + val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24.26 (*NONE*)
24.27 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25.1 --- a/src/Tools/isac/MathEngine/solve.sml Wed Apr 01 10:24:13 2020 +0200
25.2 +++ b/src/Tools/isac/MathEngine/solve.sml Wed Apr 01 12:42:39 2020 +0200
25.3 @@ -9,10 +9,10 @@
25.4 | CompleteToSubpbl | Steps of int
25.5 val autoord : auto -> int
25.6
25.7 - val all_solve : auto -> Ctree.pos' list -> Calc.T ->
25.8 - string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))
25.9 + val all_solve : auto -> Pos.pos' list -> Calc.T ->
25.10 + string * Pos.pos' list * (Ctree.ctree * (int list * Pos.pos_))
25.11 val complete_solve :
25.12 - auto -> Ctree.pos' list -> Calc.T -> string * Ctree.pos' list * Calc.T
25.13 + auto -> Pos.pos' list -> Calc.T -> string * Pos.pos' list * Calc.T
25.14
25.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25.16 (*NONE*)
25.17 @@ -87,7 +87,7 @@
25.18 let
25.19 val (_, _, mI) = get_obj g_spec pt p
25.20 val ctxt = get_ctxt pt pos
25.21 - val (_, (_, c', ptp)) = LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
25.22 + val (_, (_, c', ptp)) = LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ctxt)) (Istate.empty, ctxt) ptp
25.23 in
25.24 complete_solve auto (c @ c') ptp
25.25 end;
26.1 --- a/src/Tools/isac/MathEngine/states.sml Wed Apr 01 10:24:13 2020 +0200
26.2 +++ b/src/Tools/isac/MathEngine/states.sml Wed Apr 01 12:42:39 2020 +0200
26.3 @@ -143,7 +143,7 @@
26.4 (Celem.calcID * (* the id unique for a calculation *)
26.5 (Chead.calcstate * (* the interpreter state *)
26.6 (Celem.iterID * (* 1 sets the 'active formula': a calc. can have several visitors*)
26.7 - Ctree.pos' (* for iterator of a user *)
26.8 + Pos.pos' (* for iterator of a user *)
26.9 (* TODO iterID * pos' should go to java-frontend *)
26.10 ) list)) list);
26.11
26.12 @@ -184,7 +184,7 @@
26.13 *)
26.14 (* add users to a calcstate *)
26.15 fun get_iterID (cI: Celem.calcID)
26.16 - (p: (Celem.calcID * (Chead.calcstate * (Celem.iterID * Ctree.pos') list)) list) =
26.17 + (p: (Celem.calcID * (Chead.calcstate * (Celem.iterID * Pos.pos') list)) list) =
26.18 case assoc (p, cI) of
26.19 NONE => error ("get_iterID: no iterID " ^ (string_of_int cI))
26.20 | SOME (_, us) => (new_key us 1): Celem.iterID;
26.21 @@ -315,7 +315,7 @@
26.22 fun upd_ipos (uI:iterID) (pI:calcID) (ip:pos') =
26.23 let val (_, calc) = get_state uI pI
26.24 in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*)
26.25 -fun upd_ipos (cI: Celem.calcID) (uI: Celem.iterID) (ip: Ctree.pos') = Synchronized.change states
26.26 +fun upd_ipos (cI: Celem.calcID) (uI: Celem.iterID) (ip: Pos.pos') = Synchronized.change states
26.27 (fn s => case assoc (s, cI) of
26.28 NONE =>
26.29 error ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent")
27.1 --- a/src/Tools/isac/MathEngine/step.sml Wed Apr 01 10:24:13 2020 +0200
27.2 +++ b/src/Tools/isac/MathEngine/step.sml Wed Apr 01 12:42:39 2020 +0200
27.3 @@ -14,7 +14,7 @@
27.4 *)
27.5 signature STEP =
27.6 sig
27.7 - val do_next: Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
27.8 + val do_next: Pos.pos' -> Chead.calcstate -> string * Chead.calcstate'
27.9 val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'
27.10 (*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate'
27.11 TODO --------------------------------------"----------> ?????? Calc.T
27.12 @@ -43,7 +43,7 @@
27.13 case tac of
27.14 Tactic.Apply_Method mI =>
27.15 (*vvvvvvvvvv-------------------------------------------------------------- solve-phase *)
27.16 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt))
27.17 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
27.18 ist_ctxt (pt, (p, p_'))
27.19 | _ => ("dummy", Step_Specify.by_tactic_input tac (pt, (p, p_')))
27.20 end
28.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 01 10:24:13 2020 +0200
28.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 01 12:42:39 2020 +0200
28.3 @@ -8,9 +8,9 @@
28.4 sig
28.5 exception PTREE of string
28.6 datatype appl = Appl of Tactic.T | Notappl of string
28.7 - val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> appl
28.8 + val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> appl
28.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
28.10 - val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T
28.11 + val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
28.12 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28.13 val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
28.14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28.15 @@ -128,7 +128,7 @@
28.16 fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))
28.17 | applicable_in (p, p_) pt Tactic.Model_Problem =
28.18 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.19 - then Notappl ((Tactic.tac2str Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
28.20 + then Notappl ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
28.21 else
28.22 let
28.23 val pI' = case get_obj I pt p of
28.24 @@ -139,7 +139,7 @@
28.25 in Appl (Tactic.Model_Problem' (pI', pbl, [])) end
28.26 | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) =
28.27 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.28 - then Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
28.29 + then Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
28.30 else
28.31 let
28.32 val oris = case get_obj I pt p of
28.33 @@ -149,11 +149,11 @@
28.34 case Specify.refine_ori oris pI of
28.35 SOME pblID =>
28.36 Appl (Tactic.Refine_Tacitly' (pI, pblID, Rule.e_domID, Celem.e_metID, [](*filled in specify*)))
28.37 - | NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not applicable")
28.38 + | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
28.39 end
28.40 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
28.41 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.42 - then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
28.43 + then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
28.44 else
28.45 let
28.46 val (dI, dI', itms) = case get_obj I pt p of
28.47 @@ -163,45 +163,45 @@
28.48 val thy = if dI' = Rule.e_domID then dI else dI';
28.49 in
28.50 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
28.51 - NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
28.52 + NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
28.53 | SOME (rf as (pI', _)) =>
28.54 if pI' = pI
28.55 - then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
28.56 + then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
28.57 else Appl (Tactic.Refine_Problem' rf)
28.58 end
28.59 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
28.60 | applicable_in (p, p_) pt (Tactic.Add_Given ct') =
28.61 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.62 - then Notappl ((Tactic.tac2str (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.63 + then Notappl ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.64 else Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
28.65 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
28.66 | applicable_in (p, p_) pt (Tactic.Del_Given ct') =
28.67 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.68 - then Notappl ((Tactic.tac2str (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.69 + then Notappl ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.70 else Appl (Tactic.Del_Given' ct')
28.71 | applicable_in (p, p_) pt (Tactic.Add_Find ct') =
28.72 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.73 - then Notappl ((Tactic.tac2str (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.74 + then Notappl ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.75 else Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
28.76 | applicable_in (p, p_) pt (Tactic.Del_Find ct') =
28.77 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.78 - then Notappl ((Tactic.tac2str (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.79 + then Notappl ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.80 else Appl (Tactic.Del_Find' ct')
28.81 | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =
28.82 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.83 - then Notappl ((Tactic.tac2str (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.84 + then Notappl ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.85 else Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
28.86 | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =
28.87 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.88 - then Notappl ((Tactic.tac2str (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.89 + then Notappl ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
28.90 else Appl (Tactic.Del_Relation' ct')
28.91 | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =
28.92 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.93 - then Notappl ((Tactic.tac2str (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
28.94 + then Notappl ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
28.95 else Appl (Tactic.Specify_Theory' dI)
28.96 | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) =
28.97 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.98 - then Notappl ((Tactic.tac2str (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
28.99 + then Notappl ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
28.100 else
28.101 let
28.102 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of
28.103 @@ -218,11 +218,11 @@
28.104 end
28.105 | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =
28.106 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.107 - then Notappl ((Tactic.tac2str (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
28.108 + then Notappl ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
28.109 else Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
28.110 | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =
28.111 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
28.112 - then Notappl ((Tactic.tac2str (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
28.113 + then Notappl ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
28.114 else
28.115 let
28.116 val (dI, pI, probl, ctxt) = case get_obj I pt p of
28.117 @@ -230,7 +230,7 @@
28.118 | _ => error "applicable_in Apply_Method: uncovered case get_obj"
28.119 val {where_, ...} = Specify.get_pbt pI
28.120 val pres = map (Model.mk_env probl |> subst_atomic) where_
28.121 - val ctxt = if ContextC.is_e_ctxt ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
28.122 + val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
28.123 then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
28.124 else ctxt
28.125 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
28.126 @@ -238,17 +238,17 @@
28.127 Implement after all tests are running, since this changes
28.128 overall system behavior*)
28.129 in
28.130 - Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.e_istate (*filled in solve*), ctxt))
28.131 + Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
28.132 end
28.133 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
28.134 if member op = [Pbl, Met] p_
28.135 - then Notappl ((Tactic.tac2str (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
28.136 + then Notappl ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
28.137 else Appl (Tactic.Check_Postcond' (pI, Rule.e_term))
28.138 | applicable_in _ _ (Tactic.Take str) = Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
28.139 | applicable_in _ _ (Tactic.Free_Solve) = Appl (Tactic.Free_Solve') (* always applicable *)
28.140 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) =
28.141 if member op = [Pbl, Met] p_
28.142 - then Notappl ((Tactic.tac2str m)^" not for pos " ^ pos'2str (p, p_))
28.143 + then Notappl ((Tactic.input_to_string m)^" not for pos " ^ pos'2str (p, p_))
28.144 else
28.145 let
28.146 val pp = par_pblobj pt p;
28.147 @@ -272,7 +272,7 @@
28.148 end
28.149 | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') =
28.150 if member op = [Pbl, Met] p_
28.151 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
28.152 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
28.153 else
28.154 let
28.155 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
28.156 @@ -291,7 +291,7 @@
28.157 end
28.158 | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) =
28.159 if member op = [Pbl, Met] p_
28.160 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
28.161 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
28.162 else
28.163 let
28.164 val pp = par_pblobj pt p;
28.165 @@ -310,7 +310,7 @@
28.166 end
28.167 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) =
28.168 if member op = [Pbl, Met] p_
28.169 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
28.170 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
28.171 else
28.172 let
28.173 val pp = par_pblobj pt p;
28.174 @@ -330,7 +330,7 @@
28.175 end
28.176 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) =
28.177 if member op = [Pbl, Met] p_
28.178 - then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
28.179 + then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
28.180 else
28.181 let
28.182 val pp = par_pblobj pt p;
28.183 @@ -347,7 +347,7 @@
28.184 end
28.185 | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =
28.186 if member op = [Pbl, Met] p_
28.187 - then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
28.188 + then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
28.189 else
28.190 let
28.191 val pp = par_pblobj pt p
28.192 @@ -361,10 +361,10 @@
28.193 SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
28.194 | NONE => Notappl (rls^" not applicable")
28.195 end
28.196 - | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Ruleset)
28.197 + | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
28.198 | applicable_in (p, p_) pt (m as Tactic.Calculate op_) =
28.199 if member op = [Pbl, Met] p_
28.200 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
28.201 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
28.202 else
28.203 let
28.204 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
28.205 @@ -386,7 +386,7 @@
28.206 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
28.207 | applicable_in (p, p_) pt (m as Tactic.Substitute sube) =
28.208 if member op = [Pbl, Met] p_
28.209 - then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
28.210 + then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
28.211 else
28.212 let
28.213 val pp = par_pblobj pt p
28.214 @@ -413,29 +413,29 @@
28.215 | NONE => Notappl (Selem.sube2str sube ^ " not applicable")
28.216 end
28.217 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
28.218 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Apply_Assumption cts'))
28.219 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
28.220 (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
28.221 | applicable_in _ _ (Tactic.Take_Inst ct') =
28.222 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Take_Inst ct'))
28.223 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
28.224 | applicable_in (p, p_) _ (m as Tactic.Subproblem (domID, pblID)) =
28.225 if Pos.on_specification p_
28.226 then
28.227 - Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
28.228 + Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
28.229 else (*some fields filled later in LI*)
28.230 Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
28.231 - Rule.e_term, [], ContextC.e_ctxt, Auto_Prog.subpbl domID pblID))
28.232 + Rule.e_term, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
28.233 | applicable_in _ _ (Tactic.End_Subproblem) =
28.234 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Subproblem)
28.235 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
28.236 | applicable_in _ _ (Tactic.CAScmd ct') =
28.237 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.CAScmd ct'))
28.238 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
28.239 | applicable_in _ _ (Tactic.Split_And) =
28.240 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Split_And)
28.241 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
28.242 | applicable_in _ _ (Tactic.Conclude_And) =
28.243 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Conclude_And)
28.244 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
28.245 | applicable_in _ _ (Tactic.Split_Or) =
28.246 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Split_Or)
28.247 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
28.248 | applicable_in _ _ (Tactic.Conclude_Or) =
28.249 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Conclude_Or)
28.250 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
28.251 | applicable_in (p, p_) pt (Tactic.Begin_Trans) =
28.252 let
28.253 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
28.254 @@ -450,16 +450,16 @@
28.255 then Appl (Tactic.End_Trans' (get_obj g_result pt p))
28.256 else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
28.257 | applicable_in _ _ (Tactic.Begin_Sequ) =
28.258 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Begin_Sequ))
28.259 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
28.260 | applicable_in _ _ (Tactic.End_Sequ) =
28.261 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Sequ))
28.262 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
28.263 | applicable_in _ _ (Tactic.Split_Intersect) =
28.264 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Split_Intersect))
28.265 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
28.266 | applicable_in _ _ (Tactic.End_Intersect) =
28.267 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Intersect))
28.268 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
28.269 | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) =
28.270 if member op = [Pbl, Met] p_
28.271 - then Notappl ((Tactic.tac2str m) ^ " not for pos " ^ pos'2str (p, p_))
28.272 + then Notappl ((Tactic.input_to_string m) ^ " not for pos " ^ pos'2str (p, p_))
28.273 else
28.274 let
28.275 val pp = par_pblobj pt p;
28.276 @@ -477,7 +477,7 @@
28.277 end
28.278 | applicable_in (p, p_) pt Tactic.Or_to_List =
28.279 if member op = [Pbl, Met] p_
28.280 - then Notappl ((Tactic.tac2str Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
28.281 + then Notappl ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
28.282 else
28.283 let
28.284 val f = case p_ of
28.285 @@ -489,7 +489,7 @@
28.286 handle _ => Notappl ("'Or_to_List' not applicable to " ^ Rule.term2str f)
28.287 end
28.288 | applicable_in _ _ Tactic.Collect_Trues =
28.289 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Collect_Trues)
28.290 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
28.291 | applicable_in _ _ Tactic.Empty_Tac = Notappl "Empty_Tac is not applicable"
28.292 | applicable_in (p, p_) pt (Tactic.Tac id) =
28.293 let
28.294 @@ -518,11 +518,11 @@
28.295 | _ => Appl (Tactic.Tac_ (thy, Rule.term2str f, id, Rule.term2str f))
28.296 end
28.297 | applicable_in _ _ Tactic.End_Proof' = Appl Tactic.End_Proof''
28.298 - | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.tac2str m);
28.299 + | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.input_to_string m);
28.300
28.301 fun tac2tac_ pt p m =
28.302 case applicable_in p pt m of
28.303 Appl m' => m'
28.304 - | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.tac2str m);
28.305 + | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
28.306
28.307 end;
29.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 01 10:24:13 2020 +0200
29.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 01 12:42:39 2020 +0200
29.3 @@ -69,8 +69,8 @@
29.4 type calcstate
29.5 type calcstate'
29.6
29.7 - val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
29.8 - (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input
29.9 + val nxt_spec : Pos.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
29.10 + (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Pos.pos_ * Tactic.input
29.11
29.12 val reset_calchead : Calc.T -> Calc.T
29.13 val get_ocalhd : Calc.T -> Ctree.ocalhd
29.14 @@ -89,7 +89,7 @@
29.15 val show_pt : Ctree.ctree -> unit
29.16 val show_pt_tac : Ctree.ctree -> unit
29.17 val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list
29.18 - val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term * Tactic.input option) list
29.19 + val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
29.20
29.21 val match_ags : theory -> Celem.pat list -> term list -> Model.ori list
29.22 val match_ags_msg : Celem.pblID -> term -> term list -> unit
29.23 @@ -137,10 +137,10 @@
29.24 val chk_vars : term Model.ppc -> string * term list
29.25 val unbound_ppc : term Model.ppc -> term list
29.26 val is_complete_modspec : Calc.T -> bool
29.27 - val get_formress : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
29.28 - (string * Ctree.pos' * term) list
29.29 - val get_forms : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
29.30 - (string * Ctree.pos' * term) list
29.31 + val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
29.32 + (string * Pos.pos' * term) list
29.33 + val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
29.34 + (string * Pos.pos' * term) list
29.35 end
29.36
29.37 (**)
29.38 @@ -795,7 +795,7 @@
29.39 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
29.40 FIXME ..and dont abuse a tactic for that purpose*)
29.41 ([(Tactic.Tac msg, Tactic.Tac_ (Rule.Thy_Info_get_theory "Isac_Knowledge", msg,msg,msg),
29.42 - (e_pos', (Istate_Def.e_istate, ContextC.e_ctxt)))], [], ptp)
29.43 + (e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
29.44 end
29.45 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
29.46 let
29.47 @@ -1157,7 +1157,7 @@
29.48 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
29.49
29.50 fun postermtac2str (pos, t, SOME tac) =
29.51 - pos'2str pos ^ ", " ^ Rule.term2str t ^ "\n" ^ indent 10 ^ Tactic.tac2str tac
29.52 + pos'2str pos ^ ", " ^ Rule.term2str t ^ "\n" ^ indent 10 ^ Tactic.input_to_string tac
29.53 | postermtac2str (pos, t, NONE) =
29.54 pos'2str pos ^ ", " ^ Rule.term2str t
29.55 fun postermtacs2str pfts = (strs2str' o (map (curry op ^ "\n")) o (map postermtac2str)) pfts
30.1 --- a/src/Tools/isac/Specify/generate.sml Wed Apr 01 10:24:13 2020 +0200
30.2 +++ b/src/Tools/isac/Specify/generate.sml Wed Apr 01 12:42:39 2020 +0200
30.3 @@ -15,17 +15,17 @@
30.4 | PpcKF of pblmet * Model.item Model.ppc
30.5 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
30.6 val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T
30.7 - -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
30.8 + -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
30.9 val init_istate : Tactic.input -> term -> Istate_Def.T
30.10 val init_pbl : (string * (term * 'a)) list -> Model.itm list
30.11 val init_pbl' : (string * (term * term)) list -> Model.itm list
30.12 - val embed_deriv : taci list -> Calc.T -> Ctree.pos' list * (Calc.T) (* for inform.sml *)
30.13 + val embed_deriv : taci list -> Calc.T -> Pos.pos' list * (Calc.T) (* for inform.sml *)
30.14 val generate_hard : (* for solve.sml *)
30.15 - theory -> Tactic.T -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
30.16 - val generate : (Tactic.input * Tactic.T * (Ctree.pos' * (Istate_Def.T * Proof.context))) list ->
30.17 - Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
30.18 + theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
30.19 + val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->
30.20 + Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *)
30.21 val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Istate_Def.T * Proof.context ->
30.22 - Ctree.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
30.23 + Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
30.24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
30.25 val tacis2str : taci list -> string
30.26 val mout2str : mout -> string
30.27 @@ -63,7 +63,7 @@
30.28 in
30.29 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))
30.30 end
30.31 - | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.tac2str tac)
30.32 + | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.input_to_string tac)
30.33
30.34 (* a taci holds alle information required to build a node in the calc-tree;
30.35 a taci is assumed to be used efficiently such that the calc-tree
30.36 @@ -79,9 +79,9 @@
30.37 Tactic.T * (* for ctree generation *)
30.38 (pos' * (* after applying tac_, for ctree generation *)
30.39 (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
30.40 -val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate_Def.e_istate, ContextC.e_ctxt))): taci
30.41 +val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate_Def.empty, ContextC.empty))): taci
30.42 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
30.43 - "( " ^ Tactic.tac2str tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
30.44 + "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
30.45 Istate_Def.string_of istate ^ " ))"
30.46 fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
30.47
30.48 @@ -362,7 +362,7 @@
30.49 Frm => p | Res => lev_on p
30.50 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
30.51 in
30.52 - generate1 m' (Istate_Def.e_istate, ContextC.e_ctxt) (pt, (p, p_))
30.53 + generate1 m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))
30.54 end
30.55
30.56 (* tacis are in reverse order from do_next/specify_: last = fst to insert *)
31.1 --- a/src/Tools/isac/Specify/input-calchead.sml Wed Apr 01 10:24:13 2020 +0200
31.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Wed Apr 01 12:42:39 2020 +0200
31.3 @@ -7,7 +7,7 @@
31.4 sig
31.5 datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list
31.6 type imodel = iitem list
31.7 - type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec
31.8 + type icalhd = Pos.pos' * Rule.cterm' * imodel * Pos.pos_ * Celem.spec
31.9 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
31.10 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
31.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
31.12 @@ -73,7 +73,7 @@
31.13 val dtss = argl2dtss argl
31.14 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
31.15 val spec = (dI, pI, mI)
31.16 - val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt)
31.17 + val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
31.18 ([], Celem.e_spec) ([], Celem.e_spec, hdt, ctxt)
31.19 val pt = Ctree.update_spec pt [] spec
31.20 val pt = Ctree.update_pbl pt [] pits
31.21 @@ -96,10 +96,10 @@
31.22
31.23 (*calc-head as input*)
31.24 type icalhd =
31.25 - Ctree.pos' * (*the position of the calc-head in the calc-tree*)
31.26 + Pos.pos' * (*the position of the calc-head in the calc-tree*)
31.27 Rule.cterm' * (*the headline*)
31.28 imodel * (*the model (without Find) of the calc-head*)
31.29 - Ctree.pos_ * (*model belongs to Pbl or Met*)
31.30 + Pos.pos_ * (*model belongs to Pbl or Met*)
31.31 Celem.spec; (*specification: domID, pblID, metID*)
31.32 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
31.33
32.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed Apr 01 10:24:13 2020 +0200
32.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed Apr 01 12:42:39 2020 +0200
32.3 @@ -261,7 +261,7 @@
32.4
32.5 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
32.6
32.7 -fun prep_ori [] _ _ = ([], ContextC.e_ctxt)
32.8 +fun prep_ori [] _ _ = ([], ContextC.empty)
32.9 | prep_ori fmz thy pbt =
32.10 let
32.11 val ctxt = ContextC.initialise' thy fmz;
33.1 --- a/src/Tools/isac/Specify/specify.sml Wed Apr 01 10:24:13 2020 +0200
33.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Apr 01 12:42:39 2020 +0200
33.3 @@ -88,8 +88,8 @@
33.4 val dI = if dI = "" then Rule.theory2theory' thy else dI
33.5 val mI = if mI = [] then hd met else mI
33.6 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
33.7 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
33.8 - ([], (dI,pI,mI), hdl, ContextC.e_ctxt)
33.9 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
33.10 + ([], (dI,pI,mI), hdl, ContextC.empty)
33.11 val pt = update_spec pt [] (dI, pI, mI)
33.12 val pits = Generate.init_pbl' ppc
33.13 val pt = update_pbl pt [] pits
33.14 @@ -100,16 +100,16 @@
33.15 let
33.16 val {ppc, ...} = Specify.get_met mI
33.17 val dI = if dI = "" then "Isac_Knowledge" else dI
33.18 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI))
33.19 - ([], (dI, pI, mI), Rule.e_term, ContextC.e_ctxt)
33.20 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) ([], (dI, pI, mI))
33.21 + ([], (dI, pI, mI), Rule.e_term, ContextC.empty)
33.22 val pt = update_spec pt [] (dI, pI, mI)
33.23 val mits = Generate.init_pbl' ppc
33.24 val pt = update_met pt [] mits
33.25 in ((pt, ([], Met)), []) end
33.26 else (* new example, pepare for interactive modeling *)
33.27 let
33.28 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt)
33.29 - ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.e_ctxt)
33.30 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
33.31 + ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.empty)
33.32 in ((pt, ([], Pbl)), []) end
33.33 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
33.34 let (* both """"""""""""""""""""""""" either empty or complete *)
33.35 @@ -129,7 +129,7 @@
33.36 val hdl = case cas of
33.37 NONE => Auto_Prog.pblterm dI pI
33.38 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
33.39 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, pctxt) (fmz, (dI, pI, mI))
33.40 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) (fmz, (dI, pI, mI))
33.41 (pors, (dI, pI, mI), hdl, pctxt)
33.42 in
33.43 ((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
34.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Apr 01 10:24:13 2020 +0200
34.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Apr 01 12:42:39 2020 +0200
34.3 @@ -43,7 +43,7 @@
34.4 (*----------------------------------------------------------------*)
34.5 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
34.6 val (pos,c,_,pt) = Generate.generate1 tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
34.7 - in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
34.8 + in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)) end
34.9 | by_tactic_input (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
34.10 | by_tactic_input (Tactic.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
34.11 | by_tactic_input (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
34.12 @@ -66,7 +66,7 @@
34.13 Generate.generate1 (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
34.14 in
34.15 ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
34.16 - (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
34.17 + (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))
34.18 end
34.19 | NONE => ([], [], ptp)
34.20 end
34.21 @@ -84,7 +84,7 @@
34.22 let
34.23 val (pos,c,_,pt) = Generate.generate1 (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
34.24 in
34.25 - ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
34.26 + ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))
34.27 end
34.28 end
34.29 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
34.30 @@ -105,7 +105,7 @@
34.31 ((_, Pbl), c, _, pt) => (c, pt)
34.32 | _ => error ""
34.33 in
34.34 - ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
34.35 + ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))
34.36 end
34.37 (* transfers oris (not required in pbl) to met-model for script-env
34.38 FIXME.WN.8.03: application of several mIDs to SAME model? *)
34.39 @@ -124,7 +124,7 @@
34.40 val (pos, c, _, pt) =
34.41 Generate.generate1 (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
34.42 in
34.43 - ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
34.44 + ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))
34.45 end
34.46 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
34.47 let
34.48 @@ -142,7 +142,7 @@
34.49 in (*FIXXXME: check if met can still be parsed*)
34.50 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))
34.51 end
34.52 - | by_tactic_input m' _ = error ("by_tactic_input: not impl. for " ^ Tactic.tac2str m')
34.53 + | by_tactic_input m' _ = error ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')
34.54 (* was fun Math_Engine.nxt_specify_ *)
34.55
34.56
34.57 @@ -152,12 +152,12 @@
34.58 val thy = Celem.assoc_thy dI'
34.59 val (oris, ctxt) =
34.60 if dI' = Rule.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
34.61 - then ([], ContextC.e_ctxt)
34.62 + then ([], ContextC.empty)
34.63 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
34.64 (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
34.65 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) (fmz, spec')
34.66 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) (fmz, spec')
34.67 (oris, (dI',pI',mI'), Rule.e_term, ctxt)
34.68 - val pt = update_loc' pt [] (SOME (Istate_Def.e_istate, ctxt), NONE)
34.69 + val pt = update_loc' pt [] (SOME (Istate_Def.empty, ctxt), NONE)
34.70 in
34.71 case mI' of
34.72 ["no_met"] => ("Refine_Tacitly", ([], [], (pt, ([], Pbl))))
34.73 @@ -192,7 +192,7 @@
34.74 val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
34.75 val ((p,_), _, _, pt) =
34.76 Generate.generate1 (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
34.77 - (Istate_Def.Uistate, ContextC.e_ctxt) (pt, pos)
34.78 + (Istate_Def.Uistate, ContextC.empty) (pt, pos)
34.79 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
34.80 (* val (pbl, pre, _) = ([], [], false)*)
34.81 in
34.82 @@ -286,8 +286,8 @@
34.83 val dI = if dI = "" then Rule.theory2theory' thy else dI
34.84 val mI = if mI = [] then hd met else mI
34.85 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
34.86 - val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
34.87 - ([], (dI,pI,mI), hdl, ContextC.e_ctxt)
34.88 + val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
34.89 + ([], (dI,pI,mI), hdl, ContextC.empty)
34.90 val pt = update_spec pt [] (dI, pI, mI)
34.91 val pits = Generate.init_pbl' ppc
34.92 val pt = update_pbl pt [] pits
34.93 @@ -298,16 +298,16 @@
34.94 let
34.95 val {ppc, ...} = Specify.get_met mI
34.96 val dI = if dI = "" then "Isac_Knowledge" else dI
34.97 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt)
34.98 - ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term, ContextC.e_ctxt)
34.99 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
34.100 + ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term, ContextC.empty)
34.101 val pt = update_spec pt [] (dI, pI, mI)
34.102 val mits = Generate.init_pbl' ppc
34.103 val pt = update_met pt [] mits
34.104 in ((pt, ([], Met)), []) end
34.105 else (* new example, pepare for interactive modeling *)
34.106 let
34.107 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt)
34.108 - ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.e_ctxt)
34.109 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
34.110 + ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.empty)
34.111 in ((pt, ([], Pbl)), []) end
34.112 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
34.113 let (* both """"""""""""""""""""""""" either empty or complete *)
34.114 @@ -327,7 +327,7 @@
34.115 val hdl = case cas of
34.116 NONE => Auto_Prog.pblterm dI pI
34.117 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
34.118 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, pctxt)
34.119 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
34.120 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
34.121 in
34.122 ((pt, ([], Pbl)), fst3 (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
35.1 --- a/src/Tools/isac/TODO.thy Wed Apr 01 10:24:13 2020 +0200
35.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 01 12:42:39 2020 +0200
35.3 @@ -38,43 +38,53 @@
35.4 \item xxx
35.5 \item xxx
35.6 \item xxx
35.7 + \item xxx
35.8 + \item xxx
35.9 + \item xxx
35.10 + \item xxx
35.11 + \item xxx
35.12 + \item xxx
35.13 + \item xxx
35.14 + \item xxx
35.15 + \item xxx
35.16 + \item xxx
35.17 + \item xxx
35.18 + \item xxx
35.19 + \item xxx
35.20 + \item xxx
35.21 + \item xxx
35.22 + \item xxx
35.23 + \item xxx
35.24 + \item xxx
35.25 + \item Istate_Def.empty -> Istate.empty
35.26 + \item xxx
35.27 + \item xxx
35.28 + \item xxx
35.29 + \item distribute test/../scrtools.sml: WAIT FOR FINAL CLEANUP OF src/../Interpret
35.30 + \item cleanup test-files: test/.. tools.sml, atools.sml, ...
35.31 + \item xxx
35.32 + \item xxx
35.33 + \end{itemize}
35.34 +\<close>
35.35 +subsection \<open>Postponed from current changeset\<close>
35.36 +text \<open>
35.37 + \begin{itemize}
35.38 + \item LI.do_next (*TODO RM..*) ???
35.39 + \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
35.40 + \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
35.41 + \item get_ctxt_LI should replace get_ctxt
35.42 + \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
35.43 + \item rename Base_Tool.thy <--- Base_Tools
35.44 + \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
35.45 + \item rename field scr in meth
35.46 \item DEL double code: nxt_specify_init_calc IN specify.sml + step-specify.sml
35.47 \item xxx
35.48 - \item associate: drop ctxt from arg.+ return
35.49 \item xxx
35.50 \item xxx
35.51 \item xxx
35.52 \item xxx
35.53 \item xxx
35.54 \item xxx
35.55 - \item in check_leaf SEPARATE tracing
35.56 - collect all trace_LI --> Trace_LI
35.57 - trace_LI: replace ' by " in writeln
35.58 - \item xxx
35.59 - \item xxx
35.60 - \item relocations + renamings
35.61 - \begin{itemize}
35.62 - \item Rule.terms2str -> TermC.s_to_string
35.63 - Tactic_Def.tac2str -> Tactic_Def.input_to_string
35.64 - \item xxx
35.65 - \item xxx
35.66 - \item xxx
35.67 - \item xxx
35.68 - \end{itemize}
35.69 - \item xxx
35.70 - \item cleanup test-files
35.71 - \begin{itemize}
35.72 - \item test/.. tools.sml, atools.sml, ...
35.73 - \item xxx
35.74 - \item xxx
35.75 - \item xxx
35.76 - \item xxx
35.77 - \end{itemize}
35.78 - \item xxx
35.79 - \item see in Test_Some/300- (*TODO: DOUBLE subst, DROP ONE*)
35.80 - \item ? improve sig. eval_leaf E a v t -> (E, (a, v)) t
35.81 - \item xxx
35.82 - \item xxx
35.83 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
35.84 there it is Free ("Subproblem", "char list \<times> ..
35.85 instead of Const (|???.Subproblem", "char list \<times> ..
35.86 @@ -100,42 +110,6 @@
35.87 \<close>
35.88 \item xxx
35.89 \item xxx
35.90 - \item LI.locate_input_term cleanup, case ONLY
35.91 - \item xxx
35.92 - \item revert 9ef6e9e88178 (separate Tactic / Tactic_Def),
35.93 - because tactic.sml after ctree.sml doesn't gain much !
35.94 - ?Tactic.input -> Calc.tactic ?
35.95 - \item xxx
35.96 - \item xxx
35.97 - \item collect from_pblobj_or_detail*,
35.98 - -> Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
35.99 - \item init_istate ?-> Detail_Rls?
35.100 - \item xxx
35.101 - \item rename Ctree.pos' --> Pos.pos', type decl duplicate? delete, separate!
35.102 - \item xxx
35.103 - \item Istate_Def.e_istate -> Istate.empty
35.104 - \item xxx
35.105 - \item xxx
35.106 - \item xxx
35.107 - \item distribute test/../scrtools.sml: WAIT FOR FINAL CLEANUP OF src/../Interpret
35.108 - \item xxx
35.109 - \item xxx
35.110 - \end{itemize}
35.111 -\<close>
35.112 -subsection \<open>Postponed from current changeset\<close>
35.113 -text \<open>
35.114 - \begin{itemize}
35.115 - \item LI.do_next (*TODO RM..*) ???
35.116 - \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
35.117 - \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
35.118 - \item get_ctxt_LI should replace get_ctxt
35.119 - \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
35.120 - \item rename Base_Tool.thy <--- Base_Tools
35.121 - \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
35.122 - \item rename field scr in meth
35.123 - \item xxx
35.124 - \item xxx
35.125 - \item xxx
35.126 \item cleanup fun me:
35.127 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
35.128 | me*) (_, tac) p _(*NEW remove*) pt =
35.129 @@ -221,6 +195,8 @@
35.130 text \<open>
35.131 \begin{itemize}
35.132 \item xxx
35.133 + \item revisit bootstrap Calcelements. rule->calcelems->termC
35.134 + would be nice, but is hard: Rule.terms2str -> TermC.s_to_string
35.135 \item xxx
35.136 \item replace all Ctree.update_* with Ctree.cupdate_problem
35.137 \item xxx
35.138 @@ -416,7 +392,7 @@
35.139 \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
35.140 \item xxx
35.141 \item unify args to Ctree.state (pt, p)
35.142 - \item fun update_env .. repl_env \<rightarrow>update_istate
35.143 + \item fun update_env .. repl_env \<rightarrow>updatempty
35.144 \item xxx
35.145 \item xxx
35.146 \item xxx
35.147 @@ -632,7 +608,7 @@
35.148 \item ?OK Test_Isac_Short with
35.149 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
35.150 instead
35.151 - LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp
35.152 + LI.by_tactic tac (Istate.empty, ContextC.empty) ptp
35.153 in step-solve ?
35.154 \item xxx
35.155 \item test from last CS with outcommented re-def of code ->
36.1 --- a/src/Tools/isac/Test_Code/test-code.sml Wed Apr 01 10:24:13 2020 +0200
36.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Apr 01 12:42:39 2020 +0200
36.3 @@ -9,9 +9,9 @@
36.4 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
36.5 val f2str : Generate.mout -> Rule.cterm'
36.6 val TESTg_form : Calc.T -> Generate.mout
36.7 - val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
36.8 - val me : Tactic.input -> Ctree.pos' -> NEW -> Ctree.ctree ->
36.9 - Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
36.10 + val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
36.11 + val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
36.12 + Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
36.13 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
36.14 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
36.15 Calc.T * Tactic.input * Generate.mout
36.16 @@ -127,7 +127,7 @@
36.17 | me*) (pt, p) tac trace =
36.18 let
36.19 val _ = if quiet tac then () else
36.20 - writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.tac2str tac ^ " ==================================");
36.21 + writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
36.22 val (pt', p') =
36.23 (*Step.by_tactic is here for testing by me; do_next would suffice for doing steps*)
36.24 case Step.by_tactic tac (pt, p) of
36.25 @@ -151,7 +151,7 @@
36.26 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
36.27 | _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
36.28 val _ = if quiet tac then () else
36.29 - writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.tac2str tac'' ^ "----------------------------------");
36.30 + writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");
36.31 val _ = trace (pt'', p'') tac
36.32 in
36.33 ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))
37.1 --- a/test/Tools/isac/CalcElements/contextC.sml Wed Apr 01 10:24:13 2020 +0200
37.2 +++ b/test/Tools/isac/CalcElements/contextC.sml Wed Apr 01 12:42:39 2020 +0200
37.3 @@ -163,7 +163,7 @@
37.4 (*+*)if p = ([3], Res) andalso f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
37.5 (*+*)then
37.6 (*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
37.7 -(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))
37.8 +(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
37.9 (*+*)else error "1. Subproblem -- call changed";
37.10
37.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
37.12 @@ -182,7 +182,7 @@
37.13 if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"
37.14 then
37.15 ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
37.16 - | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))
37.17 + | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
37.18 else error "xxx";
37.19
37.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
38.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 10:24:13 2020 +0200
38.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 12:42:39 2020 +0200
38.3 @@ -74,7 +74,7 @@
38.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
38.5 val ctxt = get_ctxt pt po;
38.6
38.7 -(*generate1 m (e_istate, ctxt) (p,p_) pt;
38.8 +(*generate1 m (Istate.empty, ctxt) (p,p_) pt;
38.9 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
38.10 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
38.11 assoc_thy;
39.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 10:24:13 2020 +0200
39.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 12:42:39 2020 +0200
39.3 @@ -251,13 +251,13 @@
39.4 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
39.5 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
39.6
39.7 -(*+*)if map tac2str (specific_from_prog pt p) =
39.8 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
39.9 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
39.10 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
39.11 then () else error "specific_from_prog ([1], Res) CHANGED";
39.12 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
39.13
39.14 -(*+*)if map tac2str (specific_from_prog pt p) =
39.15 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
39.16 ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
39.17 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
39.18 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
39.19 @@ -630,7 +630,7 @@
39.20 ([3,2,1], Res), x = 0 + 1
39.21 . . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
39.22 ([3,2,2], Res), x = 1
39.23 -. . . . . . . . . . tac2str not impl. for ?!,
39.24 +. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
39.25 ([3,2], Res), x = 1
39.26 . . . . . . . . . . Check_Postcond ["LINEAR","univariate","equation","test"],
39.27 ([3], Res), [x = 1]
40.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 10:24:13 2020 +0200
40.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 12:42:39 2020 +0200
40.3 @@ -134,7 +134,7 @@
40.4 *)
40.5
40.6 (* --vvv-- ausgeliehen von test-root-equ/sml *)
40.7 -val loc = e_istate;
40.8 +val loc = Istate.empty;
40.9 val (dI',pI',mI') =
40.10 ("Program",["sqroot-test","univariate","equation"],
40.11 ["Program","squ-equ-test2"]);
40.12 @@ -162,7 +162,7 @@
40.13 Empty_Tac ("[1,2]:{(a,b). f_x(a,b) ...",[]) Complete;
40.14 val pos = lev_up pos;
40.15 (*val pos = ([1])*)
40.16 -val (pt,_) = append_result pt pos e_istate ("[1#]:{(a,b). f_x(a,b) ...",[])
40.17 +val (pt,_) = append_result pt pos Istate.empty ("[1#]:{(a,b). f_x(a,b) ...",[])
40.18 Complete;
40.19
40.20 val pos = lev_on pos;
40.21 @@ -184,7 +184,7 @@
40.22
40.23 val pos = lev_up pos;
40.24 (*pos = ([3]) *)
40.25 -val (pt,_) = append_result pt pos e_istate ("[3#]:{(a,b). f_x ..} cup..",[])
40.26 +val (pt,_) = append_result pt pos Istate.empty ("[3#]:{(a,b). f_x ..} cup..",[])
40.27 Complete;
40.28 val pos = lev_on pos;
40.29 (*val pos = [4] : pos *)
40.30 @@ -219,11 +219,11 @@
40.31 "--- 1 ---";
40.32 val pos = lev_up pos;
40.33 (*pos = ([4,1,1,1]) *)
40.34 -val (pt,_) = append_result pt pos e_istate ("[4,1,1,1#]:3x^2 -3.",[])Complete;
40.35 +val (pt,_) = append_result pt pos Istate.empty ("[4,1,1,1#]:3x^2 -3.",[])Complete;
40.36 "--- 2 ---";
40.37 val pos = lev_up pos;
40.38 (*val pos = ([4,1,1]) *)
40.39 -val (pt,_) = append_result pt pos e_istate ("[4,1,1#]:found 3x^2 -3 ...",[])
40.40 +val (pt,_) = append_result pt pos Istate.empty ("[4,1,1#]:found 3x^2 -3 ...",[])
40.41 Complete;
40.42 "--- 3 ---";
40.43 val pos = lev_on pos;
41.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Apr 01 10:24:13 2020 +0200
41.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Apr 01 12:42:39 2020 +0200
41.3 @@ -202,7 +202,7 @@
41.4 (case f of
41.5 PpcKF (Problem [], {Given = [Incompl "solveFor", Correct "equality (320 + 128 * x + -16 * x ^^^ 2 = 0)"], ...}) => ()
41.6 | _ => error ("S.68, Bsp.: 40 PblObj changed"))
41.7 - | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ tac2str (snd nxt)));
41.8 + | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string (snd nxt)));
41.9
41.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
41.11 (* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
41.12 @@ -247,7 +247,7 @@
41.13 (*+*)if p = ([3], Res) andalso f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
41.14 (*+*)then
41.15 (*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
41.16 -(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))
41.17 +(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
41.18 (*+*)else error "1. Subproblem -- call changed";
41.19
41.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
41.21 @@ -266,7 +266,7 @@
41.22 if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"
41.23 then
41.24 ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
41.25 - | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))
41.26 + | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
41.27 else error "xxx";
41.28 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
41.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
42.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Wed Apr 01 10:24:13 2020 +0200
42.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Wed Apr 01 12:42:39 2020 +0200
42.3 @@ -66,9 +66,9 @@
42.4 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
42.5
42.6 val pt = EmptyPtree;
42.7 -val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term, e_ctxt) pt;
42.8 +val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], e_spec, e_term, ContextC.empty) pt;
42.9 val ctxt = get_obj g_ctxt pt [];
42.10 -if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
42.11 +if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
42.12
42.13 "-------------- check positions in miniscript --------------------";
42.14 "-------------- check positions in miniscript --------------------";
42.15 @@ -101,7 +101,7 @@
42.16 "ctree.sml-------------- cut_tree new (from ctree above)----------";
42.17 val (pt', cuts) = cut_tree pt ([1],Frm);
42.18 "ctree.sml-------------- cappend on complete ctree from above ----";
42.19 -val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
42.20 +val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (str2term "Inform[1]");
42.21 "----------------------------------------------------------------/";
42.22
42.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
42.24 @@ -417,7 +417,7 @@
42.25 "-------------- cappend (from ctree above)------------------------";
42.26 "-------------- cappend (from ctree above)------------------------";
42.27 "-------------- cappend (from ctree above)------------------------";
42.28 -val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
42.29 +val (pt',cuts) = cappend_form pt [3,2,1] Istate.empty (str2term "newnew");
42.30 if cuts = [([3, 2, 1], Res),
42.31 ([3, 2, 2], Res),
42.32 ([3, 2], Res),
42.33 @@ -430,7 +430,7 @@
42.34 term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
42.35 then () else error "ctree.sml: diff:behav. in cappend 1";
42.36
42.37 -val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
42.38 +val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (str2term "newform")
42.39 (Tac "test") (str2term "newresult",[]) Complete;
42.40 if cuts = [([3, 2, 1], Res), (*?????????????*)
42.41 ([3, 2, 2], Res),
42.42 @@ -469,7 +469,7 @@
42.43
42.44 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
42.45 val p = ([1], Frm);
42.46 -val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
42.47 +val (pt,cuts) = cappend_form pt (fst p) Istate.empty (str2term "x + 1 = 2");
42.48 val form = get_obj g_form pt (fst p);
42.49 val (res,_) = get_obj g_result pt (fst p);
42.50 if term2str form = "x + 1 = 2" andalso res = e_term then () else
42.51 @@ -480,7 +480,7 @@
42.52 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
42.53 val p = ([1], Res);
42.54 val (pt,cuts) =
42.55 - cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
42.56 + cappend_atomic pt (fst p) Istate.empty (str2term "x + 1 = 2")
42.57 Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
42.58 val form = get_obj g_form pt (fst p);
42.59 val (res,_) = get_obj g_result pt (fst p);
42.60 @@ -492,7 +492,7 @@
42.61 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
42.62 val p = ([2], Res);
42.63 val (pt,cuts) =
42.64 - cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
42.65 + cappend_atomic pt (fst p) Istate.empty (str2term "x + 1 + -1 * 2 = 0")
42.66 Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
42.67 val form = get_obj g_form pt (fst p);
42.68 val (res,_) = get_obj g_result pt (fst p);
42.69 @@ -504,7 +504,7 @@
42.70
42.71 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
42.72 val p = ([3], Pbl);
42.73 -val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term, e_ctxt);
42.74 +val (pt,cuts) = cappend_problem pt (fst p) Istate.empty e_fmz ([],e_spec,e_term, ContextC.empty);
42.75 if is_pblobj (get_obj I pt (fst p)) then () else
42.76 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
42.77 if not (existpt ((lev_on o fst) p) pt) then () else
42.78 @@ -514,7 +514,7 @@
42.79
42.80 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
42.81 val p = ([3, 1], Frm);
42.82 -val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
42.83 +val (pt,cuts) = cappend_form pt (fst p) Istate.empty (str2term "-1 + x = 0");
42.84 val form = get_obj g_form pt (fst p);
42.85 val (res,_) = get_obj g_result pt (fst p);
42.86 if term2str form = "-1 + x = 0" andalso res = e_term then () else
42.87 @@ -525,7 +525,7 @@
42.88 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
42.89 val p = ([3, 1], Res);
42.90 val (pt,cuts) =
42.91 - cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
42.92 + cappend_atomic pt (fst p) Istate.empty (str2term "-1 + x = 0")
42.93 Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
42.94 val form = get_obj g_form pt (fst p);
42.95 val (res,_) = get_obj g_result pt (fst p);
42.96 @@ -1158,7 +1158,7 @@
42.97 "---(2) on S(606)..S(608)--------";
42.98 (*========== inhibit exn AK110726 ==============================================
42.99 (* ERROR: Can't unify istate to istate * Proof.context *)
42.100 -val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
42.101 +val (pt', cuts) = cappend_atomic pt [1] Istate.empty (str2term "Inform[1]")
42.102 (Tac "test") (str2term "Inres[1]",[]) Complete;
42.103
42.104 (*default_print_depth 99;*)
42.105 @@ -1180,7 +1180,7 @@
42.106 show_pt pt';
42.107 "---(3) on S(606)..S(608)--------";
42.108 show_pt pt;
42.109 -val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
42.110 +val (pt', cuts) = cappend_atomic pt [2] Istate.empty (str2term "Inform[2]")
42.111 (Tac "test") (str2term "Inres[2]",[]) Complete;
42.112 (*default_print_depth 99;*)
42.113 cuts;
42.114 @@ -1217,8 +1217,8 @@
42.115 *)
42.116
42.117 "---(4) on S(606)..S(608)--------";
42.118 -val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
42.119 - ([],e_spec, str2term "Inhead[3]", e_ctxt);
42.120 +val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],e_spec)
42.121 + ([],e_spec, str2term "Inhead[3]", ContextC.empty);
42.122 (*default_print_depth 99;*)
42.123 cuts;
42.124 (*default_print_depth 3;*)
42.125 @@ -1243,7 +1243,7 @@
42.126 *)
42.127
42.128 "---(6-1) on S(606)..S(608)--------";
42.129 -val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
42.130 +val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (str2term "Inform[3,1]")
42.131 (Tac "test") (str2term "Inres[3,1]",[]) Complete;
42.132 (*default_print_depth 99;*)
42.133 cuts;
42.134 @@ -1269,7 +1269,7 @@
42.135 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
42.136
42.137 "---(6) on S(606)..S(608)--------";
42.138 -val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
42.139 +val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (str2term "Inform[3,2]")
42.140 (Tac "test") (str2term "Inres[3,2]",[]) Complete;
42.141 (*default_print_depth 99;*)
42.142 cuts;
42.143 @@ -1294,7 +1294,7 @@
42.144
42.145 "---(6++) on S(606)..S(608)--------";
42.146 (**)
42.147 -val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
42.148 +val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (str2term "Inform[3,2,1]")
42.149 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
42.150 (*default_print_depth 99;*)
42.151 cuts;
43.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 01 10:24:13 2020 +0200
43.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 01 12:42:39 2020 +0200
43.3 @@ -155,8 +155,8 @@
43.4 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
43.5 cas = NONE; (*true*)
43.6 val hdl = pblterm dI pI;
43.7 - val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
43.8 - (pors, (dI, pI, mI), hdl, ContextC.e_ctxt)
43.9 + val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
43.10 + (pors, (dI, pI, mI), hdl, ContextC.empty)
43.11 ;
43.12 "~~~~~ fun Step_Specify.by_tactic_input, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
43.13 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
44.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Apr 01 10:24:13 2020 +0200
44.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Apr 01 12:42:39 2020 +0200
44.3 @@ -20,8 +20,8 @@
44.4 val hdl =
44.5 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
44.6 | _ => error "Minisubplb/100-init-rootpbl.sml no headline"
44.7 -val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
44.8 - (pors, (dI, pI, mI), hdl, ContextC.e_ctxt)
44.9 +val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
44.10 + (pors, (dI, pI, mI), hdl, ContextC.empty)
44.11 ;((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Model_Problem (pt, ([], Pbl)))) : calcstate;
44.12
44.13 (* INVESTIGATE val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];*)
45.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 10:24:13 2020 +0200
45.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 12:42:39 2020 +0200
45.3 @@ -92,7 +92,7 @@
45.4 let val (f, a) = assoc_by_type f aas
45.5 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
45.6 val env = relate_args [] formals actuals;
45.7 - (*val _ = trace_istate env;*)
45.8 + (*val _ = tracIstate.empty env;*)
45.9 val {pre, prls, ...} = Specify.get_met metID;
45.10 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
45.11 val ctxt = ctxt |> ContextC.insert_assumptions pres;
46.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Apr 01 10:24:13 2020 +0200
46.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Apr 01 12:42:39 2020 +0200
46.3 @@ -46,9 +46,9 @@
46.4
46.5 val Apply_Method mI = (*case*) tac (*of*);
46.6 (*+*)val (_, (_, _, (pt'''', p''''))) =
46.7 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
46.8 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
46.9 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
46.10 - = ((Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)), ist_ctxt, ptp);
46.11 + = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
46.12 val {ppc, ...} = Specify.get_met mI;
46.13 val (itms, oris, probl) = case get_obj I pt p of
46.14 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
47.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 01 10:24:13 2020 +0200
47.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 01 12:42:39 2020 +0200
47.3 @@ -29,7 +29,7 @@
47.4
47.5 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
47.6 Step.by_tactic tac (pt, p) (*of*);
47.7 - get_ctxt pt'''' p'''' |> is_e_ctxt; (*should NOT be true after this step*)
47.8 + get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)
47.9 "~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
47.10 val Appl m = applicable_in p pt tac;
47.11 (*if*) Tactic.for_specify' m; (*false*)
47.12 @@ -125,10 +125,10 @@
47.13 = (check_tac1 cct ist (prog_tac, form_arg));
47.14
47.15 (*+*)val (pstate, ctxt, tac) = iss;
47.16 -(*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 should NOT return e_ctxt" else ();
47.17 +(*+*)if ContextC.is_empty ctxt then error "ERROR: scan_dn1 should NOT return ContextC.empty" else ();
47.18 "~~~~~ from fun scan_up1 HOL.Let(*1*), --------------------------------- NO return:"; val () = ();
47.19
47.20 -(*+*)if is_e_ctxt ctxt''''' then error "locate_input_tactic should NOT return e_ctxt" else ();
47.21 +(*+*)if ContextC.is_empty ctxt''''' then error "locate_input_tactic should NOT return ContextC.empty" else ();
47.22
47.23 "~~~~~ from fun locate_input_tactic \<longrightarrow>Step_Solve.by_tactic , return:"; val (LI.Safe_Step (istate, ctxt, tac))
47.24 = (Safe_Step (Pstate ist''''', ctxt''''', tac'_'''''));
47.25 @@ -142,14 +142,14 @@
47.26 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
47.27 (oris, (domID, pblID, metID), hdl, ctxt_specify);
47.28
47.29 -(*+*)if is_e_ctxt ctxt_specify then error "ERROR: generate1 should NOT get input e_ctxt" else ();
47.30 -(*+*)if (get_ctxt pt pos |> is_e_ctxt) then error "generate1 MUST store ctxt"
47.31 +(*+*)if ContextC.is_empty ctxt_specify then error "ERROR: generate1 should NOT get input ContextC.empty" else ();
47.32 +(*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "generate1 MUST store ctxt"
47.33 (*+*)else ();
47.34 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
47.35
47.36 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Model_Problem*)
47.37
47.38 -if p = ([3], Pbl) andalso not (get_ctxt pt p |> is_e_ctxt)
47.39 +if p = ([3], Pbl) andalso not (get_ctxt pt p |> ContextC.is_empty)
47.40 then
47.41 case nxt of (Model_Problem) => ()
47.42 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"
48.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Apr 01 10:24:13 2020 +0200
48.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Apr 01 12:42:39 2020 +0200
48.3 @@ -31,8 +31,8 @@
48.4 val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
48.5 (*//--1 begin step into relevant call ---------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-------\\
48.6 1 relevant for all Apply_Method *)
48.7 -(*+*)if get_ctxt pt p |> is_e_ctxt then error "ctxt no initialised by specify, PblObj{ctxt,...}" else ();
48.8 -(*+*)if get_ctxt pt p |> is_e_ctxt then error "ctxt NOT initialised by Subproblem'}" else ();
48.9 +(*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt no initialised by specify, PblObj{ctxt,...}" else ();
48.10 +(*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt NOT initialised by Subproblem'}" else ();
48.11 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
48.12
48.13 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
48.14 @@ -82,5 +82,5 @@
48.15 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
48.16
48.17 if p = ([3, 1], Frm) andalso f2str f = "-1 + x = 0" andalso
48.18 - tac2str nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
48.19 + Tactic.input_to_string nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
48.20 then () else error "Minisubpbl/400-start-meth-subpbl changed";
49.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Apr 01 10:24:13 2020 +0200
49.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Apr 01 12:42:39 2020 +0200
49.3 @@ -31,16 +31,16 @@
49.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
49.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*OKnxt = Apply_Method ["Test", "solve_linear"]*)
49.6 val (p'',_,f,nxt,_,pt'') = me nxt p [] pt; (*nxt = Rewrite_Set_Inst..OK isolate_bdv*);
49.7 -get_ctxt pt'' p'' |> is_e_ctxt; (*OKfalse*)
49.8 +get_ctxt pt'' p'' |> ContextC.is_empty; (*OKfalse*)
49.9 val ctxt = get_ctxt pt'' p'';
49.10 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
49.11 -get_loc pt'' p'' |> snd |> is_e_ctxt; (**OKfalse*)
49.12 +get_loc pt'' p'' |> snd |> ContextC.is_empty; (**OKfalse*)
49.13
49.14 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set "Test_simplify"*);
49.15 -get_ctxt pt p |> is_e_ctxt; (*false*)
49.16 +get_ctxt pt p |> ContextC.is_empty; (*false*)
49.17 val ctxt = get_ctxt pt p;
49.18 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
49.19 -get_loc pt p |> snd |> is_e_ctxt; (*false*)
49.20 +get_loc pt p |> snd |> ContextC.is_empty; (*false*)
49.21 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
49.22
49.23 val (pt'''', p'''') = (pt, p);
50.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Apr 01 10:24:13 2020 +0200
50.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Apr 01 12:42:39 2020 +0200
50.3 @@ -122,7 +122,7 @@
50.4 ([1,5], Res), x + (2 + -1) = 2
50.5 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
50.6 ([1,6], Res), 2 + -1 + x = 2
50.7 -. . . . . . . . . . tac2str not impl. for ?!,
50.8 +. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
50.9 ([1], Res), 2 + -1 + x = 2
50.10 . . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]
50.11 *)
51.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 01 10:24:13 2020 +0200
51.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 01 12:42:39 2020 +0200
51.3 @@ -260,9 +260,9 @@
51.4 val oris = prep_ori ctl thy
51.5 ((#ppc o get_pbt)
51.6 ["sqroot-test","univariate","equation","test"]);
51.7 -val loc = e_istate;
51.8 +val loc = Istate.empty;
51.9 val (pt,pos) = (e_ctree,[]);
51.10 -val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term, ContextC.e_ctxt)
51.11 +val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term, ContextC.empty)
51.12 val pt = update_branch pt [] TransitiveB;
51.13 (*
51.14 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
51.15 @@ -328,7 +328,7 @@
51.16 (*val pt = union_asm pt [] (map (rpair []) asm);*)
51.17
51.18 val pos = lev_up pos;
51.19 -val (pt,_) = append_result pt pos e_istate (str2term ct,[]) Complete;
51.20 +val (pt,_) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
51.21
51.22 val pos = lev_on pos;
51.23 val rls = ("Test_simplify"); val ctold = str2term ct;
51.24 @@ -361,7 +361,7 @@
51.25 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
51.26
51.27 val pos = lev_up pos;
51.28 -val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete;
51.29 +val (pt,pos) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
51.30 Ctree.get_assumptions pt ([],Res);
51.31
51.32 writeln (pr_ctree pr_short pt);
52.1 --- a/test/Tools/isac/OLDTESTS/script.sml Wed Apr 01 10:24:13 2020 +0200
52.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Apr 01 12:42:39 2020 +0200
52.3 @@ -275,7 +275,7 @@
52.4 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
52.5 val l0 = [];
52.6 " --------------- 1. ---------------------------------------------";
52.7 -val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete;
52.8 +val (pt,_) = cappend_atomic pt[1]Istate.empty e_term(Rewrite("test",""))(str2term ct,[])Complete;
52.9 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv"
52.10 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
52.11 *)