neuper@38051
|
1 |
(* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
|
neuper@38051
|
2 |
most important types are declared in mstools.sml.
|
neuper@38051
|
3 |
Author: Walther Neuper 991122
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37934
|
6 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@37934
|
7 |
10 20 30 40 50 60 70 80
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
(* TODO interne Funktionen aus sig entfernen *)
|
neuper@37906
|
11 |
signature CALC_HEAD =
|
neuper@37906
|
12 |
sig
|
neuper@37906
|
13 |
datatype additm = Add of SpecifyTools.itm | Err of string
|
neuper@37906
|
14 |
val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
|
neuper@37906
|
15 |
val all_modspec : ptree * pos' -> ptree * pos'
|
neuper@37906
|
16 |
datatype appl = Appl of tac_ | Notappl of string
|
neuper@37906
|
17 |
val appl_add :
|
neuper@37931
|
18 |
theory ->
|
neuper@37906
|
19 |
string ->
|
neuper@37906
|
20 |
SpecifyTools.ori list ->
|
neuper@37906
|
21 |
SpecifyTools.itm list ->
|
neuper@37906
|
22 |
(string * (Term.term * Term.term)) list -> cterm' -> additm
|
neuper@37906
|
23 |
type calcstate
|
neuper@37906
|
24 |
type calcstate'
|
neuper@37934
|
25 |
val chk_vars : term ppc -> string * Term.term list
|
neuper@37906
|
26 |
val chktyp :
|
neuper@37934
|
27 |
theory -> int * term list * term list -> term
|
neuper@37906
|
28 |
val chktyps :
|
neuper@37934
|
29 |
theory -> term list * term list -> term list
|
neuper@37906
|
30 |
val complete_metitms :
|
neuper@37906
|
31 |
SpecifyTools.ori list ->
|
neuper@37906
|
32 |
SpecifyTools.itm list ->
|
neuper@37906
|
33 |
SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
|
neuper@37906
|
34 |
val complete_mod_ : ori list * pat list * pat list * itm list ->
|
neuper@37906
|
35 |
itm list * itm list
|
neuper@37906
|
36 |
val complete_mod : ptree * pos' -> ptree * (pos * pos_)
|
neuper@37906
|
37 |
val complete_spec : ptree * pos' -> ptree * pos'
|
neuper@37906
|
38 |
val cpy_nam :
|
neuper@37906
|
39 |
pat list -> preori list -> pat -> preori
|
neuper@37906
|
40 |
val e_calcstate : calcstate
|
neuper@37906
|
41 |
val e_calcstate' : calcstate'
|
neuper@37906
|
42 |
val eq1 : ''a -> 'b * (''a * 'c) -> bool
|
neuper@37906
|
43 |
val eq3 :
|
neuper@37906
|
44 |
''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
|
neuper@37906
|
45 |
val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
|
neuper@37906
|
46 |
val eq5 :
|
neuper@37906
|
47 |
'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
|
neuper@37906
|
48 |
'e * 'f * 'g * Term.term * 'h -> bool
|
neuper@37906
|
49 |
val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
|
neuper@37906
|
50 |
val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
|
neuper@37931
|
51 |
val f_mout : theory -> mout -> Term.term
|
neuper@37906
|
52 |
val filter_outs :
|
neuper@37906
|
53 |
SpecifyTools.ori list ->
|
neuper@37906
|
54 |
SpecifyTools.itm list -> SpecifyTools.ori list
|
neuper@37906
|
55 |
val filter_pbt :
|
neuper@37906
|
56 |
SpecifyTools.ori list ->
|
neuper@37906
|
57 |
('a * (Term.term * 'b)) list -> SpecifyTools.ori list
|
neuper@37906
|
58 |
val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
|
neuper@37906
|
59 |
val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
|
neuper@37906
|
60 |
val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
|
neuper@37906
|
61 |
val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
|
neuper@37906
|
62 |
val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
|
neuper@37906
|
63 |
val get_formress :
|
neuper@37906
|
64 |
(string * (pos * pos_) * Term.term) list list ->
|
neuper@37906
|
65 |
pos -> ptree list -> (string * (pos * pos_) * Term.term) list
|
neuper@37906
|
66 |
val get_forms :
|
neuper@37906
|
67 |
(string * (pos * pos_) * Term.term) list list ->
|
neuper@37906
|
68 |
posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
|
neuper@37906
|
69 |
val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
|
neuper@37906
|
70 |
val get_ocalhd : ptree * pos' -> ocalhd
|
neuper@37906
|
71 |
val get_spec_form : tac_ -> pos' -> ptree -> mout
|
neuper@37906
|
72 |
val geti_ct :
|
neuper@37931
|
73 |
theory ->
|
neuper@37906
|
74 |
SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
|
neuper@37931
|
75 |
val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
|
neuper@37906
|
76 |
val has_list_type : Term.term -> bool
|
neuper@37906
|
77 |
val header : pos_ -> pblID -> metID -> pblmet
|
neuper@37906
|
78 |
val insert_ppc :
|
neuper@37931
|
79 |
theory ->
|
neuper@37906
|
80 |
int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
|
neuper@37906
|
81 |
SpecifyTools.itm list -> SpecifyTools.itm list
|
neuper@37906
|
82 |
val insert_ppc' :
|
neuper@37906
|
83 |
SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
|
neuper@37906
|
84 |
val is_complete_mod : ptree * pos' -> bool
|
neuper@37906
|
85 |
val is_complete_mod_ : SpecifyTools.itm list -> bool
|
neuper@37906
|
86 |
val is_complete_modspec : ptree * pos' -> bool
|
neuper@37906
|
87 |
val is_complete_spec : ptree * pos' -> bool
|
neuper@37906
|
88 |
val is_copy_named : 'a * ('b * Term.term) -> bool
|
neuper@37906
|
89 |
val is_copy_named_idstr : string -> bool
|
neuper@37906
|
90 |
val is_error : SpecifyTools.itm_ -> bool
|
neuper@37906
|
91 |
val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
|
neuper@37906
|
92 |
val is_known :
|
neuper@37931
|
93 |
theory ->
|
neuper@37906
|
94 |
string ->
|
neuper@37906
|
95 |
SpecifyTools.ori list ->
|
neuper@37906
|
96 |
Term.term -> string * SpecifyTools.ori * Term.term list
|
neuper@37906
|
97 |
val is_list_type : Term.typ -> bool
|
neuper@37906
|
98 |
val is_notyet_input :
|
neuper@37931
|
99 |
theory ->
|
neuper@37906
|
100 |
SpecifyTools.itm list ->
|
neuper@37906
|
101 |
Term.term list ->
|
neuper@37906
|
102 |
SpecifyTools.ori ->
|
neuper@37906
|
103 |
('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
|
neuper@37906
|
104 |
val is_parsed : SpecifyTools.itm_ -> bool
|
neuper@37906
|
105 |
val is_untouched : SpecifyTools.itm -> bool
|
neuper@37906
|
106 |
val matc :
|
neuper@37931
|
107 |
theory ->
|
neuper@37906
|
108 |
pat list ->
|
neuper@37906
|
109 |
Term.term list ->
|
neuper@37906
|
110 |
(int list * string * Term.term * Term.term list) list ->
|
neuper@37906
|
111 |
(int list * string * Term.term * Term.term list) list
|
neuper@37906
|
112 |
val match_ags :
|
neuper@37931
|
113 |
theory -> pat list -> Term.term list -> SpecifyTools.ori list
|
neuper@37906
|
114 |
val maxl : int list -> int
|
neuper@37906
|
115 |
val match_ags_msg : string list -> Term.term -> Term.term list -> unit
|
neuper@37906
|
116 |
val memI : ''a list -> ''a -> bool
|
neuper@37906
|
117 |
val mk_additem : string -> cterm' -> tac
|
neuper@37931
|
118 |
val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
|
neuper@37906
|
119 |
val mtc :
|
neuper@37931
|
120 |
theory -> pat -> Term.term -> SpecifyTools.preori option
|
neuper@37906
|
121 |
val nxt_add :
|
neuper@37931
|
122 |
theory ->
|
neuper@37906
|
123 |
SpecifyTools.ori list ->
|
neuper@37906
|
124 |
(string * (Term.term * 'a)) list ->
|
neuper@37931
|
125 |
SpecifyTools.itm list -> (string * cterm') option
|
neuper@37906
|
126 |
val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
|
neuper@37906
|
127 |
val nxt_spec :
|
neuper@37906
|
128 |
pos_ ->
|
neuper@37906
|
129 |
bool ->
|
neuper@37906
|
130 |
SpecifyTools.ori list ->
|
neuper@37906
|
131 |
spec ->
|
neuper@37906
|
132 |
SpecifyTools.itm list * SpecifyTools.itm list ->
|
neuper@37906
|
133 |
(string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
|
neuper@37906
|
134 |
spec -> pos_ * tac
|
neuper@37906
|
135 |
val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
|
neuper@37906
|
136 |
val nxt_specif_additem :
|
neuper@37906
|
137 |
string -> cterm' -> ptree * (int list * pos_) -> calcstate'
|
neuper@37906
|
138 |
val nxt_specify_init_calc : fmz -> calcstate
|
neuper@37906
|
139 |
val ocalhd_complete :
|
neuper@37906
|
140 |
SpecifyTools.itm list ->
|
neuper@37906
|
141 |
(bool * Term.term) list -> domID * pblID * metID -> bool
|
neuper@37906
|
142 |
val ori2Coritm :
|
neuper@37906
|
143 |
pat list -> ori -> itm
|
neuper@37906
|
144 |
val ori_2itm :
|
neuper@37906
|
145 |
'a ->
|
neuper@37906
|
146 |
SpecifyTools.itm_ ->
|
neuper@37906
|
147 |
Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
|
neuper@37906
|
148 |
val overwrite_ppc :
|
neuper@37931
|
149 |
theory ->
|
neuper@37906
|
150 |
int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
|
neuper@37906
|
151 |
SpecifyTools.itm list ->
|
neuper@37906
|
152 |
(int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
|
neuper@37906
|
153 |
val parse_ok : SpecifyTools.itm_ list -> bool
|
neuper@37906
|
154 |
val posform2str : pos' * ptform -> string
|
neuper@37906
|
155 |
val posforms2str : (pos' * ptform) list -> string
|
neuper@37906
|
156 |
val posterms2str : (pos' * term) list -> string (*tests only*)
|
neuper@37906
|
157 |
val ppc135list : 'a SpecifyTools.ppc -> 'a list
|
neuper@37906
|
158 |
val ppc2list : 'a SpecifyTools.ppc -> 'a list
|
neuper@37906
|
159 |
val pt_extract :
|
neuper@37906
|
160 |
ptree * (int list * pos_) ->
|
neuper@37931
|
161 |
ptform * tac option * Term.term list
|
neuper@37906
|
162 |
val pt_form : ppobj -> ptform
|
neuper@37906
|
163 |
val pt_model : ppobj -> pos_ -> ptform
|
neuper@37906
|
164 |
val reset_calchead : ptree * pos' -> ptree * pos'
|
neuper@37906
|
165 |
val seek_oridts :
|
neuper@37931
|
166 |
theory ->
|
neuper@37906
|
167 |
string ->
|
neuper@37906
|
168 |
Term.term * Term.term list ->
|
neuper@37906
|
169 |
(int * SpecifyTools.vats * string * Term.term * Term.term list) list
|
neuper@37906
|
170 |
-> string * SpecifyTools.ori * Term.term list
|
neuper@37906
|
171 |
val seek_orits :
|
neuper@37931
|
172 |
theory ->
|
neuper@37906
|
173 |
string ->
|
neuper@37906
|
174 |
Term.term list ->
|
neuper@37906
|
175 |
(int * SpecifyTools.vats * string * Term.term * Term.term list) list
|
neuper@37906
|
176 |
-> string * SpecifyTools.ori * Term.term list
|
neuper@37906
|
177 |
val seek_ppc :
|
neuper@37931
|
178 |
int -> SpecifyTools.itm list -> SpecifyTools.itm option
|
neuper@37906
|
179 |
val show_pt : ptree -> unit
|
neuper@37906
|
180 |
val some_spec : spec -> spec -> spec
|
neuper@37906
|
181 |
val specify :
|
neuper@37906
|
182 |
tac_ ->
|
neuper@37906
|
183 |
pos' ->
|
neuper@37906
|
184 |
cid ->
|
neuper@37906
|
185 |
ptree ->
|
neuper@37906
|
186 |
(posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
|
neuper@37906
|
187 |
safe * ptree
|
neuper@37906
|
188 |
val specify_additem :
|
neuper@37906
|
189 |
string ->
|
neuper@37906
|
190 |
cterm' * 'a ->
|
neuper@37906
|
191 |
int list * pos_ ->
|
neuper@37906
|
192 |
'b ->
|
neuper@37906
|
193 |
ptree ->
|
neuper@37906
|
194 |
(pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
|
neuper@37934
|
195 |
val tag_form : theory -> term * term -> term
|
neuper@37931
|
196 |
val test_types : theory -> Term.term * Term.term list -> string
|
neuper@37906
|
197 |
val typeless : Term.term -> Term.term
|
neuper@37934
|
198 |
val unbound_ppc : term SpecifyTools.ppc -> Term.term list
|
neuper@37906
|
199 |
val vals_of_oris : SpecifyTools.ori list -> Term.term list
|
neuper@37906
|
200 |
val variants_in : Term.term list -> int
|
neuper@37906
|
201 |
val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
|
neuper@37906
|
202 |
val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
|
neuper@37906
|
203 |
end
|
neuper@37906
|
204 |
|
neuper@37906
|
205 |
|
neuper@37906
|
206 |
|
neuper@37906
|
207 |
|
neuper@37906
|
208 |
|
neuper@37906
|
209 |
(*---------------------------------------------------------------------*)
|
neuper@37906
|
210 |
structure CalcHead (**): CALC_HEAD(**) =
|
neuper@37906
|
211 |
|
neuper@37906
|
212 |
struct
|
neuper@37906
|
213 |
(*---------------------------------------------------------------------*)
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
(* datatypes *)
|
neuper@37906
|
216 |
|
neuper@37906
|
217 |
(*.the state wich is stored after each step of calculation; it contains
|
neuper@38065
|
218 |
the calc-state and a list of [tac,istate](="tacis") to be applied next.
|
neuper@37906
|
219 |
the last_elem tacis is the first to apply to the calc-state and
|
neuper@37906
|
220 |
the (only) one shown to the front-end as the 'proposed tac'.
|
neuper@37906
|
221 |
the calc-state resulting from the application of tacis is not stored,
|
neuper@38065
|
222 |
because the tacis hold enough information for efficiently rebuilding
|
neuper@37906
|
223 |
this state just by "fun generate ".*)
|
neuper@37906
|
224 |
type calcstate =
|
neuper@37906
|
225 |
(ptree * pos') * (*the calc-state to which the tacis could be applied*)
|
neuper@37906
|
226 |
(taci list); (*ev. several (hidden) steps;
|
neuper@37906
|
227 |
in REVERSE order: first tac_ to apply is last_elem*)
|
neuper@37906
|
228 |
val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
|
neuper@37906
|
229 |
|
neuper@37906
|
230 |
(*the state used during one calculation within the mathengine; it contains
|
neuper@37906
|
231 |
a list of [tac,istate](="tacis") which generated the the calc-state;
|
neuper@37906
|
232 |
while this state's tacis are extended by each (internal) step,
|
neuper@37906
|
233 |
the calc-state is used for creating new nodes in the calc-tree
|
neuper@37906
|
234 |
(eg. applicable_in requires several particular nodes of the calc-tree)
|
neuper@37906
|
235 |
and then replaced by the the newly created;
|
neuper@37906
|
236 |
on leave of the mathengine the resuing calc-state is dropped anyway,
|
neuper@37906
|
237 |
because the tacis hold enought information for efficiently rebuilding
|
neuper@37906
|
238 |
this state just by "fun generate ".*)
|
neuper@37906
|
239 |
type calcstate' =
|
neuper@37906
|
240 |
taci list * (*cas. several (hidden) steps;
|
neuper@37906
|
241 |
in REVERSE order: first tac_ to apply is last_elem*)
|
neuper@37906
|
242 |
pos' list * (*a "continuous" sequence of pos',
|
neuper@37906
|
243 |
deleted by application of taci list*)
|
neuper@37906
|
244 |
(ptree * pos'); (*the calc-state resulting from the application of tacis*)
|
neuper@37906
|
245 |
val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
|
neuper@37906
|
246 |
|
neuper@37906
|
247 |
(*FIXXXME.WN020430 intermediate hack for fun ass_up*)
|
neuper@37906
|
248 |
fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
|
neuper@38031
|
249 |
| f_mout thy _ = error "f_mout: not called with formula";
|
neuper@37906
|
250 |
|
neuper@37906
|
251 |
|
neuper@37906
|
252 |
(*.is the calchead complete ?.*)
|
neuper@37906
|
253 |
fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
|
neuper@37906
|
254 |
foldl and_ (true, map #3 its) andalso
|
neuper@37906
|
255 |
foldl and_ (true, map #1 pre) andalso
|
neuper@37906
|
256 |
dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
|
neuper@37906
|
257 |
|
neuper@37906
|
258 |
|
neuper@37906
|
259 |
(* make a term 'typeless' for comparing with another 'typeless' term;
|
neuper@37906
|
260 |
'type-less' usually is illtyped *)
|
neuper@37906
|
261 |
fun typeless (Const(s,_)) = (Const(s,e_type))
|
neuper@37906
|
262 |
| typeless (Free(s,_)) = (Free(s,e_type))
|
neuper@37906
|
263 |
| typeless (Var(n,_)) = (Var(n,e_type))
|
neuper@37906
|
264 |
| typeless (Bound i) = (Bound i)
|
neuper@37906
|
265 |
| typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
|
neuper@37906
|
266 |
| typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
|
neuper@37906
|
267 |
(*
|
neuper@37926
|
268 |
> val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
|
neuper@37906
|
269 |
> val (_,t1) = split_dsc_t hs (term_of ct);
|
neuper@37926
|
270 |
> val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
|
neuper@37906
|
271 |
> val (_,t2) = split_dsc_t hs (term_of ct);
|
neuper@37906
|
272 |
> typeless t1 = typeless t2;
|
neuper@37906
|
273 |
val it = true : bool
|
neuper@37906
|
274 |
*)
|
neuper@37906
|
275 |
|
neuper@37906
|
276 |
|
neuper@37906
|
277 |
|
neuper@37906
|
278 |
(*.to an input (d,ts) find the according ori and insert the ts.*)
|
neuper@37906
|
279 |
(*WN.11.03: + dont take first inter<>[]*)
|
neuper@37906
|
280 |
fun seek_oridts thy sel (d,ts) [] =
|
neuper@41933
|
281 |
("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
|
neuper@38053
|
282 |
(comp_dts thy (d,ts))) ^
|
neuper@41933
|
283 |
"') not found in oris (typed)", (0, [], sel, d, ts) : ori,
|
neuper@38053
|
284 |
[])
|
neuper@37906
|
285 |
| seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
|
neuper@37934
|
286 |
if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
|
neuper@37934
|
287 |
then if sel = sel'
|
neuper@37934
|
288 |
then ("",
|
neuper@37934
|
289 |
(id,vat,sel,d, inter op = ts ts'):ori,
|
neuper@37934
|
290 |
ts')
|
neuper@38053
|
291 |
else ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
|
neuper@38053
|
292 |
(comp_dts thy (d,ts))) ^ " not for " ^ sel,
|
neuper@37934
|
293 |
e_ori_,
|
neuper@37934
|
294 |
[])
|
neuper@37906
|
295 |
else seek_oridts thy sel (d,ts) oris;
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
(*.to an input (_,ts) find the according ori and insert the ts.*)
|
neuper@37906
|
298 |
fun seek_orits thy sel ts [] =
|
neuper@41933
|
299 |
("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
|
neuper@38053
|
300 |
(thy2ctxt thy))) ts) ^
|
neuper@41933
|
301 |
"') not found in oris (typed)", e_ori_, [])
|
neuper@37906
|
302 |
| seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
|
neuper@37934
|
303 |
if sel = sel' andalso (inter op = ts ts') <> []
|
neuper@38053
|
304 |
then if sel = sel'
|
neuper@38053
|
305 |
then ("",
|
neuper@38053
|
306 |
(id,vat,sel,d, inter op = ts ts'):ori,
|
neuper@38053
|
307 |
ts')
|
neuper@38053
|
308 |
else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
309 |
(thy2ctxt thy)))) ts)
|
neuper@38053
|
310 |
^ " not for " ^ sel,
|
neuper@38053
|
311 |
e_ori_,
|
neuper@38053
|
312 |
[])
|
neuper@37906
|
313 |
else seek_orits thy sel ts oris;
|
neuper@37906
|
314 |
(* false
|
neuper@37906
|
315 |
> val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
|
neuper@37906
|
316 |
> seek_orits thy sel ts [(id,vat,sel',d,ts')];
|
neuper@37906
|
317 |
uncaught exception TYPE
|
neuper@37906
|
318 |
> seek_orits thy sel ts [];
|
neuper@37906
|
319 |
uncaught exception TYPE
|
neuper@37906
|
320 |
*)
|
neuper@37906
|
321 |
|
neuper@37906
|
322 |
(*find_first item with #1 equal to id*)
|
neuper@37926
|
323 |
fun seek_ppc id [] = NONE
|
neuper@37906
|
324 |
| seek_ppc id (p::(ppc:itm list)) =
|
neuper@37926
|
325 |
if id = #1 p then SOME p else seek_ppc id ppc;
|
neuper@37906
|
326 |
|
neuper@37906
|
327 |
|
neuper@37906
|
328 |
|
neuper@37906
|
329 |
(*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
|
neuper@37906
|
330 |
|
neuper@37906
|
331 |
|
neuper@37906
|
332 |
datatype appl = Appl of tac_ | Notappl of string;
|
neuper@37906
|
333 |
|
neuper@37906
|
334 |
fun ppc2list ({Given=gis,Where=whs,Find=fis,
|
neuper@37906
|
335 |
With=wis,Relate=res}: 'a ppc) =
|
neuper@37906
|
336 |
gis @ whs @ fis @ wis @ res;
|
neuper@37906
|
337 |
fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
|
neuper@37906
|
338 |
gis @ fis @ res;
|
neuper@37906
|
339 |
|
neuper@37906
|
340 |
|
neuper@37906
|
341 |
|
neuper@37906
|
342 |
|
neuper@37906
|
343 |
(* get the number of variants in a problem in 'original',
|
neuper@37906
|
344 |
assumes equal descriptions in immediate sequence *)
|
neuper@37906
|
345 |
fun variants_in ts =
|
neuper@37906
|
346 |
let fun eq(x,y) = head_of x = head_of y;
|
neuper@37906
|
347 |
fun cnt eq [] y n = ([n],[])
|
neuper@37906
|
348 |
| cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
|
neuper@37906
|
349 |
else ([n], x::xs);
|
neuper@37906
|
350 |
fun coll eq xs [] = xs
|
neuper@37906
|
351 |
| coll eq xs (y::ys) =
|
neuper@37906
|
352 |
let val (n,ys') = cnt eq (y::ys) y 0;
|
neuper@37906
|
353 |
in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
|
neuper@37934
|
354 |
val vts = subtract op = [1] (distinct (coll eq [] ts));
|
neuper@37906
|
355 |
in case vts of [] => 1 | [n] => n
|
neuper@37906
|
356 |
| _ => error "different variants in formalization" end;
|
neuper@37906
|
357 |
(*
|
neuper@37906
|
358 |
> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
|
neuper@37906
|
359 |
val it = ([3],[4,5,5,5,5,5]) : int list * int list
|
neuper@37906
|
360 |
> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
|
neuper@37906
|
361 |
val it = [1,3,1,5] : int list
|
neuper@37906
|
362 |
*)
|
neuper@37906
|
363 |
|
neuper@37906
|
364 |
fun is_list_type (Type("List.list",_)) = true
|
neuper@37906
|
365 |
| is_list_type _ = false;
|
neuper@37906
|
366 |
(* fun destr (Type(str,sort)) = (str,sort);
|
neuper@37926
|
367 |
> val (SOME ct) = parse thy "lll::real list";
|
neuper@37906
|
368 |
> val ty = (#T o rep_cterm) ct;
|
neuper@37906
|
369 |
> is_list_type ty;
|
neuper@37906
|
370 |
val it = true : bool
|
neuper@37906
|
371 |
> destr ty;
|
neuper@37906
|
372 |
val it = ("List.list",["RealDef.real"]) : string * typ list
|
neuper@37906
|
373 |
> atomty ((#t o rep_cterm) ct);
|
neuper@37906
|
374 |
*** -------------
|
neuper@37906
|
375 |
*** Free ( lll, real list)
|
neuper@37906
|
376 |
val it = () : unit
|
neuper@37906
|
377 |
|
neuper@37926
|
378 |
> val (SOME ct) = parse thy "[lll::real]";
|
neuper@37906
|
379 |
> val ty = (#T o rep_cterm) ct;
|
neuper@37906
|
380 |
> is_list_type ty;
|
neuper@37906
|
381 |
val it = true : bool
|
neuper@37906
|
382 |
> destr ty;
|
neuper@37906
|
383 |
val it = ("List.list",["'a"]) : string * typ list
|
neuper@37906
|
384 |
> atomty ((#t o rep_cterm) ct);
|
neuper@37906
|
385 |
*** -------------
|
neuper@37906
|
386 |
*** Const ( List.list.Cons, [real, real list] => real list)
|
neuper@37906
|
387 |
*** Free ( lll, real)
|
neuper@37906
|
388 |
*** Const ( List.list.Nil, real list)
|
neuper@37906
|
389 |
|
neuper@37926
|
390 |
> val (SOME ct) = parse thy "lll";
|
neuper@37906
|
391 |
> val ty = (#T o rep_cterm) ct;
|
neuper@37906
|
392 |
> is_list_type ty;
|
neuper@37906
|
393 |
val it = false : bool *)
|
neuper@37906
|
394 |
|
neuper@37906
|
395 |
|
neuper@37906
|
396 |
fun has_list_type (Free(_,T)) = is_list_type T
|
neuper@37906
|
397 |
| has_list_type _ = false;
|
neuper@37906
|
398 |
(*
|
neuper@37926
|
399 |
> val (SOME ct) = parse thy "lll::real list";
|
neuper@37906
|
400 |
> has_list_type (term_of ct);
|
neuper@37906
|
401 |
val it = true : bool
|
neuper@37926
|
402 |
> val (SOME ct) = parse thy "[lll::real]";
|
neuper@37906
|
403 |
> has_list_type (term_of ct);
|
neuper@37906
|
404 |
val it = false : bool *)
|
neuper@37906
|
405 |
|
neuper@37906
|
406 |
fun is_parsed (Syn _) = false
|
neuper@37906
|
407 |
| is_parsed _ = true;
|
neuper@37906
|
408 |
fun parse_ok its = foldl and_ (true, map is_parsed its);
|
neuper@37906
|
409 |
|
neuper@37906
|
410 |
fun all_dsc_in itm_s =
|
neuper@37906
|
411 |
let
|
neuper@37906
|
412 |
fun d_in (Cor ((d,_),_)) = [d]
|
neuper@37906
|
413 |
| d_in (Syn c) = []
|
neuper@37906
|
414 |
| d_in (Typ c) = []
|
neuper@37906
|
415 |
| d_in (Inc ((d,_),_)) = [d]
|
neuper@37906
|
416 |
| d_in (Sup (d,_)) = [d]
|
neuper@37906
|
417 |
| d_in (Mis (d,_)) = [d];
|
neuper@37906
|
418 |
in (flat o (map d_in)) itm_s end;
|
neuper@37906
|
419 |
|
neuper@37906
|
420 |
(* 30.1.00 ---
|
neuper@37906
|
421 |
fun is_Syn (Syn _) = true
|
neuper@37906
|
422 |
| is_Syn (Typ _) = true
|
neuper@37906
|
423 |
| is_Syn _ = false;
|
neuper@37906
|
424 |
--- *)
|
neuper@37906
|
425 |
fun is_error (Cor (_,ts)) = false
|
neuper@37906
|
426 |
| is_error (Sup (_,ts)) = false
|
neuper@37906
|
427 |
| is_error (Inc (_,ts)) = false
|
neuper@37906
|
428 |
| is_error (Mis (_,ts)) = false
|
neuper@37906
|
429 |
| is_error _ = true;
|
neuper@37906
|
430 |
|
neuper@37906
|
431 |
(* 30.1.00 ---
|
neuper@37906
|
432 |
fun ct_in (Syn (c)) = c
|
neuper@37906
|
433 |
| ct_in (Typ (c)) = c
|
neuper@38031
|
434 |
| ct_in _ = error "ct_in called for Cor .. Sup";
|
neuper@37906
|
435 |
--- *)
|
neuper@37906
|
436 |
|
neuper@37906
|
437 |
(*#############################################################*)
|
neuper@37906
|
438 |
(*#############################################################*)
|
neuper@37906
|
439 |
(* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
|
neuper@37906
|
440 |
|
neuper@37906
|
441 |
|
neuper@37906
|
442 |
(* testdaten besorgen:
|
neuper@37906
|
443 |
use"test-coil-kernel.sml";
|
neuper@37906
|
444 |
val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
|
neuper@37906
|
445 |
get_obj I pt p;
|
neuper@37906
|
446 |
*)
|
neuper@37906
|
447 |
|
neuper@37906
|
448 |
(* given oris, ppc,
|
neuper@37906
|
449 |
variant V: oris union ppc => int, id ID: oris union ppc => int
|
neuper@37906
|
450 |
|
neuper@37906
|
451 |
ppc is_complete ==
|
neuper@37906
|
452 |
EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
|
neuper@37906
|
453 |
|
neuper@37906
|
454 |
and
|
neuper@37906
|
455 |
@vt = max sum(i : ppc) V i
|
neuper@37906
|
456 |
*)
|
neuper@37906
|
457 |
|
neuper@37906
|
458 |
|
neuper@37906
|
459 |
|
neuper@37906
|
460 |
(*
|
neuper@37906
|
461 |
> ((vts_cnt (vts_in itms))) itms;
|
neuper@37906
|
462 |
|
neuper@37906
|
463 |
|
neuper@37906
|
464 |
|
neuper@37906
|
465 |
---^^--test 10.3.
|
neuper@37906
|
466 |
> val vts = vts_in itms;
|
neuper@37906
|
467 |
val vts = [1,2,3] : int list
|
neuper@37906
|
468 |
> val nvts = vts_cnt vts itms;
|
neuper@37906
|
469 |
val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
|
neuper@37906
|
470 |
> val mx = max2 nvts;
|
neuper@37906
|
471 |
val mx = (3,7) : int * int
|
neuper@37906
|
472 |
> val v = max_vt itms;
|
neuper@37906
|
473 |
val v = 3 : int
|
neuper@37906
|
474 |
--------------------------
|
neuper@37906
|
475 |
>
|
neuper@37906
|
476 |
*)
|
neuper@37906
|
477 |
|
neuper@37906
|
478 |
(*.get the first term in ts from ori.*)
|
neuper@37906
|
479 |
(* val (_,_,fd,d,ts) = hd miss;
|
neuper@37906
|
480 |
*)
|
neuper@38051
|
481 |
fun getr_ct thy ((_, _, fd, d, ts) : ori) =
|
neuper@38053
|
482 |
(fd, (Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy))) o
|
neuper@38051
|
483 |
(comp_dts thy)) (d,[hd ts]) : cterm');
|
neuper@37906
|
484 |
(* val t = comp_dts thy (d,[hd ts]);
|
neuper@37906
|
485 |
*)
|
neuper@37906
|
486 |
|
neuper@38051
|
487 |
(* get a term from ori, notyet input in itm.
|
neuper@38051
|
488 |
the term from ori is thrown back to a string in order to reuse
|
neuper@38051
|
489 |
machinery for immediate input by the user. *)
|
neuper@38051
|
490 |
fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
|
neuper@38053
|
491 |
(fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
|
neuper@38053
|
492 |
(comp_dts thy))
|
neuper@38053
|
493 |
(d, subtract op = (ts_in itm_) ts) : cterm');
|
neuper@38051
|
494 |
fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
|
neuper@38051
|
495 |
(fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
|
neuper@38051
|
496 |
(comp_dts thy))
|
neuper@38051
|
497 |
(d, subtract op = (ts_in itm_) ts) : cterm');
|
neuper@37906
|
498 |
|
neuper@37906
|
499 |
(* in FE dsc, not dat: this is in itms ...*)
|
neuper@37906
|
500 |
fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
|
neuper@37906
|
501 |
| is_untouched _ = false;
|
neuper@37906
|
502 |
|
neuper@37906
|
503 |
|
neuper@37906
|
504 |
(* select an item in oris, notyet input in itms
|
neuper@37906
|
505 |
(precondition: in itms are only Cor, Sup, Inc) *)
|
neuper@37936
|
506 |
local infix mem;
|
neuper@37934
|
507 |
fun x mem [] = false
|
neuper@37934
|
508 |
| x mem (y :: ys) = x = y orelse x mem ys;
|
neuper@37934
|
509 |
in
|
neuper@37906
|
510 |
fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
|
neuper@37906
|
511 |
let
|
neuper@37906
|
512 |
fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
|
neuper@37906
|
513 |
fun is_elem itms (f,(d,t)) =
|
neuper@37906
|
514 |
case find_first (test_d d) itms of
|
neuper@37926
|
515 |
SOME _ => true | NONE => false;
|
neuper@37906
|
516 |
in case filter_out (is_elem itms) pbt of
|
neuper@37906
|
517 |
(* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
|
neuper@37906
|
518 |
*)
|
neuper@37906
|
519 |
(f,(d,_))::itms =>
|
neuper@38053
|
520 |
SOME (f : string,
|
neuper@38053
|
521 |
((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
|
neuper@38053
|
522 |
comp_dts thy) (d, []) : cterm')
|
neuper@37926
|
523 |
| _ => NONE end
|
neuper@37906
|
524 |
|
neuper@37906
|
525 |
(* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
|
neuper@37906
|
526 |
*)
|
neuper@37906
|
527 |
| nxt_add thy oris pbt itms =
|
neuper@37906
|
528 |
let
|
neuper@37906
|
529 |
fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
|
neuper@37906
|
530 |
andalso (#3 ori) <>"#undef";
|
neuper@37906
|
531 |
fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
|
neuper@37906
|
532 |
fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
|
neuper@37906
|
533 |
fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
|
neuper@37934
|
534 |
(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
|
neuper@37906
|
535 |
fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
|
neuper@37906
|
536 |
| false_and_not_Sup (i,v,false,f, _) = true
|
neuper@37906
|
537 |
| false_and_not_Sup _ = false;
|
neuper@37906
|
538 |
|
neuper@37906
|
539 |
val v = if itms = [] then 1 else max_vt itms;
|
neuper@37906
|
540 |
val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
|
neuper@37906
|
541 |
val vits = if v = 0 then itms (*because of dsc without dat*)
|
neuper@37906
|
542 |
else filter (testi_vt v) itms; (*itms..vat*)
|
neuper@37906
|
543 |
val icl = filter false_and_not_Sup vits; (* incomplete *)
|
neuper@37906
|
544 |
in if icl = []
|
neuper@37906
|
545 |
then case filter_out (test_id (map #1 vits)) vors of
|
neuper@37926
|
546 |
[] => NONE
|
neuper@37906
|
547 |
(* val miss = filter_out (test_id (map #1 vits)) vors;
|
neuper@37906
|
548 |
*)
|
neuper@37926
|
549 |
| miss => SOME (getr_ct thy (hd miss))
|
neuper@37906
|
550 |
else
|
neuper@37906
|
551 |
case find_first (test_subset (hd icl)) vors of
|
neuper@37926
|
552 |
(* val SOME ori = find_first (test_subset (hd icl)) vors;
|
neuper@37906
|
553 |
*)
|
neuper@38031
|
554 |
NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
|
neuper@37926
|
555 |
| SOME ori => SOME (geti_ct thy ori (hd icl))
|
neuper@37934
|
556 |
end
|
neuper@37934
|
557 |
end;
|
neuper@37906
|
558 |
|
neuper@37906
|
559 |
|
neuper@37906
|
560 |
|
neuper@37906
|
561 |
fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
|
neuper@37906
|
562 |
| mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
|
neuper@37906
|
563 |
| mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
|
neuper@37906
|
564 |
| mk_delete thy str _ =
|
neuper@38031
|
565 |
error ("mk_delete: called with field '"^str^"'");
|
neuper@37906
|
566 |
fun mk_additem "#Given" ct = Add_Given ct
|
neuper@37906
|
567 |
| mk_additem "#Find" ct = Add_Find ct
|
neuper@37906
|
568 |
| mk_additem "#Relate"ct = Add_Relation ct
|
neuper@37906
|
569 |
| mk_additem str _ =
|
neuper@38031
|
570 |
error ("mk_additem: called with field '"^str^"'");
|
neuper@37906
|
571 |
|
neuper@37906
|
572 |
|
neuper@38051
|
573 |
(* determine the next step of specification;
|
neuper@38051
|
574 |
not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
|
neuper@38051
|
575 |
eg. in rootpbl 'no_met':
|
neuper@37906
|
576 |
args:
|
neuper@38051
|
577 |
preok predicates are _all_ ok (and problem matches completely)
|
neuper@37906
|
578 |
oris immediately from formalization
|
neuper@37906
|
579 |
(dI',pI',mI') specification coming from author/parent-problem
|
neuper@37906
|
580 |
(pbl, item lists specified by user
|
neuper@37906
|
581 |
met) -"-, tacitly completed by copy_probl
|
neuper@37906
|
582 |
(dI,pI,mI) specification explicitly done by the user
|
neuper@37906
|
583 |
(pbt, mpc) problem type, guard of method
|
neuper@38051
|
584 |
*)
|
neuper@38051
|
585 |
fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
|
neuper@38051
|
586 |
((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
|
neuper@38051
|
587 |
((*tracing"### nxt_spec Pbl";*)
|
neuper@38051
|
588 |
if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
|
neuper@38051
|
589 |
else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
|
neuper@38051
|
590 |
else case find_first (is_error o #5) (pbl:itm list) of
|
neuper@38051
|
591 |
SOME (_, _, _, fd, itm_) =>
|
neuper@37906
|
592 |
(Pbl, mk_delete
|
neuper@38051
|
593 |
(assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
|
neuper@38051
|
594 |
| NONE =>
|
neuper@38051
|
595 |
((*tracing"### nxt_spec is_error NONE";*)
|
neuper@38051
|
596 |
case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
|
neuper@38051
|
597 |
oris pbt pbl of
|
neuper@38051
|
598 |
SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
|
neuper@38051
|
599 |
(Pbl, mk_additem fd ct'))
|
neuper@38051
|
600 |
| NONE => (*pbl-items complete*)
|
neuper@38051
|
601 |
if not preok then (Pbl, Refine_Problem pI')
|
neuper@38051
|
602 |
else
|
neuper@38051
|
603 |
if dI = e_domID then (Pbl, Specify_Theory dI')
|
neuper@38051
|
604 |
else if pI = e_pblID then (Pbl, Specify_Problem pI')
|
neuper@38051
|
605 |
else if mI = e_metID then (Pbl, Specify_Method mI')
|
neuper@38051
|
606 |
else
|
neuper@38051
|
607 |
case find_first (is_error o #5) met of
|
neuper@37926
|
608 |
SOME (_,_,_,fd,itm_) =>
|
neuper@38051
|
609 |
(Met, mk_delete (assoc_thy dI) fd itm_)
|
neuper@37926
|
610 |
| NONE =>
|
neuper@38051
|
611 |
(case nxt_add (assoc_thy dI) oris mpc met of
|
neuper@38051
|
612 |
SOME (fd,ct') => (*30.8.01: pre?!?*)
|
neuper@38051
|
613 |
(Met, mk_additem fd ct')
|
neuper@38051
|
614 |
| NONE =>
|
neuper@38051
|
615 |
((*Solv 3.4.00*)Met, Apply_Method mI))))
|
neuper@38051
|
616 |
|
neuper@37906
|
617 |
| nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
|
neuper@38015
|
618 |
((*tracing"### nxt_spec Met"; *)
|
neuper@37906
|
619 |
case find_first (is_error o #5) met of
|
neuper@37926
|
620 |
SOME (_,_,_,fd,itm_) =>
|
neuper@37906
|
621 |
(Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
|
neuper@37926
|
622 |
| NONE =>
|
neuper@37906
|
623 |
case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
|
neuper@37926
|
624 |
SOME (fd,ct') => (Met, mk_additem fd ct')
|
neuper@37926
|
625 |
| NONE =>
|
neuper@38015
|
626 |
((*tracing"### nxt_spec Met: nxt_add NONE";*)
|
neuper@37906
|
627 |
if dI = e_domID then (Met, Specify_Theory dI')
|
neuper@37906
|
628 |
else if pI = e_pblID then (Met, Specify_Problem pI')
|
neuper@37906
|
629 |
else if not preok then (Met, Specify_Method mI)
|
neuper@37906
|
630 |
else (Met, Apply_Method mI)));
|
neuper@37906
|
631 |
|
neuper@37906
|
632 |
(* di_ pI_ mI_ pos_
|
neuper@37906
|
633 |
val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
|
neuper@37906
|
634 |
(2,[2],true,"#Find",Syn("empty"))];
|
neuper@37906
|
635 |
*)
|
neuper@37906
|
636 |
|
neuper@37906
|
637 |
fun is_field_correct sel d dscpbt =
|
neuper@37906
|
638 |
case assoc (dscpbt, sel) of
|
neuper@37926
|
639 |
NONE => false
|
neuper@37934
|
640 |
| SOME ds => member op = ds d;
|
neuper@37906
|
641 |
|
neuper@37906
|
642 |
(*. update the itm_ already input, all..from ori .*)
|
neuper@37906
|
643 |
(* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
|
neuper@37906
|
644 |
*)
|
neuper@37906
|
645 |
fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
|
neuper@37906
|
646 |
let
|
neuper@37930
|
647 |
val ts' = union op = (ts_in itm_) ts;
|
neuper@37906
|
648 |
val pval = pbl_ids' thy d ts'
|
neuper@37906
|
649 |
(*WN.9.5.03: FIXXXME [#0, epsilon]
|
neuper@37906
|
650 |
here would upd_penv be called for [#0, epsilon] etc. *)
|
neuper@37934
|
651 |
val complete = if eq_set op = (ts', all) then true else false;
|
neuper@37906
|
652 |
in case itm_ of
|
neuper@37906
|
653 |
(Cor _) =>
|
neuper@37906
|
654 |
(if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
|
neuper@37906
|
655 |
else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
|
neuper@38031
|
656 |
| (Syn c) => error ("ori_2itm wants to overwrite "^c)
|
neuper@38031
|
657 |
| (Typ c) => error ("ori_2itm wants to overwrite "^c)
|
neuper@37906
|
658 |
| (Inc _) => if complete
|
neuper@37906
|
659 |
then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
|
neuper@37906
|
660 |
else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
|
neuper@37906
|
661 |
| (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
|
neuper@37906
|
662 |
(*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
|
neuper@37906
|
663 |
(*else (id,vt,complete,fd,Cor((d,ts'),e))*)
|
neuper@37906
|
664 |
(* 28.1.00: not completely clear ---^^^ etc.*)
|
neuper@37906
|
665 |
(* 4.9.01: Mis just copied---vvv *)
|
neuper@37906
|
666 |
| (Mis _) => if complete
|
neuper@37906
|
667 |
then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
|
neuper@37906
|
668 |
else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
|
neuper@37906
|
669 |
end;
|
neuper@37906
|
670 |
|
neuper@37906
|
671 |
|
neuper@37906
|
672 |
fun eq1 d (_,(d',_)) = (d = d');
|
neuper@37906
|
673 |
fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
|
neuper@37906
|
674 |
|
neuper@37906
|
675 |
|
neuper@37906
|
676 |
(* 'all' ts from ori; ts is the input; (ori carries rest of info)
|
neuper@37906
|
677 |
9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
|
neuper@37906
|
678 |
pval: value for problem-environment _NOT_ checked for 'inter' --
|
neuper@37906
|
679 |
-- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
|
neuper@37906
|
680 |
(as it has been done for input_icalhd+insert_ppc' in 11.03)*)
|
neuper@37906
|
681 |
(*. is_input ori itms <=>
|
neuper@37906
|
682 |
EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
|
neuper@37906
|
683 |
(2) ori(ts) subset itm(ts) --- Err "already input"
|
neuper@37906
|
684 |
(3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
|
neuper@37906
|
685 |
(4) -"- <> empty --- new: ori(ts) \\ inter .*)
|
neuper@37906
|
686 |
(* val(itms,(i,v,f,d,ts)) = (ppc,ori');
|
neuper@37906
|
687 |
*)
|
neuper@37906
|
688 |
fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
|
neuper@37906
|
689 |
case find_first (eq1 d) pbt of
|
neuper@37926
|
690 |
SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
|
neuper@37926
|
691 |
val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
|
neuper@37906
|
692 |
*)
|
neuper@37906
|
693 |
(case find_first (eq3 f d) itms of
|
neuper@37926
|
694 |
SOME (_,_,_,_,itm_) =>
|
neuper@37906
|
695 |
let
|
neuper@37934
|
696 |
val ts' = inter op = (ts_in itm_) ts;
|
neuper@37934
|
697 |
in if subset op = (ts, ts')
|
neuper@37906
|
698 |
then (((strs2str' o
|
neuper@38053
|
699 |
map (Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
700 |
(thy2ctxt thy)))) ts') ^
|
neuper@37906
|
701 |
" already input", e_itm) (*2*)
|
neuper@37934
|
702 |
else ("",
|
neuper@37934
|
703 |
ori_2itm thy itm_ pid all (i,v,f,d,
|
neuper@37934
|
704 |
subtract op = ts' ts)) (*3,4*)
|
neuper@37906
|
705 |
end
|
neuper@37926
|
706 |
| NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
|
neuper@37906
|
707 |
pid all (i,v,f,d,ts)) (*1*)
|
neuper@37906
|
708 |
)
|
neuper@37926
|
709 |
| NONE => ("", ori_2itm thy (Sup (d,ts))
|
neuper@37906
|
710 |
e_term all (i,v,f,d,ts));
|
neuper@37906
|
711 |
|
neuper@37906
|
712 |
fun test_types thy (d,ts) =
|
neuper@37906
|
713 |
let
|
neuper@41905
|
714 |
(*val s = !show_types; val _ = show_types:= true;*)
|
neuper@37906
|
715 |
val opt = (try (comp_dts thy)) (d,ts);
|
neuper@37906
|
716 |
val msg = case opt of
|
neuper@37926
|
717 |
SOME _ => ""
|
neuper@38053
|
718 |
| NONE => ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d) ^
|
neuper@38053
|
719 |
" " ^
|
neuper@38053
|
720 |
((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
721 |
(thy2ctxt thy)))) ts)
|
neuper@37934
|
722 |
^ " is illtyped");
|
neuper@41905
|
723 |
(*val _ = show_types:= s*)
|
neuper@37906
|
724 |
in msg end;
|
neuper@37906
|
725 |
|
neuper@37906
|
726 |
|
neuper@37906
|
727 |
|
neuper@38031
|
728 |
fun maxl [] = error "maxl of []"
|
neuper@37906
|
729 |
| maxl (y::ys) =
|
neuper@37906
|
730 |
let fun mx x [] = x
|
neuper@37906
|
731 |
| mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
|
neuper@37906
|
732 |
in mx y ys end;
|
neuper@37906
|
733 |
|
neuper@37906
|
734 |
|
neuper@37906
|
735 |
(*. is the input term t known in oris ?
|
neuper@37906
|
736 |
give feedback on all(?) strange input;
|
neuper@37906
|
737 |
return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
|
neuper@37906
|
738 |
(*WN.11.03: from lists*)
|
neuper@37906
|
739 |
fun is_known thy sel ori t =
|
neuper@37906
|
740 |
(* val (ori,t)=(oris,term_of ct);
|
neuper@37906
|
741 |
*)
|
neuper@37906
|
742 |
let
|
neuper@41933
|
743 |
val _ = tracing ("RM is_known: t=" ^ term2str t);
|
neuper@37906
|
744 |
val ots = (distinct o flat o (map #5)) (ori:ori list);
|
neuper@37906
|
745 |
val oids = ((map (fst o dest_Free)) o distinct o
|
neuper@37906
|
746 |
flat o (map vars)) ots;
|
neuper@37906
|
747 |
val (d,ts(*,pval*)) = split_dts thy t;
|
neuper@37906
|
748 |
val ids = map (fst o dest_Free)
|
neuper@37906
|
749 |
((distinct o (flat o (map vars))) ts);
|
neuper@37934
|
750 |
in if (subtract op = oids ids) <> []
|
neuper@37934
|
751 |
then (("identifiers "^(strs2str' (subtract op = oids ids))^
|
neuper@37906
|
752 |
" not in example"), e_ori_, [])
|
neuper@37906
|
753 |
else
|
neuper@37906
|
754 |
if d = e_term
|
neuper@37906
|
755 |
then
|
neuper@37934
|
756 |
if not (subset op = (map typeless ts, map typeless ots))
|
neuper@37906
|
757 |
then (("terms '"^
|
neuper@38053
|
758 |
((strs2str' o
|
neuper@38053
|
759 |
(map (Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
760 |
(thy2ctxt thy))))) ts)^
|
neuper@37906
|
761 |
"' not in example (typeless)"), e_ori_, [])
|
neuper@37906
|
762 |
else (case seek_orits thy sel ts ori of
|
neuper@37906
|
763 |
("", ori_ as (_,_,_,d,ts), all) =>
|
neuper@37906
|
764 |
(case test_types thy (d,ts) of
|
neuper@37906
|
765 |
"" => ("", ori_, all)
|
neuper@37906
|
766 |
| msg => (msg, e_ori_, []))
|
neuper@37906
|
767 |
| (msg,_,_) => (msg, e_ori_, []))
|
neuper@37906
|
768 |
else
|
neuper@37934
|
769 |
if member op = (map #4 ori) d
|
neuper@37906
|
770 |
then seek_oridts thy sel (d,ts) ori
|
neuper@38053
|
771 |
else ((Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
772 |
(thy2ctxt thy)) d) ^
|
neuper@38053
|
773 |
" not in example", (0, [], sel, d, ts), [])
|
neuper@37906
|
774 |
end;
|
neuper@37906
|
775 |
|
neuper@37906
|
776 |
|
neuper@37906
|
777 |
(*. for return-value of appl_add .*)
|
neuper@37906
|
778 |
datatype additm =
|
neuper@37906
|
779 |
Add of itm
|
neuper@37906
|
780 |
| Err of string; (*error-message*)
|
neuper@37906
|
781 |
|
neuper@37906
|
782 |
|
neuper@38051
|
783 |
(** add an item to the model; check wrt. oris and pbt **)
|
neuper@37906
|
784 |
(* in contrary to oris<>[] below, this part handles user-input
|
neuper@37906
|
785 |
extremely acceptive, i.e. accept input instead error-msg *)
|
neuper@37906
|
786 |
fun appl_add thy sel ([]:ori list) ppc pbt ct' =
|
neuper@37906
|
787 |
(* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
|
neuper@37906
|
788 |
!!!! 28.8.01: env tested _minimally_ !!!
|
neuper@37906
|
789 |
*)
|
neuper@37906
|
790 |
let
|
neuper@37906
|
791 |
val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
|
neuper@37906
|
792 |
in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
|
neuper@37926
|
793 |
NONE => Add (i,[],false,sel,Syn ct')
|
neuper@37926
|
794 |
(* val (SOME ct) = parse thy ct';
|
neuper@37906
|
795 |
*)
|
neuper@37926
|
796 |
| SOME ct =>
|
neuper@37906
|
797 |
let
|
neuper@37906
|
798 |
val (d,ts(*,pval*)) = split_dts thy (term_of ct);
|
neuper@37906
|
799 |
in if d = e_term
|
neuper@37906
|
800 |
then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
|
neuper@37906
|
801 |
|
neuper@37906
|
802 |
else
|
neuper@37906
|
803 |
(case find_first (eq1 d) pbt of
|
neuper@37926
|
804 |
NONE => Add (i,[],true,sel,Sup ((d,ts)))
|
neuper@37926
|
805 |
| SOME (f,(_,id)) =>
|
neuper@37926
|
806 |
(* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
|
neuper@37906
|
807 |
*)
|
neuper@37906
|
808 |
let
|
neuper@37906
|
809 |
fun eq2 d ((i,_,_,_,itm_):itm) =
|
neuper@37906
|
810 |
(d = (d_in itm_)) andalso i<>0;
|
neuper@37906
|
811 |
in case find_first (eq2 d) ppc of
|
neuper@37926
|
812 |
NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
|
neuper@37906
|
813 |
pbl_ids' thy d ts)))
|
neuper@37926
|
814 |
| SOME (i',_,_,_,itm_) =>
|
neuper@37926
|
815 |
(* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
|
neuper@37926
|
816 |
val NONE = find_first (eq2 d) ppc;
|
neuper@37906
|
817 |
*)
|
neuper@37906
|
818 |
if is_list_dsc d
|
neuper@37930
|
819 |
then let val ts = union op = ts (ts_in itm_)
|
neuper@37906
|
820 |
in Add (if ts_in itm_ = [] then i else i',
|
neuper@37906
|
821 |
[],true,f,Cor ((d, ts), (id, (*pval*)
|
neuper@37906
|
822 |
pbl_ids' thy d ts)))
|
neuper@37906
|
823 |
end
|
neuper@37906
|
824 |
else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
|
neuper@37906
|
825 |
pbl_ids' thy d ts)))
|
neuper@37906
|
826 |
end
|
neuper@37906
|
827 |
)
|
neuper@37906
|
828 |
end
|
neuper@37906
|
829 |
end
|
neuper@38051
|
830 |
(* add ct to ppc *)
|
neuper@37906
|
831 |
(*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
|
neuper@38051
|
832 |
| appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
|
neuper@38051
|
833 |
case parse thy str of
|
neuper@38051
|
834 |
NONE => Err ("syntax error in " ^ str)
|
neuper@38051
|
835 |
| SOME t => case is_known thy sel oris (term_of t) of
|
neuper@38051
|
836 |
("", ori', all) =>
|
neuper@38051
|
837 |
(case is_notyet_input thy ppc all ori' pbt of
|
neuper@38051
|
838 |
("", itm) => Add itm
|
neuper@38051
|
839 |
| (msg, _) => Err msg)
|
neuper@38051
|
840 |
| (msg, _, _) => Err msg;
|
neuper@37906
|
841 |
(*
|
neuper@37906
|
842 |
> val (msg,itm) = is_notyet_input thy ppc all ori';
|
neuper@37906
|
843 |
val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
|
neuper@37906
|
844 |
> val itm_ = #5 itm;
|
neuper@37906
|
845 |
> val ts = ts_in itm_;
|
neuper@37906
|
846 |
> map (atomty) ts;
|
neuper@37906
|
847 |
*)
|
neuper@37906
|
848 |
|
neuper@37906
|
849 |
(** make oris from args of the stac SubProblem and from pbt **)
|
neuper@37906
|
850 |
|
neuper@37906
|
851 |
(*.can this formal argument (of a model-pattern) be omitted in the arg-list
|
neuper@37906
|
852 |
of a SubProblem ? see ME/ptyps.sml 'type met '.*)
|
neuper@37906
|
853 |
fun is_copy_named_idstr str =
|
neuper@40836
|
854 |
case (rev o Symbol.explode) str of
|
neuper@40836
|
855 |
"'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
|
neuper@38011
|
856 |
"is_copy_named_idstr: " ^ str ^ " T"); true)
|
neuper@40836
|
857 |
| _ => (tracing ((strs2str o (rev o Symbol.explode))
|
neuper@38011
|
858 |
"is_copy_named_idstr: " ^ str ^ " F"); false);
|
neuper@38010
|
859 |
fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
|
neuper@38010
|
860 |
|
neuper@37906
|
861 |
(*.should this formal argument (of a model-pattern) create a new identifier?.*)
|
neuper@37906
|
862 |
fun is_copy_named_generating_idstr str =
|
neuper@37906
|
863 |
if is_copy_named_idstr str
|
neuper@40836
|
864 |
then case (rev o Symbol.explode) str of
|
neuper@38010
|
865 |
"'"::"'"::"'"::_ => false
|
neuper@37906
|
866 |
| _ => true
|
neuper@37906
|
867 |
else false;
|
neuper@38010
|
868 |
fun is_copy_named_generating (_, (_, t)) =
|
neuper@37906
|
869 |
(is_copy_named_generating_idstr o free2str) t;
|
neuper@37906
|
870 |
|
neuper@37906
|
871 |
(*.split type-wrapper from scr-arg and build part of an ori;
|
neuper@37906
|
872 |
an type-error is reported immediately, raises an exn,
|
neuper@37906
|
873 |
subsequent handling of exn provides 2nd part of error message.*)
|
neuper@37934
|
874 |
fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
|
neuper@37934
|
875 |
(* val (thy, (str, (dsc, _)), (ty $ var)) =
|
neuper@37934
|
876 |
(thy, p, a);
|
neuper@37934
|
877 |
*)
|
neuper@37938
|
878 |
(cterm_of thy (dsc $ var);(*type check*)
|
neuper@37934
|
879 |
SOME ((([1], str, dsc, (*[var]*)
|
neuper@37934
|
880 |
split_dts' (dsc, var))): preori)(*:ori without leading #*))
|
neuper@38011
|
881 |
handle e as TYPE _ =>
|
neuper@38015
|
882 |
(tracing (dashs 70 ^ "\n"
|
neuper@38011
|
883 |
^"*** ERROR while creating the items for the model of the ->problem\n"
|
neuper@38011
|
884 |
^"*** from the ->stac with ->typeconstructor in arglist:\n"
|
neuper@38011
|
885 |
^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
|
neuper@38011
|
886 |
^"*** description: "^(term_detail2str dsc)
|
neuper@38011
|
887 |
^"*** value: "^(term_detail2str var)
|
neuper@38011
|
888 |
^"*** typeconstructor in script: "^(term_detail2str ty)
|
neuper@38011
|
889 |
^"*** checked by theory: "^(theory2str thy)^"\n"
|
neuper@38011
|
890 |
^"*** " ^ dots 66);
|
neuper@41905
|
891 |
(*OldGoals.print_exn e; raises exn again*)
|
neuper@41905
|
892 |
writeln (PolyML.makestring e);
|
neuper@41905
|
893 |
reraise e;
|
neuper@38011
|
894 |
(*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
|
neuper@38011
|
895 |
NONE);
|
neuper@37906
|
896 |
|
neuper@37906
|
897 |
(*.match each pat of the model-pattern with an actual argument;
|
neuper@37906
|
898 |
precondition: copy-named vars are filtered out.*)
|
neuper@37906
|
899 |
fun matc thy ([]:pat list) _ (oris:preori list) = oris
|
neuper@37906
|
900 |
| matc thy pbt [] _ =
|
neuper@38015
|
901 |
(tracing (dashs 70);
|
neuper@38031
|
902 |
error ("actual arg(s) missing for '"^pats2str pbt
|
neuper@37906
|
903 |
^"' i.e. should be 'copy-named' by '*_._'"))
|
neuper@37906
|
904 |
| matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
|
neuper@37906
|
905 |
(* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
|
neuper@37906
|
906 |
(thy, pbt', ags, []);
|
neuper@37906
|
907 |
(*recursion..*)
|
neuper@37906
|
908 |
val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
|
neuper@37906
|
909 |
(thy, pbt, ags, (oris @ [ori]));
|
neuper@37906
|
910 |
*)
|
neuper@37906
|
911 |
(*del?..*)if (is_copy_named_idstr o free2str) t then oris
|
neuper@37906
|
912 |
else(*..del?*) let val opt = mtc thy p a;
|
neuper@37906
|
913 |
in case opt of
|
neuper@37926
|
914 |
(* val SOME ori = mtc thy p a;
|
neuper@37906
|
915 |
*)
|
neuper@37926
|
916 |
SOME ori => matc thy pbt ags (oris @ [ori])
|
neuper@37926
|
917 |
| NONE => [](*WN050903 skipped by exn handled in match_ags*)
|
neuper@37906
|
918 |
end;
|
neuper@37906
|
919 |
(* run subp-rooteq.sml until Init_Proof before ...
|
neuper@37906
|
920 |
> val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
|
neuper@37906
|
921 |
> fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
|
neuper@37906
|
922 |
|
neuper@37906
|
923 |
other vars as in mtc ..
|
neuper@37906
|
924 |
> matc thy (drop_last pbt) ags [];
|
neuper@37906
|
925 |
val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
|
neuper@37906
|
926 |
|
neuper@37906
|
927 |
|
neuper@38011
|
928 |
(* generate a new variable "x_i" name from a related given one "x"
|
neuper@38011
|
929 |
by use of oris relating "v_i_" (is_copy_named!) to "v_"
|
neuper@38011
|
930 |
e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
|
neuper@38011
|
931 |
|
neuper@38011
|
932 |
(* generate a new variable "x_i" name from a related given one "x"
|
neuper@38011
|
933 |
by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
|
neuper@38012
|
934 |
e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
|
neuper@38012
|
935 |
but leave is_copy_named_generating as is, e.t. ss''' *)
|
neuper@37906
|
936 |
fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
|
neuper@37906
|
937 |
(if is_copy_named_generating p
|
neuper@37906
|
938 |
then (*WN051014 kept strange old code ...*)
|
neuper@37906
|
939 |
let fun sel (_,_,d,ts) = comp_ts (d, ts)
|
neuper@40836
|
940 |
val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
|
neuper@40836
|
941 |
val ext = (last_elem o drop_last o Symbol.explode o free2str) t
|
neuper@38011
|
942 |
val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
|
neuper@37906
|
943 |
val vals = map sel oris
|
neuper@37906
|
944 |
val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
|
neuper@37906
|
945 |
in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
|
neuper@37906
|
946 |
else ([1], field, dsc, [t])
|
neuper@37906
|
947 |
)
|
neuper@38031
|
948 |
handle _ => error ("cpy_nam: for "^(term2str t));
|
neuper@37906
|
949 |
|
neuper@37906
|
950 |
(*.match the actual arguments of a SubProblem with a model-pattern
|
neuper@37906
|
951 |
and create an ori list (in root-pbl created from formalization).
|
neuper@37906
|
952 |
expects ags:pats = 1:1, while copy-named are filtered out of pats;
|
neuper@38011
|
953 |
if no 1:1 the exn raised by matc/mtc and handled at call.
|
neuper@37906
|
954 |
copy-named pats are appended in order to get them into the model-items.*)
|
neuper@37906
|
955 |
fun match_ags thy (pbt:pat list) ags =
|
neuper@37906
|
956 |
let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
|
neuper@37906
|
957 |
val pbt' = filter_out is_copy_named pbt;
|
neuper@37906
|
958 |
val cy = filter is_copy_named pbt;
|
neuper@37906
|
959 |
val oris' = matc thy pbt' ags [];
|
neuper@37906
|
960 |
val cy' = map (cpy_nam pbt' oris') cy;
|
neuper@37906
|
961 |
val ors = add_id (oris' @ cy');
|
neuper@38011
|
962 |
(*appended in order to get ^^^^^ into the model-items*)
|
neuper@37906
|
963 |
in (map flattup ors):ori list end;
|
neuper@37906
|
964 |
|
neuper@37906
|
965 |
(*.report part of the error-msg which is not available in match_args.*)
|
neuper@37906
|
966 |
fun match_ags_msg pI stac ags =
|
neuper@41905
|
967 |
let (*val s = !show_types
|
neuper@41905
|
968 |
val _ = show_types:= true*)
|
neuper@37906
|
969 |
val pats = (#ppc o get_pbt) pI
|
neuper@37906
|
970 |
val msg = (dots 70^"\n"
|
neuper@37906
|
971 |
^"*** problem "^strs2str pI^" has the ...\n"
|
neuper@37906
|
972 |
^"*** model-pattern "^pats2str pats^"\n"
|
neuper@37906
|
973 |
^"*** stac '"^term2str stac^"' has the ...\n"
|
neuper@37906
|
974 |
^"*** arg-list "^terms2str ags^"\n"
|
neuper@37906
|
975 |
^dashs 70)
|
neuper@38011
|
976 |
(*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
|
neuper@41905
|
977 |
(*val _ = show_types:= s*)
|
neuper@38015
|
978 |
in tracing msg end;
|
neuper@37906
|
979 |
|
neuper@37906
|
980 |
|
neuper@37906
|
981 |
(*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
|
neuper@37906
|
982 |
fun vars_of_pbl_ pbl_ =
|
neuper@37906
|
983 |
let fun var_of_pbl_ (gfr,(dsc,t)) = t
|
neuper@37906
|
984 |
in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
|
neuper@37906
|
985 |
fun vars_of_pbl_' pbl_ =
|
neuper@37906
|
986 |
let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
|
neuper@37906
|
987 |
in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
|
neuper@37906
|
988 |
|
neuper@37906
|
989 |
fun overwrite_ppc thy itm ppc =
|
neuper@37906
|
990 |
let
|
neuper@37906
|
991 |
fun repl ppc' (_,_,_,_,itm_) [] =
|
neuper@38031
|
992 |
error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
|
neuper@37934
|
993 |
" not found")
|
neuper@37906
|
994 |
| repl ppc' itm (p::ppc) =
|
neuper@37906
|
995 |
if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
|
neuper@37906
|
996 |
else repl (ppc' @ [p]) itm ppc
|
neuper@37906
|
997 |
in repl [] itm ppc end;
|
neuper@37906
|
998 |
|
neuper@37906
|
999 |
(*10.3.00: insert the already compiled itm into model;
|
neuper@37906
|
1000 |
ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
|
neuper@37906
|
1001 |
(* val ppc=pbl;
|
neuper@37906
|
1002 |
*)
|
neuper@37906
|
1003 |
fun insert_ppc thy itm ppc =
|
neuper@37906
|
1004 |
let
|
neuper@37906
|
1005 |
fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
|
neuper@37906
|
1006 |
| eq_untouched _ _ = false;
|
neuper@37906
|
1007 |
val ppc' =
|
neuper@37906
|
1008 |
(
|
neuper@38015
|
1009 |
(*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
|
neuper@37906
|
1010 |
case seek_ppc (#1 itm) ppc of
|
neuper@37926
|
1011 |
(* val SOME xxx = seek_ppc (#1 itm) ppc;
|
neuper@37906
|
1012 |
*)
|
neuper@37926
|
1013 |
SOME _ => (*itm updated in is_notyet_input WN.11.03*)
|
neuper@37906
|
1014 |
overwrite_ppc thy itm ppc
|
neuper@37926
|
1015 |
| NONE => (ppc @ [itm]));
|
neuper@37906
|
1016 |
in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
|
neuper@37906
|
1017 |
|
neuper@37906
|
1018 |
(*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
|
neuper@37906
|
1019 |
fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
|
neuper@37906
|
1020 |
|
neuper@37906
|
1021 |
fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
|
neuper@37906
|
1022 |
(d_in itm_) = (d_in iitm_);
|
neuper@37906
|
1023 |
(*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
|
neuper@37906
|
1024 |
handles superfluous items carelessly*)
|
neuper@37906
|
1025 |
fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
|
neuper@37906
|
1026 |
(* val eee = op=;
|
neuper@37906
|
1027 |
> gen_ins' eee (4,[1,3,5,7]);
|
neuper@37906
|
1028 |
val it = [1, 3, 5, 7, 4] : int list*)
|
neuper@37906
|
1029 |
|
neuper@37906
|
1030 |
|
neuper@37906
|
1031 |
(*. output the headline to a ppc .*)
|
neuper@37906
|
1032 |
fun header p_ pI mI =
|
neuper@37906
|
1033 |
case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
|
neuper@37906
|
1034 |
| Met => Method mI
|
neuper@38031
|
1035 |
| pos => error ("header called with "^ pos_2str pos);
|
neuper@37906
|
1036 |
|
neuper@37906
|
1037 |
|
neuper@37906
|
1038 |
fun specify_additem sel (ct,_) (p,Met) c pt =
|
neuper@37906
|
1039 |
let
|
neuper@37906
|
1040 |
val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
|
neuper@37906
|
1041 |
probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
|
neuper@37906
|
1042 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
|
neuper@37906
|
1043 |
(*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
|
neuper@37906
|
1044 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@37906
|
1045 |
val cmI = if mI = e_metID then mI' else mI;
|
neuper@37906
|
1046 |
val {ppc,pre,prls,...} = get_met cmI
|
neuper@37906
|
1047 |
in case appl_add thy sel oris met ppc ct of
|
neuper@37906
|
1048 |
Add itm (*..union old input *) =>
|
neuper@37906
|
1049 |
let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
|
neuper@37906
|
1050 |
*)
|
neuper@37906
|
1051 |
val met' = insert_ppc thy itm met;
|
neuper@37906
|
1052 |
(*val pt' = update_met pt p met';*)
|
neuper@37906
|
1053 |
val ((p,Met),_,_,pt') =
|
neuper@37906
|
1054 |
generate1 thy (case sel of
|
neuper@37906
|
1055 |
"#Given" => Add_Given' (ct, met')
|
neuper@37906
|
1056 |
| "#Find" => Add_Find' (ct, met')
|
neuper@37906
|
1057 |
| "#Relate"=> Add_Relation'(ct, met'))
|
neuper@37906
|
1058 |
Uistate (p,Met) pt
|
neuper@37906
|
1059 |
val pre' = check_preconds thy prls pre met'
|
neuper@37906
|
1060 |
val pb = foldl and_ (true, map fst pre')
|
neuper@38015
|
1061 |
(*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
|
neuper@37906
|
1062 |
val (p_,nxt) =
|
neuper@37906
|
1063 |
nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
|
neuper@37906
|
1064 |
((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
|
neuper@37906
|
1065 |
in ((p,p_), ((p,p_),Uistate),
|
neuper@37906
|
1066 |
Form' (PpcKF (0,EdUndef,(length p),Nundef,
|
neuper@37906
|
1067 |
(Method cmI, itms2itemppc thy met' pre'))),
|
neuper@37906
|
1068 |
nxt,Safe,pt') end
|
neuper@37906
|
1069 |
| Err msg =>
|
neuper@37906
|
1070 |
let val pre' = check_preconds thy prls pre met
|
neuper@37906
|
1071 |
val pb = foldl and_ (true, map fst pre')
|
neuper@38015
|
1072 |
(*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
|
neuper@37906
|
1073 |
val (p_,nxt) =
|
neuper@37906
|
1074 |
nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
|
neuper@37906
|
1075 |
((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
|
neuper@37906
|
1076 |
in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
|
neuper@37906
|
1077 |
end
|
neuper@37906
|
1078 |
(* val (p,_) = p;
|
neuper@37906
|
1079 |
*)
|
neuper@37906
|
1080 |
| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
|
neuper@37906
|
1081 |
let
|
neuper@37906
|
1082 |
val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
|
neuper@37906
|
1083 |
probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
|
neuper@37906
|
1084 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
|
neuper@37906
|
1085 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@37906
|
1086 |
val cmI = if mI = e_metID then mI' else mI;
|
neuper@37906
|
1087 |
val {ppc,where_,prls,...} = get_pbt cpI;
|
neuper@37906
|
1088 |
in case appl_add thy sel oris pbl ppc ct of
|
neuper@37906
|
1089 |
Add itm (*..union old input *) =>
|
neuper@37906
|
1090 |
(* val Add itm = appl_add thy sel oris pbl ppc ct;
|
neuper@37906
|
1091 |
*)
|
neuper@37906
|
1092 |
let
|
neuper@38015
|
1093 |
(*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
|
neuper@37906
|
1094 |
val pbl' = insert_ppc thy itm pbl
|
neuper@37906
|
1095 |
val ((p,Pbl),_,_,pt') =
|
neuper@37906
|
1096 |
generate1 thy (case sel of
|
neuper@37906
|
1097 |
"#Given" => Add_Given' (ct, pbl')
|
neuper@37906
|
1098 |
| "#Find" => Add_Find' (ct, pbl')
|
neuper@37906
|
1099 |
| "#Relate"=> Add_Relation'(ct, pbl'))
|
neuper@37906
|
1100 |
Uistate (p,Pbl) pt
|
neuper@37906
|
1101 |
val pre = check_preconds thy prls where_ pbl'
|
neuper@37906
|
1102 |
val pb = foldl and_ (true, map fst pre)
|
neuper@38015
|
1103 |
(*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
|
neuper@37906
|
1104 |
val (p_,nxt) =
|
neuper@37906
|
1105 |
nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
|
neuper@37906
|
1106 |
(ppc,(#ppc o get_met) cmI) (dI,pI,mI);
|
neuper@37906
|
1107 |
val ppc = if p_= Pbl then pbl' else met;
|
neuper@37906
|
1108 |
in ((p,p_), ((p,p_),Uistate),
|
neuper@37906
|
1109 |
Form' (PpcKF (0,EdUndef,(length p),Nundef,
|
neuper@37906
|
1110 |
(header p_ pI cmI,
|
neuper@37906
|
1111 |
itms2itemppc thy ppc pre))), nxt,Safe,pt') end
|
neuper@37906
|
1112 |
|
neuper@37906
|
1113 |
| Err msg =>
|
neuper@37906
|
1114 |
let val pre = check_preconds thy prls where_ pbl
|
neuper@37906
|
1115 |
val pb = foldl and_ (true, map fst pre)
|
neuper@38015
|
1116 |
(*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
|
neuper@37906
|
1117 |
val (p_,nxt) =
|
neuper@37906
|
1118 |
nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
|
neuper@37906
|
1119 |
(ppc,(#ppc o get_met) cmI) (dI,pI,mI);
|
neuper@37906
|
1120 |
in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
|
neuper@37906
|
1121 |
end;
|
neuper@37906
|
1122 |
(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
|
neuper@37906
|
1123 |
val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
|
neuper@37906
|
1124 |
*)
|
neuper@37906
|
1125 |
|
neuper@37906
|
1126 |
(* ori
|
neuper@37906
|
1127 |
val (msg,itm) = appl_add thy sel oris ppc ct;
|
neuper@37906
|
1128 |
val (Cor(d,ts)) = #5 itm;
|
neuper@37906
|
1129 |
map (atomty) ts;
|
neuper@37906
|
1130 |
|
neuper@37906
|
1131 |
pre
|
neuper@37906
|
1132 |
*)
|
neuper@37906
|
1133 |
|
neuper@37906
|
1134 |
|
neuper@37906
|
1135 |
(* val Init_Proof' (fmz,(dI',pI',mI')) = m;
|
neuper@37906
|
1136 |
specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
|
neuper@37906
|
1137 |
*)
|
neuper@37906
|
1138 |
fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
|
neuper@37906
|
1139 |
let (* either """"""""""""""" all empty or complete *)
|
neuper@37906
|
1140 |
val thy = assoc_thy dI';
|
neuper@37906
|
1141 |
val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
|
neuper@37906
|
1142 |
else prep_ori fmz thy ((#ppc o get_pbt) pI');
|
neuper@37906
|
1143 |
val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
|
neuper@37906
|
1144 |
(oris,(dI',pI',mI'),e_term);
|
neuper@37906
|
1145 |
val {ppc,prls,where_,...} = get_pbt pI'
|
neuper@37906
|
1146 |
(*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
|
neuper@37906
|
1147 |
val pt = update_pbl pt [] pbl;
|
neuper@37906
|
1148 |
val pre = check_preconds thy prls where_ pbl
|
neuper@37906
|
1149 |
val pb = foldl and_ (true, map fst pre)*)
|
neuper@37906
|
1150 |
val (pbl, pre, pb) = ([], [], false)
|
neuper@37906
|
1151 |
in case mI' of
|
neuper@37906
|
1152 |
["no_met"] =>
|
neuper@37906
|
1153 |
(([],Pbl), (([],Pbl),Uistate),
|
neuper@37906
|
1154 |
Form' (PpcKF (0,EdUndef,(length []),Nundef,
|
neuper@37906
|
1155 |
(Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
|
neuper@37906
|
1156 |
Refine_Tacitly pI', Safe,pt)
|
neuper@37906
|
1157 |
| _ =>
|
neuper@37906
|
1158 |
(([],Pbl), (([],Pbl),Uistate),
|
neuper@37906
|
1159 |
Form' (PpcKF (0,EdUndef,(length []),Nundef,
|
neuper@37906
|
1160 |
(Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
|
neuper@37906
|
1161 |
Model_Problem,
|
neuper@37906
|
1162 |
Safe,pt)
|
neuper@37906
|
1163 |
end
|
neuper@37906
|
1164 |
(*ONLY for STARTING modeling phase*)
|
neuper@37906
|
1165 |
| specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
|
neuper@37906
|
1166 |
let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
|
neuper@37906
|
1167 |
*)
|
neuper@37906
|
1168 |
val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
|
neuper@37906
|
1169 |
get_obj I pt p
|
neuper@37906
|
1170 |
val thy' = if dI = e_domID then dI' else dI
|
neuper@37906
|
1171 |
val thy = assoc_thy thy'
|
neuper@37906
|
1172 |
val {ppc,prls,where_,...} = get_pbt pI'
|
neuper@37906
|
1173 |
val pre = check_preconds thy prls where_ pbl
|
neuper@37906
|
1174 |
val pb = foldl and_ (true, map fst pre)
|
neuper@37906
|
1175 |
val ((p,_),_,_,pt) =
|
neuper@37906
|
1176 |
generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
|
neuper@37906
|
1177 |
val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
|
neuper@37906
|
1178 |
(ppc,(#ppc o get_met) mI') (dI',pI',mI');
|
neuper@37906
|
1179 |
in ((p,Pbl), ((p,p_),Uistate),
|
neuper@37906
|
1180 |
Form' (PpcKF (0,EdUndef,(length p),Nundef,
|
neuper@37906
|
1181 |
(Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
|
neuper@37906
|
1182 |
nxt, Safe, pt) end
|
neuper@37906
|
1183 |
|
neuper@37906
|
1184 |
(*. called only if no_met is specified .*)
|
neuper@37906
|
1185 |
| specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
|
neuper@37906
|
1186 |
let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
|
neuper@37906
|
1187 |
*)
|
neuper@37906
|
1188 |
val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
|
neuper@37906
|
1189 |
get_obj I pt p;
|
neuper@37906
|
1190 |
val {prls,met,ppc,thy,where_,...} = get_pbt pIre
|
neuper@37906
|
1191 |
(*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
|
neuper@37906
|
1192 |
(*val pt = update_pbl pt p pbl;
|
neuper@37906
|
1193 |
val pt = update_orispec pt p
|
neuper@37906
|
1194 |
(string_of_thy thy, pIre,
|
neuper@37906
|
1195 |
if length met = 0 then e_metID else hd met);*)
|
neuper@37906
|
1196 |
val (domID, metID) = (string_of_thy thy,
|
neuper@37906
|
1197 |
if length met = 0 then e_metID else hd met)
|
neuper@37906
|
1198 |
val ((p,_),_,_,pt) =
|
neuper@37906
|
1199 |
generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
|
neuper@37906
|
1200 |
Uistate pos pt
|
neuper@37906
|
1201 |
(*val pre = check_preconds thy prls where_ pbl
|
neuper@37906
|
1202 |
val pb = foldl and_ (true, map fst pre)*)
|
neuper@37906
|
1203 |
val (pbl, pre, pb) = ([], [], false)
|
neuper@37906
|
1204 |
in ((p,Pbl), (pos,Uistate),
|
neuper@37906
|
1205 |
Form' (PpcKF (0,EdUndef,(length p),Nundef,
|
neuper@37906
|
1206 |
(Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
|
neuper@37906
|
1207 |
Model_Problem, Safe, pt) end
|
neuper@37906
|
1208 |
|
neuper@37906
|
1209 |
| specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
|
neuper@38050
|
1210 |
let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
|
neuper@37906
|
1211 |
(Refine_Problem' rfd) Uistate pos pt
|
neuper@37906
|
1212 |
in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
|
neuper@37906
|
1213 |
Model_Problem, Safe, pt) end
|
neuper@37906
|
1214 |
|
neuper@37906
|
1215 |
(* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
|
neuper@37906
|
1216 |
val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
|
neuper@37906
|
1217 |
*)
|
neuper@37906
|
1218 |
| specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
|
neuper@37906
|
1219 |
let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
|
neuper@37906
|
1220 |
meth=met, ...}) = get_obj I pt p;
|
neuper@37906
|
1221 |
(*val pt = update_pbl pt p itms;
|
neuper@37906
|
1222 |
val pt = update_pblID pt p pI;*)
|
neuper@37934
|
1223 |
val thy = assoc_thy dI
|
neuper@37906
|
1224 |
val ((p,Pbl),_,_,pt)=
|
neuper@37906
|
1225 |
generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
|
neuper@37906
|
1226 |
val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
|
neuper@37906
|
1227 |
val mI'' = if mI=e_metID then mI' else mI;
|
neuper@38015
|
1228 |
(*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
|
neuper@37906
|
1229 |
val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
|
neuper@37906
|
1230 |
((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
|
neuper@37906
|
1231 |
in ((p,Pbl), (pos,Uistate),
|
neuper@37906
|
1232 |
Form' (PpcKF (0,EdUndef,(length p),Nundef,
|
neuper@37906
|
1233 |
(Problem pI, itms2itemppc dI'' itms pre))),
|
neuper@37906
|
1234 |
nxt, Safe, pt) end
|
neuper@37906
|
1235 |
(* val Specify_Method' mID = nxt; val (p,_) = p;
|
neuper@37906
|
1236 |
val Specify_Method' mID = m;
|
neuper@37906
|
1237 |
specify (Specify_Method' mID) (p,p_) c pt;
|
neuper@37906
|
1238 |
*)
|
neuper@37906
|
1239 |
| specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
|
neuper@37906
|
1240 |
let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
|
neuper@37906
|
1241 |
meth=met, ...}) = get_obj I pt p;
|
neuper@37906
|
1242 |
val {ppc,pre,prls,...} = get_met mID
|
neuper@37906
|
1243 |
val thy = assoc_thy dI
|
neuper@37906
|
1244 |
val oris = add_field' thy ppc oris;
|
neuper@37906
|
1245 |
(*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
|
neuper@37906
|
1246 |
val dI'' = if dI=e_domID then dI' else dI;
|
neuper@37906
|
1247 |
val pI'' = if pI = e_pblID then pI' else pI;
|
neuper@37906
|
1248 |
val met = if met=[] then pbl else met;
|
neuper@37906
|
1249 |
val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
|
neuper@37906
|
1250 |
(*val pt = update_met pt p itms;
|
neuper@37906
|
1251 |
val pt = update_metID pt p mID*)
|
neuper@37906
|
1252 |
val (pos,_,_,pt)=
|
neuper@37906
|
1253 |
generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
|
neuper@38015
|
1254 |
(*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
|
neuper@37906
|
1255 |
val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
|
neuper@37906
|
1256 |
((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
|
neuper@37906
|
1257 |
in (pos, (pos,Uistate),
|
neuper@37906
|
1258 |
Form' (PpcKF (0,EdUndef,(length p),Nundef,
|
neuper@37906
|
1259 |
(Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
|
neuper@37906
|
1260 |
nxt, Safe, pt) end
|
neuper@37906
|
1261 |
(* val Add_Find' ct = nxt; val sel = "#Find";
|
neuper@37906
|
1262 |
*)
|
neuper@37906
|
1263 |
| specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
|
neuper@37906
|
1264 |
| specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
|
neuper@37906
|
1265 |
| specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
|
neuper@37906
|
1266 |
(* val Specify_Theory' domID = m;
|
neuper@37906
|
1267 |
val (Specify_Theory' domID, (p,p_)) = (m, pos);
|
neuper@37906
|
1268 |
*)
|
neuper@37906
|
1269 |
| specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
|
neuper@37906
|
1270 |
let val p_ = case p_ of Met => Met | _ => Pbl
|
neuper@37906
|
1271 |
val thy = assoc_thy domID;
|
neuper@37906
|
1272 |
val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
|
neuper@37906
|
1273 |
probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
|
neuper@37906
|
1274 |
val mppc = case p_ of Met => met | _ => pbl;
|
neuper@37906
|
1275 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@37906
|
1276 |
val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
|
neuper@37906
|
1277 |
val cmI = if mI = e_metID then mI' else mI;
|
neuper@37906
|
1278 |
val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
|
neuper@37906
|
1279 |
val pre =
|
neuper@37906
|
1280 |
case p_ of
|
neuper@37906
|
1281 |
Met => (check_preconds thy mer mwh met)
|
neuper@37906
|
1282 |
| _ => (check_preconds thy per pwh pbl)
|
neuper@37906
|
1283 |
val pb = foldl and_ (true, map fst pre)
|
neuper@37906
|
1284 |
in if domID = dI
|
neuper@37906
|
1285 |
then let
|
neuper@38015
|
1286 |
(*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
|
neuper@37906
|
1287 |
val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
|
neuper@37906
|
1288 |
(pbl,met) (ppc,mpc) (dI,pI,mI);
|
neuper@37906
|
1289 |
in ((p,p_), (pos,Uistate),
|
neuper@37906
|
1290 |
Form'(PpcKF (0,EdUndef,(length p), Nundef,
|
neuper@37906
|
1291 |
(header p_ pI cmI, itms2itemppc thy mppc pre))),
|
neuper@37906
|
1292 |
nxt,Safe,pt) end
|
neuper@37906
|
1293 |
else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
|
neuper@37906
|
1294 |
let
|
neuper@37906
|
1295 |
(*val pt = update_domID pt p domID;11.8.03*)
|
neuper@37906
|
1296 |
val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
|
neuper@37906
|
1297 |
Uistate (p,p_) pt
|
neuper@38015
|
1298 |
(*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
|
neuper@37906
|
1299 |
val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
|
neuper@37906
|
1300 |
(ppc,mpc) (domID,pI,mI);
|
neuper@37906
|
1301 |
in ((p,p_), (pos,Uistate),
|
neuper@37906
|
1302 |
Form' (PpcKF (0, EdUndef, (length p),Nundef,
|
neuper@37906
|
1303 |
(header p_ pI cmI, itms2itemppc thy mppc pre))),
|
neuper@37906
|
1304 |
nxt, Safe,pt) end
|
neuper@37906
|
1305 |
end
|
neuper@37906
|
1306 |
(* itms2itemppc thy [](*mpc*) pre
|
neuper@37906
|
1307 |
*)
|
neuper@37906
|
1308 |
| specify m' _ _ _ =
|
neuper@38031
|
1309 |
error ("specify: not impl. for "^tac_2str m');
|
neuper@37906
|
1310 |
|
neuper@37906
|
1311 |
(* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
|
neuper@37906
|
1312 |
val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
|
neuper@37906
|
1313 |
*)
|
neuper@38051
|
1314 |
fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
|
neuper@37906
|
1315 |
let
|
neuper@37906
|
1316 |
val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
|
neuper@37906
|
1317 |
probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
|
neuper@37906
|
1318 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
|
neuper@37906
|
1319 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@37906
|
1320 |
in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
|
neuper@37906
|
1321 |
Add itm (*..union old input *) =>
|
neuper@37906
|
1322 |
(* val Add itm = appl_add thy sel oris pbl ppc ct;
|
neuper@37906
|
1323 |
*)
|
neuper@37906
|
1324 |
let
|
neuper@38015
|
1325 |
(*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
|
neuper@37906
|
1326 |
val pbl' = insert_ppc thy itm pbl
|
neuper@37906
|
1327 |
val (tac,tac_) =
|
neuper@37906
|
1328 |
case sel of
|
neuper@37906
|
1329 |
"#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
|
neuper@37906
|
1330 |
| "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
|
neuper@37906
|
1331 |
| "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
|
neuper@37906
|
1332 |
val ((p,Pbl),c,_,pt') =
|
neuper@37906
|
1333 |
generate1 thy tac_ Uistate (p,Pbl) pt
|
neuper@37906
|
1334 |
in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
|
neuper@37906
|
1335 |
|
neuper@37906
|
1336 |
| Err msg =>
|
neuper@37906
|
1337 |
(*TODO.WN03 pass error-msgs to the frontend..
|
neuper@37906
|
1338 |
FIXME ..and dont abuse a tactic for that purpose*)
|
neuper@37906
|
1339 |
([(Tac msg,
|
neuper@40836
|
1340 |
Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
|
neuper@37906
|
1341 |
(e_pos', e_istate))], [], ptp)
|
neuper@37906
|
1342 |
end
|
neuper@37906
|
1343 |
|
neuper@37906
|
1344 |
(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
|
neuper@37906
|
1345 |
val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
|
neuper@37906
|
1346 |
*)
|
neuper@37906
|
1347 |
| nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
|
neuper@37906
|
1348 |
let
|
neuper@37906
|
1349 |
val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
|
neuper@37906
|
1350 |
probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
|
neuper@37906
|
1351 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
|
neuper@37906
|
1352 |
val cmI = if mI = e_metID then mI' else mI;
|
neuper@37906
|
1353 |
in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
|
neuper@37906
|
1354 |
Add itm (*..union old input *) =>
|
neuper@37906
|
1355 |
let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
|
neuper@37906
|
1356 |
*)
|
neuper@37906
|
1357 |
val met' = insert_ppc thy itm met;
|
neuper@37906
|
1358 |
val (tac,tac_) =
|
neuper@37906
|
1359 |
case sel of
|
neuper@37906
|
1360 |
"#Given" => (Add_Given ct, Add_Given' (ct, met'))
|
neuper@37906
|
1361 |
| "#Find" => (Add_Find ct, Add_Find' (ct, met'))
|
neuper@37906
|
1362 |
| "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
|
neuper@37906
|
1363 |
val ((p,Met),c,_,pt') =
|
neuper@37906
|
1364 |
generate1 thy tac_ Uistate (p,Met) pt
|
neuper@37906
|
1365 |
in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
|
neuper@37906
|
1366 |
|
neuper@37906
|
1367 |
| Err msg => ([(*tacis*)], [], ptp)
|
neuper@37906
|
1368 |
(*nxt_me collects tacis until not hide; here just no progress*)
|
neuper@37906
|
1369 |
end;
|
neuper@37906
|
1370 |
|
neuper@37906
|
1371 |
(* ori
|
neuper@37906
|
1372 |
val (msg,itm) = appl_add thy sel oris ppc ct;
|
neuper@37906
|
1373 |
val (Cor(d,ts)) = #5 itm;
|
neuper@37906
|
1374 |
map (atomty) ts;
|
neuper@37906
|
1375 |
|
neuper@37906
|
1376 |
pre
|
neuper@37906
|
1377 |
*)
|
neuper@37906
|
1378 |
fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
|
neuper@37906
|
1379 |
(i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
|
neuper@38031
|
1380 |
handle _ => error ("ori2Coritm: dsc "^
|
neuper@37906
|
1381 |
term2str d^
|
neuper@37906
|
1382 |
"in ori, but not in pbt")
|
neuper@37906
|
1383 |
,ts))):itm;
|
neuper@37906
|
1384 |
fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
|
neuper@37906
|
1385 |
((i,v,true,f, Cor ((d,ts),((snd o snd o the o
|
neuper@37906
|
1386 |
(find_first (eq1 d))) pbt,ts))):itm)
|
neuper@37906
|
1387 |
handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
|
neuper@37906
|
1388 |
((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
|
neuper@37906
|
1389 |
|
neuper@37906
|
1390 |
|
neuper@37906
|
1391 |
(*filter out oris which have same description in itms*)
|
neuper@37906
|
1392 |
fun filter_outs oris [] = oris
|
neuper@37906
|
1393 |
| filter_outs oris (i::itms) =
|
neuper@37906
|
1394 |
let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
|
neuper@37906
|
1395 |
(#4:ori -> term)) oris;
|
neuper@37906
|
1396 |
in filter_outs ors itms end;
|
neuper@37906
|
1397 |
|
neuper@37934
|
1398 |
fun memI a b = member op = a b;
|
neuper@37906
|
1399 |
(*filter oris which are in pbt, too*)
|
neuper@37906
|
1400 |
fun filter_pbt oris pbt =
|
neuper@37906
|
1401 |
let val dscs = map (fst o snd) pbt
|
neuper@37906
|
1402 |
in filter ((memI dscs) o (#4: ori -> term)) oris end;
|
neuper@37906
|
1403 |
|
neuper@37906
|
1404 |
(*.combine itms from pbl + met and complete them wrt. pbt.*)
|
neuper@37906
|
1405 |
(*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
|
neuper@37936
|
1406 |
local infix mem;
|
neuper@37934
|
1407 |
fun x mem [] = false
|
neuper@37934
|
1408 |
| x mem (y :: ys) = x = y orelse x mem ys;
|
neuper@37934
|
1409 |
in
|
neuper@37906
|
1410 |
fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
|
neuper@37906
|
1411 |
(* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
|
neuper@37906
|
1412 |
*)
|
neuper@37906
|
1413 |
let val vat = max_vt pits;
|
neuper@37906
|
1414 |
val itms = pits @
|
neuper@37906
|
1415 |
(filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
|
neuper@37906
|
1416 |
val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
|
neuper@37906
|
1417 |
val os = filter_outs ors itms;
|
neuper@37906
|
1418 |
(*WN.12.03?: does _NOT_ add itms from met ?!*)
|
neuper@37934
|
1419 |
in itms @ (map (ori2Coritm met) os) end
|
neuper@37934
|
1420 |
end;
|
neuper@37906
|
1421 |
|
neuper@37906
|
1422 |
|
neuper@37906
|
1423 |
|
neuper@37906
|
1424 |
(*.complete model and guard of a calc-head .*)
|
neuper@37936
|
1425 |
local infix mem;
|
neuper@37934
|
1426 |
fun x mem [] = false
|
neuper@37934
|
1427 |
| x mem (y :: ys) = x = y orelse x mem ys;
|
neuper@37934
|
1428 |
in
|
neuper@37906
|
1429 |
fun complete_mod_ (oris, mpc, ppc, probl) =
|
neuper@37906
|
1430 |
let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
|
neuper@37906
|
1431 |
val vat = if probl = [] then 1 else max_vt probl
|
neuper@37906
|
1432 |
val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
|
neuper@37906
|
1433 |
val pors = filter_outs pors pits (*which are in pbl already*)
|
neuper@37906
|
1434 |
val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
|
neuper@37906
|
1435 |
|
neuper@37906
|
1436 |
val pits = pits @ (map (ori2Coritm ppc) pors)
|
neuper@37906
|
1437 |
val mits = complete_metitms oris pits [] mpc
|
neuper@37934
|
1438 |
in (pits, mits) end
|
neuper@37934
|
1439 |
end;
|
neuper@37906
|
1440 |
|
neuper@37906
|
1441 |
fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
|
neuper@37906
|
1442 |
(if dI = e_domID then odI else dI,
|
neuper@37906
|
1443 |
if pI = e_pblID then opI else pI,
|
neuper@37906
|
1444 |
if mI = e_metID then omI else mI):spec;
|
neuper@37906
|
1445 |
|
neuper@37906
|
1446 |
|
neuper@37906
|
1447 |
(*.find a next applicable tac (for calcstate) and update ptree
|
neuper@37906
|
1448 |
(for ev. finding several more tacs due to hide).*)
|
neuper@37906
|
1449 |
(*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
|
neuper@37906
|
1450 |
(*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
|
neuper@37906
|
1451 |
(*WN.24.10.03 fun nxt_solv = ...................................??*)
|
neuper@37906
|
1452 |
fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
|
neuper@37906
|
1453 |
let
|
neuper@38051
|
1454 |
val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
|
neuper@38051
|
1455 |
val (dI, pI, mI) = some_spec ospec spec
|
neuper@37934
|
1456 |
val thy = assoc_thy dI
|
neuper@38051
|
1457 |
val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
|
neuper@38051
|
1458 |
val {cas, ppc, ...} = get_pbt pI
|
neuper@38051
|
1459 |
val pbl = init_pbl ppc (* fill in descriptions *)
|
neuper@38051
|
1460 |
(*----------------if you think, this should be done by the Dialog
|
neuper@37906
|
1461 |
in the java front-end, search there for WN060225-modelProblem----*)
|
neuper@38051
|
1462 |
val (pbl, met) = case cas of NONE => (pbl, [])
|
neuper@37906
|
1463 |
| _ => complete_mod_ (oris, mpc, ppc, probl)
|
neuper@37906
|
1464 |
(*----------------------------------------------------------------*)
|
neuper@37906
|
1465 |
val tac_ = Model_Problem' (pI, pbl, met)
|
neuper@37906
|
1466 |
val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
|
neuper@37906
|
1467 |
in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
|
neuper@37906
|
1468 |
|
neuper@37906
|
1469 |
(* val Add_Find ct = tac;
|
neuper@37906
|
1470 |
*)
|
neuper@37906
|
1471 |
| nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
|
neuper@37906
|
1472 |
| nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
|
neuper@37906
|
1473 |
| nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
|
neuper@37906
|
1474 |
|
neuper@37906
|
1475 |
(*. called only if no_met is specified .*)
|
neuper@37906
|
1476 |
| nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
|
neuper@37906
|
1477 |
let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
|
neuper@37906
|
1478 |
val opt = refine_ori oris pI
|
neuper@37906
|
1479 |
in case opt of
|
neuper@37926
|
1480 |
SOME pI' =>
|
neuper@37906
|
1481 |
let val {met,ppc,...} = get_pbt pI'
|
neuper@37906
|
1482 |
val pbl = init_pbl ppc
|
neuper@37906
|
1483 |
(*val pt = update_pbl pt p pbl ..done by Model_Problem*)
|
neuper@37906
|
1484 |
val mI = if length met = 0 then e_metID else hd met
|
neuper@37934
|
1485 |
val thy = assoc_thy dI
|
neuper@37906
|
1486 |
val (pos,c,_,pt) =
|
neuper@37906
|
1487 |
generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
|
neuper@37906
|
1488 |
Uistate pos pt
|
neuper@37906
|
1489 |
in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
|
neuper@37906
|
1490 |
(pos, Uistate))], c, (pt,pos)) end
|
neuper@37926
|
1491 |
| NONE => ([], [], ptp)
|
neuper@37906
|
1492 |
end
|
neuper@37906
|
1493 |
|
neuper@37906
|
1494 |
| nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
|
neuper@37906
|
1495 |
let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
|
neuper@37906
|
1496 |
probl, ...}) = get_obj I pt p
|
neuper@37906
|
1497 |
val thy = if dI' = e_domID then dI else dI'
|
neuper@37906
|
1498 |
in case refine_pbl (assoc_thy thy) pI probl of
|
neuper@37926
|
1499 |
NONE => ([], [], ptp)
|
neuper@37926
|
1500 |
| SOME (rfd as (pI',_)) =>
|
neuper@37906
|
1501 |
let val (pos,c,_,pt) =
|
neuper@37906
|
1502 |
generate1 (assoc_thy thy)
|
neuper@37906
|
1503 |
(Refine_Problem' rfd) Uistate pos pt
|
neuper@37906
|
1504 |
in ([(Refine_Problem pI, Refine_Problem' rfd,
|
neuper@37906
|
1505 |
(pos, Uistate))], c, (pt,pos)) end
|
neuper@37906
|
1506 |
end
|
neuper@37906
|
1507 |
|
neuper@37906
|
1508 |
| nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
|
neuper@37906
|
1509 |
let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
|
neuper@37906
|
1510 |
probl, ...}) = get_obj I pt p;
|
neuper@37906
|
1511 |
val thy = assoc_thy (if dI' = e_domID then dI else dI');
|
neuper@37906
|
1512 |
val {ppc,where_,prls,...} = get_pbt pI
|
neuper@37906
|
1513 |
val pbl as (_,(itms,_)) =
|
neuper@37906
|
1514 |
if pI'=e_pblID andalso pI=e_pblID
|
neuper@37906
|
1515 |
then (false, (init_pbl ppc, []))
|
neuper@37906
|
1516 |
else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
|
neuper@37906
|
1517 |
(*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
|
neuper@37906
|
1518 |
val ((p,Pbl),c,_,pt)=
|
neuper@37906
|
1519 |
generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
|
neuper@37906
|
1520 |
in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
|
neuper@37906
|
1521 |
(pos,Uistate))], c, (pt,pos)) end
|
neuper@37906
|
1522 |
|
neuper@37906
|
1523 |
(*transfers oris (not required in pbl) to met-model for script-env
|
neuper@37906
|
1524 |
FIXME.WN.8.03: application of several mIDs to SAME model?*)
|
neuper@37906
|
1525 |
| nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
|
neuper@37906
|
1526 |
let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
|
neuper@37906
|
1527 |
meth=met, ...}) = get_obj I pt p;
|
neuper@37906
|
1528 |
val {ppc,pre,prls,...} = get_met mID
|
neuper@37906
|
1529 |
val thy = assoc_thy dI
|
neuper@37906
|
1530 |
val oris = add_field' thy ppc oris;
|
neuper@37906
|
1531 |
val dI'' = if dI=e_domID then dI' else dI;
|
neuper@37906
|
1532 |
val pI'' = if pI = e_pblID then pI' else pI;
|
neuper@37906
|
1533 |
val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
|
neuper@37906
|
1534 |
val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
|
neuper@37906
|
1535 |
val (pos,c,_,pt)=
|
neuper@37906
|
1536 |
generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
|
neuper@37906
|
1537 |
in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
|
neuper@37906
|
1538 |
(pos,Uistate))], c, (pt,pos)) end
|
neuper@37906
|
1539 |
|
neuper@37906
|
1540 |
| nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
|
neuper@37906
|
1541 |
let val (dI',_,_) = get_obj g_spec pt p
|
neuper@37906
|
1542 |
val (pos,c,_,pt) =
|
neuper@38050
|
1543 |
generate1 (assoc_thy "Isac") (Specify_Theory' dI)
|
neuper@37906
|
1544 |
Uistate pos pt
|
neuper@37906
|
1545 |
in (*FIXXXME: check if pbl can still be parsed*)
|
neuper@37906
|
1546 |
([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
|
neuper@37906
|
1547 |
(pt, pos)) end
|
neuper@37906
|
1548 |
|
neuper@37906
|
1549 |
| nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
|
neuper@37906
|
1550 |
let val (dI',_,_) = get_obj g_spec pt p
|
neuper@37906
|
1551 |
val (pos,c,_,pt) =
|
neuper@38050
|
1552 |
generate1 (assoc_thy "Isac") (Specify_Theory' dI)
|
neuper@37906
|
1553 |
Uistate pos pt
|
neuper@37906
|
1554 |
in (*FIXXXME: check if met can still be parsed*)
|
neuper@37906
|
1555 |
([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
|
neuper@37906
|
1556 |
(pt, pos)) end
|
neuper@37906
|
1557 |
|
neuper@37906
|
1558 |
| nxt_specif m' _ =
|
neuper@38031
|
1559 |
error ("nxt_specif: not impl. for "^tac2str m');
|
neuper@37906
|
1560 |
|
neuper@37906
|
1561 |
(*.get the values from oris; handle the term list w.r.t. penv.*)
|
neuper@37934
|
1562 |
|
neuper@37936
|
1563 |
local infix mem;
|
neuper@37934
|
1564 |
fun x mem [] = false
|
neuper@37934
|
1565 |
| x mem (y :: ys) = x = y orelse x mem ys;
|
neuper@37934
|
1566 |
in
|
neuper@37906
|
1567 |
fun vals_of_oris oris =
|
neuper@37906
|
1568 |
((map (mkval' o (#5:ori -> term list))) o
|
neuper@37934
|
1569 |
(filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
|
neuper@37934
|
1570 |
end;
|
neuper@37906
|
1571 |
|
neuper@37906
|
1572 |
|
neuper@37906
|
1573 |
|
neuper@38056
|
1574 |
(* create a calc-tree with oris via an cas.refined pbl *)
|
neuper@38056
|
1575 |
fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
|
neuper@38056
|
1576 |
if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
|
neuper@38056
|
1577 |
let val {cas, met, ppc, thy, ...} = get_pbt pI
|
neuper@37906
|
1578 |
val dI = if dI = "" then theory2theory' thy else dI
|
neuper@37906
|
1579 |
val thy = assoc_thy dI
|
neuper@37906
|
1580 |
val mI = if mI = [] then hd met else mI
|
neuper@37926
|
1581 |
val hdl = case cas of NONE => pblterm dI pI | SOME t => t
|
neuper@37906
|
1582 |
val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
|
neuper@37906
|
1583 |
([], (dI,pI,mI), hdl)
|
neuper@37906
|
1584 |
val pt = update_spec pt [] (dI,pI,mI)
|
neuper@37906
|
1585 |
val pits = init_pbl' ppc
|
neuper@37906
|
1586 |
val pt = update_pbl pt [] pits
|
neuper@38056
|
1587 |
in ((pt, ([] ,Pbl)), []) : calcstate end
|
neuper@38056
|
1588 |
else if mI <> [] then (* from met-browser *)
|
neuper@37906
|
1589 |
let val {ppc,...} = get_met mI
|
neuper@38050
|
1590 |
val dI = if dI = "" then "Isac" else dI
|
neuper@37906
|
1591 |
val thy = assoc_thy dI
|
neuper@37906
|
1592 |
val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
|
neuper@37906
|
1593 |
([], (dI,pI,mI), e_term(*FIXME met*))
|
neuper@37906
|
1594 |
val pt = update_spec pt [] (dI,pI,mI)
|
neuper@37906
|
1595 |
val mits = init_pbl' ppc
|
neuper@37906
|
1596 |
val pt = update_met pt [] mits
|
neuper@38056
|
1597 |
in ((pt, ([], Met)), []) : calcstate end
|
neuper@38056
|
1598 |
else (* new example, pepare for interactive modeling *)
|
neuper@37906
|
1599 |
let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
|
neuper@37906
|
1600 |
([], e_spec, e_term)
|
neuper@38056
|
1601 |
in ((pt,([],Pbl)), []) : calcstate end
|
neuper@38051
|
1602 |
| nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
|
neuper@38051
|
1603 |
let (* both """"""""""""""""""""""""" either empty or complete *)
|
neuper@37906
|
1604 |
val thy = assoc_thy dI
|
neuper@37906
|
1605 |
val (pI, pors, mI) =
|
neuper@37906
|
1606 |
if mI = ["no_met"]
|
neuper@37906
|
1607 |
then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
|
neuper@37906
|
1608 |
val pI' = refine_ori' pors pI;
|
neuper@38051
|
1609 |
in (pI', pors(*refinement over models with diff.precond only*),
|
neuper@37906
|
1610 |
(hd o #met o get_pbt) pI') end
|
neuper@37906
|
1611 |
else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
|
neuper@38051
|
1612 |
val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
|
neuper@37906
|
1613 |
val dI = theory2theory' (maxthy thy thy');
|
neuper@37906
|
1614 |
val hdl = case cas of
|
neuper@37926
|
1615 |
NONE => pblterm dI pI
|
neuper@37926
|
1616 |
| SOME t => subst_atomic ((vars_of_pbl_' ppc)
|
neuper@37906
|
1617 |
~~~ vals_of_oris pors) t
|
neuper@38051
|
1618 |
val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
|
neuper@38056
|
1619 |
(pors, (dI, pI, mI), hdl)
|
neuper@38056
|
1620 |
in ((pt, ([], Pbl)),
|
neuper@38056
|
1621 |
fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
|
neuper@38056
|
1622 |
end;
|
neuper@37906
|
1623 |
|
neuper@37906
|
1624 |
|
neuper@37906
|
1625 |
|
neuper@37906
|
1626 |
(*18.12.99*)
|
neuper@37906
|
1627 |
fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
|
neuper@37906
|
1628 |
(* case appl_spec p pt m of /// 19.1.00
|
neuper@37906
|
1629 |
Notappl e => Error' (Error_ e)
|
neuper@37906
|
1630 |
| Appl =>
|
neuper@37906
|
1631 |
*) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
|
neuper@37906
|
1632 |
in f end;
|
neuper@37906
|
1633 |
|
neuper@37906
|
1634 |
|
neuper@37938
|
1635 |
(*fun tag_form thy (formal, given) = cterm_of thy
|
neuper@37934
|
1636 |
(((head_of o term_of) given) $ (term_of formal)); WN100819*)
|
neuper@37934
|
1637 |
fun tag_form thy (formal, given) =
|
neuper@37934
|
1638 |
(let val gf = (head_of given) $ formal;
|
neuper@37938
|
1639 |
val _ = cterm_of thy gf
|
neuper@37934
|
1640 |
in gf end)
|
neuper@38053
|
1641 |
handle _ =>
|
neuper@38053
|
1642 |
error ("calchead.tag_form: " ^
|
neuper@38053
|
1643 |
Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
1644 |
(thy2ctxt thy)) given ^ " .. " ^
|
neuper@38053
|
1645 |
Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38053
|
1646 |
(thy2ctxt thy)) formal ^
|
neuper@38053
|
1647 |
" ..types do not match");
|
neuper@37906
|
1648 |
(* val formal = (the o (parse thy)) "[R::real]";
|
neuper@37906
|
1649 |
> val given = (the o (parse thy)) "fixed_values (cs::real list)";
|
neuper@37906
|
1650 |
> tag_form thy (formal, given);
|
neuper@37906
|
1651 |
val it = "fixed_values [R]" : cterm
|
neuper@37906
|
1652 |
*)
|
neuper@38053
|
1653 |
|
neuper@37906
|
1654 |
fun chktyp thy (n, fs, gs) =
|
neuper@38053
|
1655 |
((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
|
neuper@38053
|
1656 |
(nth n)) fs;
|
neuper@38053
|
1657 |
(writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
|
neuper@38053
|
1658 |
(nth n)) gs;
|
neuper@37906
|
1659 |
tag_form thy (nth n fs, nth n gs));
|
neuper@37906
|
1660 |
fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
|
neuper@37906
|
1661 |
|
neuper@37906
|
1662 |
(* #####################################################
|
neuper@37906
|
1663 |
find the failing item:
|
neuper@37906
|
1664 |
> val n = 2;
|
neuper@37906
|
1665 |
> val tag__form = chktyp (n,formals,givens);
|
neuper@37906
|
1666 |
> (type_of o term_of o (nth n)) formals;
|
neuper@37906
|
1667 |
> (type_of o term_of o (nth n)) givens;
|
neuper@37906
|
1668 |
> atomty ((term_of o (nth n)) formals);
|
neuper@37906
|
1669 |
> atomty ((term_of o (nth n)) givens);
|
neuper@37906
|
1670 |
> atomty (term_of tag__form);
|
neuper@37906
|
1671 |
> use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
|
neuper@37906
|
1672 |
##################################################### *)
|
neuper@37906
|
1673 |
|
neuper@37906
|
1674 |
(* #####################################################
|
neuper@37906
|
1675 |
testdata setup
|
neuper@37906
|
1676 |
val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
|
neuper@37906
|
1677 |
val formals = map (the o (parse thy)) origin;
|
neuper@37906
|
1678 |
|
neuper@37906
|
1679 |
val given = ["equation (lhs=rhs)",
|
neuper@37906
|
1680 |
"bound_variable bdv", (* TODO type *)
|
neuper@37906
|
1681 |
"error_bound apx"];
|
neuper@37906
|
1682 |
val where_ = ["e is_root_equation_in bdv",
|
neuper@37906
|
1683 |
"bdv is_var",
|
neuper@37906
|
1684 |
"apx is_const_expr"];
|
neuper@37906
|
1685 |
val find = ["L::rat set"];
|
neuper@37906
|
1686 |
val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
|
neuper@37906
|
1687 |
val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
|
neuper@37906
|
1688 |
val givens = map (the o (parse thy)) given;
|
neuper@37906
|
1689 |
|
neuper@37906
|
1690 |
val tag__forms = chktyps (formals, givens);
|
neuper@37906
|
1691 |
map ((atomty) o term_of) tag__forms;
|
neuper@37906
|
1692 |
##################################################### *)
|
neuper@37906
|
1693 |
|
neuper@37906
|
1694 |
|
neuper@37906
|
1695 |
(* check pbltypes, announces one failure a time *)
|
neuper@37930
|
1696 |
(*fun chk_vars ctppc =
|
neuper@37906
|
1697 |
let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
|
neuper@37906
|
1698 |
appc flat (mappc (vars o term_of) ctppc)
|
neuper@37906
|
1699 |
in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
|
neuper@37906
|
1700 |
else if (re\\(gi union fi)) <> []
|
neuper@37906
|
1701 |
then ("re\\(gi union fi)",re\\(gi union fi))
|
neuper@37930
|
1702 |
else ("ok",[]) end;*)
|
neuper@37930
|
1703 |
fun chk_vars ctppc =
|
neuper@37930
|
1704 |
let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
|
neuper@37934
|
1705 |
appc flat (mappc vars ctppc)
|
neuper@37932
|
1706 |
val chked = subtract op = gi wh
|
neuper@37932
|
1707 |
in if chked <> [] then ("wh\\gi", chked)
|
neuper@37930
|
1708 |
else let val chked = subtract op = (union op = gi fi) re
|
neuper@37932
|
1709 |
in if chked <> []
|
neuper@37932
|
1710 |
then ("re\\(gi union fi)", chked)
|
neuper@37932
|
1711 |
else ("ok", [])
|
neuper@37932
|
1712 |
end
|
neuper@37932
|
1713 |
end;
|
neuper@37906
|
1714 |
|
neuper@37906
|
1715 |
(* check a new pbltype: variables (Free) unbound by given, find*)
|
neuper@37906
|
1716 |
fun unbound_ppc ctppc =
|
neuper@37906
|
1717 |
let val {Given=gi,Find=fi,Relate=re,...} =
|
neuper@37934
|
1718 |
appc flat (mappc vars ctppc)
|
neuper@37930
|
1719 |
in distinct (*re\\(gi union fi)*)
|
neuper@37930
|
1720 |
(subtract op = (union op = gi fi) re) end;
|
neuper@37906
|
1721 |
(*
|
neuper@37906
|
1722 |
> val org = {Given=["[R=(R::real)]"],Where=[],
|
neuper@37906
|
1723 |
Find=["[A::real]"],With=[],
|
neuper@37906
|
1724 |
Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
|
neuper@37906
|
1725 |
}:string ppc;
|
neuper@37906
|
1726 |
> val ctppc = mappc (the o (parse thy)) org;
|
neuper@37906
|
1727 |
> unbound_ppc ctppc;
|
neuper@37906
|
1728 |
val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
|
neuper@37906
|
1729 |
*)
|
neuper@37906
|
1730 |
|
neuper@37906
|
1731 |
|
neuper@37906
|
1732 |
(* f, a binary operator, is nested rightassociative *)
|
neuper@37906
|
1733 |
fun foldr1 f xs =
|
neuper@37906
|
1734 |
let
|
neuper@37906
|
1735 |
fun fld f (x::[]) = x
|
neuper@37906
|
1736 |
| fld f (x::x'::[]) = f (x',x)
|
neuper@37906
|
1737 |
| fld f (x::x'::xs) = f (fld f (x'::xs),x);
|
neuper@37906
|
1738 |
in ((fld f) o rev) xs end;
|
neuper@37906
|
1739 |
(*
|
neuper@37926
|
1740 |
> val (SOME ct) = parse thy "[a=b,c=d,e=f]";
|
neuper@37938
|
1741 |
> val ces = map (cterm_of thy) (isalist2list (term_of ct));
|
neuper@37906
|
1742 |
> val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
|
neuper@37938
|
1743 |
> cterm_of thy conj;
|
neuper@37906
|
1744 |
val it = "(a = b & c = d) & e = f" : cterm
|
neuper@37906
|
1745 |
*)
|
neuper@37906
|
1746 |
|
neuper@37906
|
1747 |
(* f, a binary operator, is nested leftassociative *)
|
neuper@37906
|
1748 |
fun foldl1 f (x::[]) = x
|
neuper@37906
|
1749 |
| foldl1 f (x::x'::[]) = f (x,x')
|
neuper@37906
|
1750 |
| foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
|
neuper@37906
|
1751 |
(*
|
neuper@37926
|
1752 |
> val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
|
neuper@37938
|
1753 |
> val ces = map (cterm_of thy) (isalist2list (term_of ct));
|
neuper@37906
|
1754 |
> val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
|
neuper@37938
|
1755 |
> cterm_of thy conj;
|
neuper@37906
|
1756 |
val it = "a = b & c = d & e = f & g = h" : cterm
|
neuper@37906
|
1757 |
*)
|
neuper@37906
|
1758 |
|
neuper@37906
|
1759 |
|
neuper@37906
|
1760 |
(* called only once, if a Subproblem has been located in the script*)
|
neuper@37906
|
1761 |
fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
|
neuper@37906
|
1762 |
(* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
|
neuper@37906
|
1763 |
*)
|
neuper@37906
|
1764 |
(case metID of
|
neuper@37906
|
1765 |
["no_met"] =>
|
neuper@37906
|
1766 |
(snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
|
neuper@37906
|
1767 |
| _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
|
neuper@37906
|
1768 |
(*all stored in tac_ itms ^^^^^^^^^^*)
|
neuper@37906
|
1769 |
| nxt_model_pbl tac_ _ =
|
neuper@38031
|
1770 |
error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
|
neuper@37906
|
1771 |
(* run subp_rooteq.sml ''
|
neuper@38058
|
1772 |
until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
|
neuper@37906
|
1773 |
> val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
|
neuper@37906
|
1774 |
(last_elem o drop_last) ets'';
|
neuper@37906
|
1775 |
> val mst = (last_elem o drop_last) ets'';
|
neuper@37906
|
1776 |
> nxt_model_pbl mst;
|
neuper@37906
|
1777 |
val it = Refine_Tacitly ["univariate","equation"] : tac
|
neuper@37906
|
1778 |
*)
|
neuper@37906
|
1779 |
|
neuper@37906
|
1780 |
(*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
|
neuper@37934
|
1781 |
fun eq4 v (_,vts,_,_,_) = member op = vts v;
|
neuper@37906
|
1782 |
fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
|
neuper@37906
|
1783 |
|
neuper@37906
|
1784 |
|
neuper@37906
|
1785 |
(*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
|
neuper@37906
|
1786 |
+ met from fmz; assumes pos on PblObj, meth = [].*)
|
neuper@37906
|
1787 |
fun complete_mod (pt, pos as (p, p_):pos') =
|
neuper@37906
|
1788 |
(* val (pt, (p, _)) = (pt, p);
|
neuper@37906
|
1789 |
val (pt, (p, _)) = (pt, pos);
|
neuper@37906
|
1790 |
*)
|
neuper@37906
|
1791 |
let val _= if p_ <> Pbl
|
neuper@38015
|
1792 |
then tracing("###complete_mod: only impl.for Pbl, called with "^
|
neuper@37906
|
1793 |
pos'2str pos) else ()
|
neuper@37906
|
1794 |
val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
|
neuper@37906
|
1795 |
get_obj I pt p
|
neuper@37906
|
1796 |
val (dI,pI,mI) = some_spec ospec spec
|
neuper@37906
|
1797 |
val mpc = (#ppc o get_met) mI
|
neuper@37906
|
1798 |
val ppc = (#ppc o get_pbt) pI
|
neuper@37906
|
1799 |
val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
|
neuper@37906
|
1800 |
val pt = update_pblppc pt p pits
|
neuper@37906
|
1801 |
val pt = update_metppc pt p mits
|
neuper@37906
|
1802 |
in (pt, (p,Met):pos') end
|
neuper@37906
|
1803 |
;
|
neuper@37906
|
1804 |
(*| complete_mod (pt, pos as (p, Met):pos') =
|
neuper@38031
|
1805 |
error ("###complete_mod: only impl.for Pbl, called with "^
|
neuper@37906
|
1806 |
pos'2str pos);*)
|
neuper@37906
|
1807 |
|
neuper@37906
|
1808 |
(*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
|
neuper@37906
|
1809 |
oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
|
neuper@37906
|
1810 |
fun all_modspec (pt, (p,_):pos') =
|
neuper@37906
|
1811 |
(* val (pt, (p,_)) = ptp;
|
neuper@37906
|
1812 |
*)
|
neuper@37906
|
1813 |
let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
|
neuper@37906
|
1814 |
...}) = get_obj I pt p;
|
neuper@37906
|
1815 |
val thy = assoc_thy dI;
|
neuper@37906
|
1816 |
val {ppc,...} = get_met mI;
|
neuper@37906
|
1817 |
val mors = prep_ori fmz_ thy ppc;
|
neuper@37906
|
1818 |
val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
|
neuper@37906
|
1819 |
val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
|
neuper@37906
|
1820 |
val pt = update_spec pt p (dI,pI,mI);
|
neuper@37906
|
1821 |
in (pt, (p,Met): pos') end;
|
neuper@37906
|
1822 |
|
neuper@37906
|
1823 |
(*WN.12.03: use in nxt_spec, too ? what about variants ???*)
|
neuper@37906
|
1824 |
fun is_complete_mod_ ([]: itm list) = false
|
neuper@37906
|
1825 |
| is_complete_mod_ itms =
|
neuper@37906
|
1826 |
foldl and_ (true, (map #3 itms));
|
neuper@37906
|
1827 |
fun is_complete_mod (pt, pos as (p, Pbl): pos') =
|
neuper@37906
|
1828 |
if (is_pblobj o (get_obj I pt)) p
|
neuper@37906
|
1829 |
then (is_complete_mod_ o (get_obj g_pbl pt)) p
|
neuper@38031
|
1830 |
else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
|
neuper@37906
|
1831 |
| is_complete_mod (pt, pos as (p, Met)) =
|
neuper@37906
|
1832 |
if (is_pblobj o (get_obj I pt)) p
|
neuper@37906
|
1833 |
then (is_complete_mod_ o (get_obj g_met pt)) p
|
neuper@38031
|
1834 |
else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
|
neuper@37906
|
1835 |
| is_complete_mod (_, pos) =
|
neuper@38031
|
1836 |
error ("is_complete_mod called by "^pos'2str pos^
|
neuper@37906
|
1837 |
" (should be Pbl or Met)");
|
neuper@37906
|
1838 |
|
neuper@37906
|
1839 |
(*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
|
neuper@37906
|
1840 |
fun is_complete_spec (pt, pos as (p,_): pos') =
|
neuper@37906
|
1841 |
if (not o is_pblobj o (get_obj I pt)) p
|
neuper@38031
|
1842 |
then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
|
neuper@37906
|
1843 |
else let val (dI,pI,mI) = get_obj g_spec pt p
|
neuper@37906
|
1844 |
in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
|
neuper@37906
|
1845 |
(*.complete empty items in specification from origin (pbl, met ev.refined);
|
neuper@37906
|
1846 |
assumes 'is_complete_mod'.*)
|
neuper@37906
|
1847 |
fun complete_spec (pt, pos as (p,_): pos') =
|
neuper@37906
|
1848 |
let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
|
neuper@37906
|
1849 |
val pt = update_spec pt p (some_spec ospec spec)
|
neuper@37906
|
1850 |
in (pt, pos) end;
|
neuper@37906
|
1851 |
|
neuper@37906
|
1852 |
fun is_complete_modspec ptp =
|
neuper@37906
|
1853 |
is_complete_mod ptp andalso is_complete_spec ptp;
|
neuper@37906
|
1854 |
|
neuper@37906
|
1855 |
|
neuper@37906
|
1856 |
|
neuper@37906
|
1857 |
|
neuper@37906
|
1858 |
fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
|
neuper@37906
|
1859 |
(* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
|
neuper@37906
|
1860 |
*)
|
neuper@37906
|
1861 |
let val (_,_,metID) = get_somespec' spec spec'
|
neuper@37906
|
1862 |
val pre =
|
neuper@37906
|
1863 |
if metID = e_metID then []
|
neuper@37906
|
1864 |
else let val {prls,pre=where_,...} = get_met metID
|
neuper@37906
|
1865 |
val pre = check_preconds' prls where_ meth 0
|
neuper@37906
|
1866 |
in pre end
|
neuper@37906
|
1867 |
val allcorrect = is_complete_mod_ meth
|
neuper@37906
|
1868 |
andalso foldl and_ (true, (map #1 pre))
|
neuper@37906
|
1869 |
in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
|
neuper@37906
|
1870 |
| pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
|
neuper@37906
|
1871 |
(* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
|
neuper@37906
|
1872 |
*)
|
neuper@37906
|
1873 |
let val (_,pI,_) = get_somespec' spec spec'
|
neuper@37906
|
1874 |
val pre =
|
neuper@37906
|
1875 |
if pI = e_pblID then []
|
neuper@37906
|
1876 |
else let val {prls,where_,cas,...} = get_pbt pI
|
neuper@37906
|
1877 |
val pre = check_preconds' prls where_ probl 0
|
neuper@37906
|
1878 |
in pre end
|
neuper@37906
|
1879 |
val allcorrect = is_complete_mod_ probl
|
neuper@37906
|
1880 |
andalso foldl and_ (true, (map #1 pre))
|
neuper@37906
|
1881 |
in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
|
neuper@37906
|
1882 |
|
neuper@37906
|
1883 |
|
neuper@37906
|
1884 |
fun pt_form (PrfObj {form,...}) = Form form
|
neuper@37906
|
1885 |
| pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
|
neuper@37906
|
1886 |
let val (dI, pI, _) = get_somespec' spec spec'
|
neuper@37906
|
1887 |
val {cas,...} = get_pbt pI
|
neuper@37906
|
1888 |
in case cas of
|
neuper@37926
|
1889 |
NONE => Form (pblterm dI pI)
|
neuper@37926
|
1890 |
| SOME t => Form (subst_atomic (mk_env probl) t)
|
neuper@37906
|
1891 |
end;
|
neuper@37906
|
1892 |
(*vvv takes the tac _generating_ the formula=result, asm ok....
|
neuper@37906
|
1893 |
fun pt_result (PrfObj {result=(t,asm), tac,...}) =
|
neuper@37906
|
1894 |
(Form t,
|
neuper@37926
|
1895 |
if null asm then NONE else SOME asm,
|
neuper@37926
|
1896 |
SOME tac)
|
neuper@37906
|
1897 |
| pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
|
neuper@37906
|
1898 |
let val (_,_,metID) = some_spec ospec spec
|
neuper@37906
|
1899 |
in (Form t,
|
neuper@37926
|
1900 |
if null asm then NONE else SOME asm,
|
neuper@37926
|
1901 |
if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
|
neuper@37906
|
1902 |
-------------------------------------------------------------------------*)
|
neuper@37906
|
1903 |
|
neuper@37906
|
1904 |
|
neuper@37906
|
1905 |
(*.pt_extract returns
|
neuper@37906
|
1906 |
# the formula at pos
|
neuper@37906
|
1907 |
# the tactic applied to this formula
|
neuper@37906
|
1908 |
# the list of assumptions generated at this formula
|
neuper@37906
|
1909 |
(by application of another tac to the preceding formula !)
|
neuper@37906
|
1910 |
pos is assumed to come from the frontend, ie. generated by moveDown.*)
|
neuper@37906
|
1911 |
(*cannot be in ctree.sml, because ModSpec has to be calculated*)
|
neuper@37906
|
1912 |
fun pt_extract (pt,([],Res)) =
|
neuper@37906
|
1913 |
(* val (pt,([],Res)) = ptp;
|
neuper@37906
|
1914 |
*)
|
neuper@37906
|
1915 |
let val (f, asm) = get_obj g_result pt []
|
neuper@37926
|
1916 |
in (Form f, NONE, asm) end
|
neuper@37906
|
1917 |
(* val p = [3,2];
|
neuper@37906
|
1918 |
*)
|
neuper@37906
|
1919 |
| pt_extract (pt,(p,Res)) =
|
neuper@37906
|
1920 |
(* val (pt,(p,Res)) = ptp;
|
neuper@37906
|
1921 |
*)
|
neuper@37906
|
1922 |
let val (f, asm) = get_obj g_result pt p
|
neuper@37906
|
1923 |
val tac = if last_onlev pt p
|
neuper@37906
|
1924 |
then if is_pblobj' pt (lev_up p)
|
neuper@37906
|
1925 |
then let val (PblObj{spec=(_,pI,_),...}) =
|
neuper@37906
|
1926 |
get_obj I pt (lev_up p)
|
neuper@37926
|
1927 |
in if pI = e_pblID then NONE
|
neuper@37926
|
1928 |
else SOME (Check_Postcond pI) end
|
neuper@37926
|
1929 |
else SOME End_Trans (*WN0502 TODO for other branches*)
|
neuper@37906
|
1930 |
else let val p' = lev_on p
|
neuper@37906
|
1931 |
in if is_pblobj' pt p'
|
neuper@37906
|
1932 |
then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
|
neuper@37906
|
1933 |
get_obj I pt p'
|
neuper@37926
|
1934 |
in SOME (Subproblem (dI, pI)) end
|
neuper@37906
|
1935 |
else if f = get_obj g_form pt p'
|
neuper@37926
|
1936 |
then SOME (get_obj g_tac pt p')
|
neuper@37906
|
1937 |
(*because this Frm ~~~is not on worksheet*)
|
neuper@37926
|
1938 |
else SOME (Take (term2str (get_obj g_form pt p')))
|
neuper@37906
|
1939 |
end
|
neuper@37906
|
1940 |
in (Form f, tac, asm) end
|
neuper@37906
|
1941 |
|
neuper@37906
|
1942 |
| pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
|
neuper@37906
|
1943 |
(* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
|
neuper@37906
|
1944 |
val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
|
neuper@37906
|
1945 |
*)
|
neuper@37906
|
1946 |
let val ppobj = get_obj I pt p
|
neuper@37906
|
1947 |
val f = if is_pblobj ppobj then pt_model ppobj p_
|
neuper@37906
|
1948 |
else get_obj pt_form pt p
|
neuper@37906
|
1949 |
val tac = g_tac ppobj
|
neuper@37926
|
1950 |
in (f, SOME tac, []) end;
|
neuper@37906
|
1951 |
|
neuper@37906
|
1952 |
|
neuper@37906
|
1953 |
(**. get the formula from a ctree-node:
|
neuper@37906
|
1954 |
take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
|
neuper@37906
|
1955 |
take res from all other PrfObj's .**)
|
neuper@37906
|
1956 |
(*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
|
neuper@37906
|
1957 |
fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
|
neuper@37906
|
1958 |
[("headline", (p, Frm), h),
|
neuper@37906
|
1959 |
("stepform", (p, Res), r)]
|
neuper@37906
|
1960 |
| formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
|
neuper@37906
|
1961 |
[("stepform", (p, Frm), form),
|
neuper@37906
|
1962 |
("stepform", (p, Res), r)];
|
neuper@37906
|
1963 |
|
neuper@37906
|
1964 |
fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
|
neuper@37906
|
1965 |
[("stepform", (p, Res), r)]
|
neuper@37906
|
1966 |
|
neuper@37906
|
1967 |
(*assumes to take whole level, in particular hd -- for use in interSteps*)
|
neuper@37906
|
1968 |
fun get_formress fs p [] = flat fs
|
neuper@37906
|
1969 |
| get_formress fs p (nd::nds) =
|
neuper@37906
|
1970 |
(* start with 'form+res' and continue with trying 'res' only*)
|
neuper@37906
|
1971 |
get_forms (fs @ [formres p nd]) (lev_on p) nds
|
neuper@37906
|
1972 |
and get_forms fs p [] = flat fs
|
neuper@37906
|
1973 |
| get_forms fs p (nd::nds) =
|
neuper@37906
|
1974 |
if is_pblnd nd
|
neuper@37906
|
1975 |
(* start again with 'form+res' ///ugly repeat with Check_elementwise
|
neuper@37906
|
1976 |
then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
|
neuper@37906
|
1977 |
then get_forms (fs @ [formres p nd]) (lev_on p) nds
|
neuper@37906
|
1978 |
(* continue with trying 'res' only*)
|
neuper@37906
|
1979 |
else get_forms (fs @ [form p nd]) (lev_on p) nds;
|
neuper@37906
|
1980 |
|
neuper@37906
|
1981 |
(**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
|
neuper@37906
|
1982 |
(*WN050219 made robust against _'to' below or after Complete nodes
|
neuper@37906
|
1983 |
by handling exn caused by move_dn*)
|
neuper@37906
|
1984 |
(*WN0401 this functionality belongs to ctree.sml,
|
neuper@37906
|
1985 |
but fetching a calc_head requires calculations defined in modspec.sml
|
neuper@37906
|
1986 |
transfer to ME/me.sml !!!
|
neuper@37906
|
1987 |
WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
|
neuper@37906
|
1988 |
is returned !!!!!!!!!!!!!
|
neuper@37906
|
1989 |
*)
|
neuper@37906
|
1990 |
fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
|
neuper@37906
|
1991 |
| eq_pos' (p1,Res) (p2,Res) = p1 = p2
|
neuper@37906
|
1992 |
| eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
|
neuper@37906
|
1993 |
Pbl => true
|
neuper@37906
|
1994 |
| Met => true
|
neuper@37906
|
1995 |
| _ => false)
|
neuper@37906
|
1996 |
| eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
|
neuper@37906
|
1997 |
Pbl => true
|
neuper@37906
|
1998 |
| Met => true
|
neuper@37906
|
1999 |
| _ => false)
|
neuper@37906
|
2000 |
| eq_pos' _ _ = false;
|
neuper@37906
|
2001 |
|
neuper@37906
|
2002 |
(*.get an 'interval' from the ctree; 'interval' is w.r.t. the
|
neuper@37906
|
2003 |
total ordering Position#compareTo(Position p) in the java-code
|
neuper@37906
|
2004 |
val get_interval = fn
|
neuper@37906
|
2005 |
: pos' -> : from is "move_up 1st-element" to return
|
neuper@37906
|
2006 |
pos' -> : to the last element to be returned; from < to
|
neuper@37906
|
2007 |
int -> : level: 0 gets the flattest sub-tree possible
|
neuper@37906
|
2008 |
>999 gets the deepest sub-tree possible
|
neuper@37906
|
2009 |
ptree -> :
|
neuper@37906
|
2010 |
(pos' * : of the formula
|
neuper@37906
|
2011 |
Term.term) : the formula
|
neuper@37906
|
2012 |
list
|
neuper@37906
|
2013 |
.*)
|
neuper@37906
|
2014 |
fun get_interval from to level pt =
|
neuper@37906
|
2015 |
(* val (from,level) = (f,lev);
|
neuper@37906
|
2016 |
val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
|
neuper@37906
|
2017 |
*)
|
neuper@37906
|
2018 |
let fun get_inter c (from:pos') (to:pos') lev pt =
|
neuper@37906
|
2019 |
(* val (c, from, to, lev) = ([], from, to, level);
|
neuper@37906
|
2020 |
------for recursion.......
|
neuper@37906
|
2021 |
val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
|
neuper@37906
|
2022 |
*)
|
neuper@37906
|
2023 |
if eq_pos' from to orelse from = ([],Res)
|
neuper@37906
|
2024 |
(*orelse ... avoids Exception- PTREE "end of calculation" raised,
|
neuper@37906
|
2025 |
if 'to' has values NOT generated by move_dn, see systest/me.sml
|
neuper@37906
|
2026 |
TODO.WN0501: introduce an order on pos' and check "from > to"..
|
neuper@37906
|
2027 |
...there is an order in Java!
|
neuper@37906
|
2028 |
WN051224 the hack got worse with returning term instead ptform*)
|
neuper@37906
|
2029 |
then let val (f,_,_) = pt_extract (pt, from)
|
neuper@37906
|
2030 |
in case f of
|
neuper@37906
|
2031 |
ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
|
neuper@37906
|
2032 |
| Form t => c @ [(from, t)]
|
neuper@37906
|
2033 |
end
|
neuper@37906
|
2034 |
else
|
neuper@37906
|
2035 |
if lev < lev_of from
|
neuper@37906
|
2036 |
then (get_inter c (move_dn [] pt from) to lev pt)
|
neuper@37906
|
2037 |
handle (PTREE _(*from move_dn too far*)) => c
|
neuper@37906
|
2038 |
else let val (f,_,_) = pt_extract (pt, from)
|
neuper@37906
|
2039 |
val term = case f of
|
neuper@37906
|
2040 |
ModSpec (_,_,headline,_,_,_)=> headline
|
neuper@37906
|
2041 |
| Form t => t
|
neuper@37906
|
2042 |
in (get_inter (c @ [(from, term)])
|
neuper@37906
|
2043 |
(move_dn [] pt from) to lev pt)
|
neuper@37906
|
2044 |
handle (PTREE _(*from move_dn too far*))
|
neuper@37906
|
2045 |
=> c @ [(from, term)] end
|
neuper@37906
|
2046 |
in get_inter [] from to level pt end;
|
neuper@37906
|
2047 |
|
neuper@37906
|
2048 |
(*for tests*)
|
neuper@37906
|
2049 |
fun posform2str (pos:pos', form) =
|
neuper@37906
|
2050 |
"("^ pos'2str pos ^", "^
|
neuper@37906
|
2051 |
(case form of
|
neuper@37906
|
2052 |
Form f => term2str f
|
neuper@37906
|
2053 |
| ModSpec c => term2str (#3 c(*the headline*)))
|
neuper@37906
|
2054 |
^")";
|
neuper@37906
|
2055 |
fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
|
neuper@37906
|
2056 |
(map posform2str)) pfs;
|
neuper@37906
|
2057 |
fun posterm2str (pos:pos', t) =
|
neuper@37906
|
2058 |
"("^ pos'2str pos ^", "^term2str t^")";
|
neuper@37906
|
2059 |
fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
|
neuper@37906
|
2060 |
(map posterm2str)) pfs;
|
neuper@37906
|
2061 |
|
neuper@37906
|
2062 |
|
neuper@37906
|
2063 |
(*WN050225 omits the last step, if pt is incomplete*)
|
neuper@37906
|
2064 |
fun show_pt pt =
|
neuper@38015
|
2065 |
tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
|
neuper@37906
|
2066 |
|
neuper@37906
|
2067 |
(*.get a calchead from a PblObj-node in the ctree;
|
neuper@37906
|
2068 |
preconditions must be calculated.*)
|
neuper@37906
|
2069 |
fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
|
neuper@37906
|
2070 |
let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
|
neuper@37906
|
2071 |
get_obj I pt p
|
neuper@37906
|
2072 |
val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
|
neuper@38050
|
2073 |
val pre = check_preconds (assoc_thy"Isac") prls where_ probl
|
neuper@37906
|
2074 |
in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
|
neuper@37906
|
2075 |
| get_ocalhd (pt, pos' as (p,Met):pos') =
|
neuper@37906
|
2076 |
let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
|
neuper@37906
|
2077 |
spec, meth,...} =
|
neuper@37906
|
2078 |
get_obj I pt p
|
neuper@37906
|
2079 |
val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
|
neuper@38050
|
2080 |
val pre = check_preconds (assoc_thy"Isac") prls pre meth
|
neuper@37906
|
2081 |
in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
|
neuper@37906
|
2082 |
|
neuper@37906
|
2083 |
(*.at the activeFormula set the Model, the Guard and the Specification
|
neuper@37906
|
2084 |
to empty and return a CalcHead;
|
neuper@37906
|
2085 |
the 'origin' remains (for reconstructing all that).*)
|
neuper@37906
|
2086 |
fun reset_calchead (pt, pos' as (p,_):pos') =
|
neuper@37906
|
2087 |
let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
|
neuper@37906
|
2088 |
val pt = update_pbl pt p []
|
neuper@37906
|
2089 |
val pt = update_met pt p []
|
neuper@37906
|
2090 |
val pt = update_spec pt p e_spec
|
neuper@37906
|
2091 |
in (pt, (p,Pbl):pos') end;
|
neuper@37906
|
2092 |
|
neuper@37906
|
2093 |
(*---------------------------------------------------------------------*)
|
neuper@37906
|
2094 |
end
|
neuper@37906
|
2095 |
|
neuper@37906
|
2096 |
open CalcHead;
|
neuper@37906
|
2097 |
(*---------------------------------------------------------------------*)
|
neuper@37906
|
2098 |
|