1.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Mon May 04 17:08:32 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Mon May 04 18:47:27 2020 +0200
1.3 @@ -8,13 +8,13 @@
1.4 val get_last_formula: CTbasic.state -> term
1.5 val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree
1.6 val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree
1.7 - val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =vvv= ? *)
1.8 - val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =^^^= ? *)
1.9 + val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =vvv= ? *)
1.10 + val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =^^^= ? *)
1.11 val update_metID : CTbasic.ctree -> Pos.pos -> Method.id -> CTbasic.ctree
1.12 - val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =vvv= ? *)
1.13 - val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =^^^= ? *)
1.14 + val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =vvv= ? *)
1.15 + val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =^^^= ? *)
1.16 val update_pblID : CTbasic.ctree -> Pos.pos -> Problem.id -> CTbasic.ctree
1.17 - val update_oris : CTbasic.ctree -> Pos.pos -> Model_Def.ori list -> CTbasic.ctree
1.18 + val update_oris : CTbasic.ctree -> Pos.pos -> Model_Def.o_model -> CTbasic.ctree
1.19 val update_orispec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree
1.20 val update_spec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree
1.21 val update_tac : CTbasic.ctree -> Pos.pos -> Tactic.input -> CTbasic.ctree
1.22 @@ -23,9 +23,9 @@
1.23 val cappend_form : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->
1.24 CTbasic.ctree * Pos.pos' list
1.25 val cappend_problem : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
1.26 - Celem.fmz -> Model_Def.ori list * Spec.T * term * Proof.context
1.27 + Celem.fmz -> Model_Def.o_model * Spec.T * term * Proof.context
1.28 -> CTbasic.ctree * Pos.pos' list
1.29 - val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.T * Model_Def.itm list * Model_Def.itm list * Proof.context
1.30 + val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.T * Model_Def.i_model * Model_Def.i_model * Proof.context
1.31 -> CTbasic.ctree * Pos.pos' list
1.32 val append_atomic : (* for solve.sml *)
1.33 Pos.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
1.34 @@ -42,8 +42,8 @@
1.35 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.36 val append_form: Pos.pos -> Istate_Def.T * Proof.context -> term -> CTbasic.ctree -> CTbasic.ctree
1.37 val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Celem.fmz ->
1.38 - Model_Def.ori list * Spec.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
1.39 - val update_problem: Pos.pos -> Spec.T * Model_Def.itm list * Model_Def.itm list * Proof.context
1.40 + Model_Def.o_model * Spec.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
1.41 + val update_problem: Pos.pos -> Spec.T * Model_Def.i_model * Model_Def.i_model * Proof.context
1.42 -> CTbasic.ctree -> CTbasic.ctree
1.43 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.44 end
2.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon May 04 17:08:32 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon May 04 18:47:27 2020 +0200
2.3 @@ -24,9 +24,9 @@
2.4 result: Celem.result,
2.5
2.6 fmz: Celem.fmz,
2.7 - origin: Model_Def.ori list * Spec.T * term,
2.8 - probl: Model_Def.itm list,
2.9 - meth: Model_Def.itm list,
2.10 + origin: Model_Def.o_model * Spec.T * term,
2.11 + probl: Model_Def.i_model,
2.12 + meth: Model_Def.i_model,
2.13 spec: Spec.T,
2.14 ctxt: Proof.context}
2.15 | PrfObj of
2.16 @@ -49,7 +49,7 @@
2.17 val get_nd : ctree -> Pos.pos -> ctree
2.18 val just_created_ : ppobj -> bool
2.19 val just_created : state -> bool
2.20 - val e_origin : Model_Def.ori list * Spec.T * term
2.21 + val e_origin : Model_Def.o_model * Spec.T * term
2.22
2.23 val is_pblobj : ppobj -> bool
2.24 val is_pblobj' : ctree -> Pos.pos -> bool
2.25 @@ -58,14 +58,14 @@
2.26 val g_spec : ppobj -> Spec.T
2.27 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
2.28 val g_form : ppobj -> term
2.29 - val g_pbl : ppobj -> Model_Def.itm list
2.30 - val g_met : ppobj -> Model_Def.itm list
2.31 + val g_pbl : ppobj -> Model_Def.i_model
2.32 + val g_met : ppobj -> Model_Def.i_model
2.33 val g_metID : ppobj -> Method.id
2.34 val g_result : ppobj -> Celem.result
2.35 val g_tac : ppobj -> Tactic.input
2.36 val g_domID : ppobj -> ThyC.id
2.37
2.38 - val g_origin : ppobj -> Model_Def.ori list * Spec.T * term
2.39 + val g_origin : ppobj -> Model_Def.o_model * Spec.T * term
2.40 val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context
2.41 val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T
2.42 val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context
2.43 @@ -77,7 +77,7 @@
2.44 val new_val : term -> Istate_Def.T -> Istate_Def.T
2.45 (* for calchead.sml *)
2.46 type cid = cellID list
2.47 - type ocalhd = bool * Pos.pos_ * term * Model_Def.itm list * (bool * term) list * Spec.T
2.48 + type ocalhd = bool * Pos.pos_ * term * Model_Def.i_model * (bool * term) list * Spec.T
2.49 datatype ptform = Form of term | ModSpec of ocalhd
2.50 val get_somespec' : Spec.T -> Spec.T -> Spec.T
2.51 exception PTREE of string;
2.52 @@ -205,12 +205,12 @@
2.53 ostate: ostate} (* Complete <=> result is OK *)
2.54 | PblObj of (* a step serving a whole specification-phase *)
2.55 {fmz : Celem.fmz, (* from init:FIXME never use this spec;-drop *)
2.56 - origin: (Model_Def.ori list) *(* from fmz+pbt+met for efficiently adding items to probl, meth *)
2.57 + origin: (Model_Def.o_model) *(* from fmz+pbt+met for efficiently adding items to probl, meth *)
2.58 Spec.T * (* updated by Refine_Tacitly *)
2.59 term, (* headline of calc-head, as calculated initially(!) *)
2.60 spec : Spec.T, (* explicitly input *)
2.61 - probl : Model_Def.itm list, (* itms explicitly input *)
2.62 - meth : Model_Def.itm list, (* itms automatically added to copy of probl *)
2.63 + probl : Model_Def.i_model, (* itms explicitly input *)
2.64 + meth : Model_Def.i_model, (* itms automatically added to copy of probl *)
2.65 ctxt : Proof.context, (* used while specifying this SubProblem *)
2.66 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *)
2.67 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
2.68 @@ -438,10 +438,10 @@
2.69 bool * (* ALL itms+preconds true *)
2.70 pos_ * (* model belongs to Problem | Method *)
2.71 term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*)
2.72 - Model_Def.itm list * (* model: given, find, relate *)
2.73 + Model_Def.i_model * (* model: given, find, relate *)
2.74 ((bool * term) list) *(* model: preconds *)
2.75 Spec.T; (* specification *)
2.76 -val e_ocalhd = (false, Und, TermC.empty, [Model_Def.e_itm], [(false, TermC.empty)], Spec.empty);
2.77 +val e_ocalhd = (false, Und, TermC.empty, [Model_Def.i_model_empty], [(false, TermC.empty)], Spec.empty);
2.78
2.79 datatype ptform = Form of term | ModSpec of ocalhd;
2.80
3.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Mon May 04 17:08:32 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Mon May 04 18:47:27 2020 +0200
3.3 @@ -4,15 +4,27 @@
3.4 *)
3.5 signature MODEL_DEFINITION =
3.6 sig
3.7 - type vats
3.8 - type ori
3.9 - val oris2str : ori list -> string
3.10 - val e_ori : ori
3.11 - datatype itm_ = Cor of (term * (term list)) * (term * (term list))
3.12 - | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list))
3.13 - | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string
3.14 - type itm
3.15 - val e_itm : itm
3.16 +(* vats*)
3.17 + type variants
3.18 +(* ori list*)
3.19 + type o_model
3.20 +(* ori *)
3.21 + type o_model_single
3.22 +(* oris2str*)
3.23 + val o_model_to_string : o_model_single list -> string
3.24 +(* e_ori*)
3.25 + val o_model_empty : o_model_single
3.26 +
3.27 +(* itm_ *)
3.28 + datatype i_model_feedback = Cor of (term * (term list)) * (term * (term list))
3.29 + | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list))
3.30 + | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string
3.31 +(* itm*)
3.32 + type i_model_single
3.33 +(*\<rightarrow> T*)
3.34 + type i_model
3.35 +(* e_itm*)
3.36 + val i_model_empty : i_model_single
3.37 end
3.38
3.39 (**)
3.40 @@ -20,32 +32,33 @@
3.41 struct
3.42 (**)
3.43
3.44 -type vats = int list; (* variants in formalizations *)
3.45 +type variants = int list; (* variants in formalizations *)
3.46
3.47 (* example as provided by an author, complete w.r.t. pbt specified
3.48 not touched by any user action *)
3.49 -type ori =
3.50 +type o_model_single =
3.51 (int * (* id: 10.3.00ff impl. only <>0 .. touched
3.52 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *)
3.53 - vats * (* variants 21.3.02: related to pbt..discard ? *)
3.54 + variants * (* variants 21.3.02: related to pbt..discard ? *)
3.55 string * (* #Given | #Find | #Relate 21.3.02: discard ? *)
3.56 term * (* description *)
3.57 term list (* isalist2list t | [t] *)
3.58 );
3.59 -val e_ori = (0, [], "", TermC.empty, [TermC.empty]) : ori;
3.60 +type o_model = o_model_single list;
3.61 +val o_model_empty = (0, [], "", TermC.empty, [TermC.empty]) : o_model_single;
3.62
3.63 fun ori2str (i, vs, fi, t, ts) =
3.64 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
3.65 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
3.66 -val oris2str = strs2str' o (map (linefeed o ori2str));
3.67 +val o_model_to_string = strs2str' o (map (linefeed o ori2str));
3.68
3.69
3.70 (* the internal representation of a models' item
3.71 4.9.01: not consistent:
3.72 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
3.73 (involves 'is_error');
3.74 - bool in itm really necessary ???*)
3.75 -datatype itm_ =
3.76 + bool in i_model_single really necessary ???*)
3.77 +datatype i_model_feedback =
3.78 Cor of (term * (* description *)
3.79 (term list)) * (* for list: elem-wise input *)
3.80 (term * (term list)) (* elem of penv ---- penv delayed to future *)
3.81 @@ -59,13 +72,14 @@
3.82
3.83 (* data-type for working on pbl/met-ppc:
3.84 in pbl initially holds descriptions (only) for user guidance *)
3.85 -type itm =
3.86 +type i_model_single =
3.87 int * (* id =0 .. untouched - descript (only) from init
3.88 - seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
3.89 - vats * (* variants - copy from ori *)
3.90 + seems to correspond to o_model_single (fun insert_ppc) <> maintain order in item ppc? *)
3.91 + variants * (* variants - copy from o_model_single *)
3.92 bool * (* input on this item is not/complete *)
3.93 string * (* #Given | #Find | #Relate *)
3.94 - itm_; (* *)
3.95 -val e_itm = (0, [], false, "e_itm", Syn "e_itm");
3.96 + i_model_feedback; (* *)
3.97 + type i_model = i_model_single list;
3.98 +val i_model_empty = (0, [], false, "i_model_empty", Syn "i_model_empty");
3.99
3.100 (**)end(**)
4.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 17:08:32 2020 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 18:47:27 2020 +0200
4.3 @@ -10,14 +10,14 @@
4.4 signature TACTIC =
4.5 sig
4.6 datatype T =
4.7 - Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
4.8 - | Add_Relation' of TermC.as_string * Model_Def.itm list
4.9 + Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
4.10 + | Add_Relation' of TermC.as_string * Model_Def.i_model
4.11 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
4.12 - | Model_Problem' of Problem.id * Model_Def.itm list * Model_Def.itm list
4.13 - | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
4.14 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.itm list
4.15 - | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
4.16 - | Specify_Problem' of Problem.id * (bool * (Model_Def.itm list * (bool * term) list))
4.17 + | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
4.18 + | Refine_Problem' of Problem.id * (Model_Def.i_model * (bool * term) list)
4.19 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.i_model
4.20 + | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
4.21 + | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * (bool * term) list))
4.22 | Specify_Theory' of ThyC.id
4.23 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
4.24 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
4.25 @@ -32,7 +32,7 @@
4.26 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
4.27 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
4.28 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
4.29 - | Subproblem' of Spec.T * Model_Def.ori list * term * Celem.fmz_ * Proof.context * term
4.30 + | Subproblem' of Spec.T * Model_Def.o_model * term * Celem.fmz_ * Proof.context * term
4.31 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
4.32 (*RM*)| Tac_ of theory * string * string * string
4.33 | Take' of term
4.34 @@ -295,24 +295,24 @@
4.35 (** tactics for internal use **)
4.36
4.37 datatype T =
4.38 - Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
4.39 - | Add_Relation' of TermC.as_string * Model_Def.itm list (* for Step.do_next *)
4.40 + Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
4.41 + | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next *)
4.42 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
4.43 | Model_Problem' of (* first step in specify-phase *)
4.44 Problem.id * (* id in the Know_Store *)
4.45 - Model_Def.itm list * (* the model for the Problem *)
4.46 - Model_Def.itm list (* the model for the method *)
4.47 - | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
4.48 + Model_Def.i_model * (* the model for the Problem *)
4.49 + Model_Def.i_model (* the model for the method *)
4.50 + | Refine_Problem' of Problem.id * (Model_Def.i_model * (bool * term) list)
4.51 | Refine_Tacitly' of
4.52 Problem.id * (* the original id in the Know_Store *)
4.53 Problem.id * (* the id of the refined Problem *)
4.54 ThyC.id * (* the id of the refined theory *)
4.55 Method.id * (* the id of the refined Method *)
4.56 - Model_Def.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
4.57 - | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
4.58 + Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
4.59 + | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
4.60 | Specify_Problem' of Problem.id *
4.61 (bool * (* all preconditions evaluate to True *)
4.62 - (Model_Def.itm list * (* the model checked for the input id *)
4.63 + (Model_Def.i_model * (* the model checked for the input id *)
4.64 (bool * term) list)) (* individual preconditions marked true/false *)
4.65 | Specify_Theory' of ThyC.id
4.66 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
4.67 @@ -339,7 +339,7 @@
4.68 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
4.69 | Subproblem' of (* switch from solve-phase to specify-phase *)
4.70 Spec.T * (* specification of the SubProblem *)
4.71 - (Model_Def.ori list) * (* original model, filled in associate Subproblem' *)
4.72 + (Model_Def.o_model) * (* original model, filled in associate Subproblem' *)
4.73 term * (* headline of calc-head, filled -"- *)
4.74 Celem.fmz_ * (* string list from arguments of the calling Program*)
4.75 Proof.context * (* for the specify-phase *)
4.76 @@ -373,7 +373,7 @@
4.77 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
4.78 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
4.79 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
4.80 - Method.id_to_string pI ^ ", " ^ Model_Def.oris2str oris ^ ", )"
4.81 + Method.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
4.82
4.83 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
4.84 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
5.1 --- a/src/Tools/isac/Specify/i-model.sml Mon May 04 17:08:32 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon May 04 18:47:27 2020 +0200
5.3 @@ -5,19 +5,15 @@
5.4
5.5 signature MODEL_FOR_INTERACTION =
5.6 sig
5.7 -(*/------- to O_Model+I_ from ModelModel -------\*)
5.8 - type vats = Model_Def.vats
5.9 -(*\------- to O_Model+I_ from ModelModel -------/*)
5.10 -(*/------- to I_Model from Model -------\*)
5.11 - datatype itm_ = datatype Model_Def.itm_
5.12 - type itm = Model_Def.itm
5.13 - val e_itm : itm
5.14 -(*\------- to I_Model from Model -------/*)
5.15 + type variants = Model_Def.variants
5.16
5.17 - type T
5.18 - type single
5.19 -
5.20 + type T = Model_Def.i_model
5.21 + type single = Model_Def.i_model_single
5.22 + datatype feedback = datatype Model_Def.i_model_feedback
5.23 + val empty : single
5.24 +
5.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.26 + (* NONE *)
5.27 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.28 (* NONE *)
5.29 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.30 @@ -25,30 +21,12 @@
5.31
5.32 structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
5.33 struct
5.34 -(*/------- to O_Model+I_ from Mode -------\*)
5.35 -type vats = Model_Def.vats;
5.36 -(*\------- to O_Model+I_ from Model -------/*)
5.37 -(*/------- to I_Model from Model -------\*)
5.38 -(* the internal representation of a models' item
5.39 - 4.9.01: not consistent:
5.40 - after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
5.41 - (involves 'is_error');
5.42 - bool in itm really necessary ???*)
5.43 -datatype itm_ = datatype Model_Def.itm_; (* internal state from fun parsitm *)
5.44
5.45 -(* data-type for working on pbl/met-ppc:
5.46 - in pbl initially holds descriptions (only) for user guidance *)
5.47 -type itm =
5.48 - int * (* id =0 .. untouched - descript (only) from init
5.49 - seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
5.50 - vats * (* variants - copy from ori *)
5.51 - bool * (* input on this item is not/complete *)
5.52 - string * (* #Given | #Find | #Relate *)
5.53 - itm_; (* *)
5.54 -val e_itm = (0, [], false, "e_itm", Syn "e_itm");
5.55 -(*\------- to I_Model from Model -------/*)
5.56 +type variants = Model_Def.variants;
5.57
5.58 -type T = Model_Def.itm list;
5.59 -type single = Model_Def.itm;
5.60 +type T = Model_Def.i_model_single list;
5.61 +datatype feedback = datatype Model_Def.i_model_feedback;
5.62 +type single = Model_Def.i_model_single;
5.63 +val empty = Model_Def.i_model_empty;
5.64
5.65 (**)end(**);
5.66 \ No newline at end of file
6.1 --- a/src/Tools/isac/Specify/model.sml Mon May 04 17:08:32 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/model.sml Mon May 04 18:47:27 2020 +0200
6.3 @@ -9,17 +9,16 @@
6.4 signature MODEL =
6.5 sig
6.6 (*/------- to O_Model+I_ from ModelModel -------\*)
6.7 - type vats = Model_Def.vats
6.8 + type vats = Model_Def.variants
6.9 (*\------- to O_Model+I_ from ModelModel -------/*)
6.10 (*/------- to O_Model from Model -------\*)
6.11 - type ori = Model_Def.ori
6.12 + type ori = Model_Def.o_model_single
6.13 val oris2str: ori list -> string
6.14 val e_ori: ori
6.15 (*\------- to O_Model from Model -------/*)
6.16 -
6.17 (*/------- to I_Model from Model -------\*)
6.18 - datatype itm_ = datatype Model_Def.itm_
6.19 - type itm = Model_Def.itm
6.20 + datatype itm_ = datatype Model_Def.i_model_feedback
6.21 + type itm = I_Model.single
6.22 val e_itm : itm
6.23 (*\------- to I_Model from Model -------/*)
6.24
6.25 @@ -253,7 +252,7 @@
6.26 fun mkval' x = mkval TermC.empty x;
6.27
6.28 (*/------- to O_Model+I_ from Mode -------\*)
6.29 -type vats = Model_Def.vats;
6.30 +type vats = Model_Def.variants;
6.31 (*\------- to O_Model+I_ from Model -------/*)
6.32
6.33 (*/------- to I_Model from Model -------\*)
6.34 @@ -262,7 +261,7 @@
6.35 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
6.36 (involves 'is_error');
6.37 bool in itm really necessary ???*)
6.38 -datatype itm_ = datatype Model_Def.itm_; (* internal state from fun parsitm *)
6.39 +datatype itm_ = datatype Model_Def.i_model_feedback; (* internal state from fun parsitm *)
6.40
6.41 (* data-type for working on pbl/met-ppc:
6.42 in pbl initially holds descriptions (only) for user guidance *)
6.43 @@ -317,10 +316,10 @@
6.44 (*/------- to O_Model from Model -------\*)
6.45 (* example as provided by an author, complete w.r.t. pbt specified
6.46 not touched by any user action *)
6.47 -type ori = Model_Def.ori;
6.48 -val e_ori = Model_Def.e_ori;
6.49 +type ori = Model_Def.o_model_single;
6.50 +val e_ori = Model_Def.o_model_empty;
6.51
6.52 -val oris2str = Model_Def.oris2str;
6.53 +val oris2str = Model_Def.o_model_to_string;
6.54 (*\------- to O_Model from Model -------/*)
6.55
6.56 (* an or without leading integer *)
7.1 --- a/src/Tools/isac/Specify/o-model.sml Mon May 04 17:08:32 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon May 04 18:47:27 2020 +0200
7.3 @@ -5,17 +5,12 @@
7.4
7.5 signature ORIGINAL_MODEL =
7.6 sig
7.7 -(*/------- to O_Model+I_ from ModelModel -------\*)
7.8 - type vats = Model_Def.vats
7.9 -(*\------- to O_Model+I_ from ModelModel -------/*)
7.10 -(*/------- to O_Model from Model -------\*)
7.11 - type ori = Model_Def.ori
7.12 - val oris2str: ori list -> string
7.13 - val e_ori: ori
7.14 -(*\------- to O_Model from Model -------/*)
7.15 + type variants = Model_Def.variants
7.16 + type T = Model_Def.o_model
7.17 + type single = Model_Def.o_model_single
7.18
7.19 - type T
7.20 - type single
7.21 + val to_string: T -> string
7.22 + val single_empty: single
7.23
7.24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.26 @@ -25,19 +20,13 @@
7.27
7.28 structure O_Model(**) : ORIGINAL_MODEL(**) =
7.29 struct
7.30 -(*/------- to O_Model+I_ from Mode -------\*)
7.31 -type vats = Model_Def.vats;
7.32 -(*\------- to O_Model+I_ from Model -------/*)
7.33 -(*/------- to O_Model from Model -------\*)
7.34 -(* example as provided by an author, complete w.r.t. pbt specified
7.35 - not touched by any user action *)
7.36 -type ori = Model_Def.ori;
7.37 -val e_ori = Model_Def.e_ori;
7.38
7.39 -val oris2str = Model_Def.oris2str;
7.40 -(*\------- to O_Model from Model -------/*)
7.41 +type variants = Model_Def.variants;
7.42
7.43 -type T = Model_Def.ori list;
7.44 -type single = Model_Def.ori
7.45 +type T = Model_Def.o_model;
7.46 +type single = Model_Def.o_model_single
7.47 +val single_empty = Model_Def.o_model_empty;
7.48 +val to_string = Model_Def.o_model_to_string;
7.49 +
7.50
7.51 (**)end(**);
7.52 \ No newline at end of file
8.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Mon May 04 17:08:32 2020 +0200
8.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Mon May 04 18:47:27 2020 +0200
8.3 @@ -88,7 +88,7 @@
8.4 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
8.5
8.6 (*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
8.7 -(*+*)writeln (oris2str oris); (*[
8.8 +(*+*)writeln (O_Model.to_string oris); (*[
8.9 (1, ["1"], #Given,Traegerlaenge, ["L"]),
8.10 (2, ["1"], #Given,Streckenlast, ["q_0"]),
8.11 (3, ["1"], #Find,Biegelinie, ["y"]),
8.12 @@ -134,7 +134,7 @@
8.13 (*+*)p''' = ([1], Pbl);
8.14 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
8.15 (*+*)(*MISSING after Step.by_tactic:*)
8.16 -(*+*)writeln (oris2str oris); (*[
8.17 +(*+*)writeln (O_Model.to_string oris); (*[
8.18 (1, ["1"], #Given,Streckenlast, ["q_0"]),
8.19 (2, ["1"], #Given,FunktionsVariable, ["x"]),
8.20 (3, ["1"], #Find,Funktionen, ["funs'''"])]
8.21 @@ -172,7 +172,7 @@
8.22
8.23 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
8.24 (*+*)(*MISSING after locate_input_tactic:*)
8.25 -(*+*)writeln (oris2str oris); (*[
8.26 +(*+*)writeln (O_Model.to_string oris); (*[
8.27 (1, ["1"], #Given,Streckenlast, ["q_0"]),
8.28 (2, ["1"], #Given,FunktionsVariable, ["x"]),
8.29 (3, ["1"], #Find,Funktionen, ["funs'''"])]
8.30 @@ -200,10 +200,10 @@
8.31 [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
8.32 ^^^^^^^^^^^ ..ERROR arguments_from_model: 'Biegelinie' not in itms*)
8.33 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
8.34 -(*+*)if oris2str oris =
8.35 +(*+*)if O_Model.to_string oris =
8.36 (*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
8.37 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
8.38 -writeln (oris2str oris); (*[
8.39 +writeln (O_Model.to_string oris); (*[
8.40 (1, ["1"], #Given,Streckenlast, ["q_0"]),
8.41 (2, ["1"], #Given,FunktionsVariable, ["x"]),
8.42 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
8.43 @@ -240,7 +240,7 @@
8.44 val dI'' = if dI = ThyC.id_empty then dI' else dI
8.45 val pI'' = if pI = Problem.id_empty then pI' else pI
8.46 ;
8.47 -(*+*)writeln (oris2str oris); (*[
8.48 +(*+*)writeln (O_Model.to_string oris); (*[
8.49 (1, ["1"], #Given,Streckenlast, ["q_0"]),
8.50 (2, ["1"], #Given,FunktionsVariable, ["x"]),
8.51 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
9.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Mon May 04 17:08:32 2020 +0200
9.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Mon May 04 18:47:27 2020 +0200
9.3 @@ -281,7 +281,7 @@
9.4 case nxt of (_, Specify_Method ["DiffApp","max_by_calculus"]) => ()
9.5 | _ => error "diffapp.sml: max-exp me, nxt = Specify_Method";
9.6
9.7 -val oris = fst3 (get_obj g_origin pt (fst p)); writeln(oris2str oris);
9.8 +val oris = fst3 (get_obj g_origin pt (fst p)); writeln(O_Model.to_string oris);
9.9 val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits);
9.10
9.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.12 @@ -312,7 +312,7 @@
9.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.14 === inhibit exn 110722=============================================================*)
9.15
9.16 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
9.17 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
9.18 val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
9.19
9.20 (*=== inhibit exn 110722=============================================================
9.21 @@ -347,7 +347,7 @@
9.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.23 (*val nxt = Refine_Tacitly ["univariate","equation"])*)
9.24
9.25 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
9.26 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
9.27 val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
9.28
9.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.30 @@ -381,7 +381,7 @@
9.31 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
9.32 === inhibit exn 110722=============================================================*)
9.33
9.34 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
9.35 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
9.36
9.37 val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
9.38 val pits = get_obj g_pbl pt [];writeln(itms2str_ ctxt pits);
10.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Mon May 04 17:08:32 2020 +0200
10.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Mon May 04 18:47:27 2020 +0200
10.3 @@ -176,9 +176,9 @@
10.4 "----------- fun untouched ---------------------------------------------------------------------";
10.5 (*> untouched [];
10.6 val it = true : bool
10.7 -> untouched [e_itm];
10.8 +> untouched [I_Model.single_empty];
10.9 val it = true : bool
10.10 -> untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
10.11 +> untouched [I_Model.single_empty, (1,[],false,"I_Model.single_empty",Syn "I_Model.single_empty")];
10.12 val it = false : bool*)
10.13 "----------- fun pbl_ids -----------------------------------------------------------------------";
10.14 "----------- fun pbl_ids -----------------------------------------------------------------------";
11.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Mon May 04 17:08:32 2020 +0200
11.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Mon May 04 18:47:27 2020 +0200
11.3 @@ -176,9 +176,9 @@
11.4 "----------- fun untouched ---------------------------------------------------------------------";
11.5 (*> untouched [];
11.6 val it = true : bool
11.7 -> untouched [e_itm];
11.8 +> untouched [I_Model.single_empty];
11.9 val it = true : bool
11.10 -> untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
11.11 +> untouched [I_Model.single_empty, (1,[],false,"I_Model.single_empty",Syn "I_Model.single_empty")];
11.12 val it = false : bool*)
11.13 "----------- fun pbl_ids -----------------------------------------------------------------------";
11.14 "----------- fun pbl_ids -----------------------------------------------------------------------";
12.1 --- a/test/Tools/isac/Specify/specify.sml Mon May 04 17:08:32 2020 +0200
12.2 +++ b/test/Tools/isac/Specify/specify.sml Mon May 04 18:47:27 2020 +0200
12.3 @@ -98,7 +98,7 @@
12.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.5 (*nxt = Specify_Theory "DiffApp"*)
12.6 val (oris, _, _) = get_obj g_origin pt (fst p);
12.7 - writeln (oris2str oris);
12.8 + writeln (O_Model.to_string oris);
12.9 (*[
12.10 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
12.11 (2, ["1","2","3"], #Find,maximum, ["A"]),