1 (* Title: Specify/o-model.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 An \<open>O_Model\<close> holds \<open>O\<close>riginal data, \<open>descriptor\<close> and \<open>values\<close> parsed from \<open>Formalise.model\<close>
6 selected with respect to a \<open>Model_Pattern\<close> and combined with respective \<open>m_field\<close>s.
7 \<open>complete_for\<close> a \<open>Model_Pattern\<close> is done by \<open>Tactic.Model_Problem\<close>
8 (with defaults from \<open>Formalise\<close>refs), by \<open>Tactic.Specify_Problem\<close> and \<open>Tactic.Specify_Method\<close>
10 \<open>O_Model\<close> serves efficiency of student's interactive modelling via \<open>I_Model\<close>.
12 \<open>O_Model\<close> marks elements with \<open>m_field\<close> \<open>#undef\<close>, which are not required by the \<open>Model_Pattern\<close>
13 of the \<open>Problem\<close> or the \<open>Method\<close> .. TODO redes: \<open>m_field\<close> probably different in root..Subproblem
15 TODO: revise with an example with more than 1 variant.
16 + consider: drop m_field ?
19 signature ORIGINAL_MODEL =
28 val to_string: T -> string
29 val single_to_string: single -> string
30 val single_empty: single
32 (*val init: theory -> Formalise.model -> Model_Pattern.T -> T ..TODO*)
33 val init: Formalise.model -> theory -> Model_Pattern.T -> T
34 val add : theory -> Model_Pattern.T -> T -> T
35 val values : T -> term list
36 val values': T -> Formalise.model * term list
37 (*/------- rename -------\*)
38 (*val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context*)
39 val complete_for_from: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
40 (*val seek_oridts: Proof.context -> ?/////? -> descriptor * values -> T -> message * single * values*)
41 val seek_oridts: Proof.context -> m_field -> descriptor * values -> T -> message * single * values
42 (*val single_for_values:!!! values -> Proof.context -> m_field -> T -> message * single * values*)
43 val seek_orits: Proof.context -> m_field -> values -> T -> message * single * values
44 (*val ?contains:!!! term -> Proof.context -> m_field -> T -> message * single * values*)
45 val is_known: Proof.context -> m_field -> T -> term -> message * single * values
46 (*val typeless: term -> term*)
47 val typeless: term -> term
48 (*val test_types: Proof.context -> descriptor * values -> string*)
49 val test_types: Proof.context -> descriptor * values -> string
51 (*put add_id into a new auxiliary fun, see ONLY call..*)
52 val add_id: 'a list -> (int * 'a) list
54 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
55 (*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
56 val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
57 val is_copy_named: Model_Pattern.single -> bool
58 val is_copy_named_idstr: string -> bool
59 val is_copy_named_generating_idstr: string -> bool
60 val is_copy_named_generating: Model_Pattern.single -> bool
62 val preoris2str : preori list -> string
63 (*val getr_ct: theory -> single -> m_field * UnparseC.term_as_string*)
64 val getr_ct: theory -> single -> m_field * UnparseC.term_as_string
66 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
67 val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
68 val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
69 (*val max: variants -> int*)
70 val max: variants -> int
71 (*val coll_variants: ('a * ''b) list -> ('a list * ''b) list*)
72 val coll_variants: ('a * ''b) list -> ('a list * ''b) list
73 (*val replace_0: int -> int list -> int list*)
74 val replace_0: int -> int list -> int list
75 val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
76 (*val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list*)
77 val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
78 (*\------- rename -------/*)
79 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
83 structure O_Model(**) : ORIGINAL_MODEL(**) =
89 type variants = Model_Def.variants;
90 type m_field = Model_Def.m_field;
91 type descriptor = Model_Def.descriptor;
92 type values = Model_Def.values;
93 type message = string;
95 type T = Model_Def.o_model;
96 type single = Model_Def.o_model_single
97 val single_empty = Model_Def.o_model_empty;
98 val single_to_string = Model_Def.o_model_single_to_string;
99 val to_string = Model_Def.o_model_to_string;
101 (* O_Model.single without leading integer *)
102 type preori = (variants * m_field * term * term list);
103 fun preori2str (vs, fi, t, ts) =
104 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
105 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
106 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
108 (* get the first term in ts from ori *)
109 fun getr_ct thy (_, _, fd, d, ts) =
110 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
113 (** initialise O_Model **)
115 (* compare d and dsc in pbt and transfer field to pre-ori *)
116 fun add_field (_: theory) pbt (d,ts) =
117 let fun eq d pt = (d = (fst o snd) pt);
118 in case filter (eq d) pbt of
119 [(fi, (_, _))] => (fi, d, ts)
120 | [] => ("#undef", d, ts) (*may come with met.ppc*)
121 | _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
125 mark an element with the position within a plateau;
126 a plateau with length 1 is marked with 0
128 fun mark _ [] = raise ERROR "mark []"
131 fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
132 | mar _ _ [] _ = raise ERROR "mark []"
133 | mar xx eq (x:: x' :: xs) n =
134 if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
135 else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
136 in mar [] eq xs 1 end;
139 assumes equal descriptions to be in adjacent 'plateaus',
140 items at a certain position within the plateaus form a variant;
141 length = 1 ... marked with 0: covers all variants
143 fun add_variants fdts =
145 fun eq (a, b) = curry op= (snd3 a) (snd3 b);
148 fun max [] = raise ERROR "max of []"
151 | mx x (y :: ys) = if x < y then mx y ys else mx x ys;
154 fun coll_variants (((v,x) :: vxs)) =
156 fun col xs (vs, x) [] = xs @ [(vs, x)]
157 | col xs (vs, x) ((v', x') :: vxs') =
158 if x = x' then col xs (vs @ [v'], x') vxs'
159 else col (xs @ [(vs, x)]) ([v'], x') vxs';
160 in col [] ([v], x) vxs end
161 | coll_variants _ = raise ERROR "coll_variants: called with []";
163 fun replace_0 vm [0] = intsto vm
164 | replace_0 _ vs = vs;
166 fun add_id [] = raise ERROR "O_Model.add_id []"
170 | add n (x :: xs) = (n, x) :: add (n + 1) xs;
173 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
180 |> TermC.parseNEW'' thy
181 |> Input_Descript.split
182 |> add_field thy pbt) fmz)
184 val maxv = model |> map fst |> max;
185 val maxv = if maxv = 0 then 1 else maxv;
188 |> map (replace_0 maxv |> apfst)
194 (** add new m_field's from method \<rightarrow> REPLACE BY complete_for_from **)
196 (* for the root-problem *)
199 fun eq d pt = (d = (fst o snd) pt);
200 fun repl mpc (i, v, _, d, ts) =
201 case filter (eq d) mpc of
202 [(fi, (_, _))] => [(i, v, fi, d, ts)]
203 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
204 | _ => raise ERROR ("O_Model.add: " ^ UnparseC.term d ^ " more than once in met");
205 in flat ((map (repl mpc)) ori) end;
208 (** get the values **)
210 fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"
212 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
213 fun mkval' x = mkval TermC.empty x;
214 (*TODO: unify with values'*)
215 fun values (oris:T) =
216 ((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
219 (** complete wrt. Model_Pattern.T by use of root's O_Model.T **)
221 fun complete_for_from m_patt root_model (o_model, ctxt) =
223 val missing = m_patt |> filter_out
224 (fn (_, (descriptor, _)) => (Library.member op = (map #4 o_model) descriptor))
225 val add = (root_model
227 (fn (_, _, _, descriptor, _) => (Library.member op = (map (fst o snd) missing)) descriptor))
228 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
230 (* indicate, that m_field ---------^^^^^^^^ might change from root- to sub-Model_Pattern * )
231 |> map (fn (a, b, _, d, e) => (a, b, "#undef", d, e))
232 ( * indicate, that m_field ---------^^^^^^^^ might change from root- to sub-Model_Pattern *)
235 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
236 |> add_id (* for correct enumeration *)
237 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
238 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
244 (* make oris from args of the stac SubProblem and from pbt.
245 can this formal argument (of a model-pattern) be omitted in the arg-list
246 of a SubProblem ? see calcelems.sml 'type met ' *)
247 fun is_copy_named_idstr str =
248 case (rev o Symbol.explode) str of
249 "'" :: _ :: "'" :: _ => true
251 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
253 (* should this formal argument (of a model-pattern) create a new identifier? *)
254 fun is_copy_named_generating_idstr str =
255 if is_copy_named_idstr str
257 case (rev o Symbol.explode) str of
258 "'" :: "'" :: "'" :: _ => false
261 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
263 (* generate a new variable "x_i" name from a related given one "x"
264 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
265 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
266 but leave is_copy_named_generating as is, e.t. ss''' *)
267 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
268 (if is_copy_named_generating p
269 then (*WN051014 kept strange old code ...*)
270 let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
271 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
272 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
273 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
274 val vals = map sel oris
275 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
276 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
277 else ([1], field, dsc, [t])
278 ) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
280 (* ["BOOL (1+x=2)", "REAL x"] --match_ags--> oris
281 --values'--> ["equality (1+x=2)", "boundVariable x", "solutions L"] *)
282 (*TODO: unify with values*)
284 let fun ori2fmz_vals (_, _, _, dsc, ts) =
285 ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
286 handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
287 in (split_list o (map ori2fmz_vals)) oris end
290 (** tools for I_Model **)
293 fun seek_oridts ctxt sel (d, ts) [] =
294 ("seek_oridts: input ('" ^
295 (UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",
298 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
299 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
300 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
301 else seek_oridts ctxt sel (d, ts) oris
303 fun seek_oridts ctxt m_field (descript, vals) [] =
304 ("seek_oridts: input ('" ^ UnparseC.term_in_ctxt ctxt (Input_Descript.join (descript, vals)) ^
305 "') not found in oris (typed)", (0, [], m_field, descript, vals), [])
306 | seek_oridts ctxt m_field (descript, vals) ((id, vat, m_field', descript', vals') :: oris) =
307 if (inter op = vals vals') <> [] andalso descript = descript' then
308 if m_field = "#undef" then (* m_field may change from root- to sub-Model_Pattern *)
309 ("", (id, vat, m_field, descript, inter op = vals vals'), vals')
310 else if m_field = m_field' then
311 ("", (id, vat, m_field, descript, inter op = vals vals'), vals')
313 (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) vals) ^
314 " not for " ^ m_field, single_empty, [])
315 else seek_oridts ctxt m_field (descript, vals) oris
317 (* to an input (_,ts) find the according ori and insert the ts *)
318 fun seek_orits ctxt _ values [] =
319 ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) values) ^
320 "') not found in oris (typed)", single_empty, [])
321 | seek_orits ctxt sel values ((id, vat, sel', d, values') :: oris) =
322 if (inter op = values values') <> [] then
323 if sel = "#undef" then (* indicates that m_field changed from root- to sub-Model_Pattern *)
324 ("", (id, vat, sel, d, inter op = values values'), values')
325 else if sel = sel' then
326 ("", (id, vat, sel, d, inter op = values values'), values')
328 (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) values) ^
329 " not for " ^ sel, single_empty, [])
330 else seek_orits ctxt sel values oris
332 fun test_types ctxt (d,ts) =
334 val opt = (try Input_Descript.join) (d, ts)
335 val msg = case opt of
337 | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
338 (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts ^ " is illtyped")
341 (* make a term 'typeless' for comparing with another 'typeless' term;
342 'type-less' usually is illtyped *)
343 fun typeless (Const (s, _)) = (Const (s, TermC.typ_empty))
344 | typeless (Free (s, _)) = (Free (s, TermC.typ_empty))
345 | typeless (Var (n, _)) = (Var (n, TermC.typ_empty))
346 | typeless (Bound i) = (Bound i)
347 | typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, typeless t)
348 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
350 (* is the term t input (or taken from fmz) known in O_Model ?
351 give feedback on all(?) strange input;
352 return _all_ terms already input to this item (e.g. valuesFor a,b) *)
353 fun is_known ctxt sel ori t =
355 val ots = (distinct o flat o (map #5)) ori
356 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
357 val (d, ts) = Input_Descript.split t
358 val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
360 if (subtract op = oids ids) <> []
361 then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", single_empty, [])
365 if not (subset op = (map typeless ts, map typeless ots))
366 then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^
367 "' not in example (typeless)", single_empty, [])
369 (case seek_orits ctxt sel ts(*..values*) ori of
370 ("", ori_ as (_, _, _, d, ts), all) =>
371 (case test_types ctxt (d,ts) of
372 "" => ("", ori_, all)
373 | msg => (msg, single_empty, []))
374 | (msg, _, _) => (msg, single_empty, []))
376 if member op = (map #4 ori) d
377 then seek_oridts ctxt sel (d, ts) ori
378 else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])