1 (* Title: Specify/i-model.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 \<open>I_Model\<close> serves students' interactive modelling and gives feedback in the specify-phase.
8 signature MODEL_FOR_INTERACTION =
14 val empty_single: single
19 datatype feedback = datatype Model_Def.i_model_feedback
22 val feedback_to_string': feedback -> string
23 val feedback_to_string: Proof.context -> feedback -> string
24 val single_to_string: Proof.context -> single -> string
25 val to_string: Proof.context -> T -> string
27 datatype add_single = Add of single | Err of string
28 val init: Model_Pattern.T -> T
29 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
30 TermC.as_string -> add_single
31 val add_single: theory -> single -> T -> T
33 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
34 val descriptor: feedback -> descriptor
35 val o_model_values: feedback -> O_Model.values
36 val variables: T -> term list
37 val max_variant: T -> int
38 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
40 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
42 val environment: T -> Env.T
43 val penvval_in: feedback -> term list
45 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
46 val add: single -> T -> T
47 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
48 val is_error: feedback -> bool
49 val complete': Model_Pattern.T -> O_Model.single -> single
51 val is_complete: T -> bool
52 val to_p_model: theory -> feedback -> string
53 val eq1: ''a -> 'b * (''a * 'c) -> bool
57 structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
63 type variant = Model_Def.variant;
64 type variants = Model_Def.variants;
65 type m_field = Model_Def.m_field;
66 type descriptor = Model_Def.descriptor;
68 type T = Model_Def.i_model_single list;
69 datatype feedback = datatype Model_Def.i_model_feedback;
70 type single = Model_Def.i_model_single;
71 val empty_single = Model_Def.i_model_empty;
73 type message = string;
75 fun pen2str ctxt (t, ts) =
76 pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term ctxt)) ts);
78 fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
79 "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
80 | feedback_to_string _ (Syn c) = "Syn " ^ c
81 | feedback_to_string _ (Typ c) = "Typ " ^ c
82 | feedback_to_string ctxt (Inc ((d, ts), penv)) =
83 "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
84 | feedback_to_string ctxt (Sup (d, ts)) =
85 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
86 | feedback_to_string ctxt (Mis (d, pid)) =
87 "Mis "^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
88 | feedback_to_string _ (Par s) = "Trm "^s;
89 fun feedback_to_string' t = feedback_to_string (ContextC.for_ERROR ()) t;
91 fun single_to_string ctxt (i, is, b, s, itm_) =
92 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
93 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
94 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
97 fun make_tactic m_field (term_as_string, i_model) =
99 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
100 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
101 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
102 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
105 (** initialise a model **)
109 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
110 in map pbt2itm pbt end
113 (** check input on a model **)
115 (* find most frequent variant v in itms *)
116 fun variants itms = ((distinct op =) o flat o (map #2)) (itms: T);
118 fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
119 fun count_variants vts itms = map (cnt itms) vts;
120 fun max2 [] = raise ERROR "max2 of []"
123 fun mx (a,x) [] = (a,x)
124 | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
127 (* get the constant value from a penv *)
128 fun getval (id, values) =
130 [] => raise ERROR ("penv_value: no values in '" ^ UnparseC.term (ContextC.for_ERROR ()) id)
132 | (v1 :: v2 :: _) => (case v1 of
133 Const (\<^const_name>\<open>Program.Arbfix\<close>, _) => (id, v2)
136 (* find the variant with most items already input *)
137 fun max_variant itms =
138 let val vts = (count_variants (variants itms)) itms;
139 in if vts = [] then 0 else (fst o max2) vts end;
141 (* TODO ev. make more efficient by avoiding flat *)
142 fun mk_e (Cor (_, iv)) = [getval iv]
145 | mk_e (Inc (_, iv)) = [getval iv]
148 | mk_e _ = raise ERROR "mk_e: uncovered case in fun.def.";
149 fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
151 (* extract the environment from an item list; takes the variant with most items *)
152 fun environment itms =
153 let val vt = max_variant itms
154 in (flat o (map (mk_en vt))) itms end;
156 fun o_model_values (Cor ((_, ts), _)) = ts
157 | o_model_values (Syn _) = []
158 | o_model_values (Typ _) = []
159 | o_model_values (Inc ((_, ts), _)) = ts
160 | o_model_values (Sup (_, ts)) = ts
161 | o_model_values (Mis _) = []
162 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
164 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
165 fun descriptor (Cor ((d ,_), _)) = d
166 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
167 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
168 | descriptor (Inc ((d, _), _)) = d
169 | descriptor (Sup (d, _)) = d
170 | descriptor (Mis (d, _)) = d
171 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
173 (*val string_of_descr_values: term * (term list) -> string
174 fun string_of_descr_values (d, ts) = pair2str (UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.terms ts);*)
175 fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d, ts)]
176 | penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
177 | penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
178 | penvval_in (Inc (_, (_, ts))) = ts
179 | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ string_of_descr_values dts);*) [])
180 | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
181 pair2str(UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.term (ContextC.for_ERROR ()) t));*) [])
182 | penvval_in _ = raise ERROR "penvval_in: uncovered case in fun.def.";
184 fun variables itms = itms |> environment |> map snd
186 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
188 (* get a term from O_Model, notyet input in I_Model.
189 the term from O_Model is thrown back to a string in order to reuse
190 machinery for immediate input by the user. *)
191 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
192 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
194 (* update the itm_ already input, all..from ori *)
195 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
197 val ts' = union op = (o_model_values itm_) ts;
198 val pval = [Input_Descript.join'''' (d, ts')]
199 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
200 val complete = if eq_set op = (ts', all) then true else false
204 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
205 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
206 | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
207 | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
210 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
211 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
212 | (Sup (d,ts')) => (*4.9.01 lost env*)
213 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
214 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
215 (* 28.1.00: not completely clear ---^^^ etc.*)
216 | (Mis _) => (* 4.9.01: Mis just copied *)
218 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
219 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
220 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string' i)
223 fun eq1 d (_, (d', _)) = (d = d')
224 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
226 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
227 case find_first (eq1 d) pbt of
228 SOME (_, (_, pid)) =>
229 (case find_first (eq3 f d) itms of
230 SOME (_, _, _, _, itm_) =>
231 let val ts' = inter op = (o_model_values itm_) ts
233 if subset op = (ts, ts')
234 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
235 else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
237 | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
238 | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
240 datatype add_single =
241 Add of single (* return-value of check_single *)
242 | Err of string (* error-message *)
245 Create feedback for input of TermC.as_string to m_field;
246 check w.r.t. O_Model.T and Model_Pattern.T.
247 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
248 check_single is extremely permissive.
250 (*will come directly from PIDE -----------------vvvvvvvvvvv
251 in case t comes from Step.specify_do_next -----------vvv = Position.none*)
252 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
254 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
255 (*/------------ replace by ParseC.term_position -----------\*)
256 val t = Syntax.read_term ctxt ct
257 handle ERROR msg => error (msg (*^ Position.here pos*))
258 (*\------------ replace by ParseC.term_position -----------/*)
259 (*NONE => Add (i, [], false, m_field, Syn ct)*)
260 val (d, ts) = Input_Descript.split t
262 if d = TermC.empty then
263 Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
265 (case find_first (eq1 d) m_patt of
266 NONE => Add (i, [], true, m_field, Sup (d,ts))
267 | SOME (f, (_, id)) =>
269 fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
271 case find_first (eq2 d) i_model of
272 NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
273 | SOME (i', _, _, _, itm_) =>
274 if Input_Descript.for_list d then
276 val in_itm = o_model_values itm_
277 val ts' = union op = ts in_itm
278 val i'' = if in_itm = [] then i else i'
279 in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
280 else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
283 (* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
284 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
285 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
287 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
288 handle ERROR msg => error (msg (*^ Position.here pp*))
289 (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
291 case Model_Pattern.get_field descriptor m_patt of
292 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
293 UnparseC.term ctxt descriptor ^ "\"")
295 if m_field <> m_field' then
296 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
297 "\" not for field \"" ^ m_field ^ "\"")
299 case O_Model.contains ctxt m_field o_model t of
301 (case is_notyet_input ctxt i_model all ori' m_patt of
303 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
304 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
310 fun overwrite_ppc thy itm model =
312 fun repl _ (_, _, _, _, itm_) [] =
313 raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_
315 | repl model' itm (p :: model) =
317 then model' @ [itm] @ model
318 else repl (model' @ [p]) itm model
319 in repl [] itm model end
321 (* find_first item with #1 equal to id *)
322 fun seek_ppc _ [] = NONE
323 | seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model
325 (* 10.3.00: insert the already compiled itm into model;
326 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
327 fun add_single thy itm model =
329 fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)
330 | eq_untouched _ _ = false
331 val model' = case seek_ppc (#1 itm) model of
332 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
333 | NONE => (model @ [itm])
334 in filter_out (eq_untouched ((descriptor o #5) itm)) model' end
336 fun complete' pbt (i, v, f, d, ts) =
337 case \<^try>\<open> (i, v, true, f, Cor ((d, ts),
338 ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)
341 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
343 (* filter out oris which have same description in itms *)
344 fun filter_outs oris [] = oris
345 | filter_outs oris (i::itms) =
347 val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris
352 (* filter oris which are in pbt, too *)
353 fun filter_pbt oris pbt =
355 val dscs = map (fst o snd) pbt
357 filter ((member op= dscs) o (#4)) oris
360 fun is_error (Cor _) = false
361 | is_error (Sup _) = false
362 | is_error (Inc _) = false
363 | is_error (Mis _) = false
366 (*create output-string for itm_*)
367 fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
368 | to_p_model _ (Syn c) = c
369 | to_p_model _ (Typ c) = c
370 | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
371 | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
372 | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid
373 | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
375 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)
377 (* insert_ppc = add for appl_add', input_icalhd 11.03,
378 handles superfluous items carelessly *)
379 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
381 (* combine itms from pbl + met and complete them wrt. pbt *)
382 (* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
383 fun complete oris pits mits met =
385 val vat = max_variant pits;
386 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
387 val ors = filter ((member_swap op= vat) o (#2)) oris
388 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
390 itms @ (map (complete' met) os)
393 (* complete model and guard of a calc-head *)
394 fun complete_method (oris, mpc, model, probl) =
396 val pits = filter_out ((curry op= false) o (#3)) probl
397 val vat = if probl = [] then 1 else max_variant probl
398 val pors = filter ((member_swap op = vat) o (#2)) oris
399 val pors = filter_outs pors pits (*which are in pbl already*)
400 val pors = (filter_pbt pors model) (*which are in pbt, too*)
401 val pits = pits @ (map (complete' model) pors)
402 val mits = complete oris pits [] mpc
405 (* TODO: also check if all elements are I_Model.Cor *)
406 fun is_complete ([]: T) = false
407 | is_complete itms = foldl and_ (true, (map #3 itms))