1 (* Title: Specify/o-model.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 This model combines Formalise.T and Model_Pattern.T;
6 it makes student's editing via I_Model.T more efficient.
8 TODO: revise with an example with more than 1 variant.
12 signature ORIGINAL_MODEL =
21 val to_string: T -> string
22 val single_to_string: single -> string
23 val single_empty: single
25 (*val init: theory -> Formalise.model -> Model_Pattern.T -> T ..TODO*)
26 val init: Formalise.model -> theory -> Model_Pattern.T -> T
27 val add : theory -> Model_Pattern.T -> T -> T
28 val values : T -> term list
29 val values': T -> Formalise.model * term list
30 val complete_for_from: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
31 (*/------- rename -------\*)
32 (*val seek_oridts: Proof.context -> ?/////? -> descriptor * values -> T -> message * single * values*)
33 val seek_oridts: Proof.context -> m_field -> descriptor * values -> T -> message * single * values
34 (*val seek_orits: Proof.context -> m_field -> values -> T -> message * single * values*)
35 val seek_orits: Proof.context -> m_field -> values -> T -> message * single * values
37 (*put add_id into a new auxiliary fun, see ONLY call..*)
38 val add_id: 'a list -> (int * 'a) list
40 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
41 (*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
42 val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
43 val is_copy_named: Model_Pattern.single -> bool
44 val is_copy_named_idstr: string -> bool
45 val is_copy_named_generating_idstr: string -> bool
46 val is_copy_named_generating: Model_Pattern.single -> bool
48 val preoris2str : preori list -> string
49 (*val getr_ct: theory -> single -> m_field * UnparseC.term_as_string*)
50 val getr_ct: theory -> single -> m_field * UnparseC.term_as_string
52 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
53 val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
54 val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
55 (*val max: variants -> int*)
56 val max: variants -> int
57 (*val coll_variants: ('a * ''b) list -> ('a list * ''b) list*)
58 val coll_variants: ('a * ''b) list -> ('a list * ''b) list
59 (*val replace_0: int -> int list -> int list*)
60 val replace_0: int -> int list -> int list
61 val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
62 (*val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list*)
63 val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
64 (*\------- rename -------/*)
65 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
69 structure O_Model(**) : ORIGINAL_MODEL(**) =
75 type variants = Model_Def.variants;
76 type m_field = Model_Def.m_field;
77 type descriptor = Model_Def.descriptor;
78 type values = Model_Def.values;
79 type message = string;
81 type T = Model_Def.o_model;
82 type single = Model_Def.o_model_single
83 val single_empty = Model_Def.o_model_empty;
84 val single_to_string = Model_Def.o_model_single_to_string;
85 val to_string = Model_Def.o_model_to_string;
87 (* O_Model.single without leading integer *)
88 type preori = (variants * m_field * term * term list);
89 fun preori2str (vs, fi, t, ts) =
90 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
91 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
92 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
94 (* get the first term in ts from ori *)
95 fun getr_ct thy (_, _, fd, d, ts) =
96 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
99 (** initialise O_Model **)
101 (* compare d and dsc in pbt and transfer field to pre-ori *)
102 fun add_field (_: theory) pbt (d,ts) =
103 let fun eq d pt = (d = (fst o snd) pt);
104 in case filter (eq d) pbt of
105 [(fi, (_, _))] => (fi, d, ts)
106 | [] => ("#undef", d, ts) (*may come with met.ppc*)
107 | _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
111 mark an element with the position within a plateau;
112 a plateau with length 1 is marked with 0
114 fun mark _ [] = raise ERROR "mark []"
117 fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
118 | mar _ _ [] _ = raise ERROR "mark []"
119 | mar xx eq (x:: x' :: xs) n =
120 if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
121 else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
122 in mar [] eq xs 1 end;
125 assumes equal descriptions to be in adjacent 'plateaus',
126 items at a certain position within the plateaus form a variant;
127 length = 1 ... marked with 0: covers all variants
129 fun add_variants fdts =
131 fun eq (a, b) = curry op= (snd3 a) (snd3 b);
134 fun max [] = raise ERROR "max of []"
137 | mx x (y :: ys) = if x < y then mx y ys else mx x ys;
140 fun coll_variants (((v,x) :: vxs)) =
142 fun col xs (vs, x) [] = xs @ [(vs, x)]
143 | col xs (vs, x) ((v', x') :: vxs') =
144 if x = x' then col xs (vs @ [v'], x') vxs'
145 else col (xs @ [(vs, x)]) ([v'], x') vxs';
146 in col [] ([v], x) vxs end
147 | coll_variants _ = raise ERROR "coll_variants: called with []";
149 fun replace_0 vm [0] = intsto vm
150 | replace_0 _ vs = vs;
152 fun add_id [] = raise ERROR "O_Model.add_id []"
156 | add n (x :: xs) = (n, x) :: add (n + 1) xs;
159 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
166 |> TermC.parseNEW'' thy
167 |> Input_Descript.split
168 |> add_field thy pbt) fmz)
170 val maxv = model |> map fst |> max;
171 val maxv = if maxv = 0 then 1 else maxv;
174 |> map (replace_0 maxv |> apfst)
180 (** add new m_field's from method \<rightarrow> REPLACE BY complete_for_from **)
182 (* for the root-problem *)
185 fun eq d pt = (d = (fst o snd) pt);
186 fun repl mpc (i, v, _, d, ts) =
187 case filter (eq d) mpc of
188 [(fi, (_, _))] => [(i, v, fi, d, ts)]
189 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
190 | _ => raise ERROR ("O_Model.add: " ^ UnparseC.term d ^ " more than once in met");
191 in flat ((map (repl mpc)) ori) end;
194 (** get the values **)
196 fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"
198 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
199 fun mkval' x = mkval TermC.empty x;
200 (*TODO: unify with values'*)
201 fun values (oris:T) =
202 ((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
205 (** complete wrt. Model_Pattern.T by use of root's O_Model.T **)
207 fun complete_for_from m_patt root_model (o_model, ctxt) =
209 val missing = m_patt |> filter_out
210 (fn (_, (descriptor, _)) => (Library.member op = (map #4 o_model) descriptor))
211 val add = (root_model |> filter
212 (fn (_, _, _, descriptor, _) => (Library.member op = (map (fst o snd) missing)) descriptor))
215 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration*)
216 |> add_id (* for correct enumeration*)
217 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))(* for correct enumeration*),
218 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
224 (* make oris from args of the stac SubProblem and from pbt.
225 can this formal argument (of a model-pattern) be omitted in the arg-list
226 of a SubProblem ? see calcelems.sml 'type met ' *)
227 fun is_copy_named_idstr str =
228 case (rev o Symbol.explode) str of
229 "'" :: _ :: "'" :: _ => true
231 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
233 (* should this formal argument (of a model-pattern) create a new identifier? *)
234 fun is_copy_named_generating_idstr str =
235 if is_copy_named_idstr str
237 case (rev o Symbol.explode) str of
238 "'" :: "'" :: "'" :: _ => false
241 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
243 (* generate a new variable "x_i" name from a related given one "x"
244 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
245 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
246 but leave is_copy_named_generating as is, e.t. ss''' *)
247 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
248 (if is_copy_named_generating p
249 then (*WN051014 kept strange old code ...*)
250 let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
251 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
252 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
253 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
254 val vals = map sel oris
255 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
256 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
257 else ([1], field, dsc, [t])
258 ) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
260 (* ["BOOL (1+x=2)", "REAL x"] --match_ags--> oris
261 --values'--> ["equality (1+x=2)", "boundVariable x", "solutions L"] *)
262 (*TODO: unify with values*)
264 let fun ori2fmz_vals (_, _, _, dsc, ts) =
265 ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
266 handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
267 in (split_list o (map ori2fmz_vals)) oris end
272 fun seek_oridts ctxt sel (d, ts) [] =
273 ("seek_oridts: input ('" ^
274 (UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",
277 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
278 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
279 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
280 else seek_oridts ctxt sel (d, ts) oris
282 (* to an input (_,ts) find the according ori and insert the ts *)
283 fun seek_orits ctxt _ ts [] =
284 ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^
285 "') not found in oris (typed)", single_empty, [])
286 | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
287 if sel = sel' andalso (inter op = ts ts') <> []
290 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
291 else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, single_empty, [])
292 else seek_orits ctxt sel ts oris