1 (* Title: Specify/i-model.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
6 signature MODEL_FOR_INTERACTION =
9 type variants = Model_Def.variants
12 type T = Model_Def.i_model
14 type single = Model_Def.i_model_single
16 datatype feedback = datatype Model_Def.i_model_feedback
20 (*/------- to I_Model from Model 1 -------\*)
21 (*val itm_2str: feedback -> string*)
22 val feedback_to_string': feedback -> string
23 (*val itm_2str_: Proof.context -> feedback -> string*)
24 val feedback_to_string: Proof.context -> feedback -> string
25 (*val itm2str_: Proof.context -> single -> string*)
26 val single_to_string: Proof.context -> single -> string
27 (*val itms2str: Proof.context -> T -> string*)
28 val to_string: Proof.context -> T -> string
30 val untouched : T -> bool
31 (*\------- to I_Model from Model 1 -------/*)
32 (*/------- to I_Model from Model 1a -------\*)
33 val comp_dts : term * term list -> term
34 val comp_dts' : term * term list -> term
35 val comp_dts'' : term * term list -> string
36 val comp_ts : term * term list -> term
37 val split_dts : term -> term * term list
38 val split_dts' : term * term -> term list
39 (*\------- to I_Model from Model 1a -------/*)
41 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
43 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
45 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
49 structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
52 type variants = Model_Def.variants;
54 type T = Model_Def.i_model_single list;
55 datatype feedback = datatype Model_Def.i_model_feedback;
56 type single = Model_Def.i_model_single;
57 val empty = Model_Def.i_model_empty;
59 (*/------- to I_Model from Model 1b -------\*)
60 val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
61 val e_listReal = script_parse "[]::(real list)";
62 val e_listBool = script_parse "[]::(bool list)";
64 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
66 let val elems = TermC.isalist2list t
67 in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
68 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
69 let val elems = (flat o (map TermC.isalist2list)) ts;
70 in TermC.list2isalist (type_of (hd elems)) elems end;
71 (*\------- to I_Model from Model 1b -------/*)
72 (*/------- to I_Model from Model 1a -------\*)
73 fun is_var (Free _) = true
76 (* special handling for lists. ?WN:14.5.03 ??!? *)
77 fun dest_list (d, ts) =
79 if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
80 then TermC.isalist2list t
82 in (flat o (map dest)) ts end;
84 (* revert split_dts only for ts; compare comp_dts *)
86 if Input_Descript.is_list_dsc d
87 then if TermC.is_list (hd ts)
88 then if Input_Descript.is_unl d
89 then (hd ts) (* e.g. someList [1,3,2] *)
90 else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
91 else (hd ts) (* a variable or metavariable for a list *)
93 fun comp_dts (d, []) =
94 if Input_Descript.is_reall_dsc d
96 else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
97 | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
98 handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
99 fun comp_dts' (d, []) =
100 if Input_Descript.is_reall_dsc d
101 then (d $ e_listReal)
102 else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
103 | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
104 handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
105 fun comp_dts'' (d, []) =
106 if Input_Descript.is_reall_dsc d
107 then UnparseC.term (d $ e_listReal)
108 else if Input_Descript.is_booll_dsc d
109 then UnparseC.term (d $ e_listBool)
111 | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))
112 handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
114 (* decompose an input into description, terms (ev. elems of lists),
115 and the value for the problem-environment; inv to comp_dts *)
116 fun split_dts (t as d $ arg) =
117 if Input_Descript.is_dsc d
118 then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
119 then (d, take_apart arg)
121 else (TermC.empty, TermC.dest_list' t)
123 let val t' as (h, _) = strip_comb t;
125 if Input_Descript.is_dsc h
126 then (h, dest_list t')
127 else (TermC.empty, TermC.dest_list' t)
129 (* version returning ts only *)
130 fun I_Model.split_dts' (d, arg) =
131 if Input_Descript.is_dsc d
132 then if Input_Descript.is_list_dsc d
133 then if TermC.is_list arg
134 then if Input_Descript.is_unl d
135 then ([arg]) (* e.g. someList [1,3,2] *)
136 else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
137 else ([arg]) (* a variable or metavariable for a list *)
139 else (TermC.dest_list' arg)
140 (* WN170204: Warning "redundant"
141 | I_Model.split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
142 let val (h,argl) = strip_comb t
146 else (dest_list (h,argl))
149 WN050903 we do NOT know which is from subtheory, description or term;
150 typecheck thus may lead to TYPE-error 'unknown constant';
151 solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
152 (*fun comp_dts thy (d,[]) =
153 Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
154 (Thy_Info_get_theory "Isac_Knowledge")
155 (*comp_dts:FIXXME stay with term for efficiency !!!*)
156 (if is_reall_dsc d then (d $ e_listReal)
157 else if is_booll_dsc d then (d $ e_listBool)
160 (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
161 (Thy_Info_get_theory "Isac_Knowledge")
162 (*comp_dts:FIXXME stay with term for efficiency !!*)
163 (d $ (comp_ts (d, ts)))
164 handle _ => error ("comp_dts: "^(term2str d)^
165 " $ "^(term2str (hd ts))));*)
166 (*\------- to I_Model from Model 1a -------/*)
168 (*/------- to I_Model from Model 1c -------\*)
169 (* 27.8.01: problem-environment
170 WN.6.5.03: FIXXME reconsider if penv is worth the effort --
171 -- just rerun a whole expl with num/var may show the same ?!
172 WN.9.5.03: penv-concept stalled, immediately generate script env !
173 but [#0, epsilon] only outcommented for eventual reconsideration *)
174 type penv = (* problem-environment *)
176 * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
178 fun pen2str ctxt (t, ts) =
179 pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
180 fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
181 (*\------- to I_Model from Model 1c -------/*)
182 (*/------- to I_Model from Model 1 -------\*)
183 fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
184 "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
185 | feedback_to_string _ (Syn c) = "Syn " ^ c
186 | feedback_to_string _ (Typ c) = "Typ " ^ c
187 | feedback_to_string ctxt (Inc ((d, ts), penv)) =
188 "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
189 | feedback_to_string ctxt (Sup (d, ts)) =
190 "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts))
191 | feedback_to_string ctxt (Mis (d, pid)) =
192 "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
193 | feedback_to_string _ (Par s) = "Trm "^s;
194 fun feedback_to_string' t = feedback_to_string (ThyC.id_to_ctxt "Isac_Knowledge") t;
196 fun single_to_string ctxt (i, is, b, s, itm_) =
197 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
198 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
199 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
201 (* in CalcTree/Subproblem an 'untouched' model is created
202 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
203 fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : single -> int)) itms);
204 (*\------- to I_Model from Model 1 -------/*)