32 \<close> ML \<open> |
32 \<close> ML \<open> |
33 \<close> ML \<open> |
33 \<close> ML \<open> |
34 \<close> ML \<open> |
34 \<close> ML \<open> |
35 \<close> ML \<open> (** preliminary handling of References **) |
35 \<close> ML \<open> (** preliminary handling of References **) |
36 \<close> ML \<open> (* assumption: we read the Specfication as a whole *) |
36 \<close> ML \<open> (* assumption: we read the Specfication as a whole *) |
37 (*/-------------------- state of src/../preliminary at that time -----------------------------\*) |
37 (*/-------------------- state of src/../preliminary.sml at that time -------------------------\*) |
38 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*))) |
38 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*))) |
39 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*))) |
39 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*))) |
40 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*))) |
40 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*))) |
41 ; |
41 ; |
42 re_eval_all: unit -> unit; |
42 re_eval_all: unit -> unit; |
59 \<close> ML \<open> |
59 \<close> ML \<open> |
60 \<close> ML \<open> |
60 \<close> ML \<open> |
61 \<close> ML \<open> |
61 \<close> ML \<open> |
62 \<close> ML \<open> |
62 \<close> ML \<open> |
63 \<close> ML \<open> |
63 \<close> ML \<open> |
64 (*\-------------------- state of src/../preliminary at that time -----------------------------/*) |
64 (*\-------------------- state of src/../preliminary.sml at that time -------------------------/*) |
65 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*) |
65 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*) |
66 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; |
66 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; |
67 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; |
67 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; |
68 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; |
68 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; |
69 "----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------"; |
69 "----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------"; |
92 case the_data thy of |
92 case the_data thy of |
93 Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id |
93 Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id |
94 | _ => the_data thy |
94 | _ => the_data thy |
95 \<close> ML \<open> |
95 \<close> ML \<open> |
96 (*let*) |
96 (*let*) |
97 val ctree = the_data thy |
|
98 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} = |
97 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} = |
99 Ctree.get_obj I ctree [(*Pos will become variable*)] |> Ctree.rep_specify_data |
98 Ctree.get_obj I state [(*Pos will become variable*)] |> Ctree.rep_specify_data |
100 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref) |
99 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref) |
101 val (model, where_) = Model_Pattern.parse_pos ctxt model_input (*+check syntax*) |
100 val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input (*+check syntax*) |
102 \<close> ML \<open> |
101 \<close> ML \<open> |
103 \<close> ML \<open> |
102 (model, where_) (*GOON*) |
104 (*Specify.check_input \<longrightarrow> specify.sml*) |
|
105 fun check_input _ = 123 |
|
106 \<close> ML \<open> |
|
107 \<close> ML \<open> |
|
108 \<close> ML \<open> |
|
109 \<close> ML \<open> |
103 \<close> ML \<open> |
110 (**) |
104 (**) |
111 val _ = re_eval References.empty References.empty; |
105 val _ = re_eval References.empty References.empty; |
112 (**) |
106 (**) |
113 \<close> ML \<open> |
107 \<close> ML \<open> |
114 (*in*) Preliminary.update_state_TEST thy |
108 (*in*) Preliminary.update_state_TEST thy |
115 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy) |
109 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy) |
116 (*end*) |
110 (*end*) |
117 \<close> ML \<open> |
111 \<close> ML \<open> |
|
112 (*POSTPONED Specify.check_input \<longrightarrow> specify.sml*) |
|
113 fun check_input _ = 123 |
118 \<close> ML \<open> |
114 \<close> ML \<open> |
119 \<close> ML \<open> |
115 \<close> ML \<open> |
120 \<close> ML \<open> |
116 \<close> ML \<open> |
121 \<close> ML \<open> |
117 \<close> ML \<open> |
122 \<close> ML \<open> |
118 \<close> ML \<open> |
140 case the_data thy of |
136 case the_data thy of |
141 Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id |
137 Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id |
142 | _ => |
138 | _ => |
143 let |
139 let |
144 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} = |
140 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} = |
145 Ctree.get_obj I (the_data thy) [] |> Ctree.rep_specify_data |
141 Ctree.get_obj I state [] |> Ctree.rep_specify_data |
146 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref) |
142 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref) |
147 val (model, where_) = Model_Pattern.parse_pos ctxt model_input |
143 val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input |
148 (**) |
144 (**) |
149 val _ = re_eval References.empty References.empty |
145 val _ = re_eval References.empty References.empty |
150 (**) |
146 (**) |
151 in Preliminary.update_state_TEST thy |
147 in |
|
148 Preliminary.update_state_TEST thy |
152 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy) |
149 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy) |
153 end |
150 end |
154 in set_data state thy end))); |
151 in set_data state thy end))); |
155 \<close> ML \<open> |
152 \<close> ML \<open> |
156 \<close> ML \<open> (*Example_TEST below*) |
153 \<close> ML \<open> (*Example_TEST below*) |
157 \<close> |
154 \<close> |
158 |
155 |
178 (*Solution:*) |
175 (*Solution:*) |
179 |
176 |
180 text \<open> |
177 text \<open> |
181 Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a" |
178 Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a" |
182 \<close> |
179 \<close> |
183 Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) |
180 (* |
|
181 Example: no syntax check of terms, OK. |
|
182 Example_TEST: proper syntax check of terms with Model_Pattern.parse_pos, |
|
183 but with parse_pos_TEST ERROR Malformed YXML: unbalanced element "input" |
|
184 *) |
|
185 (**)Example |
|
186 (** )Example_TEST( **) "Diff_App-No.123a" (*complete Model, empty References*) |
184 Specification: |
187 Specification: |
185 Model: |
188 Model: |
186 Given: \<open>Constants [r = 7]\<close> |
189 Given: \<open>Constants [r = 7]\<close> |
187 Where: \<open>0 < r\<close> |
190 Where: \<open>0 < r\<close> |
188 Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close> |
191 Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close> |