1.1 --- a/src/Tools/isac/Specify/Specify.thy Mon May 04 16:25:14 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/Specify.thy Mon May 04 16:47:32 2020 +0200
1.3 @@ -7,6 +7,8 @@
1.4 imports "~~/src/Tools/isac/MathEngBasic/MathEngBasic"
1.5 begin
1.6 (* removed all warnings here, only "handle _" remains *)
1.7 + ML_file "o-model.sml"
1.8 + ML_file "i-model.sml"
1.9 ML_file "model.sml"
1.10 ML_file "mstools.sml"
1.11 ML_file ptyps.sml
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon May 04 16:47:32 2020 +0200
2.3 @@ -0,0 +1,49 @@
2.4 +(* Title: Specify/i-model.sml
2.5 + Author: Walther Neuper 110226
2.6 + (c) due to copyright terms
2.7 + *)
2.8 +
2.9 +signature MODEL_FOR_INTERACTION =
2.10 +sig
2.11 +(*/------- to O_Model+I_ from ModelModel -------\*)
2.12 + type vats = Model_Def.vats
2.13 +(*\------- to O_Model+I_ from ModelModel -------/*)
2.14 +(*/------- to I_Model from Model -------\*)
2.15 + datatype itm_ = datatype Model_Def.itm_
2.16 + type itm = Model_Def.itm
2.17 + val e_itm : itm
2.18 +(*\------- to I_Model from Model -------/*)
2.19 +
2.20 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.21 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.22 + (* NONE *)
2.23 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.24 +end
2.25 +
2.26 +structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
2.27 +struct
2.28 +(*/------- to O_Model+I_ from Mode -------\*)
2.29 +type vats = Model_Def.vats;
2.30 +(*\------- to O_Model+I_ from Model -------/*)
2.31 +(*/------- to I_Model from Model -------\*)
2.32 +(* the internal representation of a models' item
2.33 + 4.9.01: not consistent:
2.34 + after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
2.35 + (involves 'is_error');
2.36 + bool in itm really necessary ???*)
2.37 +datatype itm_ = datatype Model_Def.itm_; (* internal state from fun parsitm *)
2.38 +
2.39 +(* data-type for working on pbl/met-ppc:
2.40 + in pbl initially holds descriptions (only) for user guidance *)
2.41 +type itm =
2.42 + int * (* id =0 .. untouched - descript (only) from init
2.43 + seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
2.44 + vats * (* variants - copy from ori *)
2.45 + bool * (* input on this item is not/complete *)
2.46 + string * (* #Given | #Find | #Relate *)
2.47 + itm_; (* *)
2.48 +val e_itm = (0, [], false, "e_itm", Syn "e_itm");
2.49 +(*\------- to I_Model from Model -------/*)
2.50 +
2.51 +
2.52 +(**)end(**);
2.53 \ No newline at end of file
3.1 --- a/src/Tools/isac/Specify/model.sml Mon May 04 16:25:14 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/model.sml Mon May 04 16:47:32 2020 +0200
3.3 @@ -8,14 +8,20 @@
3.4
3.5 signature MODEL =
3.6 sig
3.7 +(*/------- to O_Model+I_ from ModelModel -------\*)
3.8 type vats = Model_Def.vats
3.9 +(*\------- to O_Model+I_ from ModelModel -------/*)
3.10 +(*/------- to O_Model from Model -------\*)
3.11 type ori = Model_Def.ori
3.12 val oris2str: ori list -> string
3.13 val e_ori: ori
3.14 +(*\------- to O_Model from Model -------/*)
3.15
3.16 +(*/------- to I_Model from Model -------\*)
3.17 datatype itm_ = datatype Model_Def.itm_
3.18 type itm = Model_Def.itm
3.19 val e_itm : itm
3.20 +(*\------- to I_Model from Model -------/*)
3.21
3.22 datatype item
3.23 = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
3.24 @@ -246,6 +252,11 @@
3.25 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
3.26 fun mkval' x = mkval TermC.empty x;
3.27
3.28 +(*/------- to O_Model+I_ from Mode -------\*)
3.29 +type vats = Model_Def.vats;
3.30 +(*\------- to O_Model+I_ from Model -------/*)
3.31 +
3.32 +(*/------- to I_Model from Model -------\*)
3.33 (* the internal representation of a models' item
3.34 4.9.01: not consistent:
3.35 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
3.36 @@ -253,8 +264,6 @@
3.37 bool in itm really necessary ???*)
3.38 datatype itm_ = datatype Model_Def.itm_; (* internal state from fun parsitm *)
3.39
3.40 -type vats = Model_Def.vats;
3.41 -
3.42 (* data-type for working on pbl/met-ppc:
3.43 in pbl initially holds descriptions (only) for user guidance *)
3.44 type itm =
3.45 @@ -265,6 +274,7 @@
3.46 string * (* #Given | #Find | #Relate *)
3.47 itm_; (* *)
3.48 val e_itm = (0, [], false, "e_itm", Syn "e_itm");
3.49 +(*\------- to I_Model from Model -------/*)
3.50
3.51 (* in CalcTree/Subproblem an 'untouched' model is created
3.52 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
3.53 @@ -304,12 +314,14 @@
3.54
3.55
3.56
3.57 +(*/------- to O_Model from Model -------\*)
3.58 (* example as provided by an author, complete w.r.t. pbt specified
3.59 not touched by any user action *)
3.60 type ori = Model_Def.ori;
3.61 val e_ori = Model_Def.e_ori;
3.62
3.63 val oris2str = Model_Def.oris2str;
3.64 +(*\------- to O_Model from Model -------/*)
3.65
3.66 (* an or without leading integer *)
3.67 type preori = (vats * string * term * term list);
3.68 @@ -450,4 +462,4 @@
3.69
3.70 fun vars_of itms = itms |> mk_env |> map snd
3.71
3.72 -end;
3.73 \ No newline at end of file
3.74 +(**)end(**);
3.75 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon May 04 16:47:32 2020 +0200
4.3 @@ -0,0 +1,38 @@
4.4 +(* Title: Specify/o-model.sml
4.5 + Author: Walther Neuper 110226
4.6 + (c) due to copyright terms
4.7 + *)
4.8 +
4.9 +signature ORIGINAL_MODEL =
4.10 +sig
4.11 +(*/------- to O_Model+I_ from ModelModel -------\*)
4.12 + type vats = Model_Def.vats
4.13 +(*\------- to O_Model+I_ from ModelModel -------/*)
4.14 +(*/------- to O_Model from Model -------\*)
4.15 + type ori = Model_Def.ori
4.16 + val oris2str: ori list -> string
4.17 + val e_ori: ori
4.18 +(*\------- to O_Model from Model -------/*)
4.19 +
4.20 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.21 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.22 + (* NONE *)
4.23 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.24 +end
4.25 +
4.26 +structure O_Model(**) : ORIGINAL_MODEL(**) =
4.27 +struct
4.28 +(*/------- to O_Model+I_ from Mode -------\*)
4.29 +type vats = Model_Def.vats;
4.30 +(*\------- to O_Model+I_ from Model -------/*)
4.31 +(*/------- to O_Model from Model -------\*)
4.32 +(* example as provided by an author, complete w.r.t. pbt specified
4.33 + not touched by any user action *)
4.34 +type ori = Model_Def.ori;
4.35 +val e_ori = Model_Def.e_ori;
4.36 +
4.37 +val oris2str = Model_Def.oris2str;
4.38 +(*\------- to O_Model from Model -------/*)
4.39 +
4.40 +
4.41 +(**)end(**);
4.42 \ No newline at end of file
5.1 --- a/src/Tools/isac/TODO.thy Mon May 04 16:25:14 2020 +0200
5.2 +++ b/src/Tools/isac/TODO.thy Mon May 04 16:47:32 2020 +0200
5.3 @@ -23,8 +23,8 @@
5.4 \<close>
5.5 subsection \<open>Current changeset\<close>
5.6 text \<open>
5.7 -(*/------- to from -------\*)
5.8 -(*\------- to from -------/*)
5.9 +(*/------- to from -------\*)
5.10 +(*\------- to from -------/*)
5.11 \begin{itemize}
5.12 \item xxx
5.13 \item rename Tactic.Calculate -> Tactic.Evaluate