//reduce the number of TermC.parse*; "//"means: tests broken .
broken tests are outcommented with "reduce the number of TermC.parse*"
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 =
18 datatype feedback = datatype Model_Def.i_model_feedback
21 val feedback_to_string': feedback -> string
22 val feedback_to_string: Proof.context -> feedback -> string
23 val single_to_string: Proof.context -> single -> string
24 val to_string: Proof.context -> T -> string
26 (*/------- rename -------\*)
27 datatype additm = Add of single | Err of string
28 (*\------- rename -------/*)
29 val initPIDE: Problem.id -> T
30 val init: Model_Pattern.T -> T
31 (*val check_single: Proof.context -> *)
32 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
33 TermC.as_string -> additm
34 val add_single: theory -> single -> T -> T
36 (*/------- rename -------\*)
37 (*val make_tactic: m_field -> TermC.as_string * T -> Tactic.T*)
38 val get_tac: m_field -> TermC.as_string * T -> Tactic.T
39 (*val d_in: feedback -> descriptor*)
40 val d_in: feedback -> descriptor
41 (*val ts_in: feedback -> O_Model.values*)
42 val ts_in: feedback -> O_Model.values
43 (*val vars_of: T -> term list*)
44 val vars_of: T -> term list
45 (*val max_vt: T -> int*)
47 (*val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
49 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
51 (*val dsc_unknown: term*)
53 (*val geti_ct: theory -> O_Model.single -> single -> m_field * UnparseC.term_as_string*)
54 val geti_ct: theory -> O_Model.single -> single -> m_field * UnparseC.term_as_string
55 (*val pbl_ids': term -> term list -> term list*)
56 val pbl_ids': term -> term list -> term list
58 val mk_env: T -> (term * term) list
59 val penvval_in: feedback -> term list
60 (*\------- rename -------/*)
62 val complete: O_Model.T -> T -> T -> Model_Pattern.T -> T
63 val add: single -> T -> T
64 (*val complete_method: O_Model.T -> Model_Pattern.T * Model_Pattern.T * T -> T * T*)
65 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
66 val is_error: feedback -> bool
67 val complete': Model_Pattern.T -> O_Model.single -> single
69 val is_complete: T -> bool
70 val to_p_model: theory -> feedback -> string
71 (*/------- rename -------\*)
72 (*val dts2str: term * (term list) -> string*)
73 val dts2str: term * (term list) -> string
74 val eq1: ''a -> 'b * (''a * 'c) -> bool
75 (*\------- rename -------/*)
76 (*/------- rename -------\*)
78 val vts_in: T -> int list
83 structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
89 type variant = Model_Def.variant;
90 type variants = Model_Def.variants;
91 type m_field = Model_Def.m_field;
92 type descriptor = Model_Def.descriptor;
94 type T = Model_Def.i_model_single list;
95 datatype feedback = datatype Model_Def.i_model_feedback;
96 type single = Model_Def.i_model_single;
97 val empty = Model_Def.i_model_empty;
98 type message = string;
100 fun pen2str ctxt (t, ts) =
101 pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
103 fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
104 "Cor " ^ UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
105 | feedback_to_string _ (Syn c) = "Syn " ^ c
106 | feedback_to_string _ (Typ c) = "Typ " ^ c
107 | feedback_to_string ctxt (Inc ((d, ts), penv)) =
108 "Inc " ^ UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
109 | feedback_to_string ctxt (Sup (d, ts)) =
110 "Sup " ^ UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))
111 | feedback_to_string ctxt (Mis (d, pid)) =
112 "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
113 | feedback_to_string _ (Par s) = "Trm "^s;
114 fun feedback_to_string' t = feedback_to_string (ThyC.id_to_ctxt "Isac_Knowledge") t;
116 fun single_to_string ctxt (i, is, b, s, itm_) =
117 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
118 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
119 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
122 fun get_tac m_field (term_as_string, i_model) =
124 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
125 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
126 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
127 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
130 (** initialise a model **)
134 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
135 in map pbt2itm pbt end
137 fun initPIDE pbl_id = pbl_id |> Problem.from_store |> #ppc |> init
140 (** check input on a model **)
142 (* find most frequent variant v in itms *)
143 fun vts_in itms = ((distinct op =) o flat o (map #2)) (itms: T);
145 fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
146 fun vts_cnt vts itms = map (cnt itms) vts;
147 fun max2 [] = raise ERROR "max2 of []"
150 fun mx (a,x) [] = (a,x)
151 | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
154 (* get the constant value from a penv *)
155 fun getval (id, values) =
157 [] => raise ERROR ("penv_value: no values in '" ^ UnparseC.term id)
159 | (v1 :: v2 :: _) => (case v1 of
160 Const (\<^const_name>\<open>Program.Arbfix\<close>, _) => (id, v2)
163 (* find the variant with most items already input *)
165 let val vts = (vts_cnt (vts_in itms)) itms;
166 in if vts = [] then 0 else (fst o max2) vts end;
168 (* TODO ev. make more efficient by avoiding flat *)
169 fun mk_e (Cor (_, iv)) = [getval iv]
172 | mk_e (Inc (_, iv)) = [getval iv]
175 | mk_e _ = raise ERROR "mk_e: uncovered case in fun.def.";
176 fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
178 (* extract the environment from an item list; takes the variant with most items *)
180 let val vt = max_vt itms
181 in (flat o (map (mk_en vt))) itms end;
183 fun ts_in (Cor ((_, ts), _)) = ts
186 | ts_in (Inc ((_, ts), _)) = ts
187 | ts_in (Sup (_, ts)) = ts
189 | ts_in _ = raise ERROR "ts_in: uncovered case in fun.def.";
191 val unique = TermC.parseNEW'' @{theory "Real"} "UnIqE_tErM";
192 fun d_in (Cor ((d ,_), _)) = d
193 | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
194 | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
195 | d_in (Inc ((d, _), _)) = d
196 | d_in (Sup (d, _)) = d
197 | d_in (Mis (d, _)) = d
198 | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
200 fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
201 fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d, ts)]
202 | penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
203 | penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
204 | penvval_in (Inc (_, (_, ts))) = ts
205 | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
206 | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
207 pair2str(UnparseC.term d, UnparseC.term t));*) [])
208 | penvval_in _ = raise ERROR "penvval_in: uncovered case in fun.def.";
210 fun vars_of itms = itms |> mk_env |> map snd
212 val dsc_unknown = TermC.parseNEW'' @{theory} "unknown::'a => unknow";
214 (* get a term from ori, notyet input in itm.
215 the term from ori is thrown back to a string in order to reuse
216 machinery for immediate input by the user. *)
217 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
218 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (ts_in itm_) ts))
220 (* 9.5.03 penv postponed: pbl_ids' *)
221 fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];
223 (* update the itm_ already input, all..from ori *)
224 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
226 val ts' = union op = (ts_in itm_) ts;
227 val pval =pbl_ids' d ts'
228 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
229 val complete = if eq_set op = (ts', all) then true else false
233 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
234 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
235 | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
236 | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
239 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
240 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
241 | (Sup (d,ts')) => (*4.9.01 lost env*)
242 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
243 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
244 (* 28.1.00: not completely clear ---^^^ etc.*)
245 | (Mis _) => (* 4.9.01: Mis just copied *)
247 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
248 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
249 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string' i)
252 fun eq1 d (_, (d', _)) = (d = d')
253 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
255 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
256 case find_first (eq1 d) pbt of
257 SOME (_, (_, pid)) =>
258 (case find_first (eq3 f d) itms of
259 SOME (_, _, _, _, itm_) =>
260 let val ts' = inter op = (ts_in itm_) ts
262 if subset op = (ts, ts')
263 then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", empty)
264 else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
266 | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
267 | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
270 Add of single (* return-value of check_single *)
271 | Err of string (* error-message *)
274 Create feedback for input of TermC.as_string to m_field;
275 check w.r.t. O_Model.T and Model_Pattern.T.
276 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
277 check_single is extremely permissive.
279 fun check_single ctxt m_field [] i_model m_patt ct =
281 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
283 case TermC.parseNEW ctxt ct of
284 NONE => Add (i, [], false, m_field, Syn ct)
287 val (d, ts) = Input_Descript.split t
289 if d = TermC.empty then
290 Add (i, [], false, m_field, Mis (dsc_unknown, hd ts))
292 (case find_first (eq1 d) m_patt of
293 NONE => Add (i, [], true, m_field, Sup (d,ts))
294 | SOME (f, (_, id)) =>
296 fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
298 case find_first (eq2 d) i_model of
299 NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
300 | SOME (i', _, _, _, itm_) =>
301 if Input_Descript.for_list d then
303 val in_itm = ts_in itm_
304 val ts' = union op = ts in_itm
305 val i'' = if in_itm = [] then i else i'
306 in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
307 else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
311 (* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
312 | check_single ctxt m_field o_model i_model m_patt str =
313 case TermC.parseNEW ctxt str of
314 NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")
315 | SOME (t as (descriptor $ _)) =>
316 (case Model_Pattern.get_field descriptor m_patt of
317 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
318 UnparseC.term_in_ctxt ctxt descriptor ^ "\"")
320 if m_field <> m_field' then
321 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"" ^
322 "\" not for field \"" ^ m_field ^ "\"")
324 case O_Model.is_known ctxt m_field o_model t of
326 (case is_notyet_input ctxt i_model all ori' m_patt of
328 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
329 | (msg, _, _) => Err ("ERROR I_Model.check_single: is_known: " ^ msg))
330 | SOME t => Err ("ERROR I_Model.check_single: impossible for input \"" ^
331 UnparseC.term_in_ctxt ctxt t ^ "\"");
336 fun overwrite_ppc thy itm ppc =
338 fun repl _ (_, _, _, _, itm_) [] =
339 raise ERROR ("overwrite_ppc: " ^ (feedback_to_string (ThyC.to_ctxt thy) itm_) ^ " not found")
340 | repl ppc' itm (p :: ppc) =
342 then ppc' @ [itm] @ ppc
343 else repl (ppc' @ [p]) itm ppc
344 in repl [] itm ppc end
346 (* find_first item with #1 equal to id *)
347 fun seek_ppc _ [] = NONE
348 | seek_ppc id (p :: ppc) = if id = #1 (p: single) then SOME p else seek_ppc id ppc
350 (* 10.3.00: insert the already compiled itm into model;
351 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
352 fun add_single thy itm ppc =
354 fun eq_untouched d (0, _, _, _, itm_) = (d = d_in itm_)
355 | eq_untouched _ _ = false
356 val ppc' = case seek_ppc (#1 itm) ppc of
357 SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
358 | NONE => (ppc @ [itm])
359 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end
361 fun complete' pbt (i, v, f, d, ts) =
362 case \<^try>\<open> (i, v, true, f, Cor ((d, ts), ((snd o snd o the o (find_first (eq1 d))) pbt, ts)))\<close> of
364 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
365 (*descriptor in O_Model, but not in Problem_Pattern.T, thus keep this descriptor*)
367 (* filter out oris which have same description in itms *)
368 fun filter_outs oris [] = oris
369 | filter_outs oris (i::itms) =
371 val ors = filter_out ((curry op = ((d_in o #5) i)) o (#4)) oris
376 (* filter oris which are in pbt, too *)
377 fun filter_pbt oris pbt =
379 val dscs = map (fst o snd) pbt
381 filter ((member op= dscs) o (#4)) oris
384 fun is_error (Cor _) = false
385 | is_error (Sup _) = false
386 | is_error (Inc _) = false
387 | is_error (Mis _) = false
390 (*create output-string for itm_*)
391 fun to_p_model _ (Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
392 | to_p_model _ (Syn c) = c
393 | to_p_model _ (Typ c) = c
394 | to_p_model _ (Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
395 | to_p_model _ (Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
396 | to_p_model _ (Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
397 | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
399 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (d_in itm_ = d_in iitm_)
401 (* insert_ppc = add for appl_add', input_icalhd 11.03,
402 handles superfluous items carelessly *)
403 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
405 (* combine itms from pbl + met and complete them wrt. pbt *)
406 (* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
407 fun complete oris pits mits met =
409 val vat = max_vt pits;
410 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
411 val ors = filter ((member_swap op= vat) o (#2)) oris
412 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
414 itms @ (map (complete' met) os)
417 (* complete model and guard of a calc-head *)
418 fun complete_method (oris, mpc, ppc, probl) =
420 val pits = filter_out ((curry op= false) o (#3)) probl
421 val vat = if probl = [] then 1 else max_vt probl
422 val pors = filter ((member_swap op = vat) o (#2)) oris
423 val pors = filter_outs pors pits (*which are in pbl already*)
424 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
425 val pits = pits @ (map (complete' ppc) pors)
426 val mits = complete oris pits [] mpc
429 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
430 fun is_complete ([]: T) = false
431 | is_complete itms = foldl and_ (true, (map #3 itms))