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@59998
|
5 |
This model combines Formalise.T and Model_Pattern.T;
|
walther@59998
|
6 |
it makes student's editing via I_Model.T more efficient.
|
walther@59998
|
7 |
|
walther@59953
|
8 |
TODO: revise with an example with more than 1 variant.
|
walther@59998
|
9 |
+ consider to add
|
walther@59953
|
10 |
*)
|
walther@59938
|
11 |
|
walther@59938
|
12 |
signature ORIGINAL_MODEL =
|
walther@59938
|
13 |
sig
|
walther@59961
|
14 |
type T
|
walther@59961
|
15 |
type single
|
walther@59961
|
16 |
type variants
|
walther@59961
|
17 |
type m_field
|
walther@59961
|
18 |
type descriptor
|
walther@59998
|
19 |
type values
|
walther@59940
|
20 |
val to_string: T -> string
|
walther@59957
|
21 |
val single_to_string: single -> string
|
walther@59940
|
22 |
val single_empty: single
|
walther@59939
|
23 |
|
walther@59998
|
24 |
(*val init: theory -> Formalise.model -> Model_Pattern.T -> T ..TODO*)
|
walther@59952
|
25 |
val init: Formalise.model -> theory -> Model_Pattern.T -> T
|
walther@59960
|
26 |
val add : theory -> Model_Pattern.T -> T -> T
|
walther@59969
|
27 |
val values : T -> term list
|
walther@59987
|
28 |
val values': T -> Formalise.model * term list
|
walther@59998
|
29 |
val complete_for_from: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
|
walther@59969
|
30 |
|
walther@59987
|
31 |
(*/------- rename -------\*)
|
walther@59998
|
32 |
(*put add_id into a new auxiliary fun, see ONLY call..*)
|
walther@59961
|
33 |
val add_id: 'a list -> (int * 'a) list
|
walther@59961
|
34 |
type preori
|
walther@59961
|
35 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59998
|
36 |
(*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
|
walther@59986
|
37 |
val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
|
walther@59986
|
38 |
val is_copy_named: Model_Pattern.single -> bool
|
walther@59986
|
39 |
val is_copy_named_idstr: string -> bool
|
walther@59986
|
40 |
val is_copy_named_generating_idstr: string -> bool
|
walther@59986
|
41 |
val is_copy_named_generating: Model_Pattern.single -> bool
|
walther@59986
|
42 |
|
walther@59961
|
43 |
val preoris2str : preori list -> string
|
walther@59998
|
44 |
(*val getr_ct: theory -> single -> m_field * UnparseC.term_as_string*)
|
walther@59992
|
45 |
val getr_ct: theory -> single -> m_field * UnparseC.term_as_string
|
walther@59992
|
46 |
|
walther@59961
|
47 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59998
|
48 |
val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
|
walther@59952
|
49 |
val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
|
walther@59998
|
50 |
(*val max: variants -> int*)
|
walther@59952
|
51 |
val max: variants -> int
|
walther@59998
|
52 |
(*val coll_variants: ('a * ''b) list -> ('a list * ''b) list*)
|
walther@59947
|
53 |
val coll_variants: ('a * ''b) list -> ('a list * ''b) list
|
walther@59998
|
54 |
(*val replace_0: int -> int list -> int list*)
|
walther@59947
|
55 |
val replace_0: int -> int list -> int list
|
walther@59947
|
56 |
val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
|
walther@59998
|
57 |
(*val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list*)
|
walther@59998
|
58 |
val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
|
walther@59987
|
59 |
(*\------- rename -------/*)
|
walther@59938
|
60 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59938
|
61 |
end
|
walther@59938
|
62 |
|
walther@59974
|
63 |
(**)
|
walther@59938
|
64 |
structure O_Model(**) : ORIGINAL_MODEL(**) =
|
walther@59938
|
65 |
struct
|
walther@59974
|
66 |
(**)
|
walther@59938
|
67 |
|
walther@59960
|
68 |
(** types **)
|
walther@59960
|
69 |
|
walther@59940
|
70 |
type variants = Model_Def.variants;
|
walther@59952
|
71 |
type m_field = Model_Def.m_field;
|
walther@59952
|
72 |
type descriptor = Model_Def.descriptor;
|
walther@59998
|
73 |
type values = Model_Def.values;
|
walther@59938
|
74 |
|
walther@59940
|
75 |
type T = Model_Def.o_model;
|
walther@59940
|
76 |
type single = Model_Def.o_model_single
|
walther@59940
|
77 |
val single_empty = Model_Def.o_model_empty;
|
walther@59957
|
78 |
val single_to_string = Model_Def.o_model_single_to_string;
|
walther@59940
|
79 |
val to_string = Model_Def.o_model_to_string;
|
walther@59940
|
80 |
|
walther@59952
|
81 |
(* O_Model.single without leading integer *)
|
walther@59952
|
82 |
type preori = (variants * m_field * term * term list);
|
walther@59942
|
83 |
fun preori2str (vs, fi, t, ts) =
|
walther@59942
|
84 |
"(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
|
walther@59942
|
85 |
UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
|
walther@59942
|
86 |
val preoris2str = (strs2str' o (map (linefeed o preori2str)));
|
walther@59942
|
87 |
|
walther@59992
|
88 |
(* get the first term in ts from ori *)
|
walther@59992
|
89 |
fun getr_ct thy (_, _, fd, d, ts) =
|
walther@59992
|
90 |
(fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
|
walther@59992
|
91 |
|
walther@59960
|
92 |
|
walther@59960
|
93 |
(** initialise O_Model **)
|
walther@59960
|
94 |
|
walther@59947
|
95 |
(* compare d and dsc in pbt and transfer field to pre-ori *)
|
walther@59947
|
96 |
fun add_field (_: theory) pbt (d,ts) =
|
walther@59947
|
97 |
let fun eq d pt = (d = (fst o snd) pt);
|
walther@59947
|
98 |
in case filter (eq d) pbt of
|
walther@59947
|
99 |
[(fi, (_, _))] => (fi, d, ts)
|
walther@59947
|
100 |
| [] => ("#undef", d, ts) (*may come with met.ppc*)
|
walther@59952
|
101 |
| _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
|
walther@59947
|
102 |
end;
|
walther@59947
|
103 |
|
walther@59952
|
104 |
(*
|
walther@59952
|
105 |
mark an element with the position within a plateau;
|
walther@59952
|
106 |
a plateau with length 1 is marked with 0
|
walther@59952
|
107 |
*)
|
walther@59952
|
108 |
fun mark _ [] = raise ERROR "mark []"
|
walther@59952
|
109 |
| mark eq xs =
|
walther@59952
|
110 |
let
|
walther@59952
|
111 |
fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
|
walther@59952
|
112 |
| mar _ _ [] _ = raise ERROR "mark []"
|
walther@59952
|
113 |
| mar xx eq (x:: x' :: xs) n =
|
walther@59952
|
114 |
if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
|
walther@59952
|
115 |
else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
|
walther@59952
|
116 |
in mar [] eq xs 1 end;
|
walther@59952
|
117 |
|
walther@59952
|
118 |
(*
|
walther@59952
|
119 |
assumes equal descriptions to be in adjacent 'plateaus',
|
walther@59952
|
120 |
items at a certain position within the plateaus form a variant;
|
walther@59952
|
121 |
length = 1 ... marked with 0: covers all variants
|
walther@59952
|
122 |
*)
|
walther@59947
|
123 |
fun add_variants fdts =
|
walther@59947
|
124 |
let
|
walther@59947
|
125 |
fun eq (a, b) = curry op= (snd3 a) (snd3 b);
|
walther@59947
|
126 |
in mark eq fdts end;
|
walther@59947
|
127 |
|
walther@59952
|
128 |
fun max [] = raise ERROR "max of []"
|
walther@59947
|
129 |
| max (y :: ys) =
|
walther@59947
|
130 |
let fun mx x [] = x
|
walther@59947
|
131 |
| mx x (y :: ys) = if x < y then mx y ys else mx x ys;
|
walther@59947
|
132 |
in mx y ys end;
|
walther@59947
|
133 |
|
walther@59947
|
134 |
fun coll_variants (((v,x) :: vxs)) =
|
walther@59947
|
135 |
let
|
walther@59947
|
136 |
fun col xs (vs, x) [] = xs @ [(vs, x)]
|
walther@59947
|
137 |
| col xs (vs, x) ((v', x') :: vxs') =
|
walther@59947
|
138 |
if x = x' then col xs (vs @ [v'], x') vxs'
|
walther@59947
|
139 |
else col (xs @ [(vs, x)]) ([v'], x') vxs';
|
walther@59947
|
140 |
in col [] ([v], x) vxs end
|
walther@59952
|
141 |
| coll_variants _ = raise ERROR "coll_variants: called with []";
|
walther@59947
|
142 |
|
walther@59947
|
143 |
fun replace_0 vm [0] = intsto vm
|
walther@59947
|
144 |
| replace_0 _ vs = vs;
|
walther@59947
|
145 |
|
walther@59961
|
146 |
fun add_id [] = raise ERROR "O_Model.add_id []"
|
walther@59947
|
147 |
| add_id xs =
|
walther@59947
|
148 |
let
|
walther@59947
|
149 |
fun add _ [] = []
|
walther@59947
|
150 |
| add n (x :: xs) = (n, x) :: add (n + 1) xs;
|
walther@59947
|
151 |
in add 1 xs end;
|
walther@59947
|
152 |
|
walther@59947
|
153 |
fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
|
walther@59947
|
154 |
|
walther@59952
|
155 |
fun init [] _ _ = []
|
walther@59952
|
156 |
| init fmz thy pbt =
|
walther@59947
|
157 |
let
|
walther@59996
|
158 |
val model =
|
walther@59996
|
159 |
(map (fn str => str
|
walther@59996
|
160 |
|> TermC.parseNEW'' thy
|
walther@59996
|
161 |
|> Input_Descript.split
|
walther@59996
|
162 |
|> add_field thy pbt) fmz)
|
walther@59996
|
163 |
|> add_variants;
|
walther@59952
|
164 |
val maxv = model |> map fst |> max;
|
walther@59947
|
165 |
val maxv = if maxv = 0 then 1 else maxv;
|
walther@59952
|
166 |
val model' = model
|
walther@59952
|
167 |
|> coll_variants
|
walther@59947
|
168 |
|> map (replace_0 maxv |> apfst)
|
walther@59947
|
169 |
|> add_id
|
walther@59947
|
170 |
|> map flattup;
|
walther@59952
|
171 |
in model' end;
|
walther@59938
|
172 |
|
walther@59960
|
173 |
|
walther@59998
|
174 |
(** add new m_field's from method \<rightarrow> REPLACE BY complete_for_from **)
|
walther@59960
|
175 |
|
walther@59998
|
176 |
(* for the root-problem *)
|
walther@59960
|
177 |
fun add _ mpc ori =
|
walther@59960
|
178 |
let
|
walther@59960
|
179 |
fun eq d pt = (d = (fst o snd) pt);
|
walther@59960
|
180 |
fun repl mpc (i, v, _, d, ts) =
|
walther@59960
|
181 |
case filter (eq d) mpc of
|
walther@59960
|
182 |
[(fi, (_, _))] => [(i, v, fi, d, ts)]
|
walther@59960
|
183 |
| [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
|
walther@59962
|
184 |
| _ => raise ERROR ("O_Model.add: " ^ UnparseC.term d ^ " more than once in met");
|
walther@59960
|
185 |
in flat ((map (repl mpc)) ori) end;
|
walther@59960
|
186 |
|
walther@59969
|
187 |
|
walther@59969
|
188 |
(** get the values **)
|
walther@59969
|
189 |
|
walther@59969
|
190 |
fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"
|
walther@59969
|
191 |
| mkval _ [t] = t
|
walther@59969
|
192 |
| mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
|
walther@59969
|
193 |
fun mkval' x = mkval TermC.empty x;
|
walther@59987
|
194 |
(*TODO: unify with values'*)
|
walther@59987
|
195 |
fun values (oris:T) =
|
walther@59969
|
196 |
((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
|
walther@59969
|
197 |
|
walther@59986
|
198 |
|
walther@59998
|
199 |
(** complete wrt. Model_Pattern.T by use of root's O_Model.T **)
|
walther@59998
|
200 |
|
walther@59998
|
201 |
fun complete_for_from m_patt root_model (o_model, ctxt) =
|
walther@59998
|
202 |
let
|
walther@59998
|
203 |
val missing = m_patt |> filter_out
|
walther@59998
|
204 |
(fn (_, (descriptor, _)) => (Library.member op = (map #4 o_model) descriptor))
|
walther@59998
|
205 |
val add = (root_model |> filter
|
walther@59998
|
206 |
(fn (_, _, _, descriptor, _) => (Library.member op = (map (fst o snd) missing)) descriptor))
|
walther@59998
|
207 |
in
|
walther@59998
|
208 |
((o_model @ add)
|
walther@59998
|
209 |
|> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration*)
|
walther@59998
|
210 |
|> add_id (* for correct enumeration*)
|
walther@59998
|
211 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))(* for correct enumeration*),
|
walther@59998
|
212 |
ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
|
walther@59998
|
213 |
end
|
walther@59998
|
214 |
|
walther@59998
|
215 |
|
walther@59986
|
216 |
(** ? ? ? **)
|
walther@59986
|
217 |
|
walther@59986
|
218 |
(* make oris from args of the stac SubProblem and from pbt.
|
walther@59986
|
219 |
can this formal argument (of a model-pattern) be omitted in the arg-list
|
walther@59986
|
220 |
of a SubProblem ? see calcelems.sml 'type met ' *)
|
walther@59986
|
221 |
fun is_copy_named_idstr str =
|
walther@59986
|
222 |
case (rev o Symbol.explode) str of
|
walther@59986
|
223 |
"'" :: _ :: "'" :: _ => true
|
walther@59986
|
224 |
| _ => false
|
walther@59986
|
225 |
fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
|
walther@59986
|
226 |
|
walther@59986
|
227 |
(* should this formal argument (of a model-pattern) create a new identifier? *)
|
walther@59986
|
228 |
fun is_copy_named_generating_idstr str =
|
walther@59986
|
229 |
if is_copy_named_idstr str
|
walther@59986
|
230 |
then
|
walther@59986
|
231 |
case (rev o Symbol.explode) str of
|
walther@59986
|
232 |
"'" :: "'" :: "'" :: _ => false
|
walther@59986
|
233 |
| _ => true
|
walther@59986
|
234 |
else false
|
walther@59986
|
235 |
fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
|
walther@59986
|
236 |
|
walther@59986
|
237 |
(* generate a new variable "x_i" name from a related given one "x"
|
walther@59986
|
238 |
by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
|
walther@59986
|
239 |
e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
|
walther@59986
|
240 |
but leave is_copy_named_generating as is, e.t. ss''' *)
|
walther@59986
|
241 |
fun cpy_nam pbt oris (p as (field, (dsc, t))) =
|
walther@59986
|
242 |
(if is_copy_named_generating p
|
walther@59986
|
243 |
then (*WN051014 kept strange old code ...*)
|
walther@59986
|
244 |
let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
|
walther@59986
|
245 |
val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
|
walther@59986
|
246 |
val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
|
walther@59986
|
247 |
val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
|
walther@59986
|
248 |
val vals = map sel oris
|
walther@59986
|
249 |
val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
|
walther@59986
|
250 |
in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
|
walther@59986
|
251 |
else ([1], field, dsc, [t])
|
walther@59986
|
252 |
) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
|
walther@59986
|
253 |
|
walther@59997
|
254 |
(* ["BOOL (1+x=2)", "REAL x"] --match_ags--> oris
|
walther@59997
|
255 |
--values'--> ["equality (1+x=2)", "boundVariable x", "solutions L"] *)
|
walther@59987
|
256 |
(*TODO: unify with values*)
|
walther@59987
|
257 |
fun values' oris =
|
walther@59986
|
258 |
let fun ori2fmz_vals (_, _, _, dsc, ts) =
|
walther@59986
|
259 |
((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
|
walther@59986
|
260 |
handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
|
walther@59986
|
261 |
in (split_list o (map ori2fmz_vals)) oris end
|
walther@59986
|
262 |
|
walther@59938
|
263 |
(**)end(**); |