1.1 --- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Jun 20 17:36:25 2022 +0200
1.2 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Jun 20 17:42:49 2022 +0200
1.3 @@ -1168,7 +1168,7 @@
1.4 % ppc : pat list,
1.5 % (*this is the model-pattern;
1.6 % it contains "#Given","#Where","#Find","#Relate"-patterns
1.7 -% for constraints on identifiers see "fun cpy_nam"*)
1.8 +% for constraints on identifiers see "fun copy_name"*)
1.9 % met : metID list}; (* methods solving the pbt*)
1.10 %
1.11 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
2.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Mon Jun 20 17:36:25 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Mon Jun 20 17:42:49 2022 +0200
2.3 @@ -47,7 +47,7 @@
2.4 scr : Rule.program, (* filled in MethodC.prep_input *)
2.5 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
2.6 ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate"
2.7 - for constraints on identifiers see "O_Model.cpy_nam" *)
2.8 + for constraints on identifiers see "O_Model.copy_name" *)
2.9 pre : term list (* ? DEL, as soon as they are input interactively ? *)
2.10 };
2.11 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
3.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Jun 20 17:36:25 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Jun 20 17:42:49 2022 +0200
3.3 @@ -47,7 +47,7 @@
3.4 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
3.5 where_ : term list, (* ? DEL, as soon as they are input interactively ? *)
3.6 ppc : Model_Pattern.T (* contains "#Given", "#Where", "#Find", "#Relate"
3.7 - for constraints on identifiers see "O_Model.cpy_nam" *)
3.8 + for constraints on identifiers see "O_Model.copy_name" *)
3.9 }
3.10 val empty = {guh = "pbl_empty", mathauthors = [], init = id_empty, thy = @{theory "Pure"},
3.11 cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : T
4.1 --- a/src/Tools/isac/Specify/m-match.sml Mon Jun 20 17:36:25 2022 +0200
4.2 +++ b/src/Tools/isac/Specify/m-match.sml Mon Jun 20 17:42:49 2022 +0200
4.3 @@ -188,7 +188,7 @@
4.4 end
4.5
4.6 (* match the actual arguments of a SubProblem with a model-pattern
4.7 - and create an ori list (in root-pbl created from formalization).
4.8 + and create an O_Model (in root-pbl created from Formalise.model).
4.9 expects ags:pats = 1:1, while copy-named are filtered out of pats;
4.10 if no 1:1 then exn raised by matc/mtc and handled at call.
4.11 copy-named pats are appended in order to get them into the Model-items *)
4.12 @@ -198,7 +198,7 @@
4.13 val pbt' = filter_out O_Model.is_copy_named pbt
4.14 val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
4.15 val oris' = matc thy pbt' ags []
4.16 - val cy' = map (O_Model.cpy_nam pbt' oris') cy
4.17 + val cy' = map (O_Model.copy_name pbt' oris') cy
4.18 val ors = O_Model.add_enumerate (oris' @ cy') (*...appended in order to get into the Model-items *)
4.19 in (map flattup ors) end
4.20
5.1 --- a/src/Tools/isac/Specify/o-model.sml Mon Jun 20 17:36:25 2022 +0200
5.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon Jun 20 17:42:49 2022 +0200
5.3 @@ -44,8 +44,8 @@
5.4
5.5 val add_enumerate: 'a list -> (int * 'a) list
5.6 type preori
5.7 -(*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
5.8 - val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
5.9 +(*val copy_name: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
5.10 + val copy_name: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
5.11 val is_copy_named: Model_Pattern.single -> bool
5.12 val is_copy_named_idstr: string -> bool
5.13 \<^isac_test>\<open>
5.14 @@ -261,7 +261,7 @@
5.15 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
5.16 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
5.17 but leave is_copy_named_generating as is, e.t. ss''' *)
5.18 -fun cpy_nam pbt oris (p as (field, (dsc, t))) =
5.19 +fun copy_name pbt oris (p as (field, (dsc, t))) =
5.20 case \<^try>\<open>
5.21 if is_copy_named_generating p
5.22 then (*WN051014 kept strange old code ...*)
5.23 @@ -275,7 +275,7 @@
5.24 else ([1], field, dsc, [t])
5.25 \<close> of
5.26 SOME x => x
5.27 - | NONE => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
5.28 + | NONE => raise ERROR ("copy_name: for "^ UnparseC.term t)
5.29
5.30
5.31 (** tools for I_Model **)
6.1 --- a/test/Tools/isac/Specify/m-match.sml Mon Jun 20 17:36:25 2022 +0200
6.2 +++ b/test/Tools/isac/Specify/m-match.sml Mon Jun 20 17:42:49 2022 +0200
6.3 @@ -8,7 +8,7 @@
6.4 "-----------------------------------------------------------------------------------------------";
6.5 "----------- fun match_pbl ---------------------------------------------------------------------";
6.6 "----------- fun match_oris --------------------------------------------------------------------";
6.7 -"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
6.8 +"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ----------------------";
6.9 "-----------------------------------------------------------------------------------------------";
6.10 "-----------------------------------------------------------------------------------------------";
6.11 "-----------------------------------------------------------------------------------------------";
6.12 @@ -52,9 +52,9 @@
6.13 then () else error "fun match_oris CHANGED";
6.14
6.15
6.16 -"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
6.17 -"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
6.18 -"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
6.19 +"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ----------------------";
6.20 +"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ----------------------";
6.21 +"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ----------------------";
6.22 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
6.23 (Const (\<^const_name>\<open>Pair\<close>,_) $
6.24 Free (dI',_) $
6.25 @@ -145,7 +145,7 @@
6.26 ============ inhibit exn AK110726 ==============================================*)
6.27
6.28 "-------------------------------------step through end---";
6.29 -"--------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!)--";
6.30 +"--------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)--";
6.31 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
6.32 (Const (\<^const_name>\<open>Pair\<close>,_) $
6.33 Free (dI',_) $
6.34 @@ -304,8 +304,8 @@
6.35 "-d3-----------------------------------------------------";
6.36 pbt = []; (*true, base case*)
6.37 "-----------------continue step through code M_Match.arguments---";
6.38 - val oris' = oris @ [ori]; (*result 2 oris, O_Model.cpy_nam added later*)
6.39 -"--------------------------------step through O_Model.cpy_nam----";
6.40 + val oris' = oris @ [ori]; (*result 2 oris, O_Model.copy_name added later*)
6.41 +"--------------------------------step through O_Model.copy_name----";
6.42 val (pbt, oris, p as (field, (dsc, t)):Model_Pattern.single) = (pbt', oris', hd cy);
6.43 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
6.44 "--------------------------------------------------------";
6.45 @@ -336,7 +336,7 @@
6.46 val cy_ext = (free2str o the) (LibraryC.assoc (vars'~~vals, cy'))^"_"^ext;
6.47 (*x_i*)
6.48 "-----------------continue step through code M_Match.arguments---";
6.49 - val cy' = map (O_Model.cpy_nam pbt' oris') cy;
6.50 + val cy' = map (O_Model.copy_name pbt' oris') cy;
6.51 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
6.52 "-------------------------------------step through end---";
6.53
7.1 --- a/test/Tools/isac/Specify/o-model.sml Mon Jun 20 17:36:25 2022 +0200
7.2 +++ b/test/Tools/isac/Specify/o-model.sml Mon Jun 20 17:42:49 2022 +0200
7.3 @@ -12,7 +12,7 @@
7.4 "----------- fun add_enumerate ------------------------------------------------------------------------";
7.5 "----------- fun filter_vat --------------------------------------------------------------------";
7.6 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
7.7 -"----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
7.8 +"----------- .. CONTINUED regr.test fun O_Model.copy_name ----------------------------------------";
7.9 "-----------------------------------------------------------------------------------------------";
7.10 "-----------------------------------------------------------------------------------------------";
7.11 "-----------------------------------------------------------------------------------------------";
7.12 @@ -228,10 +228,10 @@
7.13 if is_copy_named_generating trm then error "regr. O_Model.is_copy_named" else ();
7.14 *)
7.15
7.16 -"----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
7.17 -"----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
7.18 -"----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
7.19 -(*data from above - M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!)-:*)
7.20 +"----------- .. CONTINUED regr.test fun O_Model.copy_name ----------------------------------------";
7.21 +"----------- .. CONTINUED regr.test fun O_Model.copy_name ----------------------------------------";
7.22 +"----------- .. CONTINUED regr.test fun O_Model.copy_name ----------------------------------------";
7.23 +(*data from above - M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)-:*)
7.24 (*the model-pattern, O_Model.is_copy_named are filter_out*)
7.25 val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
7.26 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
7.27 @@ -241,11 +241,11 @@
7.28 val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
7.29 (*...all must be true*)
7.30
7.31 -case O_Model.cpy_nam pbt oris (hd cy) of
7.32 +case O_Model.copy_name pbt oris (hd cy) of
7.33 ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()
7.34 - | _ => error "calchead.sml regr.test O_Model.cpy_nam-1-";
7.35 + | _ => error "calchead.sml regr.test O_Model.copy_name-1-";
7.36
7.37 -(*new data: O_Model.cpy_nam without changing the name*)
7.38 +(*new data: O_Model.copy_name without changing the name*)
7.39 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
7.40 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
7.41 @{term "solution"}; type_of @{term "ss''' :: bool list"};
7.42 @@ -258,7 +258,7 @@
7.43 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
7.44 (*could be more than 1*)];
7.45
7.46 -case O_Model.cpy_nam pbt oris (hd cy) of
7.47 +case O_Model.copy_name pbt oris (hd cy) of
7.48 ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
7.49 - | _ => error "calchead.sml regr.test O_Model.cpy_nam-2-";
7.50 + | _ => error "calchead.sml regr.test O_Model.copy_name-2-";
7.51