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@60004
|
13 |
of the \<open>Problem\<close> or the \<open>Method\<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@59961
|
22 |
type single
|
walther@59961
|
23 |
type variants
|
walther@59961
|
24 |
type m_field
|
walther@59961
|
25 |
type descriptor
|
walther@59998
|
26 |
type values
|
walther@59999
|
27 |
type message
|
walther@59940
|
28 |
val to_string: T -> string
|
walther@59957
|
29 |
val single_to_string: single -> string
|
walther@59940
|
30 |
val single_empty: single
|
walther@59939
|
31 |
|
walther@59998
|
32 |
(*val init: theory -> Formalise.model -> Model_Pattern.T -> T ..TODO*)
|
walther@59952
|
33 |
val init: Formalise.model -> theory -> Model_Pattern.T -> T
|
walther@59960
|
34 |
val add : theory -> Model_Pattern.T -> T -> T
|
walther@59969
|
35 |
val values : T -> term list
|
walther@59987
|
36 |
val values': T -> Formalise.model * term list
|
walther@60004
|
37 |
(*/------- rename -------\*)
|
walther@60004
|
38 |
(*val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context*)
|
walther@59998
|
39 |
val complete_for_from: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
|
walther@59999
|
40 |
(*val seek_oridts: Proof.context -> ?/////? -> descriptor * values -> T -> message * single * values*)
|
walther@59999
|
41 |
val seek_oridts: Proof.context -> m_field -> descriptor * values -> T -> message * single * values
|
walther@60001
|
42 |
(*val single_for_values:!!! values -> Proof.context -> m_field -> T -> message * single * values*)
|
walther@59999
|
43 |
val seek_orits: Proof.context -> m_field -> values -> T -> message * single * values
|
walther@60004
|
44 |
(*val ?contains:!!! term -> Proof.context -> m_field -> T -> message * single * values*)
|
walther@60001
|
45 |
val is_known: Proof.context -> m_field -> T -> term -> message * single * values
|
walther@60000
|
46 |
(*val typeless: term -> term*)
|
walther@60000
|
47 |
val typeless: term -> term
|
walther@60000
|
48 |
(*val test_types: Proof.context -> descriptor * values -> string*)
|
walther@60000
|
49 |
val test_types: Proof.context -> descriptor * values -> string
|
walther@59969
|
50 |
|
walther@59998
|
51 |
(*put add_id into a new auxiliary fun, see ONLY call..*)
|
walther@59961
|
52 |
val add_id: 'a list -> (int * 'a) list
|
walther@59961
|
53 |
type preori
|
walther@59961
|
54 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59998
|
55 |
(*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
|
walther@59986
|
56 |
val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
|
walther@59986
|
57 |
val is_copy_named: Model_Pattern.single -> bool
|
walther@59986
|
58 |
val is_copy_named_idstr: string -> bool
|
walther@59986
|
59 |
val is_copy_named_generating_idstr: string -> bool
|
walther@59986
|
60 |
val is_copy_named_generating: Model_Pattern.single -> bool
|
walther@59986
|
61 |
|
walther@59961
|
62 |
val preoris2str : preori list -> string
|
walther@59998
|
63 |
(*val getr_ct: theory -> single -> m_field * UnparseC.term_as_string*)
|
walther@59992
|
64 |
val getr_ct: theory -> single -> m_field * UnparseC.term_as_string
|
walther@59992
|
65 |
|
walther@59961
|
66 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59998
|
67 |
val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
|
walther@59952
|
68 |
val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
|
walther@59998
|
69 |
(*val max: variants -> int*)
|
walther@59952
|
70 |
val max: variants -> int
|
walther@59998
|
71 |
(*val coll_variants: ('a * ''b) list -> ('a list * ''b) list*)
|
walther@59947
|
72 |
val coll_variants: ('a * ''b) list -> ('a list * ''b) list
|
walther@59998
|
73 |
(*val replace_0: int -> int list -> int list*)
|
walther@59947
|
74 |
val replace_0: int -> int list -> int list
|
walther@59947
|
75 |
val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
|
walther@59998
|
76 |
(*val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list*)
|
walther@59998
|
77 |
val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
|
walther@59987
|
78 |
(*\------- rename -------/*)
|
walther@59938
|
79 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59938
|
80 |
end
|
walther@59938
|
81 |
|
walther@59974
|
82 |
(**)
|
walther@59938
|
83 |
structure O_Model(**) : ORIGINAL_MODEL(**) =
|
walther@59938
|
84 |
struct
|
walther@59974
|
85 |
(**)
|
walther@59938
|
86 |
|
walther@59960
|
87 |
(** types **)
|
walther@59960
|
88 |
|
walther@59940
|
89 |
type variants = Model_Def.variants;
|
walther@59952
|
90 |
type m_field = Model_Def.m_field;
|
walther@59952
|
91 |
type descriptor = Model_Def.descriptor;
|
walther@59998
|
92 |
type values = Model_Def.values;
|
walther@59999
|
93 |
type message = string;
|
walther@59938
|
94 |
|
walther@59940
|
95 |
type T = Model_Def.o_model;
|
walther@59940
|
96 |
type single = Model_Def.o_model_single
|
walther@59940
|
97 |
val single_empty = Model_Def.o_model_empty;
|
walther@59957
|
98 |
val single_to_string = Model_Def.o_model_single_to_string;
|
walther@59940
|
99 |
val to_string = Model_Def.o_model_to_string;
|
walther@59940
|
100 |
|
walther@59952
|
101 |
(* O_Model.single without leading integer *)
|
walther@59952
|
102 |
type preori = (variants * m_field * term * term list);
|
walther@59942
|
103 |
fun preori2str (vs, fi, t, ts) =
|
walther@59942
|
104 |
"(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
|
walther@59942
|
105 |
UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
|
walther@59942
|
106 |
val preoris2str = (strs2str' o (map (linefeed o preori2str)));
|
walther@59942
|
107 |
|
walther@59992
|
108 |
(* get the first term in ts from ori *)
|
walther@59992
|
109 |
fun getr_ct thy (_, _, fd, d, ts) =
|
walther@59992
|
110 |
(fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
|
walther@59992
|
111 |
|
walther@59960
|
112 |
|
walther@59960
|
113 |
(** initialise O_Model **)
|
walther@59960
|
114 |
|
walther@59947
|
115 |
(* compare d and dsc in pbt and transfer field to pre-ori *)
|
walther@59947
|
116 |
fun add_field (_: theory) pbt (d,ts) =
|
walther@59947
|
117 |
let fun eq d pt = (d = (fst o snd) pt);
|
walther@59947
|
118 |
in case filter (eq d) pbt of
|
walther@59947
|
119 |
[(fi, (_, _))] => (fi, d, ts)
|
walther@59947
|
120 |
| [] => ("#undef", d, ts) (*may come with met.ppc*)
|
walther@59952
|
121 |
| _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
|
walther@59947
|
122 |
end;
|
walther@59947
|
123 |
|
walther@59952
|
124 |
(*
|
walther@59952
|
125 |
mark an element with the position within a plateau;
|
walther@59952
|
126 |
a plateau with length 1 is marked with 0
|
walther@59952
|
127 |
*)
|
walther@59952
|
128 |
fun mark _ [] = raise ERROR "mark []"
|
walther@59952
|
129 |
| mark eq xs =
|
walther@59952
|
130 |
let
|
walther@59952
|
131 |
fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
|
walther@59952
|
132 |
| mar _ _ [] _ = raise ERROR "mark []"
|
walther@59952
|
133 |
| mar xx eq (x:: x' :: xs) n =
|
walther@59952
|
134 |
if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
|
walther@59952
|
135 |
else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
|
walther@59952
|
136 |
in mar [] eq xs 1 end;
|
walther@59952
|
137 |
|
walther@59952
|
138 |
(*
|
walther@59952
|
139 |
assumes equal descriptions to be in adjacent 'plateaus',
|
walther@59952
|
140 |
items at a certain position within the plateaus form a variant;
|
walther@59952
|
141 |
length = 1 ... marked with 0: covers all variants
|
walther@59952
|
142 |
*)
|
walther@59947
|
143 |
fun add_variants fdts =
|
walther@59947
|
144 |
let
|
walther@59947
|
145 |
fun eq (a, b) = curry op= (snd3 a) (snd3 b);
|
walther@59947
|
146 |
in mark eq fdts end;
|
walther@59947
|
147 |
|
walther@59952
|
148 |
fun max [] = raise ERROR "max of []"
|
walther@59947
|
149 |
| max (y :: ys) =
|
walther@59947
|
150 |
let fun mx x [] = x
|
walther@59947
|
151 |
| mx x (y :: ys) = if x < y then mx y ys else mx x ys;
|
walther@59947
|
152 |
in mx y ys end;
|
walther@59947
|
153 |
|
walther@59947
|
154 |
fun coll_variants (((v,x) :: vxs)) =
|
walther@59947
|
155 |
let
|
walther@59947
|
156 |
fun col xs (vs, x) [] = xs @ [(vs, x)]
|
walther@59947
|
157 |
| col xs (vs, x) ((v', x') :: vxs') =
|
walther@59947
|
158 |
if x = x' then col xs (vs @ [v'], x') vxs'
|
walther@59947
|
159 |
else col (xs @ [(vs, x)]) ([v'], x') vxs';
|
walther@59947
|
160 |
in col [] ([v], x) vxs end
|
walther@59952
|
161 |
| coll_variants _ = raise ERROR "coll_variants: called with []";
|
walther@59947
|
162 |
|
walther@59947
|
163 |
fun replace_0 vm [0] = intsto vm
|
walther@59947
|
164 |
| replace_0 _ vs = vs;
|
walther@59947
|
165 |
|
walther@59961
|
166 |
fun add_id [] = raise ERROR "O_Model.add_id []"
|
walther@59947
|
167 |
| add_id xs =
|
walther@59947
|
168 |
let
|
walther@59947
|
169 |
fun add _ [] = []
|
walther@59947
|
170 |
| add n (x :: xs) = (n, x) :: add (n + 1) xs;
|
walther@59947
|
171 |
in add 1 xs end;
|
walther@59947
|
172 |
|
walther@59947
|
173 |
fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
|
walther@59947
|
174 |
|
walther@59952
|
175 |
fun init [] _ _ = []
|
walther@59952
|
176 |
| init fmz thy pbt =
|
walther@59947
|
177 |
let
|
walther@59996
|
178 |
val model =
|
walther@59996
|
179 |
(map (fn str => str
|
walther@59996
|
180 |
|> TermC.parseNEW'' thy
|
walther@59996
|
181 |
|> Input_Descript.split
|
walther@59996
|
182 |
|> add_field thy pbt) fmz)
|
walther@59996
|
183 |
|> add_variants;
|
walther@59952
|
184 |
val maxv = model |> map fst |> max;
|
walther@59947
|
185 |
val maxv = if maxv = 0 then 1 else maxv;
|
walther@59952
|
186 |
val model' = model
|
walther@59952
|
187 |
|> coll_variants
|
walther@59947
|
188 |
|> map (replace_0 maxv |> apfst)
|
walther@59947
|
189 |
|> add_id
|
walther@59947
|
190 |
|> map flattup;
|
walther@59952
|
191 |
in model' end;
|
walther@59938
|
192 |
|
walther@59960
|
193 |
|
walther@59998
|
194 |
(** add new m_field's from method \<rightarrow> REPLACE BY complete_for_from **)
|
walther@59960
|
195 |
|
walther@59998
|
196 |
(* for the root-problem *)
|
walther@59960
|
197 |
fun add _ mpc ori =
|
walther@59960
|
198 |
let
|
walther@59960
|
199 |
fun eq d pt = (d = (fst o snd) pt);
|
walther@59960
|
200 |
fun repl mpc (i, v, _, d, ts) =
|
walther@59960
|
201 |
case filter (eq d) mpc of
|
walther@59960
|
202 |
[(fi, (_, _))] => [(i, v, fi, d, ts)]
|
walther@59960
|
203 |
| [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
|
walther@59962
|
204 |
| _ => raise ERROR ("O_Model.add: " ^ UnparseC.term d ^ " more than once in met");
|
walther@59960
|
205 |
in flat ((map (repl mpc)) ori) end;
|
walther@59960
|
206 |
|
walther@59969
|
207 |
|
walther@59969
|
208 |
(** get the values **)
|
walther@59969
|
209 |
|
walther@59969
|
210 |
fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"
|
walther@59969
|
211 |
| mkval _ [t] = t
|
walther@59969
|
212 |
| mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
|
walther@59969
|
213 |
fun mkval' x = mkval TermC.empty x;
|
walther@59987
|
214 |
(*TODO: unify with values'*)
|
walther@59987
|
215 |
fun values (oris:T) =
|
walther@59969
|
216 |
((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
|
walther@59969
|
217 |
|
walther@59986
|
218 |
|
walther@59998
|
219 |
(** complete wrt. Model_Pattern.T by use of root's O_Model.T **)
|
walther@59998
|
220 |
|
walther@59998
|
221 |
fun complete_for_from m_patt root_model (o_model, ctxt) =
|
walther@59998
|
222 |
let
|
walther@59998
|
223 |
val missing = m_patt |> filter_out
|
walther@59998
|
224 |
(fn (_, (descriptor, _)) => (Library.member op = (map #4 o_model) descriptor))
|
walther@60001
|
225 |
val add = (root_model
|
walther@60001
|
226 |
|> filter
|
walther@59998
|
227 |
(fn (_, _, _, descriptor, _) => (Library.member op = (map (fst o snd) missing)) descriptor))
|
walther@60001
|
228 |
|> map (fn (a, b, _, d, e) => (a, b, "#undef", d, e))
|
walther@60001
|
229 |
(* indicate, that m_field ---------^^^^^^^^ might change from root- to sub-Model_Pattern *)
|
walther@59998
|
230 |
in
|
walther@59998
|
231 |
((o_model @ add)
|
walther@60001
|
232 |
|> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
|
walther@60001
|
233 |
|> add_id (* for correct enumeration *)
|
walther@60001
|
234 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
|
walther@59998
|
235 |
ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
|
walther@59998
|
236 |
end
|
walther@59998
|
237 |
|
walther@59998
|
238 |
|
walther@59986
|
239 |
(** ? ? ? **)
|
walther@59986
|
240 |
|
walther@59986
|
241 |
(* make oris from args of the stac SubProblem and from pbt.
|
walther@59986
|
242 |
can this formal argument (of a model-pattern) be omitted in the arg-list
|
walther@59986
|
243 |
of a SubProblem ? see calcelems.sml 'type met ' *)
|
walther@59986
|
244 |
fun is_copy_named_idstr str =
|
walther@59986
|
245 |
case (rev o Symbol.explode) str of
|
walther@59986
|
246 |
"'" :: _ :: "'" :: _ => true
|
walther@59986
|
247 |
| _ => false
|
walther@59986
|
248 |
fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
|
walther@59986
|
249 |
|
walther@59986
|
250 |
(* should this formal argument (of a model-pattern) create a new identifier? *)
|
walther@59986
|
251 |
fun is_copy_named_generating_idstr str =
|
walther@59986
|
252 |
if is_copy_named_idstr str
|
walther@59986
|
253 |
then
|
walther@59986
|
254 |
case (rev o Symbol.explode) str of
|
walther@59986
|
255 |
"'" :: "'" :: "'" :: _ => false
|
walther@59986
|
256 |
| _ => true
|
walther@59986
|
257 |
else false
|
walther@59986
|
258 |
fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
|
walther@59986
|
259 |
|
walther@59986
|
260 |
(* generate a new variable "x_i" name from a related given one "x"
|
walther@59986
|
261 |
by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
|
walther@59986
|
262 |
e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
|
walther@59986
|
263 |
but leave is_copy_named_generating as is, e.t. ss''' *)
|
walther@59986
|
264 |
fun cpy_nam pbt oris (p as (field, (dsc, t))) =
|
walther@59986
|
265 |
(if is_copy_named_generating p
|
walther@59986
|
266 |
then (*WN051014 kept strange old code ...*)
|
walther@59986
|
267 |
let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
|
walther@59986
|
268 |
val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
|
walther@59986
|
269 |
val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
|
walther@59986
|
270 |
val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
|
walther@59986
|
271 |
val vals = map sel oris
|
walther@59986
|
272 |
val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
|
walther@59986
|
273 |
in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
|
walther@59986
|
274 |
else ([1], field, dsc, [t])
|
walther@59986
|
275 |
) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
|
walther@59986
|
276 |
|
walther@59997
|
277 |
(* ["BOOL (1+x=2)", "REAL x"] --match_ags--> oris
|
walther@59997
|
278 |
--values'--> ["equality (1+x=2)", "boundVariable x", "solutions L"] *)
|
walther@59987
|
279 |
(*TODO: unify with values*)
|
walther@59987
|
280 |
fun values' oris =
|
walther@59986
|
281 |
let fun ori2fmz_vals (_, _, _, dsc, ts) =
|
walther@59986
|
282 |
((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
|
walther@59986
|
283 |
handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
|
walther@59986
|
284 |
in (split_list o (map ori2fmz_vals)) oris end
|
walther@59986
|
285 |
|
walther@59999
|
286 |
|
walther@60000
|
287 |
(** tools for I_Model **)
|
walther@59999
|
288 |
|
walther@60004
|
289 |
(** )
|
walther@59999
|
290 |
fun seek_oridts ctxt sel (d, ts) [] =
|
walther@59999
|
291 |
("seek_oridts: input ('" ^
|
walther@59999
|
292 |
(UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",
|
walther@59999
|
293 |
(0, [], sel, d, ts),
|
walther@59999
|
294 |
[])
|
walther@59999
|
295 |
| seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
|
walther@59999
|
296 |
if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
|
walther@59999
|
297 |
then ("", (id, vat, sel, d, inter op = ts ts'), ts')
|
walther@59999
|
298 |
else seek_oridts ctxt sel (d, ts) oris
|
walther@60004
|
299 |
( **)
|
walther@60003
|
300 |
fun seek_oridts ctxt m_field (descript, vals) [] =
|
walther@60003
|
301 |
("seek_oridts: input ('" ^ UnparseC.term_in_ctxt ctxt (Input_Descript.join (descript, vals)) ^
|
walther@60003
|
302 |
"') not found in oris (typed)", (0, [], m_field, descript, vals), [])
|
walther@60003
|
303 |
| seek_oridts ctxt m_field (descript, vals) ((id, vat, m_field', descript', vals') :: oris) =
|
walther@60003
|
304 |
if (inter op = vals vals') <> [] andalso descript = descript' then
|
walther@60004
|
305 |
if m_field = "#undef" then (* m_field may change from root- to sub-Model_Pattern *)
|
walther@60003
|
306 |
("", (id, vat, m_field, descript, inter op = vals vals'), vals')
|
walther@60003
|
307 |
else if m_field = m_field' then
|
walther@60003
|
308 |
("", (id, vat, m_field, descript, inter op = vals vals'), vals')
|
walther@60003
|
309 |
else
|
walther@60003
|
310 |
(((strs2str' o map (UnparseC.term_in_ctxt ctxt)) vals) ^
|
walther@60003
|
311 |
" not for " ^ m_field, single_empty, [])
|
walther@60003
|
312 |
else seek_oridts ctxt m_field (descript, vals) oris
|
walther@59999
|
313 |
|
walther@59999
|
314 |
(* to an input (_,ts) find the according ori and insert the ts *)
|
walther@60001
|
315 |
fun seek_orits ctxt _ values [] =
|
walther@60001
|
316 |
("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) values) ^
|
walther@59999
|
317 |
"') not found in oris (typed)", single_empty, [])
|
walther@60001
|
318 |
| seek_orits ctxt sel values ((id, vat, sel', d, values') :: oris) =
|
walther@60001
|
319 |
if (inter op = values values') <> [] then
|
walther@60001
|
320 |
if sel = "#undef" then (* indicates that m_field changed from root- to sub-Model_Pattern *)
|
walther@60001
|
321 |
("", (id, vat, sel, d, inter op = values values'), values')
|
walther@60001
|
322 |
else if sel = sel' then
|
walther@60001
|
323 |
("", (id, vat, sel, d, inter op = values values'), values')
|
walther@60001
|
324 |
else
|
walther@60001
|
325 |
(((strs2str' o map (UnparseC.term_in_ctxt ctxt)) values) ^
|
walther@60001
|
326 |
" not for " ^ sel, single_empty, [])
|
walther@60001
|
327 |
else seek_orits ctxt sel values oris
|
walther@59999
|
328 |
|
walther@60000
|
329 |
fun test_types ctxt (d,ts) =
|
walther@60000
|
330 |
let
|
walther@60000
|
331 |
val opt = (try Input_Descript.join) (d, ts)
|
walther@60000
|
332 |
val msg = case opt of
|
walther@60000
|
333 |
SOME _ => ""
|
walther@60000
|
334 |
| NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
|
walther@60000
|
335 |
(strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts ^ " is illtyped")
|
walther@60000
|
336 |
in msg end
|
walther@60000
|
337 |
|
walther@60000
|
338 |
(* make a term 'typeless' for comparing with another 'typeless' term;
|
walther@60000
|
339 |
'type-less' usually is illtyped *)
|
walther@60000
|
340 |
fun typeless (Const (s, _)) = (Const (s, TermC.typ_empty))
|
walther@60000
|
341 |
| typeless (Free (s, _)) = (Free (s, TermC.typ_empty))
|
walther@60000
|
342 |
| typeless (Var (n, _)) = (Var (n, TermC.typ_empty))
|
walther@60000
|
343 |
| typeless (Bound i) = (Bound i)
|
walther@60000
|
344 |
| typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, typeless t)
|
walther@60000
|
345 |
| typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
|
walther@60000
|
346 |
|
walther@60000
|
347 |
(* is the term t input (or taken from fmz) known in O_Model ?
|
walther@60000
|
348 |
give feedback on all(?) strange input;
|
walther@60000
|
349 |
return _all_ terms already input to this item (e.g. valuesFor a,b) *)
|
walther@60000
|
350 |
fun is_known ctxt sel ori t =
|
walther@60000
|
351 |
let
|
walther@60000
|
352 |
val ots = (distinct o flat o (map #5)) ori
|
walther@60000
|
353 |
val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
|
walther@60000
|
354 |
val (d, ts) = Input_Descript.split t
|
walther@60000
|
355 |
val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
|
walther@60000
|
356 |
in
|
walther@60000
|
357 |
if (subtract op = oids ids) <> []
|
walther@60000
|
358 |
then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", single_empty, [])
|
walther@60000
|
359 |
else
|
walther@60000
|
360 |
if d = TermC.empty
|
walther@60000
|
361 |
then
|
walther@60000
|
362 |
if not (subset op = (map typeless ts, map typeless ots))
|
walther@60000
|
363 |
then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^
|
walther@60000
|
364 |
"' not in example (typeless)", single_empty, [])
|
walther@60000
|
365 |
else
|
walther@60001
|
366 |
(case seek_orits ctxt sel ts(*..values*) ori of
|
walther@60001
|
367 |
("", ori_ as (_, _, _, d, ts), all) =>
|
walther@60000
|
368 |
(case test_types ctxt (d,ts) of
|
walther@60000
|
369 |
"" => ("", ori_, all)
|
walther@60000
|
370 |
| msg => (msg, single_empty, []))
|
walther@60000
|
371 |
| (msg, _, _) => (msg, single_empty, []))
|
walther@60000
|
372 |
else
|
walther@60000
|
373 |
if member op = (map #4 ori) d
|
walther@60000
|
374 |
then seek_oridts ctxt sel (d, ts) ori
|
walther@60000
|
375 |
else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])
|
walther@60000
|
376 |
end
|
walther@59999
|
377 |
|
walther@59938
|
378 |
(**)end(**); |