1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon May 04 13:27:45 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon May 04 16:25:14 2020 +0200
1.3 @@ -400,7 +400,7 @@
1.4 (xml_to_strs items, xml_to_spec spec)
1.5 | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
1.6
1.7 -fun xml_of_fmz [] = xml_of_fmz [Selem.e_fmz]
1.8 +fun xml_of_fmz [] = xml_of_fmz [Celem.e_fmz]
1.9 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
1.10 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
1.11 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 04 13:27:45 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 04 16:25:14 2020 +0200
2.3 @@ -14,7 +14,7 @@
2.4 val appendFormula : calcID -> TermC.as_string -> XML.tree (*unit future*)
2.5 val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
2.6 val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree
2.7 - val CalcTree : Selem.fmz list -> XML.tree
2.8 + val CalcTree : Celem.fmz list -> XML.tree
2.9 val checkContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
2.10 val DEconstrCalcTree : calcID -> XML.tree
2.11 val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
3.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon May 04 13:27:45 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon May 04 16:25:14 2020 +0200
3.3 @@ -14,11 +14,10 @@
3.4 ML_file "cas-command.sml"
3.5
3.6 ML_file rewrite.sml
3.7 + ML_file "model-def.sml"
3.8 + ML_file "istate-def.sml"
3.9 ML_file "calc-tree-elem.sml"
3.10 - ML_file model.sml
3.11 - ML_file mstools.sml
3.12 - ML_file "specification-elems.sml"
3.13 - ML_file "istate-def.sml"
3.14 +
3.15 ML_file tactic.sml
3.16 ML_file applicable.sml
3.17
3.18 @@ -27,6 +26,7 @@
3.19 ML_file "ctree-access.sml"
3.20 ML_file "ctree-navi.sml"
3.21 ML_file ctree.sml
3.22 +
3.23 ML_file "state-steps.sml"
3.24 ML_file calculation.sml
3.25
4.1 --- a/src/Tools/isac/MathEngBasic/calc-tree-elem.sml Mon May 04 13:27:45 2020 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/calc-tree-elem.sml Mon May 04 16:25:14 2020 +0200
4.3 @@ -4,17 +4,31 @@
4.4 *)
4.5 signature CALC_TREE_ELEMENT =
4.6 sig
4.7 + type fmz
4.8 + type fmz_
4.9 + val e_fmz : fmz_ * Spec.T (* for datatypes.sml *)
4.10 + type result
4.11 + val res2str : term * term list -> string
4.12
4.13 datatype safe = Sundef | Safe | Unsafe | Helpless_;
4.14 val safe2str: safe -> string
4.15 -
4.16 end
4.17
4.18 (**)
4.19 -structure Telem(**): CALC_TREE_ELEMENT(**) =
4.20 +structure Celem(**): CALC_TREE_ELEMENT(**) =
4.21 struct
4.22 (**)
4.23
4.24 +type fmz_ = TermC.as_string list;
4.25 +(* a formalization of an example contains data
4.26 + sufficient for mechanically finding the solution for the example.
4.27 + FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
4.28 +type fmz = fmz_ * Spec.T;
4.29 +val e_fmz = ([], Spec.empty);
4.30 +
4.31 +type result = term * term list
4.32 +fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)
4.33 +
4.34 datatype safe = Sundef | Safe | Unsafe | Helpless_;
4.35 fun safe2str Sundef = "Sundef"
4.36 | safe2str Safe = "Safe"
5.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Mon May 04 13:27:45 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Mon May 04 16:25:14 2020 +0200
5.3 @@ -8,13 +8,13 @@
5.4 val get_last_formula: CTbasic.state -> term
5.5 val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree
5.6 val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree
5.7 - val update_met : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
5.8 - val update_metppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
5.9 + val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =vvv= ? *)
5.10 + val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =^^^= ? *)
5.11 val update_metID : CTbasic.ctree -> Pos.pos -> Method.id -> CTbasic.ctree
5.12 - val update_pbl : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
5.13 - val update_pblppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
5.14 + val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =vvv= ? *)
5.15 + val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =^^^= ? *)
5.16 val update_pblID : CTbasic.ctree -> Pos.pos -> Problem.id -> CTbasic.ctree
5.17 - val update_oris : CTbasic.ctree -> Pos.pos -> Model.ori list -> CTbasic.ctree
5.18 + val update_oris : CTbasic.ctree -> Pos.pos -> Model_Def.ori list -> CTbasic.ctree
5.19 val update_orispec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree
5.20 val update_spec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree
5.21 val update_tac : CTbasic.ctree -> Pos.pos -> Tactic.input -> CTbasic.ctree
5.22 @@ -23,17 +23,17 @@
5.23 val cappend_form : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->
5.24 CTbasic.ctree * Pos.pos' list
5.25 val cappend_problem : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
5.26 - Selem.fmz -> Model.ori list * Spec.T * term * Proof.context
5.27 + Celem.fmz -> Model_Def.ori list * Spec.T * term * Proof.context
5.28 -> CTbasic.ctree * Pos.pos' list
5.29 - val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.T * Model.itm list * Model.itm list * Proof.context
5.30 + val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.T * Model_Def.itm list * Model_Def.itm list * Proof.context
5.31 -> CTbasic.ctree * Pos.pos' list
5.32 val append_atomic : (* for solve.sml *)
5.33 Pos.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
5.34 - term -> Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
5.35 + term -> Tactic.input -> Celem.result -> CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
5.36 val cappend_atomic : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->
5.37 - Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * Pos.pos' list
5.38 + Tactic.input -> Celem.result -> CTbasic.ostate -> CTbasic.ctree * Pos.pos' list
5.39 val append_result : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
5.40 - Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
5.41 + Celem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
5.42
5.43 val update_loc' : CTbasic.ctree -> Pos.pos ->
5.44 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
5.45 @@ -41,9 +41,9 @@
5.46 (*NONE*)
5.47 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.48 val append_form: Pos.pos -> Istate_Def.T * Proof.context -> term -> CTbasic.ctree -> CTbasic.ctree
5.49 - val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Selem.fmz ->
5.50 - Model.ori list * Spec.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
5.51 - val update_problem: Pos.pos -> Spec.T * Model.itm list * Model.itm list * Proof.context
5.52 + val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Celem.fmz ->
5.53 + Model_Def.ori list * Spec.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
5.54 + val update_problem: Pos.pos -> Spec.T * Model_Def.itm list * Model_Def.itm list * Proof.context
5.55 -> CTbasic.ctree -> CTbasic.ctree
5.56 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.57 end
6.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon May 04 13:27:45 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon May 04 16:25:14 2020 +0200
6.3 @@ -21,19 +21,19 @@
6.4 {branch: branch,
6.5 loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
6.6 ostate: ostate,
6.7 - result: Selem.result,
6.8 + result: Celem.result,
6.9
6.10 - fmz: Selem.fmz,
6.11 - origin: Model.ori list * Spec.T * term,
6.12 - probl: Model.itm list,
6.13 - meth: Model.itm list,
6.14 + fmz: Celem.fmz,
6.15 + origin: Model_Def.ori list * Spec.T * term,
6.16 + probl: Model_Def.itm list,
6.17 + meth: Model_Def.itm list,
6.18 spec: Spec.T,
6.19 ctxt: Proof.context}
6.20 | PrfObj of
6.21 {branch: branch,
6.22 loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
6.23 ostate: ostate,
6.24 - result: Selem.result,
6.25 + result: Celem.result,
6.26
6.27 form: term,
6.28 tac: Tactic.input}
6.29 @@ -49,7 +49,7 @@
6.30 val get_nd : ctree -> Pos.pos -> ctree
6.31 val just_created_ : ppobj -> bool
6.32 val just_created : state -> bool
6.33 - val e_origin : Model.ori list * Spec.T * term
6.34 + val e_origin : Model_Def.ori list * Spec.T * term
6.35
6.36 val is_pblobj : ppobj -> bool
6.37 val is_pblobj' : ctree -> Pos.pos -> bool
6.38 @@ -58,14 +58,14 @@
6.39 val g_spec : ppobj -> Spec.T
6.40 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
6.41 val g_form : ppobj -> term
6.42 - val g_pbl : ppobj -> Model.itm list
6.43 - val g_met : ppobj -> Model.itm list
6.44 + val g_pbl : ppobj -> Model_Def.itm list
6.45 + val g_met : ppobj -> Model_Def.itm list
6.46 val g_metID : ppobj -> Method.id
6.47 - val g_result : ppobj -> Selem.result
6.48 + val g_result : ppobj -> Celem.result
6.49 val g_tac : ppobj -> Tactic.input
6.50 val g_domID : ppobj -> ThyC.id
6.51
6.52 - val g_origin : ppobj -> Model.ori list * Spec.T * term
6.53 + val g_origin : ppobj -> Model_Def.ori list * Spec.T * term
6.54 val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context
6.55 val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T
6.56 val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context
6.57 @@ -77,7 +77,7 @@
6.58 val new_val : term -> Istate_Def.T -> Istate_Def.T
6.59 (* for calchead.sml *)
6.60 type cid = cellID list
6.61 - type ocalhd = bool * Pos.pos_ * term * Model.itm list * (bool * term) list * Spec.T
6.62 + type ocalhd = bool * Pos.pos_ * term * Model_Def.itm list * (bool * term) list * Spec.T
6.63 datatype ptform = Form of term | ModSpec of ocalhd
6.64 val get_somespec' : Spec.T -> Spec.T -> Spec.T
6.65 exception PTREE of string;
6.66 @@ -105,7 +105,7 @@
6.67 val pr_ctree : (Pos.pos -> ppobj -> string) -> ctree -> string
6.68 val pr_short : Pos.pos -> ppobj -> string
6.69 val g_ctxt : ppobj -> Proof.context
6.70 - val g_fmz : ppobj -> Selem.fmz
6.71 + val g_fmz : ppobj -> Celem.fmz
6.72 val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list
6.73 val get_allps : (Pos.pos * Pos.pos_) list -> Pos.posel list -> ctree list -> Pos.pos' list
6.74 val get_allpos' : Pos.pos * Pos.posel -> ctree -> Pos.pos' list
6.75 @@ -171,7 +171,7 @@
6.76 Env.T * (* with results of (ready) tacs *)
6.77 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
6.78 term * (* result value of the tac *)
6.79 - Telem.safe))
6.80 + Celem.safe))
6.81 list;
6.82
6.83 fun ets2s (l,(m,eno,env,iar,res,s)) =
6.84 @@ -180,7 +180,7 @@
6.85 ",\n env= " ^ Env.subst2str env ^
6.86 ",\n iar= " ^ UnparseC.term iar ^
6.87 ",\n res= " ^ UnparseC.term res ^
6.88 - ",\n " ^ Telem.safe2str s ^ "))";
6.89 + ",\n " ^ Celem.safe2str s ^ "))";
6.90 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)
6.91
6.92 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
6.93 @@ -201,21 +201,21 @@
6.94 option, (* both for interpreter location on Res *)
6.95 (*(NONE,NONE) <==> empty ! see update_loc, get_loc *)
6.96 branch: branch, (* only rudimentary *)
6.97 - result: Selem.result, (* result and assumptions *)
6.98 + result: Celem.result, (* result and assumptions *)
6.99 ostate: ostate} (* Complete <=> result is OK *)
6.100 | PblObj of (* a step serving a whole specification-phase *)
6.101 - {fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
6.102 - origin: (Model.ori list) *(* from fmz+pbt+met for efficiently adding items to probl, meth *)
6.103 + {fmz : Celem.fmz, (* from init:FIXME never use this spec;-drop *)
6.104 + origin: (Model_Def.ori list) *(* from fmz+pbt+met for efficiently adding items to probl, meth *)
6.105 Spec.T * (* updated by Refine_Tacitly *)
6.106 term, (* headline of calc-head, as calculated initially(!) *)
6.107 spec : Spec.T, (* explicitly input *)
6.108 - probl : Model.itm list, (* itms explicitly input *)
6.109 - meth : Model.itm list, (* itms automatically added to copy of probl *)
6.110 + probl : Model_Def.itm list, (* itms explicitly input *)
6.111 + meth : Model_Def.itm list, (* itms automatically added to copy of probl *)
6.112 ctxt : Proof.context, (* used while specifying this SubProblem *)
6.113 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *)
6.114 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
6.115 branch: branch, (* like PrfObj *)
6.116 - result: Selem.result, (* like PrfObj *)
6.117 + result: Celem.result, (* like PrfObj *)
6.118 ostate: ostate}; (* like PrfObj *)
6.119
6.120 (* this tree contains isac's calculations;
6.121 @@ -438,10 +438,10 @@
6.122 bool * (* ALL itms+preconds true *)
6.123 pos_ * (* model belongs to Problem | Method *)
6.124 term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*)
6.125 - Model.itm list * (* model: given, find, relate *)
6.126 + Model_Def.itm list * (* model: given, find, relate *)
6.127 ((bool * term) list) *(* model: preconds *)
6.128 Spec.T; (* specification *)
6.129 -val e_ocalhd = (false, Und, TermC.empty, [Model.e_itm], [(false, TermC.empty)], Spec.empty);
6.130 +val e_ocalhd = (false, Und, TermC.empty, [Model_Def.e_itm], [(false, TermC.empty)], Spec.empty);
6.131
6.132 datatype ptform = Form of term | ModSpec of ocalhd;
6.133
6.134 @@ -545,7 +545,7 @@
6.135 (apfst bool2str)))) bts;
6.136 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
6.137 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term hdf ^
6.138 - ", " ^ Model.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms ^
6.139 + ", " ^ "\<forall>itms2str itms\<forall>" (*Model_Def.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms*) ^
6.140 ", " ^ preconds2str prec ^ ", \n" ^ Spec.to_string spec ^ " )";
6.141
6.142 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Mon May 04 16:25:14 2020 +0200
7.3 @@ -0,0 +1,71 @@
7.4 +(* Title: MathEngBasic/calc-tree-elem.sml
7.5 + Author: Walther Neuper 191026
7.6 + (c) due to copyright terms
7.7 +*)
7.8 +signature MODEL_DEFINITION =
7.9 +sig
7.10 + type vats
7.11 + type ori
7.12 + val oris2str : ori list -> string
7.13 + val e_ori : ori
7.14 + datatype itm_ = Cor of (term * (term list)) * (term * (term list))
7.15 + | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list))
7.16 + | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string
7.17 + type itm
7.18 + val e_itm : itm
7.19 +end
7.20 +
7.21 +(**)
7.22 +structure Model_Def(**): MODEL_DEFINITION(**) =
7.23 +struct
7.24 +(**)
7.25 +
7.26 +type vats = int list; (* variants in formalizations *)
7.27 +
7.28 +(* example as provided by an author, complete w.r.t. pbt specified
7.29 + not touched by any user action *)
7.30 +type ori =
7.31 + (int * (* id: 10.3.00ff impl. only <>0 .. touched
7.32 + 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *)
7.33 + vats * (* variants 21.3.02: related to pbt..discard ? *)
7.34 + string * (* #Given | #Find | #Relate 21.3.02: discard ? *)
7.35 + term * (* description *)
7.36 + term list (* isalist2list t | [t] *)
7.37 + );
7.38 +val e_ori = (0, [], "", TermC.empty, [TermC.empty]) : ori;
7.39 +
7.40 +fun ori2str (i, vs, fi, t, ts) =
7.41 + "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
7.42 + UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
7.43 +val oris2str = strs2str' o (map (linefeed o ori2str));
7.44 +
7.45 +
7.46 +(* the internal representation of a models' item
7.47 + 4.9.01: not consistent:
7.48 + after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
7.49 + (involves 'is_error');
7.50 + bool in itm really necessary ???*)
7.51 +datatype itm_ =
7.52 + Cor of (term * (* description *)
7.53 + (term list)) * (* for list: elem-wise input *)
7.54 + (term * (term list)) (* elem of penv ---- penv delayed to future *)
7.55 +| Syn of TermC.as_string
7.56 +| Typ of TermC.as_string
7.57 +| Inc of (term * (term list)) * (term * (term list)) (*lists,
7.58 + + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
7.59 +| Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
7.60 +| Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
7.61 +| Par of TermC.as_string; (* internal state from fun parsitm *)
7.62 +
7.63 +(* data-type for working on pbl/met-ppc:
7.64 + in pbl initially holds descriptions (only) for user guidance *)
7.65 +type itm =
7.66 + int * (* id =0 .. untouched - descript (only) from init
7.67 + seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
7.68 + vats * (* variants - copy from ori *)
7.69 + bool * (* input on this item is not/complete *)
7.70 + string * (* #Given | #Find | #Relate *)
7.71 + itm_; (* *)
7.72 +val e_itm = (0, [], false, "e_itm", Syn "e_itm");
7.73 +
7.74 +(**)end(**)
8.1 --- a/src/Tools/isac/MathEngBasic/model.sml Mon May 04 13:27:45 2020 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,470 +0,0 @@
8.4 -(* Title: Model for (sub-)calculations.
8.5 - Various representations: item and ppc for frontend, itm_ and itm for internal functions.
8.6 - The former are related to structure Specify, the latter to structure Chead --
8.7 - -- apt to re-arrangement of structures
8.8 - Author: Walther Neuper 170207
8.9 - (c) due to copyright terms
8.10 -*)
8.11 -
8.12 -signature MODEL =
8.13 -sig
8.14 - type ori
8.15 - val oris2str : ori list -> string
8.16 - val e_ori : ori
8.17 - datatype item
8.18 - = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
8.19 - | SyntaxE of string | TypeE of string
8.20 - datatype itm_ = Cor of (term * (term list)) * (term * (term list))
8.21 - | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list))
8.22 - | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string
8.23 - val itm_2str : itm_ -> string
8.24 - val itm_2str_ : Proof.context -> itm_ -> string
8.25 - type itm
8.26 - val itm2str_ : Proof.context -> itm -> string
8.27 - val itms2str_ : Proof.context -> itm list -> string
8.28 - val e_itm : itm
8.29 - type 'a ppc
8.30 - val empty_ppc : item ppc
8.31 - val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
8.32 - With: string list} -> string
8.33 - val itemppc2str : item ppc -> string
8.34 -
8.35 - type vats
8.36 - val comp_dts : term * term list -> term
8.37 - val comp_dts' : term * term list -> term
8.38 - val comp_dts'' : term * term list -> string
8.39 - val comp_ts : term * term list -> term
8.40 - val split_dts : term -> term * term list
8.41 - val split_dts' : term * term -> term list
8.42 - val pbl_ids' : term -> term list -> term list
8.43 - val mkval' : term list -> term
8.44 -
8.45 - val d_in : itm_ -> term
8.46 - val ts_in : itm_ -> term list
8.47 - val penvval_in : itm_ -> term list
8.48 - val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
8.49 - val vars_of : itm list -> term list
8.50 - val max_vt : itm list -> int
8.51 -
8.52 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.53 - type penv
8.54 - val penv2str_ : Proof.context -> penv -> string (* NONE *)
8.55 - type preori
8.56 - val preoris2str : preori list -> string
8.57 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.58 - (* NONE *)
8.59 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.60 -
8.61 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
8.62 - val untouched : itm list -> bool
8.63 - type envv
8.64 - val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv
8.65 - val item_ppc : string ppc -> item ppc
8.66 - val all_ts_in : itm_ list -> term list
8.67 - val pres2str : (bool * term) list -> string
8.68 -end
8.69 -
8.70 -structure Model(**) : MODEL(**) =
8.71 -struct
8.72 -(*==========================================================================
8.73 -23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
8.74 -(1) kinds of itms:
8.75 - (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
8.76 - =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
8.77 - (1.2) Syn,Typ,Sup: not related to oris
8.78 - Syn, Typ (presently) should be accepted in appl_add (instead Error')
8.79 - Sup (presently) should be accepted in appl_add (instead Error')
8.80 - _could_ be w.r.t current vat (and then _is_ related to vat
8.81 - Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
8.82 -- dsc in itm_ is timeconsuming -- keep id for respective queries ?
8.83 -- order of items in ppc should be stable w.r.t order of itms
8.84 -
8.85 -- stepwise input of itms --- match_itms (in one go) ..not coordinated
8.86 - - unify code
8.87 - - match_itms / match_itms_oris ..2 versions ?!
8.88 - (fast, for refine / slow, for modeling)
8.89 -
8.90 -- clarify: efficiency <--> simplicity !!!
8.91 - ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
8.92 - | take int for perserving order of item ppc in itms
8.93 - | make all(!?) handling of itms stable against reordering(?)
8.94 - | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
8.95 - -"- "#undef" ?= not touched ?= (id,..)
8.96 ------------------------------------------------------------------
8.97 -27.3.02:
8.98 -def: type pbt = (field, (dsc, pid)) *** design considerations ***
8.99 -
8.100 -(1) fmz + pbt -> oris
8.101 -(2) input + oris -> itm
8.102 -(3) match_itms : schnell(?) f"ur refine
8.103 - match_itms_oris : r"uckmeldung f"ur item ppc
8.104 -
8.105 -(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
8.106 ----------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
8.107 -
8.108 -(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
8.109 - wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
8.110 - (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
8.111 - (b)
8.112 -==========================================================================*)
8.113 -
8.114 -val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
8.115 -val e_listReal = script_parse "[]::(real list)";
8.116 -val e_listBool = script_parse "[]::(bool list)";
8.117 -
8.118 -(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
8.119 -fun take_apart t =
8.120 - let val elems = TermC.isalist2list t
8.121 - in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
8.122 -fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
8.123 - let val elems = (flat o (map TermC.isalist2list)) ts;
8.124 - in TermC.list2isalist (type_of (hd elems)) elems end;
8.125 -
8.126 -fun is_var (Free _) = true
8.127 - | is_var _ = false;
8.128 -
8.129 -(* special handling for lists. ?WN:14.5.03 ??!? *)
8.130 -fun dest_list (d, ts) =
8.131 - let fun dest t =
8.132 - if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
8.133 - then TermC.isalist2list t
8.134 - else [t]
8.135 - in (flat o (map dest)) ts end;
8.136 -
8.137 -(* revert split_dts only for ts; compare comp_dts *)
8.138 -fun comp_ts (d, ts) =
8.139 - if Input_Descript.is_list_dsc d
8.140 - then if TermC.is_list (hd ts)
8.141 - then if Input_Descript.is_unl d
8.142 - then (hd ts) (* e.g. someList [1,3,2] *)
8.143 - else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
8.144 - else (hd ts) (* a variable or metavariable for a list *)
8.145 - else (hd ts);
8.146 -fun comp_dts (d, []) =
8.147 - if Input_Descript.is_reall_dsc d
8.148 - then (d $ e_listReal)
8.149 - else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
8.150 - | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
8.151 - handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
8.152 -fun comp_dts' (d, []) =
8.153 - if Input_Descript.is_reall_dsc d
8.154 - then (d $ e_listReal)
8.155 - else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
8.156 - | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
8.157 - handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
8.158 -fun comp_dts'' (d, []) =
8.159 - if Input_Descript.is_reall_dsc d
8.160 - then UnparseC.term (d $ e_listReal)
8.161 - else if Input_Descript.is_booll_dsc d
8.162 - then UnparseC.term (d $ e_listBool)
8.163 - else UnparseC.term d
8.164 - | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))
8.165 - handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
8.166 -
8.167 -(* decompose an input into description, terms (ev. elems of lists),
8.168 - and the value for the problem-environment; inv to comp_dts *)
8.169 -fun split_dts (t as d $ arg) =
8.170 - if Input_Descript.is_dsc d
8.171 - then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
8.172 - then (d, take_apart arg)
8.173 - else (d, [arg])
8.174 - else (TermC.empty, TermC.dest_list' t)
8.175 - | split_dts t =
8.176 - let val t' as (h, _) = strip_comb t;
8.177 - in
8.178 - if Input_Descript.is_dsc h
8.179 - then (h, dest_list t')
8.180 - else (TermC.empty, TermC.dest_list' t)
8.181 - end;
8.182 -(* version returning ts only *)
8.183 -fun split_dts' (d, arg) =
8.184 - if Input_Descript.is_dsc d
8.185 - then if Input_Descript.is_list_dsc d
8.186 - then if TermC.is_list arg
8.187 - then if Input_Descript.is_unl d
8.188 - then ([arg]) (* e.g. someList [1,3,2] *)
8.189 - else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
8.190 - else ([arg]) (* a variable or metavariable for a list *)
8.191 - else ([arg])
8.192 - else (TermC.dest_list' arg)
8.193 -(* WN170204: Warning "redundant"
8.194 - | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
8.195 - let val (h,argl) = strip_comb t
8.196 - in
8.197 - if (not o is_dsc) h
8.198 - then (dest_list' t)
8.199 - else (dest_list (h,argl))
8.200 - end;*)
8.201 -(* revert split_:
8.202 - WN050903 we do NOT know which is from subtheory, description or term;
8.203 - typecheck thus may lead to TYPE-error 'unknown constant';
8.204 - solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
8.205 -(*fun comp_dts thy (d,[]) =
8.206 - Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
8.207 - (Thy_Info_get_theory "Isac_Knowledge")
8.208 - (*comp_dts:FIXXME stay with term for efficiency !!!*)
8.209 - (if is_reall_dsc d then (d $ e_listReal)
8.210 - else if is_booll_dsc d then (d $ e_listBool)
8.211 - else d)
8.212 - | comp_dts (d,ts) =
8.213 - (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
8.214 - (Thy_Info_get_theory "Isac_Knowledge")
8.215 - (*comp_dts:FIXXME stay with term for efficiency !!*)
8.216 - (d $ (comp_ts (d, ts)))
8.217 - handle _ => error ("comp_dts: "^(term2str d)^
8.218 - " $ "^(term2str (hd ts))));*)
8.219 -
8.220 -(* 27.8.01: problem-environment
8.221 -WN.6.5.03: FIXXME reconsider if penv is worth the effort --
8.222 - -- just rerun a whole expl with num/var may show the same ?!
8.223 -WN.9.5.03: penv-concept stalled, immediately generate script env !
8.224 - but [#0, epsilon] only outcommented for eventual reconsideration *)
8.225 -type penv = (* problem-environment *)
8.226 - (term (* err_ *)
8.227 - * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
8.228 - ) list;
8.229 -fun pen2str ctxt (t, ts) =
8.230 - pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
8.231 -fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
8.232 -
8.233 -(* get the constant value from a penv *)
8.234 -fun getval (id, values) =
8.235 - case values of
8.236 - [] => error ("penv_value: no values in '" ^ UnparseC.term id)
8.237 - | [v] => (id, v)
8.238 - | (v1 :: v2 :: _) => (case v1 of
8.239 - Const ("Program.Arbfix",_) => (id, v2)
8.240 - | _ => (id, v1));
8.241 -
8.242 -(* 9.5.03: still unused, but left for eventual future development *)
8.243 -type envv = (int * penv) list; (* over variants *)
8.244 -
8.245 -(* 14.9.01: not used after putting penv-values into itm_
8.246 - make the result of split_* a value of problem-environment *)
8.247 -fun mkval _(*dsc*) [] = error "mkval called with []"
8.248 - | mkval _ [t] = t
8.249 - | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
8.250 -fun mkval' x = mkval TermC.empty x;
8.251 -
8.252 -(* the internal representation of a models' item
8.253 - 4.9.01: not consistent:
8.254 - after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
8.255 - (involves 'is_error');
8.256 - bool in itm really necessary ???*)
8.257 -datatype itm_ =
8.258 - Cor of (term * (* description *)
8.259 - (term list)) * (* for list: elem-wise input *)
8.260 - (term * (term list)) (* elem of penv ---- penv delayed to future *)
8.261 -| Syn of TermC.as_string
8.262 -| Typ of TermC.as_string
8.263 -| Inc of (term * (term list)) * (term * (term list)) (*lists,
8.264 - + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
8.265 -| Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
8.266 -| Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
8.267 -| Par of TermC.as_string; (* internal state from fun parsitm *)
8.268 -
8.269 -type vats = int list; (* variants in formalizations *)
8.270 -
8.271 -(* data-type for working on pbl/met-ppc:
8.272 - in pbl initially holds descriptions (only) for user guidance *)
8.273 -type itm =
8.274 - int * (* id =0 .. untouched - descript (only) from init
8.275 - seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
8.276 - vats * (* variants - copy from ori *)
8.277 - bool * (* input on this item is not/complete *)
8.278 - string * (* #Given | #Find | #Relate *)
8.279 - itm_; (* *)
8.280 -val e_itm = (0, [], false, "e_itm", Syn "e_itm");
8.281 -
8.282 -(* in CalcTree/Subproblem an 'untouched' model is created
8.283 - FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
8.284 -fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
8.285 -
8.286 -(* find most frequent variant v in itms *)
8.287 -fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
8.288 -
8.289 -fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
8.290 -fun vts_cnt vts itms = map (cnt itms) vts;
8.291 -fun max2 [] = error "max2 of []"
8.292 - | max2 (y :: ys) =
8.293 - let
8.294 - fun mx (a,x) [] = (a,x)
8.295 - | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
8.296 - in mx y ys end;
8.297 -
8.298 -(* find the variant with most items already input *)
8.299 -fun max_vt itms =
8.300 - let val vts = (vts_cnt (vts_in itms)) itms;
8.301 - in if vts = [] then 0 else (fst o max2) vts end;
8.302 -
8.303 -(* TODO ev. make more efficient by avoiding flat *)
8.304 -fun mk_e (Cor (_, iv)) = [getval iv]
8.305 - | mk_e (Syn _) = []
8.306 - | mk_e (Typ _) = []
8.307 - | mk_e (Inc (_, iv)) = [getval iv]
8.308 - | mk_e (Sup _) = []
8.309 - | mk_e (Mis _) = []
8.310 - | mk_e _ = error "mk_e: uncovered case in fun.def.";
8.311 -fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
8.312 -
8.313 -(* extract the environment from an item list; takes the variant with most items *)
8.314 -fun mk_env itms =
8.315 - let val vt = max_vt itms
8.316 - in (flat o (map (mk_en vt))) itms end;
8.317 -
8.318 -(* example as provided by an author, complete w.r.t. pbt specified
8.319 - not touched by any user action *)
8.320 -type ori =
8.321 - (int * (* id: 10.3.00ff impl. only <>0 .. touched
8.322 - 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *)
8.323 - vats * (* variants 21.3.02: related to pbt..discard ? *)
8.324 - string * (* #Given | #Find | #Relate 21.3.02: discard ? *)
8.325 - term * (* description *)
8.326 - term list (* isalist2list t | [t] *)
8.327 - );
8.328 -val e_ori = (0, [], "", TermC.empty, [TermC.empty]) : ori;
8.329 -
8.330 -fun ori2str (i, vs, fi, t, ts) =
8.331 - "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
8.332 - UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
8.333 -val oris2str = strs2str' o (map (linefeed o ori2str));
8.334 -
8.335 -(* an or without leading integer *)
8.336 -type preori = (vats * string * term * term list);
8.337 -fun preori2str (vs, fi, t, ts) =
8.338 - "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
8.339 - UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
8.340 -val preoris2str = (strs2str' o (map (linefeed o preori2str)));
8.341 -
8.342 -(* 9.5.03 penv postponed: pbl_ids' *)
8.343 -fun pbl_ids' d vs = [comp_ts (d, vs)];
8.344 -
8.345 -(* 14.9.01: not used after putting values for penv into itm_
8.346 - WN.5.5.03: used in upd .. upd_envv *)
8.347 -fun upd_penv ctxt penv dsc (id, vl) =
8.348 -((*tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.349 - tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.350 - tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";*)
8.351 - overwrite (penv, (id, Input_Descript.pbl_ids ctxt dsc vl))
8.352 -);
8.353 -
8.354 -(* WN.9.5.03: not reconsidered; looks strange !!!*)
8.355 -fun upd thy envv dsc (id, vl) i =
8.356 - let val penv = case assoc (envv, i) of
8.357 - SOME e => e
8.358 - | NONE => [];
8.359 - val penv' = upd_penv thy penv dsc (id, vl);
8.360 - in (i, penv') end;
8.361 -
8.362 -(* 14.9.01: not used after putting pre-penv into itm_*)
8.363 -fun upd_envv thy envv vats dsc id vl =
8.364 - let val vats = if length vats = 0
8.365 - then (*unknown id to _all_ variants*)
8.366 - if length envv = 0 then [1]
8.367 - else (intsto o length) envv
8.368 - else vats
8.369 - fun isin vats (i, _) = member op = vats i;
8.370 - val envs_notin_vat = filter_out (isin vats) envv;
8.371 - in (map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat end;
8.372 -
8.373 -(* update envv by folding from a list of arguments *)
8.374 -fun upds_envv _ envv [] = envv
8.375 - | upds_envv thy envv ((vs, dsc, id, vl) :: ps) =
8.376 - upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
8.377 -
8.378 -(* for _output_ of the items of a Model *)
8.379 -datatype item =
8.380 - Correct of TermC.as_string (* labels a correct formula (type cterm') *)
8.381 - | SyntaxE of string (**)
8.382 - | TypeE of string (**)
8.383 - | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
8.384 - | Incompl of TermC.as_string (**)
8.385 - | Superfl of string (**)
8.386 - | Missing of TermC.as_string;
8.387 -fun item2str (Correct s) ="Correct " ^ s
8.388 - | item2str (SyntaxE s) ="SyntaxE " ^ s
8.389 - | item2str (TypeE s) ="TypeE " ^ s
8.390 - | item2str (False s) ="False " ^ s
8.391 - | item2str (Incompl s) ="Incompl " ^ s
8.392 - | item2str (Superfl s) ="Superfl " ^ s
8.393 - | item2str (Missing s) ="Missing " ^ s;
8.394 -(*make string for error-msgs*)
8.395 -fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
8.396 - "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
8.397 - | itm_2str_ _ (Syn c) = "Syn " ^ c
8.398 - | itm_2str_ _ (Typ c) = "Typ " ^ c
8.399 - | itm_2str_ ctxt (Inc ((d, ts), penv)) =
8.400 - "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
8.401 - | itm_2str_ ctxt (Sup (d, ts)) =
8.402 - "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts))
8.403 - | itm_2str_ ctxt (Mis (d, pid)) =
8.404 - "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
8.405 - | itm_2str_ _ (Par s) = "Trm "^s;
8.406 -fun itm_2str t = itm_2str_ (ThyC.id_to_ctxt "Isac_Knowledge") t;
8.407 -fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
8.408 - "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
8.409 - s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
8.410 -fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
8.411 -fun init_item str = SyntaxE str;
8.412 -
8.413 -type 'a ppc =
8.414 - {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
8.415 -fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
8.416 - "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find =" ^ strs2str Find ^
8.417 - ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";
8.418 -
8.419 -fun item_ppc {Given = gi, Where= wh, Find = fi, With = wi, Relate= re} =
8.420 - {Given = map init_item gi, Where= map init_item wh, Find = map init_item fi,
8.421 - With = map init_item wi, Relate= map init_item re};
8.422 -fun itemppc2str ({Given=Given,Where=Where,
8.423 - Find=Find,With=With,Relate=Relate}:item ppc)=
8.424 - ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
8.425 - ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
8.426 - ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
8.427 - ",With =" ^ ((strs2str' o (map item2str)) With ) ^
8.428 - ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
8.429 -
8.430 -val empty_ppc = {Given = [], Where= [], Find = [], With = [], Relate= []};
8.431 -
8.432 -fun ts_in (Cor ((_, ts), _)) = ts
8.433 - | ts_in (Syn _) = []
8.434 - | ts_in (Typ _) = []
8.435 - | ts_in (Inc ((_, ts), _)) = ts
8.436 - | ts_in (Sup (_, ts)) = ts
8.437 - | ts_in (Mis _) = []
8.438 - | ts_in _ = error "ts_in: uncovered case in fun.def.";
8.439 -(*WN050629 unused*)
8.440 -fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
8.441 -val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
8.442 -fun d_in (Cor ((d ,_), _)) = d
8.443 - | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
8.444 - | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
8.445 - | d_in (Inc ((d, _), _)) = d
8.446 - | d_in (Sup (d, _)) = d
8.447 - | d_in (Mis (d, _)) = d
8.448 - | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
8.449 -
8.450 -fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
8.451 -fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
8.452 - | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
8.453 - | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
8.454 - | penvval_in (Inc (_, (_, ts))) = ts
8.455 - | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
8.456 - | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
8.457 - pair2str(UnparseC.term d, UnparseC.term t));*) [])
8.458 - | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
8.459 -
8.460 -(* check a predicate labelled with indication of incomplete substitution;
8.461 - rls -> (* for eval_true *)
8.462 - bool * (* have _all_ variables(Free) from the model-pattern
8.463 - been substituted by a value from the pattern's environment ?*)
8.464 - term -> (* the precondition *)
8.465 - bool * (* has the precondition evaluated to true *)
8.466 - term (* the precondition (for map) *)
8.467 -*)
8.468 -fun pre2str (b, t) = pair2str(bool2str b, UnparseC.term t);
8.469 -fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
8.470 -
8.471 -fun vars_of itms = itms |> mk_env |> map snd
8.472 -
8.473 -end;
8.474 \ No newline at end of file
9.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Mon May 04 13:27:45 2020 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,98 +0,0 @@
9.4 -(* Title: tools for 'modeling' und 'specifying' to be used in
9.5 - modspec.sml. The types are separated into this file,
9.6 - because some of them are stored in the calc-tree, and thus are required
9.7 - _before_ ctree.sml.
9.8 - TODO: allocate elements of Selem and of Stool appropriately
9.9 - Author: Walther Neuper, Mathias Lehnfeld
9.10 - (c) due to copyright terms
9.11 -*)
9.12 -
9.13 -signature SPECIFY_TOOL =
9.14 -sig
9.15 - val check_preconds : 'a -> Rule_Set.T -> term list -> Model.itm list -> (bool * term) list
9.16 - val check_preconds' : Rule_Set.T -> term list -> Model.itm list -> 'a -> (bool * term) list
9.17 -
9.18 - datatype match_ = Match_ of Problem.id * (Model.itm list * (bool * term) list) | NoMatch_
9.19 - val refined_ : match_ list -> match_ option
9.20 - datatype match = Matches of Problem.id * Model.item Model.ppc | NoMatch of Problem.id * Model.item Model.ppc
9.21 - val matchs2str : match list -> string
9.22 - val common_subthy : theory * theory -> theory
9.23 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.24 - val pres2str : (bool * term) list -> string
9.25 - val refined : match list -> Problem.id
9.26 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.27 - (*NONE*)
9.28 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.29 -
9.30 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
9.31 - val pblID_of_match : match -> Problem.id
9.32 - val refined_IDitms : match list -> match option
9.33 -end
9.34 -
9.35 -structure Stool(**) : SPECIFY_TOOL(**) =
9.36 -struct
9.37 -
9.38 -datatype match =
9.39 - Matches of Problem.id * Model.item Model.ppc
9.40 -| NoMatch of Problem.id * Model.item Model.ppc;
9.41 -fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")"
9.42 - | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")";
9.43 -fun matchs2str ms = (strs2str o (map match2str)) ms;
9.44 -fun pblID_of_match (Matches (pI, _)) = pI
9.45 - | pblID_of_match (NoMatch (pI, _)) = pI;
9.46 -
9.47 -(* 10.03 for Refine_Problem *)
9.48 -datatype match_ =
9.49 - Match_ of Problem.id * (( Model.itm list) * ((bool * term) list))
9.50 -| NoMatch_;
9.51 -
9.52 -(* the refined pbt is the last_element Matches in the list *)
9.53 -fun is_matches (Matches _) = true
9.54 - | is_matches _ = false;
9.55 -fun matches_pblID (Matches (pI, _)) = pI
9.56 - | matches_pblID _ = error "matches_pblID: uncovered case in fun.def.";
9.57 -fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
9.58 - handle _ => [];
9.59 -fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
9.60 -
9.61 -(* the refined pbt is the last_element Matches in the list, for Refine_Problem, tryrefine *)
9.62 -fun is_matches_ (Match_ _) = true
9.63 - | is_matches_ _ = false;
9.64 -fun refined_ ms = ((find_first is_matches_) o rev) ms;
9.65 -
9.66 -(* check a predicate labelled with indication of incomplete substitution;
9.67 - rls -> (* for eval_true *)
9.68 - bool * (* have _all_ variables(Free) from the model-pattern
9.69 - been substituted by a value from the pattern's environment ?*)
9.70 - term -> (* the precondition *)
9.71 - bool * (* has the precondition evaluated to true *)
9.72 - term (* the precondition (for map) *)
9.73 -*)
9.74 -fun evalprecond _ (false, pre) =
9.75 - (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
9.76 - (false, pre)
9.77 - | evalprecond prls (true, pre) =
9.78 - if Rewrite.eval_true (ThyC.get_theory "Isac_Knowledge") (* for Pattern.match *)
9.79 - [pre] prls (* pre parsed, prls.thy *)
9.80 - then (true , pre)
9.81 - else (false , pre);
9.82 -
9.83 -fun pre2str (b, t) = pair2str (bool2str b, UnparseC.term t);
9.84 -fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
9.85 -
9.86 -(* check preconditions, return true if all true *)
9.87 -fun check_preconds' _ [] _ _ = [] (* empty preconditions are true *)
9.88 - | check_preconds' prls pres pbl _ (* FIXME.WN0308 mvat re-introduce *) =
9.89 - let
9.90 - val env = Model.mk_env pbl;
9.91 - val pres' = map (TermC.subst_atomic_all env) pres;
9.92 - in map (evalprecond prls) pres' end;
9.93 -fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl);
9.94 -
9.95 -
9.96 -fun common_subthy (thy1, thy2) =
9.97 - if Context.subthy (thy1, thy2) then thy2
9.98 - else if Context.subthy (thy2, thy1) then thy1
9.99 - else ThyC.get_theory "Isac_Knowledge"
9.100 -
9.101 -end;
10.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Mon May 04 13:27:45 2020 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,38 +0,0 @@
10.4 -(* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
10.5 - most important types are declared in mstools.sml.
10.6 - TODO: allocate elements of Selem and of Stool appropriately
10.7 - Author: Walther Neuper 991122, Mathias Lehnfeld
10.8 - (c) due to copyright terms
10.9 -*)
10.10 -signature SPECIFY_ELEMENT =
10.11 -sig
10.12 - type fmz
10.13 - type fmz_
10.14 - type result
10.15 - val res2str : term * term list -> string
10.16 -
10.17 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.18 - val e_fmz : fmz_ * Spec.T (* for datatypes.sml *)
10.19 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.20 - (* NONE *)
10.21 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.22 -
10.23 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
10.24 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
10.25 - (* NONE *)
10.26 -end
10.27 -
10.28 -structure Selem(**): SPECIFY_ELEMENT(**) =
10.29 -struct
10.30 -
10.31 -type fmz_ = TermC.as_string list;
10.32 -(* a formalization of an example contains data
10.33 - sufficient for mechanically finding the solution for the example.
10.34 - FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
10.35 -type fmz = fmz_ * Spec.T;
10.36 -val e_fmz = ([], Spec.empty);
10.37 -
10.38 -type result = term * term list
10.39 -fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)
10.40 -
10.41 -(**)end(**)
11.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 13:27:45 2020 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 16:25:14 2020 +0200
11.3 @@ -10,34 +10,34 @@
11.4 signature TACTIC =
11.5 sig
11.6 datatype T =
11.7 - Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
11.8 - | Add_Relation' of TermC.as_string * Model.itm list
11.9 + Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
11.10 + | Add_Relation' of TermC.as_string * Model_Def.itm list
11.11 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
11.12 - | Model_Problem' of Problem.id * Model.itm list * Model.itm list
11.13 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
11.14 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
11.15 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
11.16 - | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
11.17 + | Model_Problem' of Problem.id * Model_Def.itm list * Model_Def.itm list
11.18 + | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
11.19 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.itm list
11.20 + | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
11.21 + | Specify_Problem' of Problem.id * (bool * (Model_Def.itm list * (bool * term) list))
11.22 | Specify_Theory' of ThyC.id
11.23 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
11.24 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
11.25 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
11.26 | Check_Postcond' of Problem.id * term
11.27 - | Check_elementwise' of term * TermC.as_string * Selem.result
11.28 + | Check_elementwise' of term * TermC.as_string * Celem.result
11.29 | Derive' of Rule_Set.T
11.30 | Empty_Tac_
11.31 | Free_Solve'
11.32 | Or_to_List' of term * term
11.33 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
11.34 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
11.35 - | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
11.36 - | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
11.37 - | Subproblem' of Spec.T * Model.ori list * term * Selem.fmz_ * Proof.context * term
11.38 + | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
11.39 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
11.40 + | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
11.41 + | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
11.42 + | Subproblem' of Spec.T * Model_Def.ori list * term * Celem.fmz_ * Proof.context * term
11.43 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
11.44 (*RM*)| Tac_ of theory * string * string * string
11.45 | Take' of term
11.46 - | End_Detail' of Selem.result
11.47 - | Begin_Trans' of term | End_Trans' of Selem.result
11.48 + | End_Detail' of Celem.result
11.49 + | Begin_Trans' of term | End_Trans' of Celem.result
11.50 | End_Proof''
11.51
11.52 val string_of: T -> string
11.53 @@ -295,24 +295,24 @@
11.54 (** tactics for internal use **)
11.55
11.56 datatype T =
11.57 - Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
11.58 - | Add_Relation' of TermC.as_string * Model.itm list (* for Step.do_next *)
11.59 + Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
11.60 + | Add_Relation' of TermC.as_string * Model_Def.itm list (* for Step.do_next *)
11.61 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
11.62 | Model_Problem' of (* first step in specify-phase *)
11.63 Problem.id * (* id in the Know_Store *)
11.64 - Model.itm list * (* the model for the Problem *)
11.65 - Model.itm list (* the model for the method *)
11.66 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
11.67 + Model_Def.itm list * (* the model for the Problem *)
11.68 + Model_Def.itm list (* the model for the method *)
11.69 + | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
11.70 | Refine_Tacitly' of
11.71 Problem.id * (* the original id in the Know_Store *)
11.72 Problem.id * (* the id of the refined Problem *)
11.73 ThyC.id * (* the id of the refined theory *)
11.74 Method.id * (* the id of the refined Method *)
11.75 - Model.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
11.76 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
11.77 + Model_Def.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
11.78 + | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
11.79 | Specify_Problem' of Problem.id *
11.80 (bool * (* all preconditions evaluate to True *)
11.81 - (Model.itm list * (* the model checked for the input id *)
11.82 + (Model_Def.itm list * (* the model checked for the input id *)
11.83 (bool * term) list)) (* individual preconditions marked true/false *)
11.84 | Specify_Theory' of ThyC.id
11.85 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
11.86 @@ -328,20 +328,20 @@
11.87 | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
11.88 term * (* the current formula: [x=1,x=...] *)
11.89 string * (* the pred from Check_elementwise *)
11.90 - Selem.result (* composed from (1) and (2): {x. pred} *)
11.91 + Celem.result (* composed from (1) and (2): {x. pred} *)
11.92 | Derive' of Rule_Set.T(* for Generate.embed_deriv *)
11.93 | Empty_Tac_
11.94 | Free_Solve'
11.95 | Or_to_List' of term * term
11.96 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
11.97 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
11.98 - | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
11.99 - | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
11.100 + | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
11.101 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
11.102 + | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
11.103 + | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
11.104 | Subproblem' of (* switch from solve-phase to specify-phase *)
11.105 Spec.T * (* specification of the SubProblem *)
11.106 - (Model.ori list) * (* original model, filled in associate Subproblem' *)
11.107 + (Model_Def.ori list) * (* original model, filled in associate Subproblem' *)
11.108 term * (* headline of calc-head, filled -"- *)
11.109 - Selem.fmz_ * (* string list from arguments of the calling Program*)
11.110 + Celem.fmz_ * (* string list from arguments of the calling Program*)
11.111 Proof.context * (* for the specify-phase *)
11.112 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
11.113 | Substitute' of (* substitute variables (TODO: from the context) *)
11.114 @@ -352,9 +352,9 @@
11.115 term (* resulting from the substitution *)
11.116 (*RM*)| Tac_ of theory * string * string * string
11.117 | Take' of term
11.118 - | End_Detail' of Selem.result (* for intermediate steps into Rewrite_Set *)
11.119 + | End_Detail' of Celem.result (* for intermediate steps into Rewrite_Set *)
11.120 | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *)
11.121 - | End_Trans' of Selem.result (* for intermediate steps into Rewrite_Set *)
11.122 + | End_Trans' of Celem.result (* for intermediate steps into Rewrite_Set *)
11.123 | End_Proof''
11.124
11.125 fun string_of ma = case ma of
11.126 @@ -373,7 +373,7 @@
11.127 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
11.128 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
11.129 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
11.130 - Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
11.131 + Method.id_to_string pI ^ ", " ^ Model_Def.oris2str oris ^ ", )"
11.132
11.133 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
11.134 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
12.1 --- a/src/Tools/isac/Specify/Specify.thy Mon May 04 13:27:45 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/Specify.thy Mon May 04 16:25:14 2020 +0200
12.3 @@ -7,6 +7,8 @@
12.4 imports "~~/src/Tools/isac/MathEngBasic/MathEngBasic"
12.5 begin
12.6 (* removed all warnings here, only "handle _" remains *)
12.7 + ML_file "model.sml"
12.8 + ML_file "mstools.sml"
12.9 ML_file ptyps.sml
12.10 ML_file generate.sml
12.11 ML_file "specify-step.sml"
12.12 @@ -16,8 +18,7 @@
12.13 ML_file specify.sml
12.14
12.15 ML \<open>
12.16 -\<close> text \<open>
12.17 -State_Steps.T
12.18 +\<close> ML \<open>
12.19 \<close> ML \<open>
12.20 \<close>
12.21 end
13.1 --- a/src/Tools/isac/Specify/input-calchead.sml Mon May 04 13:27:45 2020 +0200
13.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Mon May 04 16:25:14 2020 +0200
13.3 @@ -111,7 +111,7 @@
13.4 Spec.T; (*specification: domID, pblID, metID*)
13.5 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty)
13.6
13.7 -fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Selem.fmz) =
13.8 +fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Celem.fmz) =
13.9 hdf <> "" andalso fmz_ = [] andalso spec = Spec.empty
13.10
13.11 (* re-parse itms with a new thy and prepare for checking with ori list *)
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/isac/Specify/model.sml Mon May 04 16:25:14 2020 +0200
14.3 @@ -0,0 +1,453 @@
14.4 +(* Title: Model for (sub-)calculations.
14.5 + Various representations: item and ppc for frontend, itm_ and itm for internal functions.
14.6 + The former are related to structure Specify, the latter to structure Chead --
14.7 + -- apt to re-arrangement of structures
14.8 + Author: Walther Neuper 170207
14.9 + (c) due to copyright terms
14.10 +*)
14.11 +
14.12 +signature MODEL =
14.13 +sig
14.14 + type vats = Model_Def.vats
14.15 + type ori = Model_Def.ori
14.16 + val oris2str: ori list -> string
14.17 + val e_ori: ori
14.18 +
14.19 + datatype itm_ = datatype Model_Def.itm_
14.20 + type itm = Model_Def.itm
14.21 + val e_itm : itm
14.22 +
14.23 + datatype item
14.24 + = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
14.25 + | SyntaxE of string | TypeE of string
14.26 + val itm_2str : itm_ -> string
14.27 + val itm_2str_ : Proof.context -> itm_ -> string
14.28 + val itm2str_ : Proof.context -> itm -> string
14.29 + val itms2str_ : Proof.context -> itm list -> string
14.30 + type 'a ppc
14.31 + val empty_ppc : item ppc
14.32 + val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
14.33 + With: string list} -> string
14.34 + val itemppc2str : item ppc -> string
14.35 +
14.36 + val comp_dts : term * term list -> term
14.37 + val comp_dts' : term * term list -> term
14.38 + val comp_dts'' : term * term list -> string
14.39 + val comp_ts : term * term list -> term
14.40 + val split_dts : term -> term * term list
14.41 + val split_dts' : term * term -> term list
14.42 + val pbl_ids' : term -> term list -> term list
14.43 + val mkval' : term list -> term
14.44 +
14.45 + val d_in : itm_ -> term
14.46 + val ts_in : itm_ -> term list
14.47 + val penvval_in : itm_ -> term list
14.48 + val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
14.49 + val vars_of : itm list -> term list
14.50 + val max_vt : itm list -> int
14.51 +
14.52 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.53 + type penv
14.54 + val penv2str_ : Proof.context -> penv -> string (* NONE *)
14.55 + type preori
14.56 + val preoris2str : preori list -> string
14.57 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
14.58 + (* NONE *)
14.59 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.60 +
14.61 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
14.62 + val untouched : itm list -> bool
14.63 + type envv
14.64 + val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv
14.65 + val item_ppc : string ppc -> item ppc
14.66 + val all_ts_in : itm_ list -> term list
14.67 + val pres2str : (bool * term) list -> string
14.68 +end
14.69 +
14.70 +structure Model(**) : MODEL(**) =
14.71 +struct
14.72 +(*==========================================================================
14.73 +23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
14.74 +(1) kinds of itms:
14.75 + (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
14.76 + =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
14.77 + (1.2) Syn,Typ,Sup: not related to oris
14.78 + Syn, Typ (presently) should be accepted in appl_add (instead Error')
14.79 + Sup (presently) should be accepted in appl_add (instead Error')
14.80 + _could_ be w.r.t current vat (and then _is_ related to vat
14.81 + Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
14.82 +- dsc in itm_ is timeconsuming -- keep id for respective queries ?
14.83 +- order of items in ppc should be stable w.r.t order of itms
14.84 +
14.85 +- stepwise input of itms --- match_itms (in one go) ..not coordinated
14.86 + - unify code
14.87 + - match_itms / match_itms_oris ..2 versions ?!
14.88 + (fast, for refine / slow, for modeling)
14.89 +
14.90 +- clarify: efficiency <--> simplicity !!!
14.91 + ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
14.92 + | take int for perserving order of item ppc in itms
14.93 + | make all(!?) handling of itms stable against reordering(?)
14.94 + | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
14.95 + -"- "#undef" ?= not touched ?= (id,..)
14.96 +-----------------------------------------------------------------
14.97 +27.3.02:
14.98 +def: type pbt = (field, (dsc, pid)) *** design considerations ***
14.99 +
14.100 +(1) fmz + pbt -> oris
14.101 +(2) input + oris -> itm
14.102 +(3) match_itms : schnell(?) f"ur refine
14.103 + match_itms_oris : r"uckmeldung f"ur item ppc
14.104 +
14.105 +(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
14.106 +---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
14.107 +
14.108 +(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
14.109 + wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
14.110 + (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
14.111 + (b)
14.112 +==========================================================================*)
14.113 +
14.114 +val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
14.115 +val e_listReal = script_parse "[]::(real list)";
14.116 +val e_listBool = script_parse "[]::(bool list)";
14.117 +
14.118 +(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
14.119 +fun take_apart t =
14.120 + let val elems = TermC.isalist2list t
14.121 + in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
14.122 +fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
14.123 + let val elems = (flat o (map TermC.isalist2list)) ts;
14.124 + in TermC.list2isalist (type_of (hd elems)) elems end;
14.125 +
14.126 +fun is_var (Free _) = true
14.127 + | is_var _ = false;
14.128 +
14.129 +(* special handling for lists. ?WN:14.5.03 ??!? *)
14.130 +fun dest_list (d, ts) =
14.131 + let fun dest t =
14.132 + if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
14.133 + then TermC.isalist2list t
14.134 + else [t]
14.135 + in (flat o (map dest)) ts end;
14.136 +
14.137 +(* revert split_dts only for ts; compare comp_dts *)
14.138 +fun comp_ts (d, ts) =
14.139 + if Input_Descript.is_list_dsc d
14.140 + then if TermC.is_list (hd ts)
14.141 + then if Input_Descript.is_unl d
14.142 + then (hd ts) (* e.g. someList [1,3,2] *)
14.143 + else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
14.144 + else (hd ts) (* a variable or metavariable for a list *)
14.145 + else (hd ts);
14.146 +fun comp_dts (d, []) =
14.147 + if Input_Descript.is_reall_dsc d
14.148 + then (d $ e_listReal)
14.149 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
14.150 + | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
14.151 + handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
14.152 +fun comp_dts' (d, []) =
14.153 + if Input_Descript.is_reall_dsc d
14.154 + then (d $ e_listReal)
14.155 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
14.156 + | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
14.157 + handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
14.158 +fun comp_dts'' (d, []) =
14.159 + if Input_Descript.is_reall_dsc d
14.160 + then UnparseC.term (d $ e_listReal)
14.161 + else if Input_Descript.is_booll_dsc d
14.162 + then UnparseC.term (d $ e_listBool)
14.163 + else UnparseC.term d
14.164 + | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))
14.165 + handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
14.166 +
14.167 +(* decompose an input into description, terms (ev. elems of lists),
14.168 + and the value for the problem-environment; inv to comp_dts *)
14.169 +fun split_dts (t as d $ arg) =
14.170 + if Input_Descript.is_dsc d
14.171 + then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
14.172 + then (d, take_apart arg)
14.173 + else (d, [arg])
14.174 + else (TermC.empty, TermC.dest_list' t)
14.175 + | split_dts t =
14.176 + let val t' as (h, _) = strip_comb t;
14.177 + in
14.178 + if Input_Descript.is_dsc h
14.179 + then (h, dest_list t')
14.180 + else (TermC.empty, TermC.dest_list' t)
14.181 + end;
14.182 +(* version returning ts only *)
14.183 +fun split_dts' (d, arg) =
14.184 + if Input_Descript.is_dsc d
14.185 + then if Input_Descript.is_list_dsc d
14.186 + then if TermC.is_list arg
14.187 + then if Input_Descript.is_unl d
14.188 + then ([arg]) (* e.g. someList [1,3,2] *)
14.189 + else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
14.190 + else ([arg]) (* a variable or metavariable for a list *)
14.191 + else ([arg])
14.192 + else (TermC.dest_list' arg)
14.193 +(* WN170204: Warning "redundant"
14.194 + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
14.195 + let val (h,argl) = strip_comb t
14.196 + in
14.197 + if (not o is_dsc) h
14.198 + then (dest_list' t)
14.199 + else (dest_list (h,argl))
14.200 + end;*)
14.201 +(* revert split_:
14.202 + WN050903 we do NOT know which is from subtheory, description or term;
14.203 + typecheck thus may lead to TYPE-error 'unknown constant';
14.204 + solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
14.205 +(*fun comp_dts thy (d,[]) =
14.206 + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
14.207 + (Thy_Info_get_theory "Isac_Knowledge")
14.208 + (*comp_dts:FIXXME stay with term for efficiency !!!*)
14.209 + (if is_reall_dsc d then (d $ e_listReal)
14.210 + else if is_booll_dsc d then (d $ e_listBool)
14.211 + else d)
14.212 + | comp_dts (d,ts) =
14.213 + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
14.214 + (Thy_Info_get_theory "Isac_Knowledge")
14.215 + (*comp_dts:FIXXME stay with term for efficiency !!*)
14.216 + (d $ (comp_ts (d, ts)))
14.217 + handle _ => error ("comp_dts: "^(term2str d)^
14.218 + " $ "^(term2str (hd ts))));*)
14.219 +
14.220 +(* 27.8.01: problem-environment
14.221 +WN.6.5.03: FIXXME reconsider if penv is worth the effort --
14.222 + -- just rerun a whole expl with num/var may show the same ?!
14.223 +WN.9.5.03: penv-concept stalled, immediately generate script env !
14.224 + but [#0, epsilon] only outcommented for eventual reconsideration *)
14.225 +type penv = (* problem-environment *)
14.226 + (term (* err_ *)
14.227 + * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
14.228 + ) list;
14.229 +fun pen2str ctxt (t, ts) =
14.230 + pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
14.231 +fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
14.232 +
14.233 +(* get the constant value from a penv *)
14.234 +fun getval (id, values) =
14.235 + case values of
14.236 + [] => error ("penv_value: no values in '" ^ UnparseC.term id)
14.237 + | [v] => (id, v)
14.238 + | (v1 :: v2 :: _) => (case v1 of
14.239 + Const ("Program.Arbfix",_) => (id, v2)
14.240 + | _ => (id, v1));
14.241 +
14.242 +(* 9.5.03: still unused, but left for eventual future development *)
14.243 +type envv = (int * penv) list; (* over variants *)
14.244 +
14.245 +(* 14.9.01: not used after putting penv-values into itm_
14.246 + make the result of split_* a value of problem-environment *)
14.247 +fun mkval _(*dsc*) [] = error "mkval called with []"
14.248 + | mkval _ [t] = t
14.249 + | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
14.250 +fun mkval' x = mkval TermC.empty x;
14.251 +
14.252 +(* the internal representation of a models' item
14.253 + 4.9.01: not consistent:
14.254 + after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
14.255 + (involves 'is_error');
14.256 + bool in itm really necessary ???*)
14.257 +datatype itm_ = datatype Model_Def.itm_; (* internal state from fun parsitm *)
14.258 +
14.259 +type vats = Model_Def.vats;
14.260 +
14.261 +(* data-type for working on pbl/met-ppc:
14.262 + in pbl initially holds descriptions (only) for user guidance *)
14.263 +type itm =
14.264 + int * (* id =0 .. untouched - descript (only) from init
14.265 + seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
14.266 + vats * (* variants - copy from ori *)
14.267 + bool * (* input on this item is not/complete *)
14.268 + string * (* #Given | #Find | #Relate *)
14.269 + itm_; (* *)
14.270 +val e_itm = (0, [], false, "e_itm", Syn "e_itm");
14.271 +
14.272 +(* in CalcTree/Subproblem an 'untouched' model is created
14.273 + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
14.274 +fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
14.275 +
14.276 +(* find most frequent variant v in itms *)
14.277 +fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
14.278 +
14.279 +fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
14.280 +fun vts_cnt vts itms = map (cnt itms) vts;
14.281 +fun max2 [] = error "max2 of []"
14.282 + | max2 (y :: ys) =
14.283 + let
14.284 + fun mx (a,x) [] = (a,x)
14.285 + | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
14.286 + in mx y ys end;
14.287 +
14.288 +(* find the variant with most items already input *)
14.289 +fun max_vt itms =
14.290 + let val vts = (vts_cnt (vts_in itms)) itms;
14.291 + in if vts = [] then 0 else (fst o max2) vts end;
14.292 +
14.293 +(* TODO ev. make more efficient by avoiding flat *)
14.294 +fun mk_e (Cor (_, iv)) = [getval iv]
14.295 + | mk_e (Syn _) = []
14.296 + | mk_e (Typ _) = []
14.297 + | mk_e (Inc (_, iv)) = [getval iv]
14.298 + | mk_e (Sup _) = []
14.299 + | mk_e (Mis _) = []
14.300 + | mk_e _ = error "mk_e: uncovered case in fun.def.";
14.301 +fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
14.302 +
14.303 +(* extract the environment from an item list; takes the variant with most items *)
14.304 +fun mk_env itms =
14.305 + let val vt = max_vt itms
14.306 + in (flat o (map (mk_en vt))) itms end;
14.307 +
14.308 +
14.309 +
14.310 +(* example as provided by an author, complete w.r.t. pbt specified
14.311 + not touched by any user action *)
14.312 +type ori = Model_Def.ori;
14.313 +val e_ori = Model_Def.e_ori;
14.314 +
14.315 +val oris2str = Model_Def.oris2str;
14.316 +
14.317 +(* an or without leading integer *)
14.318 +type preori = (vats * string * term * term list);
14.319 +fun preori2str (vs, fi, t, ts) =
14.320 + "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
14.321 + UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
14.322 +val preoris2str = (strs2str' o (map (linefeed o preori2str)));
14.323 +
14.324 +(* 9.5.03 penv postponed: pbl_ids' *)
14.325 +fun pbl_ids' d vs = [comp_ts (d, vs)];
14.326 +
14.327 +(* 14.9.01: not used after putting values for penv into itm_
14.328 + WN.5.5.03: used in upd .. upd_envv *)
14.329 +fun upd_penv ctxt penv dsc (id, vl) =
14.330 +((*tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
14.331 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
14.332 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";*)
14.333 + overwrite (penv, (id, Input_Descript.pbl_ids ctxt dsc vl))
14.334 +);
14.335 +
14.336 +(* WN.9.5.03: not reconsidered; looks strange !!!*)
14.337 +fun upd thy envv dsc (id, vl) i =
14.338 + let val penv = case assoc (envv, i) of
14.339 + SOME e => e
14.340 + | NONE => [];
14.341 + val penv' = upd_penv thy penv dsc (id, vl);
14.342 + in (i, penv') end;
14.343 +
14.344 +(* 14.9.01: not used after putting pre-penv into itm_*)
14.345 +fun upd_envv thy envv vats dsc id vl =
14.346 + let val vats = if length vats = 0
14.347 + then (*unknown id to _all_ variants*)
14.348 + if length envv = 0 then [1]
14.349 + else (intsto o length) envv
14.350 + else vats
14.351 + fun isin vats (i, _) = member op = vats i;
14.352 + val envs_notin_vat = filter_out (isin vats) envv;
14.353 + in (map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat end;
14.354 +
14.355 +(* update envv by folding from a list of arguments *)
14.356 +fun upds_envv _ envv [] = envv
14.357 + | upds_envv thy envv ((vs, dsc, id, vl) :: ps) =
14.358 + upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
14.359 +
14.360 +(* for _output_ of the items of a Model *)
14.361 +datatype item =
14.362 + Correct of TermC.as_string (* labels a correct formula (type cterm') *)
14.363 + | SyntaxE of string (**)
14.364 + | TypeE of string (**)
14.365 + | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
14.366 + | Incompl of TermC.as_string (**)
14.367 + | Superfl of string (**)
14.368 + | Missing of TermC.as_string;
14.369 +fun item2str (Correct s) = "Correct " ^ s
14.370 + | item2str (SyntaxE s) = "SyntaxE " ^ s
14.371 + | item2str (TypeE s) = "TypeE " ^ s
14.372 + | item2str (False s) = "False " ^ s
14.373 + | item2str (Incompl s) = "Incompl " ^ s
14.374 + | item2str (Superfl s) = "Superfl " ^ s
14.375 + | item2str (Missing s) = "Missing " ^ s;
14.376 +
14.377 +fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
14.378 + "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
14.379 + | itm_2str_ _ (Syn c) = "Syn " ^ c
14.380 + | itm_2str_ _ (Typ c) = "Typ " ^ c
14.381 + | itm_2str_ ctxt (Inc ((d, ts), penv)) =
14.382 + "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
14.383 + | itm_2str_ ctxt (Sup (d, ts)) =
14.384 + "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts))
14.385 + | itm_2str_ ctxt (Mis (d, pid)) =
14.386 + "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
14.387 + | itm_2str_ _ (Par s) = "Trm "^s;
14.388 +fun itm_2str t = itm_2str_ (ThyC.id_to_ctxt "Isac_Knowledge") t;
14.389 +
14.390 +fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
14.391 + "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
14.392 + s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
14.393 +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
14.394 +fun init_item str = SyntaxE str;
14.395 +
14.396 +type 'a ppc =
14.397 + {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
14.398 +fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
14.399 + "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find =" ^ strs2str Find ^
14.400 + ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";
14.401 +
14.402 +fun item_ppc {Given = gi, Where= wh, Find = fi, With = wi, Relate= re} =
14.403 + {Given = map init_item gi, Where= map init_item wh, Find = map init_item fi,
14.404 + With = map init_item wi, Relate= map init_item re};
14.405 +fun itemppc2str ({Given=Given,Where=Where,
14.406 + Find=Find,With=With,Relate=Relate}:item ppc)=
14.407 + ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
14.408 + ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
14.409 + ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
14.410 + ",With =" ^ ((strs2str' o (map item2str)) With ) ^
14.411 + ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
14.412 +
14.413 +val empty_ppc = {Given = [], Where= [], Find = [], With = [], Relate= []};
14.414 +
14.415 +fun ts_in (Cor ((_, ts), _)) = ts
14.416 + | ts_in (Syn _) = []
14.417 + | ts_in (Typ _) = []
14.418 + | ts_in (Inc ((_, ts), _)) = ts
14.419 + | ts_in (Sup (_, ts)) = ts
14.420 + | ts_in (Mis _) = []
14.421 + | ts_in _ = error "ts_in: uncovered case in fun.def.";
14.422 +(*WN050629 unused*)
14.423 +fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
14.424 +val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
14.425 +fun d_in (Cor ((d ,_), _)) = d
14.426 + | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
14.427 + | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
14.428 + | d_in (Inc ((d, _), _)) = d
14.429 + | d_in (Sup (d, _)) = d
14.430 + | d_in (Mis (d, _)) = d
14.431 + | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
14.432 +
14.433 +fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
14.434 +fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
14.435 + | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
14.436 + | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
14.437 + | penvval_in (Inc (_, (_, ts))) = ts
14.438 + | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
14.439 + | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
14.440 + pair2str(UnparseC.term d, UnparseC.term t));*) [])
14.441 + | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
14.442 +
14.443 +(* check a predicate labelled with indication of incomplete substitution;
14.444 + rls -> (* for eval_true *)
14.445 + bool * (* have _all_ variables(Free) from the model-pattern
14.446 + been substituted by a value from the pattern's environment ?*)
14.447 + term -> (* the precondition *)
14.448 + bool * (* has the precondition evaluated to true *)
14.449 + term (* the precondition (for map) *)
14.450 +*)
14.451 +fun pre2str (b, t) = pair2str(bool2str b, UnparseC.term t);
14.452 +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
14.453 +
14.454 +fun vars_of itms = itms |> mk_env |> map snd
14.455 +
14.456 +end;
14.457 \ No newline at end of file
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/Tools/isac/Specify/mstools.sml Mon May 04 16:25:14 2020 +0200
15.3 @@ -0,0 +1,98 @@
15.4 +(* Title: tools for 'modeling' und 'specifying' to be used in
15.5 + modspec.sml. The types are separated into this file,
15.6 + because some of them are stored in the calc-tree, and thus are required
15.7 + _before_ ctree.sml.
15.8 + TODO: allocate elements of Selem and of Stool appropriately
15.9 + Author: Walther Neuper, Mathias Lehnfeld
15.10 + (c) due to copyright terms
15.11 +*)
15.12 +
15.13 +signature SPECIFY_TOOL =
15.14 +sig
15.15 + val check_preconds : 'a -> Rule_Set.T -> term list -> Model.itm list -> (bool * term) list
15.16 + val check_preconds' : Rule_Set.T -> term list -> Model.itm list -> 'a -> (bool * term) list
15.17 +
15.18 + datatype match_ = Match_ of Problem.id * (Model.itm list * (bool * term) list) | NoMatch_
15.19 + val refined_ : match_ list -> match_ option
15.20 + datatype match = Matches of Problem.id * Model.item Model.ppc | NoMatch of Problem.id * Model.item Model.ppc
15.21 + val matchs2str : match list -> string
15.22 + val common_subthy : theory * theory -> theory
15.23 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.24 + val pres2str : (bool * term) list -> string
15.25 + val refined : match list -> Problem.id
15.26 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15.27 + (*NONE*)
15.28 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
15.29 +
15.30 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
15.31 + val pblID_of_match : match -> Problem.id
15.32 + val refined_IDitms : match list -> match option
15.33 +end
15.34 +
15.35 +structure Stool(**) : SPECIFY_TOOL(**) =
15.36 +struct
15.37 +
15.38 +datatype match =
15.39 + Matches of Problem.id * Model.item Model.ppc
15.40 +| NoMatch of Problem.id * Model.item Model.ppc;
15.41 +fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")"
15.42 + | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")";
15.43 +fun matchs2str ms = (strs2str o (map match2str)) ms;
15.44 +fun pblID_of_match (Matches (pI, _)) = pI
15.45 + | pblID_of_match (NoMatch (pI, _)) = pI;
15.46 +
15.47 +(* 10.03 for Refine_Problem *)
15.48 +datatype match_ =
15.49 + Match_ of Problem.id * (( Model.itm list) * ((bool * term) list))
15.50 +| NoMatch_;
15.51 +
15.52 +(* the refined pbt is the last_element Matches in the list *)
15.53 +fun is_matches (Matches _) = true
15.54 + | is_matches _ = false;
15.55 +fun matches_pblID (Matches (pI, _)) = pI
15.56 + | matches_pblID _ = error "matches_pblID: uncovered case in fun.def.";
15.57 +fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
15.58 + handle _ => [];
15.59 +fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
15.60 +
15.61 +(* the refined pbt is the last_element Matches in the list, for Refine_Problem, tryrefine *)
15.62 +fun is_matches_ (Match_ _) = true
15.63 + | is_matches_ _ = false;
15.64 +fun refined_ ms = ((find_first is_matches_) o rev) ms;
15.65 +
15.66 +(* check a predicate labelled with indication of incomplete substitution;
15.67 + rls -> (* for eval_true *)
15.68 + bool * (* have _all_ variables(Free) from the model-pattern
15.69 + been substituted by a value from the pattern's environment ?*)
15.70 + term -> (* the precondition *)
15.71 + bool * (* has the precondition evaluated to true *)
15.72 + term (* the precondition (for map) *)
15.73 +*)
15.74 +fun evalprecond _ (false, pre) =
15.75 + (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
15.76 + (false, pre)
15.77 + | evalprecond prls (true, pre) =
15.78 + if Rewrite.eval_true (ThyC.get_theory "Isac_Knowledge") (* for Pattern.match *)
15.79 + [pre] prls (* pre parsed, prls.thy *)
15.80 + then (true , pre)
15.81 + else (false , pre);
15.82 +
15.83 +fun pre2str (b, t) = pair2str (bool2str b, UnparseC.term t);
15.84 +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
15.85 +
15.86 +(* check preconditions, return true if all true *)
15.87 +fun check_preconds' _ [] _ _ = [] (* empty preconditions are true *)
15.88 + | check_preconds' prls pres pbl _ (* FIXME.WN0308 mvat re-introduce *) =
15.89 + let
15.90 + val env = Model.mk_env pbl;
15.91 + val pres' = map (TermC.subst_atomic_all env) pres;
15.92 + in map (evalprecond prls) pres' end;
15.93 +fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl);
15.94 +
15.95 +
15.96 +fun common_subthy (thy1, thy2) =
15.97 + if Context.subthy (thy1, thy2) then thy2
15.98 + else if Context.subthy (thy2, thy1) then thy1
15.99 + else ThyC.get_theory "Isac_Knowledge"
15.100 +
15.101 +end;
16.1 --- a/src/Tools/isac/Specify/ptyps.sml Mon May 04 13:27:45 2020 +0200
16.2 +++ b/src/Tools/isac/Specify/ptyps.sml Mon May 04 16:25:14 2020 +0200
16.3 @@ -11,7 +11,7 @@
16.4 val get_fun_ids : theory -> (string * typ) list
16.5 type field
16.6 (* for calchead.sml, if below at left margin *)
16.7 - val prep_ori : Selem.fmz_ -> theory -> field list -> Model.ori list * Proof.context
16.8 + val prep_ori : Celem.fmz_ -> theory -> field list -> Model.ori list * Proof.context
16.9 val add_id : 'a list -> (int * 'a) list
16.10 val add_field' : theory -> field list -> Model.ori list -> Model.ori list
16.11 val match_itms_oris : theory -> Model.itm list -> field list * term list * Rule_Set.T ->
16.12 @@ -60,8 +60,8 @@
16.13 val show_ptyps : unit -> unit
16.14 val show_mets : unit -> unit
16.15 datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
16.16 - val match_pbl : Selem.fmz_ -> Problem.T -> match'
16.17 - val refine : Selem.fmz_ -> Problem.id -> Stool.match list
16.18 + val match_pbl : Celem.fmz_ -> Problem.T -> match'
16.19 + val refine : Celem.fmz_ -> Problem.id -> Stool.match list
16.20 val e_errpat : Error_Pattern_Def.T
16.21 val show_pblguhs : unit -> unit
16.22 val sort_pblguhs : unit -> unit
17.1 --- a/src/Tools/isac/Specify/specify.sml Mon May 04 13:27:45 2020 +0200
17.2 +++ b/src/Tools/isac/Specify/specify.sml Mon May 04 16:25:14 2020 +0200
17.3 @@ -1,7 +1,7 @@
17.4 signature SPECIFY_NEW =
17.5 sig
17.6 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
17.7 - val nxt_specify_init_calc : Selem.fmz -> Chead.calcstate
17.8 + val nxt_specify_init_calc : Celem.fmz -> Chead.calcstate
17.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
17.10 (*NONE*)
17.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
18.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon May 04 13:27:45 2020 +0200
18.2 +++ b/src/Tools/isac/Specify/step-specify.sml Mon May 04 16:25:14 2020 +0200
18.3 @@ -9,7 +9,7 @@
18.4 val by_tactic_input: Tactic.input -> Calc.T -> Chead.calcstate'
18.5 val by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
18.6 (* ---- keep, probably required later in devel. ----------------------------------------------- *)
18.7 - val nxt_specify_init_calc: Selem.fmz
18.8 + val nxt_specify_init_calc: Celem.fmz
18.9 -> Calc.T * State_Steps.T
18.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
18.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19.1 --- a/src/Tools/isac/TODO.thy Mon May 04 13:27:45 2020 +0200
19.2 +++ b/src/Tools/isac/TODO.thy Mon May 04 16:25:14 2020 +0200
19.3 @@ -29,7 +29,6 @@
19.4 \item xxx
19.5 \item rename Tactic.Calculate -> Tactic.Evaluate
19.6 \item xxx
19.7 - \item rename/relocate: Selem.result -> Calc.result ?OR? (NEW..)Formula.result
19.8 \item xxx
19.9 \item replace src/ Erls by Rule_Set.Empty
19.10 \item xxx
19.11 @@ -332,7 +331,6 @@
19.12 \item special naming for solutions of equation solving: x_1, x_2, ...
19.13 \end{itemize}
19.14 \item xxx
19.15 - \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
19.16 \item xxx
19.17 \item this has been written in one go:
19.18 \begin{itemize}
20.1 --- a/src/Tools/isac/Test_Code/test-code.sml Mon May 04 13:27:45 2020 +0200
20.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Mon May 04 16:25:14 2020 +0200
20.3 @@ -10,9 +10,9 @@
20.4 val f2str : Generate.mout -> TermC.as_string
20.5 val TESTg_form : Calc.T -> Generate.mout
20.6
20.7 - val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
20.8 + val CalcTreeTEST : Celem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Celem.safe * Ctree.ctree
20.9 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
20.10 - Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
20.11 + Pos.pos' * NEW * Generate.mout * Tactic.input * Celem.safe * Ctree.ctree
20.12
20.13 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
20.14 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
20.15 @@ -58,7 +58,7 @@
20.16 val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
20.17 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
20.18 val f = TESTg_form (pt,p)
20.19 - in (p, []:NEW, f, tac, Telem.Sundef, pt) end
20.20 + in (p, []:NEW, f, tac, Celem.Sundef, pt) end
20.21 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
20.22
20.23 fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
20.24 @@ -87,7 +87,7 @@
20.25 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
20.26 in
20.27 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
20.28 - tac, Telem.Sundef, pt)
20.29 + tac, Celem.Sundef, pt)
20.30 end
20.31
20.32
21.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Mon May 04 13:27:45 2020 +0200
21.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Mon May 04 16:25:14 2020 +0200
21.3 @@ -298,7 +298,7 @@
21.4
21.5 "~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
21.6 = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
21.7 - tac, Telem.Sundef, pt);
21.8 + tac, Celem.Sundef, pt);
21.9 (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
21.10
21.11 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
22.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon May 04 13:27:45 2020 +0200
22.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon May 04 16:25:14 2020 +0200
22.3 @@ -192,9 +192,9 @@
22.4 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
22.5 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
22.6
22.7 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
22.8 + (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
22.9 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
22.10 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
22.11 + = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
22.12
22.13 (*//--------------------- check results from modified me ----------------------------------\\*)
22.14 if p = ([2], Res) andalso
23.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon May 04 13:27:45 2020 +0200
23.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon May 04 16:25:14 2020 +0200
23.3 @@ -282,7 +282,7 @@
23.4 "solveForVars [c, c_2]", "solution LL"];
23.5
23.6 (*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*)
23.7 -"~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]);
23.8 +"~~~~~ fun refine, args:"; val ((fmz: Celem.fmz_), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]);
23.9 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
23.10 ((rev o tl) pblID, fmz, [(*match list*)],
23.11 ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node));
24.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Mon May 04 13:27:45 2020 +0200
24.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Mon May 04 16:25:14 2020 +0200
24.3 @@ -66,7 +66,7 @@
24.4 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
24.5
24.6 val pt = EmptyPtree;
24.7 -val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt;
24.8 +val pt = append_problem [] (Istate.empty, ContextC.empty) Celem.e_fmz ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt;
24.9 val ctxt = get_obj g_ctxt pt [];
24.10 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
24.11
25.1 --- a/test/Tools/isac/MathEngBasic/specification-elems.sml Mon May 04 13:27:45 2020 +0200
25.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
25.3 @@ -1,18 +0,0 @@
25.4 -(* ~~/test/Tools/isac/Interpret/specification-elems.sml
25.5 - Author: Walther Neuper
25.6 - Use is subject to license terms.
25.7 -*)
25.8 -
25.9 -"-----------------------------------------------------------------------------";
25.10 -"-----------------------------------------------------------------------------";
25.11 -"table of contents -----------------------------------------------------------";
25.12 -"-----------------------------------------------------------------------------";
25.13 -"-------- TODO'---------------------------------------------------------------";
25.14 -"-----------------------------------------------------------------------------";
25.15 -"-----------------------------------------------------------------------------";
25.16 -"-----------------------------------------------------------------------------";
25.17 -
25.18 -
25.19 -"-------- TODO'---------------------------------------------------------------";
25.20 -"-------- TODO'---------------------------------------------------------------";
25.21 -"-------- TODO'---------------------------------------------------------------";
26.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml Mon May 04 13:27:45 2020 +0200
26.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml Mon May 04 16:25:14 2020 +0200
26.3 @@ -18,7 +18,7 @@
26.4 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
26.5 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
26.6 ;
26.7 -Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * result -> Tactic.T;
26.8 +Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
26.9 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
26.10 ;
26.11 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
27.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 04 13:27:45 2020 +0200
27.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 04 16:25:14 2020 +0200
27.3 @@ -144,7 +144,7 @@
27.4 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
27.5 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
27.6
27.7 -"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
27.8 +"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):Celem.fmz] = [(fmz, (dI,pI,mI))];
27.9 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
27.10 val thy = ThyC.get_theory dI;
27.11 mI = ["no_met"]; (*false*)
28.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon May 04 13:27:45 2020 +0200
28.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon May 04 16:25:14 2020 +0200
28.3 @@ -10,8 +10,8 @@
28.4 val (dI',pI',mI') =
28.5 ("Isac_Knowledge", ["sqroot-test","univariate","equation","test"],
28.6 ["Test","squ-equ-test-subpbl1"]);
28.7 -"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
28.8 -"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : fmz_, (dI, pI, mI) : Spec.T) = (fmz, sp);
28.9 +"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp): Celem.fmz] = [(fmz, (dI',pI',mI'))];
28.10 +"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Celem.fmz_, (dI, pI, mI) : Spec.T) = (fmz, sp);
28.11 val thy = ThyC.get_theory dI;
28.12 (*if*) mI = ["no_met"]; (*else*)
28.13 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
29.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon May 04 13:27:45 2020 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Mon May 04 16:25:14 2020 +0200
29.3 @@ -85,7 +85,7 @@
29.4 val tacis as (_::_) = (*case*) ts (*of*);
29.5 val (tac, _, _) = last_elem tacis;
29.6
29.7 - (p, [] : NEW, TESTg_form (pt'''''_', p'''''_'), tac, Telem.Sundef, pt) (*return from me*);
29.8 + (p, [] : NEW, TESTg_form (pt'''''_', p'''''_'), tac, Celem.Sundef, pt) (*return from me*);
29.9 (*\------------------- end step into 1 -----------------------------------------------------/*)
29.10
29.11 (*/------------------- begin step into 2 ---------------------------------------------------\*)
30.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon May 04 13:27:45 2020 +0200
30.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon May 04 16:25:14 2020 +0200
30.3 @@ -118,7 +118,6 @@
30.4 open Step_Solve;
30.5 open Step;
30.6 open Solve; (* NONE *)
30.7 - open Selem; e_fmz;
30.8 open Stool; (* NONE *)
30.9 open ContextC; transfer_asms_from_to;
30.10 open Tactic; (* NONE *)
30.11 @@ -235,7 +234,6 @@
30.12 ML_file "MathEngBasic/rewrite.sml"
30.13 ML_file "MathEngBasic/model.sml"
30.14 ML_file "MathEngBasic/mstools.sml"
30.15 - ML_file "MathEngBasic/specification-elems.sml"
30.16 ML_file "MathEngBasic/tactic.sml"
30.17 ML_file "MathEngBasic/ctree.sml"
30.18 ML_file "MathEngBasic/calculation.sml"