walther@59938
|
1 |
(* Title: Specify/o-model.sml
|
walther@59938
|
2 |
Author: Walther Neuper 110226
|
walther@59938
|
3 |
(c) due to copyright terms
|
walther@59953
|
4 |
|
walther@60004
|
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>
|
walther@60004
|
6 |
selected with respect to a \<open>Model_Pattern\<close> and combined with respective \<open>m_field\<close>s.
|
walther@60004
|
7 |
\<open>complete_for\<close> a \<open>Model_Pattern\<close> is done by \<open>Tactic.Model_Problem\<close>
|
walther@60004
|
8 |
(with defaults from \<open>Formalise\<close>refs), by \<open>Tactic.Specify_Problem\<close> and \<open>Tactic.Specify_Method\<close>
|
walther@60004
|
9 |
|
walther@60004
|
10 |
\<open>O_Model\<close> serves efficiency of student's interactive modelling via \<open>I_Model\<close>.
|
walther@60004
|
11 |
|
walther@60004
|
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>
|
walther@60154
|
13 |
of the \<open>Problem\<close> or the \<open>MethodC\<close> .. TODO redes: \<open>m_field\<close> probably different in root..Subproblem
|
walther@59998
|
14 |
|
walther@59953
|
15 |
TODO: revise with an example with more than 1 variant.
|
walther@60004
|
16 |
+ consider: drop m_field ?
|
walther@59953
|
17 |
*)
|
walther@59938
|
18 |
|
walther@59938
|
19 |
signature ORIGINAL_MODEL =
|
walther@59938
|
20 |
sig
|
walther@59961
|
21 |
type T
|
Walther@60442
|
22 |
val empty: T
|
walther@59961
|
23 |
type single
|
walther@60018
|
24 |
type variant
|
walther@59961
|
25 |
type variants
|
walther@59961
|
26 |
type m_field
|
walther@59961
|
27 |
type descriptor
|
walther@59998
|
28 |
type values
|
walther@59999
|
29 |
type message
|
Walther@60655
|
30 |
val to_string: Proof.context -> T -> string
|
Walther@60655
|
31 |
val single_to_string: Proof.context -> single -> string
|
walther@59940
|
32 |
val single_empty: single
|
walther@59939
|
33 |
|
Walther@60653
|
34 |
val init: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context
|
walther@59969
|
35 |
val values : T -> term list
|
Walther@60609
|
36 |
val values': Proof.context -> T -> Formalise.model * term list
|
walther@60009
|
37 |
val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
|
Walther@60471
|
38 |
val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values
|
Walther@60471
|
39 |
val associate_input': Proof.context -> m_field -> values -> T -> message * single * values
|
Walther@60471
|
40 |
val contains: Proof.context -> m_field -> T -> term -> message * single * values
|
Walther@60471
|
41 |
val make_typeless: term -> term
|
walther@60000
|
42 |
val test_types: Proof.context -> descriptor * values -> string
|
walther@59969
|
43 |
|
Walther@60472
|
44 |
val add_enumerate: 'a list -> (int * 'a) list
|
walther@59961
|
45 |
type preori
|
Walther@60473
|
46 |
val copy_name: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
|
walther@59986
|
47 |
val is_copy_named: Model_Pattern.single -> bool
|
Walther@60475
|
48 |
val is_copy_named': string -> bool
|
Walther@60469
|
49 |
val is_copy_named_generating: Model_Pattern.single -> bool
|
Walther@60469
|
50 |
|
walther@60251
|
51 |
\<^isac_test>\<open>
|
walther@59986
|
52 |
val is_copy_named_generating_idstr: string -> bool
|
Walther@60475
|
53 |
val string_of_preoris : preori list -> string
|
walther@59998
|
54 |
val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
|
Walther@60475
|
55 |
|
walther@59952
|
56 |
val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
|
Walther@60734
|
57 |
val get_max_variant: variants -> variant
|
Walther@60475
|
58 |
val partition_variants: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
|
Walther@60475
|
59 |
val collect_variants: ('a * ''b) list -> ('a list * ''b) list
|
Walther@60475
|
60 |
|
walther@59947
|
61 |
val replace_0: int -> int list -> int list
|
walther@59947
|
62 |
val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
|
wenzelm@60223
|
63 |
\<close>
|
walther@59938
|
64 |
end
|
walther@59938
|
65 |
|
walther@59974
|
66 |
(**)
|
walther@59938
|
67 |
structure O_Model(**) : ORIGINAL_MODEL(**) =
|
walther@59938
|
68 |
struct
|
walther@59974
|
69 |
(**)
|
walther@59938
|
70 |
|
walther@59960
|
71 |
(** types **)
|
walther@59960
|
72 |
|
walther@60018
|
73 |
type variant = Model_Def.variant;
|
walther@59940
|
74 |
type variants = Model_Def.variants;
|
walther@59952
|
75 |
type m_field = Model_Def.m_field;
|
walther@59952
|
76 |
type descriptor = Model_Def.descriptor;
|
Walther@60766
|
77 |
type values = Model_Def.values;
|
walther@59999
|
78 |
type message = string;
|
walther@59938
|
79 |
|
walther@59940
|
80 |
type T = Model_Def.o_model;
|
Walther@60442
|
81 |
val empty = [] : Model_Def.o_model;
|
walther@59940
|
82 |
type single = Model_Def.o_model_single
|
walther@59940
|
83 |
val single_empty = Model_Def.o_model_empty;
|
Walther@60655
|
84 |
|
walther@59957
|
85 |
val single_to_string = Model_Def.o_model_single_to_string;
|
walther@59940
|
86 |
val to_string = Model_Def.o_model_to_string;
|
walther@59940
|
87 |
|
walther@59952
|
88 |
(* O_Model.single without leading integer *)
|
walther@59952
|
89 |
type preori = (variants * m_field * term * term list);
|
walther@60268
|
90 |
\<^isac_test>\<open>
|
walther@59942
|
91 |
fun preori2str (vs, fi, t, ts) =
|
walther@59942
|
92 |
"(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
|
Walther@60678
|
93 |
UnparseC.term (ContextC.for_ERROR ()) t ^ ", " ^
|
Walther@60678
|
94 |
(strs2str o (map (UnparseC.term (ContextC.for_ERROR ())) ) ) ts ^ ")";
|
Walther@60475
|
95 |
val string_of_preoris = (strs2str' o (map (linefeed o preori2str)));
|
walther@60268
|
96 |
\<close>
|
walther@59942
|
97 |
|
walther@59960
|
98 |
|
walther@59960
|
99 |
(** initialise O_Model **)
|
walther@59960
|
100 |
|
Walther@60586
|
101 |
(* compare d and dsc in pbt and transfer field to where_-ori *)
|
Walther@60673
|
102 |
fun add_field thy pbt (d,ts) =
|
walther@59947
|
103 |
let fun eq d pt = (d = (fst o snd) pt);
|
walther@59947
|
104 |
in case filter (eq d) pbt of
|
walther@59947
|
105 |
[(fi, (_, _))] => (fi, d, ts)
|
Walther@60586
|
106 |
| [] => ("#undef", d, ts) (*may come with met.model*)
|
Walther@60673
|
107 |
| _ => raise ERROR ("add_field: " ^ UnparseC.term_in_thy thy d ^ " more than once in pbt")
|
walther@59947
|
108 |
end;
|
walther@59947
|
109 |
|
walther@59952
|
110 |
(*
|
walther@59952
|
111 |
mark an element with the position within a plateau;
|
walther@59952
|
112 |
a plateau with length 1 is marked with 0
|
walther@59952
|
113 |
*)
|
Walther@60475
|
114 |
fun partition_variants _ [] = raise ERROR "partition_variants []"
|
Walther@60475
|
115 |
| partition_variants eq xs =
|
walther@59952
|
116 |
let
|
walther@59952
|
117 |
fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
|
Walther@60475
|
118 |
| mar _ _ [] _ = raise ERROR "partition_variants []"
|
Walther@60475
|
119 |
| mar xx eq (x :: x' :: xs) n =
|
Walther@60475
|
120 |
if eq (x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
|
walther@59952
|
121 |
else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
|
walther@59952
|
122 |
in mar [] eq xs 1 end;
|
walther@59952
|
123 |
|
walther@59952
|
124 |
(*
|
walther@59952
|
125 |
assumes equal descriptions to be in adjacent 'plateaus',
|
walther@59952
|
126 |
items at a certain position within the plateaus form a variant;
|
walther@59952
|
127 |
length = 1 ... marked with 0: covers all variants
|
walther@59952
|
128 |
*)
|
walther@59947
|
129 |
fun add_variants fdts =
|
walther@59947
|
130 |
let
|
walther@59947
|
131 |
fun eq (a, b) = curry op= (snd3 a) (snd3 b);
|
Walther@60475
|
132 |
in partition_variants eq fdts end;
|
walther@59947
|
133 |
|
Walther@60734
|
134 |
fun get_max_variant [] = raise ERROR "get_max_variant of []"
|
Walther@60734
|
135 |
| get_max_variant (y :: ys) =
|
walther@59947
|
136 |
let fun mx x [] = x
|
walther@59947
|
137 |
| mx x (y :: ys) = if x < y then mx y ys else mx x ys;
|
walther@59947
|
138 |
in mx y ys end;
|
walther@59947
|
139 |
|
Walther@60475
|
140 |
fun collect_variants (((v,x) :: vxs)) =
|
walther@59947
|
141 |
let
|
walther@59947
|
142 |
fun col xs (vs, x) [] = xs @ [(vs, x)]
|
walther@59947
|
143 |
| col xs (vs, x) ((v', x') :: vxs') =
|
walther@59947
|
144 |
if x = x' then col xs (vs @ [v'], x') vxs'
|
walther@59947
|
145 |
else col (xs @ [(vs, x)]) ([v'], x') vxs';
|
walther@59947
|
146 |
in col [] ([v], x) vxs end
|
Walther@60475
|
147 |
| collect_variants _ = raise ERROR "collect_variants: called with []";
|
walther@59947
|
148 |
|
walther@59947
|
149 |
fun replace_0 vm [0] = intsto vm
|
walther@59947
|
150 |
| replace_0 _ vs = vs;
|
walther@59947
|
151 |
|
Walther@60472
|
152 |
fun add_enumerate [] = raise ERROR "O_Model.add_enumerate []"
|
Walther@60472
|
153 |
| add_enumerate xs =
|
walther@59947
|
154 |
let
|
walther@59947
|
155 |
fun add _ [] = []
|
walther@59947
|
156 |
| add n (x :: xs) = (n, x) :: add (n + 1) xs;
|
walther@59947
|
157 |
in add 1 xs end;
|
walther@59947
|
158 |
|
walther@59947
|
159 |
fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
|
walther@59947
|
160 |
|
Walther@60653
|
161 |
fun init _ [] _ = ([], ContextC.empty)
|
Walther@60470
|
162 |
| init thy fmz pbt =
|
walther@59947
|
163 |
let
|
Walther@60656
|
164 |
val (ts, ctxt) = ContextC.init_while_parsing fmz thy
|
Walther@60651
|
165 |
val model =
|
Walther@60651
|
166 |
(map (fn t => t
|
Walther@60651
|
167 |
|> Input_Descript.split
|
Walther@60651
|
168 |
|> add_field thy pbt) ts)
|
Walther@60651
|
169 |
|> add_variants;
|
Walther@60734
|
170 |
val maxv = model |> map fst |> get_max_variant;
|
Walther@60651
|
171 |
val maxv = if maxv = 0 then 1 else maxv;
|
Walther@60651
|
172 |
val model' = model
|
Walther@60651
|
173 |
|> collect_variants
|
Walther@60651
|
174 |
|> map (replace_0 maxv |> apfst)
|
Walther@60651
|
175 |
|> add_enumerate
|
Walther@60651
|
176 |
|> map flattup
|
Walther@60651
|
177 |
in (model', ctxt) end
|
walther@59960
|
178 |
|
walther@59969
|
179 |
(** get the values **)
|
walther@59969
|
180 |
|
walther@59969
|
181 |
fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"
|
walther@59969
|
182 |
| mkval _ [t] = t
|
walther@59969
|
183 |
| mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
|
walther@59969
|
184 |
fun mkval' x = mkval TermC.empty x;
|
Walther@60470
|
185 |
(* from an O_Model create values for ctxt *)
|
Walther@60475
|
186 |
fun values oris =
|
walther@59969
|
187 |
((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
|
walther@59969
|
188 |
|
Walther@60470
|
189 |
(* from an O_Model create (Formalise.model, values)
|
Walther@60470
|
190 |
e.g. Subproblem ["BOOL (1+x=2)", "REAL x"]
|
Walther@60470
|
191 |
--match_ags--> O_Model.T
|
Walther@60470
|
192 |
O_Model.T --values'--> (["equality (1+x=2)", "boundVariable x", "solutions L"], values)
|
Walther@60470
|
193 |
*)
|
Walther@60609
|
194 |
fun values' ctxt oris =
|
Walther@60470
|
195 |
let
|
Walther@60470
|
196 |
fun ori2fmz_vals (_, _, _, dsc, ts) =
|
Walther@60675
|
197 |
case \<^try>\<open>(((UnparseC.term ctxt) o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of
|
Walther@60470
|
198 |
SOME x => x
|
Walther@60675
|
199 |
| NONE => raise ERROR ("O_Model.values' called with " ^ UnparseC.terms ctxt ts)
|
Walther@60470
|
200 |
in (split_list o (map ori2fmz_vals)) oris end
|
Walther@60470
|
201 |
|
walther@59986
|
202 |
|
walther@59998
|
203 |
(** complete wrt. Model_Pattern.T by use of root's O_Model.T **)
|
walther@59998
|
204 |
|
walther@60009
|
205 |
fun complete_for m_patt root_model (o_model, ctxt) =
|
walther@59998
|
206 |
let
|
walther@59998
|
207 |
val missing = m_patt |> filter_out
|
walther@60017
|
208 |
(fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
|
walther@60001
|
209 |
val add = (root_model
|
walther@60001
|
210 |
|> filter
|
walther@60017
|
211 |
(fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
|
walther@60009
|
212 |
in
|
walther@60009
|
213 |
((o_model @ add)
|
walther@60011
|
214 |
|> map (fn (a, b, _, descr, e) =>
|
walther@60011
|
215 |
case Model_Pattern.get_field descr m_patt of
|
walther@60011
|
216 |
SOME m_field => (a, b, m_field, descr, e)
|
walther@60011
|
217 |
| NONE => (a, b, "#undef", descr, e))
|
Walther@60760
|
218 |
|> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
|
Walther@60760
|
219 |
|> add_enumerate (* for correct enumeration *)
|
walther@60001
|
220 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
|
walther@59998
|
221 |
ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
|
walther@59998
|
222 |
end
|
walther@59998
|
223 |
|
walther@59998
|
224 |
|
walther@59986
|
225 |
(** ? ? ? **)
|
walther@59986
|
226 |
|
walther@59986
|
227 |
(* make oris from args of the stac SubProblem and from pbt.
|
walther@59986
|
228 |
can this formal argument (of a model-pattern) be omitted in the arg-list
|
walther@59986
|
229 |
of a SubProblem ? see calcelems.sml 'type met ' *)
|
Walther@60475
|
230 |
fun is_copy_named' str =
|
walther@59986
|
231 |
case (rev o Symbol.explode) str of
|
walther@59986
|
232 |
"'" :: _ :: "'" :: _ => true
|
walther@59986
|
233 |
| _ => false
|
Walther@60475
|
234 |
fun is_copy_named (_, (_, t)) = (is_copy_named' o TermC.free2str) t
|
walther@59986
|
235 |
|
walther@59986
|
236 |
(* should this formal argument (of a model-pattern) create a new identifier? *)
|
walther@59986
|
237 |
fun is_copy_named_generating_idstr str =
|
Walther@60475
|
238 |
if is_copy_named' str
|
walther@59986
|
239 |
then
|
walther@59986
|
240 |
case (rev o Symbol.explode) str of
|
walther@59986
|
241 |
"'" :: "'" :: "'" :: _ => false
|
walther@59986
|
242 |
| _ => true
|
walther@59986
|
243 |
else false
|
walther@59986
|
244 |
fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
|
walther@59986
|
245 |
|
walther@59986
|
246 |
(* generate a new variable "x_i" name from a related given one "x"
|
walther@59986
|
247 |
by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
|
walther@59986
|
248 |
e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
|
walther@59986
|
249 |
but leave is_copy_named_generating as is, e.t. ss''' *)
|
Walther@60473
|
250 |
fun copy_name pbt oris (p as (field, (dsc, t))) =
|
walther@60265
|
251 |
case \<^try>\<open>
|
walther@60265
|
252 |
if is_copy_named_generating p
|
walther@60265
|
253 |
then (*WN051014 kept strange old code ...*)
|
walther@60265
|
254 |
let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
|
walther@60265
|
255 |
val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
|
walther@60265
|
256 |
val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
|
walther@60265
|
257 |
val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
|
walther@60265
|
258 |
val vals = map sel oris
|
walther@60265
|
259 |
val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
|
walther@60265
|
260 |
in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
|
walther@60265
|
261 |
else ([1], field, dsc, [t])
|
walther@60265
|
262 |
\<close> of
|
walther@60265
|
263 |
SOME x => x
|
Walther@60678
|
264 |
| NONE => raise ERROR ("copy_name: for " ^ UnparseC.term (ContextC.for_ERROR ()) t)
|
walther@59986
|
265 |
|
walther@59999
|
266 |
|
walther@60000
|
267 |
(** tools for I_Model **)
|
walther@59999
|
268 |
|
Walther@60470
|
269 |
(* to an input (_ $ values) find the according O_Model.single and insert the values *)
|
Walther@60471
|
270 |
fun associate_input ctxt m_field (descript, vals) [] =
|
Walther@60471
|
271 |
("associate_input: input ('" ^
|
Walther@60675
|
272 |
(UnparseC.term ctxt (Input_Descript.join (descript, vals))) ^
|
walther@60012
|
273 |
"') not found in oris (typed)", (0, [], m_field, descript, vals), [])
|
Walther@60471
|
274 |
| associate_input ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
|
walther@59999
|
275 |
if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
|
walther@59999
|
276 |
then ("", (id, vat, sel, d, inter op = ts ts'), ts')
|
Walther@60471
|
277 |
else associate_input ctxt sel (d, ts) oris
|
walther@59999
|
278 |
|
walther@60012
|
279 |
(* to an input (_ $ values) find the according O_Model.single and insert the values *)
|
Walther@60471
|
280 |
fun associate_input' ctxt _ vals [] =
|
Walther@60675
|
281 |
("associate_input': input (_, '" ^ strs2str (map (UnparseC.term ctxt) vals) ^
|
walther@59999
|
282 |
"') not found in oris (typed)", single_empty, [])
|
Walther@60471
|
283 |
| associate_input' ctxt m_field vals ((id, vat, m_field', descr, vals') :: oris) =
|
walther@60012
|
284 |
if m_field = m_field' andalso (inter op = vals vals') <> []
|
walther@60012
|
285 |
then
|
walther@60012
|
286 |
if m_field = m_field'
|
walther@60012
|
287 |
then ("", (id, vat, m_field, descr, inter op = vals vals'), vals')
|
Walther@60675
|
288 |
else ((strs2str' o map (UnparseC.term ctxt)) vals ^
|
walther@60012
|
289 |
" not for " ^ m_field, single_empty, [])
|
Walther@60471
|
290 |
else associate_input' ctxt m_field vals oris
|
walther@59999
|
291 |
|
walther@60000
|
292 |
fun test_types ctxt (d,ts) =
|
walther@60000
|
293 |
let
|
walther@60000
|
294 |
val opt = (try Input_Descript.join) (d, ts)
|
walther@60000
|
295 |
val msg = case opt of
|
walther@60000
|
296 |
SOME _ => ""
|
Walther@60675
|
297 |
| NONE => (UnparseC.term ctxt d ^ " " ^
|
Walther@60675
|
298 |
(strs2str' o map (UnparseC.term ctxt)) ts ^ " is illtyped")
|
walther@60000
|
299 |
in msg end
|
walther@60000
|
300 |
|
walther@60000
|
301 |
(* make a term 'typeless' for comparing with another 'typeless' term;
|
walther@60000
|
302 |
'type-less' usually is illtyped *)
|
Walther@60471
|
303 |
fun make_typeless (Const (s, _)) = (Const (s, TermC.typ_empty))
|
Walther@60471
|
304 |
| make_typeless (Free (s, _)) = (Free (s, TermC.typ_empty))
|
Walther@60471
|
305 |
| make_typeless (Var (n, _)) = (Var (n, TermC.typ_empty))
|
Walther@60471
|
306 |
| make_typeless (Bound i) = (Bound i)
|
Walther@60471
|
307 |
| make_typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, make_typeless t)
|
Walther@60471
|
308 |
| make_typeless (t1 $ t2) = (make_typeless t1) $ (make_typeless t2)
|
walther@60000
|
309 |
|
walther@60000
|
310 |
(* is the term t input (or taken from fmz) known in O_Model ?
|
walther@60000
|
311 |
give feedback on all(?) strange input;
|
walther@60000
|
312 |
return _all_ terms already input to this item (e.g. valuesFor a,b) *)
|
Walther@60471
|
313 |
fun contains ctxt sel ori t =
|
walther@60000
|
314 |
let
|
walther@60017
|
315 |
val ots = ((distinct op =) o flat o (map #5)) ori
|
walther@60017
|
316 |
val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
|
walther@60000
|
317 |
val (d, ts) = Input_Descript.split t
|
walther@60017
|
318 |
val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts)
|
walther@60000
|
319 |
in
|
walther@60000
|
320 |
if (subtract op = oids ids) <> []
|
walther@60000
|
321 |
then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", single_empty, [])
|
walther@60000
|
322 |
else
|
walther@60000
|
323 |
if d = TermC.empty
|
walther@60000
|
324 |
then
|
Walther@60471
|
325 |
if not (subset op = (map make_typeless ts, map make_typeless ots))
|
Walther@60675
|
326 |
then ("terms '" ^ (strs2str' o (map (UnparseC.term ctxt))) ts ^
|
Walther@60471
|
327 |
"' not in example (make_typeless)", single_empty, [])
|
walther@60000
|
328 |
else
|
Walther@60471
|
329 |
(case associate_input' ctxt sel ts(*..values*) ori of
|
walther@60001
|
330 |
("", ori_ as (_, _, _, d, ts), all) =>
|
walther@60000
|
331 |
(case test_types ctxt (d,ts) of
|
walther@60000
|
332 |
"" => ("", ori_, all)
|
walther@60000
|
333 |
| msg => (msg, single_empty, []))
|
walther@60000
|
334 |
| (msg, _, _) => (msg, single_empty, []))
|
walther@60000
|
335 |
else
|
walther@60000
|
336 |
if member op = (map #4 ori) d
|
Walther@60471
|
337 |
then associate_input ctxt sel (d, ts) ori
|
Walther@60675
|
338 |
else (UnparseC.term ctxt d ^ " not in example", (0, [], sel, d, ts), [])
|
walther@60000
|
339 |
end
|
walther@59999
|
340 |
|
Walther@60474
|
341 |
(**)end(**);
|