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.
|
e0726734@41962
|
3 |
Author: Walther Neuper 991122, Mathias Lehnfeld
|
neuper@37906
|
4 |
(c) due to copyright terms
|
wneuper@59265
|
5 |
*)
|
wneuper@59265
|
6 |
signature CALC_HEAD =
|
wneuper@59265
|
7 |
sig
|
wneuper@59265
|
8 |
type calcstate
|
wneuper@59265
|
9 |
type calcstate'
|
wneuper@59276
|
10 |
datatype appl = Appl of Ctree.tac_ | Notappl of string
|
wneuper@59276
|
11 |
val nxt_specify_init_calc : Ctree.fmz -> calcstate
|
wneuper@59276
|
12 |
val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree ->
|
wneuper@59276
|
13 |
Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree
|
wneuper@59276
|
14 |
val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate'
|
wneuper@59276
|
15 |
val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
|
wneuper@59276
|
16 |
(string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
|
neuper@37906
|
17 |
|
wneuper@59276
|
18 |
val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
|
wneuper@59276
|
19 |
val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd
|
wneuper@59265
|
20 |
val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
|
wneuper@59276
|
21 |
val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
|
neuper@37906
|
22 |
|
wneuper@59265
|
23 |
val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
|
wneuper@59265
|
24 |
val insert_ppc' : itm -> itm list -> itm list
|
neuper@37906
|
25 |
|
wneuper@59276
|
26 |
val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
|
wneuper@59276
|
27 |
val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool
|
wneuper@59276
|
28 |
val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
|
wneuper@59276
|
29 |
val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool
|
wneuper@59265
|
30 |
val some_spec : spec -> spec -> spec
|
wneuper@59265
|
31 |
(* these could go to Ctree ..*)
|
wneuper@59276
|
32 |
val show_pt : Ctree.ptree -> unit
|
wneuper@59276
|
33 |
val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list
|
wneuper@59276
|
34 |
val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list
|
neuper@37906
|
35 |
|
wneuper@59265
|
36 |
val match_ags : theory -> pat list -> term list -> ori list
|
wneuper@59265
|
37 |
val match_ags_msg : pblID -> term -> term list -> unit
|
wneuper@59265
|
38 |
val oris2fmz_vals : ori list -> string list * term list
|
wneuper@59265
|
39 |
val vars_of_pbl_' : ('a * ('b * term)) list -> term list
|
wneuper@59265
|
40 |
val is_known : Proof.context -> string -> ori list -> term -> string * ori * term list
|
wneuper@59265
|
41 |
val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list
|
wneuper@59265
|
42 |
-> string * itm
|
wneuper@59265
|
43 |
val e_calcstate' : calcstate'
|
wneuper@59265
|
44 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59265
|
45 |
val vals_of_oris : ori list -> term list
|
wneuper@59265
|
46 |
val is_error : itm_ -> bool
|
wneuper@59265
|
47 |
val is_copy_named : 'a * ('b * term) -> bool
|
wneuper@59265
|
48 |
val ori2Coritm : pat list -> ori -> itm
|
wneuper@59265
|
49 |
val ppc2list : 'a ppc -> 'a list
|
wneuper@59265
|
50 |
val is_copy_named_idstr : string -> bool
|
wneuper@59265
|
51 |
val matc : theory -> (string * (term * term)) list -> term list -> preori list -> preori list
|
wneuper@59265
|
52 |
val mtc : theory -> pat -> term -> preori option
|
wneuper@59265
|
53 |
val cpy_nam : pat list -> preori list -> pat -> preori
|
wneuper@59265
|
54 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59265
|
55 |
end
|
neuper@37906
|
56 |
|
wneuper@59265
|
57 |
structure Chead(**): CALC_HEAD(**) =
|
neuper@37906
|
58 |
struct
|
wneuper@59276
|
59 |
open Ctree
|
neuper@37906
|
60 |
(* datatypes *)
|
neuper@37906
|
61 |
|
wneuper@59265
|
62 |
(* the state wich is stored after each step of calculation; it contains
|
neuper@38065
|
63 |
the calc-state and a list of [tac,istate](="tacis") to be applied next.
|
neuper@37906
|
64 |
the last_elem tacis is the first to apply to the calc-state and
|
neuper@37906
|
65 |
the (only) one shown to the front-end as the 'proposed tac'.
|
neuper@37906
|
66 |
the calc-state resulting from the application of tacis is not stored,
|
neuper@38065
|
67 |
because the tacis hold enough information for efficiently rebuilding
|
wneuper@59265
|
68 |
this state just by "fun generate "
|
wneuper@59265
|
69 |
*)
|
neuper@37906
|
70 |
type calcstate =
|
wneuper@59265
|
71 |
(ptree * pos') * (* the calc-state to which the tacis could be applied *)
|
wneuper@59271
|
72 |
(Generate.taci list) (* ev. several (hidden) steps;
|
wneuper@59265
|
73 |
in REVERSE order: first tac_ to apply is last_elem *)
|
wneuper@59271
|
74 |
val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate;
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
(*the state used during one calculation within the mathengine; it contains
|
neuper@37906
|
77 |
a list of [tac,istate](="tacis") which generated the the calc-state;
|
neuper@37906
|
78 |
while this state's tacis are extended by each (internal) step,
|
neuper@37906
|
79 |
the calc-state is used for creating new nodes in the calc-tree
|
neuper@37906
|
80 |
(eg. applicable_in requires several particular nodes of the calc-tree)
|
neuper@37906
|
81 |
and then replaced by the the newly created;
|
neuper@37906
|
82 |
on leave of the mathengine the resuing calc-state is dropped anyway,
|
neuper@37906
|
83 |
because the tacis hold enought information for efficiently rebuilding
|
neuper@37906
|
84 |
this state just by "fun generate ".*)
|
neuper@37906
|
85 |
type calcstate' =
|
wneuper@59271
|
86 |
Generate.taci list * (* cas. several (hidden) steps;
|
wneuper@59266
|
87 |
in REVERSE order: first tac_ to apply is last_elem *)
|
wneuper@59266
|
88 |
pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
|
wneuper@59266
|
89 |
(ptree * pos') (* the calc-state resulting from the application of tacis *)
|
wneuper@59271
|
90 |
val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
|
neuper@37906
|
91 |
|
wneuper@59265
|
92 |
(* FIXXXME.WN020430 intermediate hack for fun ass_up *)
|
wneuper@59271
|
93 |
fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f
|
wneuper@59265
|
94 |
| f_mout _ _ = error "f_mout: not called with formula";
|
neuper@37906
|
95 |
|
wneuper@59265
|
96 |
(* is the calchead complete ? *)
|
wneuper@59265
|
97 |
fun ocalhd_complete its pre (dI, pI, mI) =
|
wneuper@59265
|
98 |
foldl and_ (true, map #3 its) andalso
|
wneuper@59265
|
99 |
foldl and_ (true, map #1 pre) andalso
|
wneuper@59265
|
100 |
dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID
|
neuper@37906
|
101 |
|
wneuper@59265
|
102 |
(* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
|
wneuper@59265
|
103 |
--oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
|
neuper@42092
|
104 |
fun oris2fmz_vals oris =
|
wneuper@59265
|
105 |
let fun ori2fmz_vals ((_, _, _, dsc, ts): ori) =
|
wneuper@59265
|
106 |
((term2str o comp_dts') (dsc, ts), last_elem ts)
|
wneuper@59265
|
107 |
handle _ => error ("ori2fmz_env called with " ^ terms2str ts)
|
wneuper@59265
|
108 |
in (split_list o (map ori2fmz_vals)) oris end
|
neuper@37906
|
109 |
|
neuper@37906
|
110 |
(* make a term 'typeless' for comparing with another 'typeless' term;
|
neuper@37906
|
111 |
'type-less' usually is illtyped *)
|
wneuper@59265
|
112 |
fun typeless (Const (s, _)) = (Const (s, e_type))
|
wneuper@59265
|
113 |
| typeless (Free (s, _)) = (Free (s, e_type))
|
wneuper@59265
|
114 |
| typeless (Var (n, _)) = (Var (n, e_type))
|
neuper@37906
|
115 |
| typeless (Bound i) = (Bound i)
|
wneuper@59265
|
116 |
| typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t)
|
wneuper@59265
|
117 |
| typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
|
neuper@37906
|
118 |
|
wneuper@59265
|
119 |
(* to an input (d,ts) find the according ori and insert the ts)
|
wneuper@59265
|
120 |
WN.11.03: + dont take first inter<>[] *)
|
wneuper@59265
|
121 |
fun seek_oridts ctxt sel (d, ts) [] =
|
bonzai@41952
|
122 |
("seek_oridts: input ('" ^
|
wneuper@59265
|
123 |
(term_to_string' ctxt (comp_dts (d, ts))) ^ "') not found in oris (typed)",
|
bonzai@41952
|
124 |
(0, [], sel, d, ts),
|
bonzai@41952
|
125 |
[])
|
wneuper@59265
|
126 |
| seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
|
wneuper@59265
|
127 |
if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
|
wneuper@59265
|
128 |
then ("", (id, vat, sel, d, inter op = ts ts'), ts')
|
wneuper@59265
|
129 |
else seek_oridts ctxt sel (d, ts) oris
|
neuper@37906
|
130 |
|
wneuper@59265
|
131 |
(* to an input (_,ts) find the according ori and insert the ts *)
|
wneuper@59265
|
132 |
fun seek_orits ctxt _ ts [] =
|
neuper@52070
|
133 |
("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
|
neuper@52070
|
134 |
"') not found in oris (typed)", e_ori_, [])
|
wneuper@59265
|
135 |
| seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: (oris: ori list)) =
|
neuper@37934
|
136 |
if sel = sel' andalso (inter op = ts ts') <> []
|
wneuper@59265
|
137 |
then
|
wneuper@59265
|
138 |
if sel = sel'
|
wneuper@59265
|
139 |
then ("", (id, vat, sel, d, inter op = ts ts'): ori, ts')
|
wneuper@59265
|
140 |
else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
|
wneuper@59265
|
141 |
else seek_orits ctxt sel ts oris
|
neuper@37906
|
142 |
|
wneuper@59265
|
143 |
(* find_first item with #1 equal to id *)
|
wneuper@59265
|
144 |
fun seek_ppc _ [] = NONE
|
wneuper@59265
|
145 |
| seek_ppc id (p :: (ppc: itm list)) = if id = #1 p then SOME p else seek_ppc id ppc
|
neuper@37906
|
146 |
|
wneuper@59265
|
147 |
datatype appl =
|
wneuper@59265
|
148 |
Appl of tac_ (* tactic is applicable at a certain position in the Ctree *)
|
wneuper@59265
|
149 |
| Notappl of string (* tactic is NOT applicable *)
|
neuper@37906
|
150 |
|
wneuper@59265
|
151 |
fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) =
|
wneuper@59265
|
152 |
gis @ whs @ fis @ wis @ res
|
wneuper@59265
|
153 |
fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
(* get the number of variants in a problem in 'original',
|
neuper@37906
|
156 |
assumes equal descriptions in immediate sequence *)
|
neuper@37906
|
157 |
fun variants_in ts =
|
wneuper@59265
|
158 |
let
|
wneuper@59265
|
159 |
fun eq (x, y) = head_of x = head_of y
|
wneuper@59265
|
160 |
fun cnt _ [] _ n = ([n], [])
|
wneuper@59265
|
161 |
| cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
|
wneuper@59265
|
162 |
fun coll _ xs [] = xs
|
wneuper@59265
|
163 |
| coll eq xs (y :: ys) =
|
wneuper@59265
|
164 |
let val (n, ys') = cnt eq (y :: ys) y 0
|
wneuper@59265
|
165 |
in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
|
wneuper@59265
|
166 |
val vts = subtract op = [1] (distinct (coll eq [] ts))
|
wneuper@59265
|
167 |
in
|
wneuper@59265
|
168 |
case vts of
|
wneuper@59265
|
169 |
[] => 1
|
wneuper@59265
|
170 |
| [n] => n
|
wneuper@59265
|
171 |
| _ => error "different variants in formalization"
|
wneuper@59265
|
172 |
end
|
neuper@37906
|
173 |
|
wneuper@59265
|
174 |
fun is_list_type (Type ("List.list", _)) = true
|
wneuper@59265
|
175 |
| is_list_type _ = false
|
wneuper@59265
|
176 |
fun has_list_type (Free (_, T)) = is_list_type T
|
wneuper@59265
|
177 |
| has_list_type _ = false
|
neuper@37906
|
178 |
fun is_parsed (Syn _) = false
|
wneuper@59265
|
179 |
| is_parsed _ = true
|
wneuper@59265
|
180 |
fun parse_ok its = foldl and_ (true, map is_parsed its)
|
neuper@37906
|
181 |
|
neuper@37906
|
182 |
fun all_dsc_in itm_s =
|
neuper@37906
|
183 |
let
|
wneuper@59265
|
184 |
fun d_in (Cor ((d, _), _)) = [d]
|
wneuper@59265
|
185 |
| d_in (Syn _) = []
|
wneuper@59265
|
186 |
| d_in (Typ _) = []
|
neuper@37906
|
187 |
| d_in (Inc ((d,_),_)) = [d]
|
neuper@37906
|
188 |
| d_in (Sup (d,_)) = [d]
|
wneuper@59265
|
189 |
| d_in (Mis (d,_)) = [d]
|
wneuper@59265
|
190 |
| d_in i = error ("all_dsc_in: uncovered case with " ^ itm_2str i)
|
wneuper@59265
|
191 |
in (flat o (map d_in)) itm_s end;
|
neuper@37906
|
192 |
|
wneuper@59265
|
193 |
fun is_error (Cor _) = false
|
wneuper@59265
|
194 |
| is_error (Sup _) = false
|
wneuper@59265
|
195 |
| is_error (Inc _) = false
|
wneuper@59265
|
196 |
| is_error (Mis _) = false
|
wneuper@59265
|
197 |
| is_error _ = true
|
neuper@37906
|
198 |
|
wneuper@59265
|
199 |
(* get the first term in ts from ori *)
|
neuper@38051
|
200 |
fun getr_ct thy ((_, _, fd, d, ts) : ori) =
|
wneuper@59265
|
201 |
(fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm')
|
neuper@37906
|
202 |
|
neuper@38051
|
203 |
(* get a term from ori, notyet input in itm.
|
neuper@38051
|
204 |
the term from ori is thrown back to a string in order to reuse
|
neuper@38051
|
205 |
machinery for immediate input by the user. *)
|
neuper@52070
|
206 |
fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
|
neuper@52070
|
207 |
(fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
|
neuper@37906
|
208 |
|
neuper@37906
|
209 |
(* in FE dsc, not dat: this is in itms ...*)
|
wneuper@59265
|
210 |
fun is_untouched ((_, _, false, _, Inc ((_, []), _)): itm) = true
|
wneuper@59265
|
211 |
| is_untouched _ = false
|
neuper@37906
|
212 |
|
neuper@37906
|
213 |
(* select an item in oris, notyet input in itms
|
neuper@37906
|
214 |
(precondition: in itms are only Cor, Sup, Inc) *)
|
wneuper@59235
|
215 |
(*args of nxt_add
|
wneuper@59235
|
216 |
thy : for?
|
wneuper@59235
|
217 |
oris: from formalization 'type fmz', structured for efficient access
|
wneuper@59235
|
218 |
pbt : the problem-pattern to be matched with oris in order to get itms
|
wneuper@59235
|
219 |
itms: already input items
|
wneuper@59235
|
220 |
*)
|
neuper@37906
|
221 |
fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
|
wneuper@59265
|
222 |
let
|
wneuper@59265
|
223 |
fun test_d d ((i, _, _, _, itm_): itm) = (d = (d_in itm_)) andalso i <> 0
|
wneuper@59265
|
224 |
fun is_elem itms (_, (d, _)) =
|
wneuper@59265
|
225 |
case find_first (test_d d) itms of SOME _ => true | NONE => false
|
wneuper@59265
|
226 |
in
|
wneuper@59265
|
227 |
case filter_out (is_elem itms) pbt of
|
wneuper@59265
|
228 |
(f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
|
wneuper@59265
|
229 |
| _ => NONE
|
wneuper@59265
|
230 |
end
|
wneuper@59265
|
231 |
| nxt_add thy oris _ itms =
|
wneuper@59265
|
232 |
let
|
wneuper@59265
|
233 |
fun testr_vt v ori = member op= (#2 (ori:ori)) v andalso (#3 ori) <> "#undef"
|
wneuper@59265
|
234 |
fun testi_vt v itm =member op= (#2 (itm:itm)) v
|
wneuper@59265
|
235 |
fun test_id ids r = member op= ids (#1 (r:ori))
|
wneuper@59265
|
236 |
fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
|
wneuper@59265
|
237 |
(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts)
|
wneuper@59265
|
238 |
fun false_and_not_Sup ((_, _, false, _, Sup _): itm) = false
|
wneuper@59265
|
239 |
| false_and_not_Sup (_, _, false, _, _) = true
|
wneuper@59265
|
240 |
| false_and_not_Sup _ = false
|
wneuper@59265
|
241 |
val v = if itms = [] then 1 else max_vt itms
|
wneuper@59265
|
242 |
val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
|
wneuper@59265
|
243 |
val vits =
|
wneuper@59265
|
244 |
if v = 0
|
wneuper@59265
|
245 |
then itms (* because of dsc without dat *)
|
wneuper@59265
|
246 |
else filter (testi_vt v) itms; (* itms..vat *)
|
wneuper@59265
|
247 |
val icl = filter false_and_not_Sup vits; (* incomplete *)
|
wneuper@59265
|
248 |
in
|
wneuper@59265
|
249 |
if icl = []
|
wneuper@59265
|
250 |
then case filter_out (test_id (map #1 vits)) vors of
|
wneuper@59265
|
251 |
[] => NONE
|
wneuper@59265
|
252 |
| miss => SOME (getr_ct thy (hd miss))
|
wneuper@59265
|
253 |
else
|
wneuper@59265
|
254 |
case find_first (test_subset (hd icl)) vors of
|
wneuper@59265
|
255 |
NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
|
wneuper@59265
|
256 |
| SOME ori => SOME (geti_ct thy ori (hd icl))
|
wneuper@59265
|
257 |
end
|
neuper@37906
|
258 |
|
wneuper@59269
|
259 |
fun mk_delete thy "#Given" itm_ = Del_Given (Specify.itm_out thy itm_)
|
wneuper@59269
|
260 |
| mk_delete thy "#Find" itm_ = Del_Find (Specify.itm_out thy itm_)
|
wneuper@59269
|
261 |
| mk_delete thy "#Relate" itm_ = Del_Relation(Specify.itm_out thy itm_)
|
wneuper@59265
|
262 |
| mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
|
neuper@37906
|
263 |
fun mk_additem "#Given" ct = Add_Given ct
|
wneuper@59265
|
264 |
| mk_additem "#Find" ct = Add_Find ct
|
neuper@37906
|
265 |
| mk_additem "#Relate"ct = Add_Relation ct
|
wneuper@59265
|
266 |
| mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
|
neuper@37906
|
267 |
|
neuper@38051
|
268 |
(* determine the next step of specification;
|
neuper@38051
|
269 |
not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
|
neuper@38051
|
270 |
eg. in rootpbl 'no_met':
|
neuper@37906
|
271 |
args:
|
neuper@38051
|
272 |
preok predicates are _all_ ok (and problem matches completely)
|
neuper@37906
|
273 |
oris immediately from formalization
|
neuper@37906
|
274 |
(dI',pI',mI') specification coming from author/parent-problem
|
neuper@37906
|
275 |
(pbl, item lists specified by user
|
neuper@37906
|
276 |
met) -"-, tacitly completed by copy_probl
|
neuper@37906
|
277 |
(dI,pI,mI) specification explicitly done by the user
|
neuper@37906
|
278 |
(pbt, mpc) problem type, guard of method
|
neuper@38051
|
279 |
*)
|
neuper@38051
|
280 |
fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
|
wneuper@59265
|
281 |
((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
|
wneuper@59265
|
282 |
(if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
|
neuper@38051
|
283 |
else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
|
wneuper@59265
|
284 |
else
|
wneuper@59265
|
285 |
case find_first (is_error o #5) (pbl:itm list) of
|
wneuper@59265
|
286 |
SOME (_, _, _, fd, itm_) =>
|
wneuper@59265
|
287 |
(Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
|
wneuper@59265
|
288 |
| NONE =>
|
wneuper@59265
|
289 |
(case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of
|
wneuper@59265
|
290 |
SOME (fd,ct') => (Pbl, mk_additem fd ct')
|
wneuper@59265
|
291 |
| NONE => (*pbl-items complete*)
|
wneuper@59265
|
292 |
if not preok then (Pbl, Refine_Problem pI')
|
wneuper@59265
|
293 |
else if dI = e_domID then (Pbl, Specify_Theory dI')
|
wneuper@59265
|
294 |
else if pI = e_pblID then (Pbl, Specify_Problem pI')
|
wneuper@59265
|
295 |
else if mI = e_metID then (Pbl, Specify_Method mI')
|
wneuper@59265
|
296 |
else
|
wneuper@59265
|
297 |
case find_first (is_error o #5) met of
|
wneuper@59265
|
298 |
SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_)
|
wneuper@59265
|
299 |
| NONE =>
|
wneuper@59265
|
300 |
(case nxt_add (assoc_thy dI) oris mpc met of
|
wneuper@59265
|
301 |
SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
|
wneuper@59265
|
302 |
| NONE => (Met, Apply_Method mI))))
|
wneuper@59265
|
303 |
| nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
|
wneuper@59265
|
304 |
(case find_first (is_error o #5) met of
|
wneuper@59265
|
305 |
SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
|
wneuper@59265
|
306 |
| NONE =>
|
wneuper@59265
|
307 |
case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
|
wneuper@59265
|
308 |
SOME (fd,ct') => (Met, mk_additem fd ct')
|
wneuper@59265
|
309 |
| NONE =>
|
wneuper@59265
|
310 |
(if dI = e_domID then (Met, Specify_Theory dI')
|
wneuper@59265
|
311 |
else if pI = e_pblID then (Met, Specify_Problem pI')
|
wneuper@59265
|
312 |
else if not preok then (Met, Specify_Method mI)
|
wneuper@59265
|
313 |
else (Met, Apply_Method mI)))
|
wneuper@59265
|
314 |
| nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
|
neuper@37906
|
315 |
|
neuper@37906
|
316 |
fun is_field_correct sel d dscpbt =
|
neuper@37906
|
317 |
case assoc (dscpbt, sel) of
|
neuper@37926
|
318 |
NONE => false
|
wneuper@59265
|
319 |
| SOME ds => member op = ds d
|
neuper@37906
|
320 |
|
wneuper@59265
|
321 |
(* update the itm_ already input, all..from ori *)
|
wneuper@59265
|
322 |
fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) =
|
neuper@37906
|
323 |
let
|
neuper@37930
|
324 |
val ts' = union op = (ts_in itm_) ts;
|
bonzai@41949
|
325 |
val pval = pbl_ids' d ts'
|
wneuper@59265
|
326 |
(* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
|
wneuper@59265
|
327 |
val complete = if eq_set op = (ts', all) then true else false
|
wneuper@59265
|
328 |
in
|
wneuper@59265
|
329 |
case itm_ of
|
wneuper@59265
|
330 |
(Cor _) =>
|
wneuper@59265
|
331 |
(if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
|
wneuper@59265
|
332 |
else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval)))): itm
|
wneuper@59265
|
333 |
| (Syn c) => error ("ori_2itm wants to overwrite " ^ c)
|
wneuper@59265
|
334 |
| (Typ c) => error ("ori_2itm wants to overwrite " ^ c)
|
wneuper@59265
|
335 |
| (Inc _) =>
|
wneuper@59265
|
336 |
if complete
|
wneuper@59265
|
337 |
then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
|
wneuper@59265
|
338 |
else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
|
wneuper@59265
|
339 |
| (Sup (d,ts')) => (*4.9.01 lost env*)
|
wneuper@59265
|
340 |
(*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
|
wneuper@59265
|
341 |
(*else (id,vt,complete,fd,Cor((d,ts'),e))*)
|
wneuper@59265
|
342 |
(* 28.1.00: not completely clear ---^^^ etc.*)
|
wneuper@59265
|
343 |
| (Mis _) => (* 4.9.01: Mis just copied *)
|
wneuper@59265
|
344 |
if complete
|
wneuper@59265
|
345 |
then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
|
wneuper@59265
|
346 |
else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
|
wneuper@59265
|
347 |
| i => error ("ori_2itm: uncovered case of "^ itm_2str i)
|
wneuper@59265
|
348 |
end
|
neuper@37906
|
349 |
|
wneuper@59265
|
350 |
fun eq1 d (_, (d', _)) = (d = d')
|
wneuper@59265
|
351 |
fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
|
neuper@37906
|
352 |
|
neuper@37906
|
353 |
(* 'all' ts from ori; ts is the input; (ori carries rest of info)
|
neuper@37906
|
354 |
9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
|
neuper@37906
|
355 |
pval: value for problem-environment _NOT_ checked for 'inter' --
|
neuper@37906
|
356 |
-- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
|
neuper@37906
|
357 |
(as it has been done for input_icalhd+insert_ppc' in 11.03)*)
|
neuper@37906
|
358 |
(*. is_input ori itms <=>
|
neuper@37906
|
359 |
EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
|
neuper@37906
|
360 |
(2) ori(ts) subset itm(ts) --- Err "already input"
|
neuper@37906
|
361 |
(3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
|
neuper@37906
|
362 |
(4) -"- <> empty --- new: ori(ts) \\ inter .*)
|
wneuper@59265
|
363 |
fun is_notyet_input ctxt (itms: itm list) all ((i, v, f, d, ts): ori) pbt =
|
neuper@37906
|
364 |
case find_first (eq1 d) pbt of
|
wneuper@59265
|
365 |
SOME (_, (_, pid)) =>
|
neuper@37906
|
366 |
(case find_first (eq3 f d) itms of
|
neuper@52070
|
367 |
SOME (_,_,_,_,itm_) =>
|
wneuper@59265
|
368 |
let val ts' = inter op = (ts_in itm_) ts
|
wneuper@59265
|
369 |
in
|
wneuper@59265
|
370 |
if subset op = (ts, ts')
|
wneuper@59265
|
371 |
then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm) (*2*)
|
wneuper@59265
|
372 |
else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
|
neuper@52070
|
373 |
end
|
wneuper@59265
|
374 |
| NONE => ("", ori_2itm (Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
|
wneuper@59265
|
375 |
| NONE => ("", ori_2itm (Sup (d, ts)) e_term all (i, v, f, d, ts))
|
neuper@37906
|
376 |
|
bonzai@41949
|
377 |
fun test_types ctxt (d,ts) =
|
neuper@37906
|
378 |
let
|
wneuper@59265
|
379 |
val opt = (try comp_dts) (d, ts)
|
neuper@37906
|
380 |
val msg = case opt of
|
neuper@37926
|
381 |
SOME _ => ""
|
neuper@52070
|
382 |
| NONE => (term_to_string' ctxt d ^ " " ^
|
wneuper@59265
|
383 |
(strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped")
|
wneuper@59265
|
384 |
in msg end
|
neuper@37906
|
385 |
|
wneuper@59265
|
386 |
(* is the input term t known in oris ?
|
wneuper@59265
|
387 |
give feedback on all(?) strange input;
|
wneuper@59265
|
388 |
return _all_ terms already input to this item (e.g. valuesFor a,b) *)
|
bonzai@41949
|
389 |
fun is_known ctxt sel ori t =
|
neuper@37906
|
390 |
let
|
wneuper@59265
|
391 |
val _ = tracing ("RM is_known: t=" ^ term2str t)
|
wneuper@59265
|
392 |
val ots = (distinct o flat o (map #5)) (ori:ori list)
|
wneuper@59265
|
393 |
val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots
|
wneuper@59265
|
394 |
val (d, ts) = split_dts t
|
wneuper@59265
|
395 |
val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts)
|
wneuper@59265
|
396 |
in
|
wneuper@59265
|
397 |
if (subtract op = oids ids) <> []
|
wneuper@59265
|
398 |
then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), e_ori_, [])
|
wneuper@59265
|
399 |
else
|
wneuper@59265
|
400 |
if d = e_term
|
wneuper@59265
|
401 |
then
|
wneuper@59265
|
402 |
if not (subset op = (map typeless ts, map typeless ots))
|
wneuper@59265
|
403 |
then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
|
wneuper@59265
|
404 |
"' not in example (typeless)", e_ori_, [])
|
wneuper@59265
|
405 |
else
|
wneuper@59265
|
406 |
(case seek_orits ctxt sel ts ori of
|
wneuper@59265
|
407 |
("", ori_ as (_,_,_,d,ts), all) =>
|
wneuper@59265
|
408 |
(case test_types ctxt (d,ts) of
|
wneuper@59265
|
409 |
"" => ("", ori_, all)
|
wneuper@59265
|
410 |
| msg => (msg, e_ori_, []))
|
wneuper@59265
|
411 |
| (msg,_,_) => (msg, e_ori_, []))
|
wneuper@59265
|
412 |
else
|
wneuper@59265
|
413 |
if member op = (map #4 ori) d
|
wneuper@59265
|
414 |
then seek_oridts ctxt sel (d, ts) ori
|
wneuper@59265
|
415 |
else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
|
wneuper@59265
|
416 |
end
|
neuper@37906
|
417 |
|
wneuper@59265
|
418 |
|
neuper@37906
|
419 |
datatype additm =
|
wneuper@59265
|
420 |
Add of itm (* return-value of appl_add *)
|
wneuper@59265
|
421 |
| Err of string (* error-message *)
|
neuper@37906
|
422 |
|
wneuper@59265
|
423 |
(* add an item to the model; check wrt. oris and pbt.
|
wneuper@59265
|
424 |
in contrary to oris<>[] below, this part handles user-input
|
wneuper@59265
|
425 |
extremely acceptive, i.e. accept input instead error-msg *)
|
wneuper@59265
|
426 |
fun appl_add ctxt sel [] ppc pbt ct =
|
wneuper@59265
|
427 |
let
|
wneuper@59265
|
428 |
val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
|
wneuper@59265
|
429 |
in
|
wneuper@59265
|
430 |
case parseNEW ctxt ct of
|
wneuper@59265
|
431 |
NONE => Add (i, [], false, sel, Syn ct)
|
wneuper@59265
|
432 |
| SOME t =>
|
wneuper@59265
|
433 |
let val (d, ts) = split_dts t
|
wneuper@59265
|
434 |
in
|
wneuper@59265
|
435 |
if d = e_term
|
wneuper@59269
|
436 |
then Add (i, [], false, sel, Mis (Specify.dsc_unknown, hd ts))
|
wneuper@59265
|
437 |
else
|
wneuper@59265
|
438 |
(case find_first (eq1 d) pbt of
|
wneuper@59265
|
439 |
NONE => Add (i, [], true, sel, Sup (d,ts))
|
wneuper@59265
|
440 |
| SOME (f, (_, id)) =>
|
wneuper@59265
|
441 |
let fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
|
wneuper@59265
|
442 |
in case find_first (eq2 d) ppc of
|
wneuper@59265
|
443 |
NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
|
wneuper@59265
|
444 |
| SOME (i', _, _, _, itm_) =>
|
wneuper@59265
|
445 |
if is_list_dsc d
|
wneuper@59265
|
446 |
then
|
wneuper@59265
|
447 |
let
|
wneuper@59265
|
448 |
val in_itm = ts_in itm_
|
wneuper@59265
|
449 |
val ts' = union op = ts in_itm
|
wneuper@59265
|
450 |
val i'' = if in_itm = [] then i else i'
|
wneuper@59265
|
451 |
in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
|
wneuper@59265
|
452 |
else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
|
wneuper@59265
|
453 |
end)
|
wneuper@59265
|
454 |
end
|
wneuper@59265
|
455 |
end
|
wneuper@59265
|
456 |
| appl_add ctxt sel oris ppc pbt str =
|
wneuper@59265
|
457 |
case parseNEW ctxt str of
|
wneuper@59265
|
458 |
NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
|
wneuper@59265
|
459 |
| SOME t =>
|
wneuper@59265
|
460 |
case is_known ctxt sel oris t of
|
wneuper@59265
|
461 |
("", ori', all) =>
|
wneuper@59265
|
462 |
(case is_notyet_input ctxt ppc all ori' pbt of
|
wneuper@59265
|
463 |
("", itm) => Add itm
|
wneuper@59265
|
464 |
| (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
|
wneuper@59265
|
465 |
| (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
|
neuper@37906
|
466 |
|
wneuper@59265
|
467 |
(* make oris from args of the stac SubProblem and from pbt.
|
wneuper@59265
|
468 |
can this formal argument (of a model-pattern) be omitted in the arg-list
|
wneuper@59265
|
469 |
of a SubProblem ? see calcelems.sml 'type met ' *)
|
wneuper@59265
|
470 |
fun is_copy_named_idstr str =
|
wneuper@59265
|
471 |
case (rev o Symbol.explode) str of
|
wneuper@59265
|
472 |
"'" :: _ :: "'" :: _ =>
|
wneuper@59265
|
473 |
(tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true)
|
wneuper@59265
|
474 |
| _ =>
|
wneuper@59265
|
475 |
(tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false)
|
wneuper@59265
|
476 |
fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t
|
neuper@41973
|
477 |
|
wneuper@59265
|
478 |
(* should this formal argument (of a model-pattern) create a new identifier? *)
|
wneuper@59265
|
479 |
fun is_copy_named_generating_idstr str =
|
wneuper@59265
|
480 |
if is_copy_named_idstr str
|
wneuper@59265
|
481 |
then
|
wneuper@59265
|
482 |
case (rev o Symbol.explode) str of
|
wneuper@59265
|
483 |
"'" :: "'" :: "'" :: _ => false
|
wneuper@59265
|
484 |
| _ => true
|
wneuper@59265
|
485 |
else false
|
wneuper@59265
|
486 |
fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t
|
neuper@37906
|
487 |
|
wneuper@59265
|
488 |
(* split type-wrapper from scr-arg and build part of an ori;
|
wneuper@59265
|
489 |
an type-error is reported immediately, raises an exn,
|
wneuper@59265
|
490 |
subsequent handling of exn provides 2nd part of error message *)
|
wneuper@59265
|
491 |
fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
|
wneuper@59265
|
492 |
((Thm.global_cterm_of thy (dsc $ var);(*type check*)
|
wneuper@59265
|
493 |
SOME ((([1], str, dsc, (*[var]*)
|
wneuper@59265
|
494 |
split_dts' (dsc, var))): preori)(*:ori without leading #*))
|
wneuper@59265
|
495 |
handle e as TYPE _ =>
|
wneuper@59265
|
496 |
(tracing (dashs 70 ^ "\n"
|
wneuper@59265
|
497 |
^ "*** ERROR while creating the items for the model of the ->problem\n"
|
wneuper@59265
|
498 |
^ "*** from the ->stac with ->typeconstructor in arglist:\n"
|
wneuper@59265
|
499 |
^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n"
|
wneuper@59265
|
500 |
^ "*** description: " ^ term_detail2str dsc
|
wneuper@59265
|
501 |
^ "*** value: " ^ term_detail2str var
|
wneuper@59265
|
502 |
^ "*** typeconstructor in script: " ^ term_detail2str ty
|
wneuper@59265
|
503 |
^ "*** checked by theory: " ^ theory2str thy ^ "\n"
|
wneuper@59265
|
504 |
^ "*** " ^ dots 66);
|
wneuper@59265
|
505 |
writeln (PolyML.makestring e);
|
wneuper@59265
|
506 |
reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
|
wneuper@59265
|
507 |
NONE))
|
wneuper@59265
|
508 |
| mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t)
|
neuper@38010
|
509 |
|
wneuper@59265
|
510 |
(* match each pat of the model-pattern with an actual argument;
|
wneuper@59265
|
511 |
precondition: copy-named vars are filtered out *)
|
wneuper@59265
|
512 |
fun matc _ ([]:pat list) _ (oris:preori list) = oris
|
wneuper@59265
|
513 |
| matc _ pbt [] _ =
|
neuper@38015
|
514 |
(tracing (dashs 70);
|
wneuper@59265
|
515 |
error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
|
wneuper@59265
|
516 |
| matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
|
neuper@37906
|
517 |
(*del?..*)if (is_copy_named_idstr o free2str) t then oris
|
wneuper@59265
|
518 |
else(*..del?*)
|
wneuper@59265
|
519 |
let val opt = mtc thy p a
|
wneuper@59265
|
520 |
in
|
wneuper@59265
|
521 |
case opt of
|
wneuper@59265
|
522 |
SOME ori => matc thy pbt ags (oris @ [ori])
|
neuper@37926
|
523 |
| NONE => [](*WN050903 skipped by exn handled in match_ags*)
|
wneuper@59265
|
524 |
end
|
neuper@38011
|
525 |
|
neuper@38011
|
526 |
(* generate a new variable "x_i" name from a related given one "x"
|
neuper@38011
|
527 |
by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
|
neuper@38012
|
528 |
e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
|
neuper@38012
|
529 |
but leave is_copy_named_generating as is, e.t. ss''' *)
|
wneuper@59265
|
530 |
fun cpy_nam (pbt: pat list) (oris: preori list) (p as (field, (dsc, t)): pat) =
|
neuper@37906
|
531 |
(if is_copy_named_generating p
|
neuper@37906
|
532 |
then (*WN051014 kept strange old code ...*)
|
wneuper@59265
|
533 |
let fun sel (_,_,d,ts) = comp_ts (d, ts)
|
wneuper@59265
|
534 |
val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
|
wneuper@59265
|
535 |
val ext = (last_elem o drop_last o Symbol.explode o free2str) t
|
wneuper@59265
|
536 |
val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
|
wneuper@59265
|
537 |
val vals = map sel oris
|
wneuper@59265
|
538 |
val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
|
wneuper@59265
|
539 |
in ([1], field, dsc, [mk_free (type_of t) cy_ext]): preori end
|
neuper@37906
|
540 |
else ([1], field, dsc, [t])
|
wneuper@59265
|
541 |
) handle _ => error ("cpy_nam: for "^(term2str t))
|
neuper@37906
|
542 |
|
wneuper@59265
|
543 |
(* match the actual arguments of a SubProblem with a model-pattern
|
neuper@37906
|
544 |
and create an ori list (in root-pbl created from formalization).
|
neuper@37906
|
545 |
expects ags:pats = 1:1, while copy-named are filtered out of pats;
|
neuper@38011
|
546 |
if no 1:1 the exn raised by matc/mtc and handled at call.
|
wneuper@59265
|
547 |
copy-named pats are appended in order to get them into the model-items *)
|
wneuper@59265
|
548 |
fun match_ags thy (pbt: pat list) ags =
|
wneuper@59265
|
549 |
let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_)
|
wneuper@59265
|
550 |
val pbt' = filter_out is_copy_named pbt
|
wneuper@59265
|
551 |
val cy = filter is_copy_named pbt
|
wneuper@59265
|
552 |
val oris' = matc thy pbt' ags []
|
wneuper@59265
|
553 |
val cy' = map (cpy_nam pbt' oris') cy
|
wneuper@59269
|
554 |
val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
|
wneuper@59265
|
555 |
in (map flattup ors): ori list end
|
neuper@37906
|
556 |
|
wneuper@59265
|
557 |
(* report part of the error-msg which is not available in match_args *)
|
neuper@37906
|
558 |
fun match_ags_msg pI stac ags =
|
wneuper@59265
|
559 |
let
|
wneuper@59269
|
560 |
val pats = (#ppc o Specify.get_pbt) pI
|
wneuper@59265
|
561 |
val msg = (dots 70^"\n"
|
wneuper@59265
|
562 |
^ "*** problem "^strs2str pI ^ " has the ...\n"
|
wneuper@59265
|
563 |
^ "*** model-pattern "^pats2str pats ^ "\n"
|
wneuper@59265
|
564 |
^ "*** stac '"^term2str stac ^ "' has the ...\n"
|
wneuper@59265
|
565 |
^ "*** arg-list "^terms2str ags ^ "\n"
|
wneuper@59265
|
566 |
^ dashs 70)
|
wneuper@59265
|
567 |
(*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
|
wneuper@59265
|
568 |
in tracing msg end
|
neuper@37906
|
569 |
|
wneuper@59265
|
570 |
(* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
|
neuper@37906
|
571 |
fun vars_of_pbl_ pbl_ =
|
wneuper@59265
|
572 |
let
|
wneuper@59265
|
573 |
fun var_of_pbl_ (_, (_, t)) = t
|
wneuper@59265
|
574 |
in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end
|
neuper@37906
|
575 |
fun vars_of_pbl_' pbl_ =
|
wneuper@59265
|
576 |
let
|
wneuper@59265
|
577 |
fun var_of_pbl_ (_, (_, t)) = t: term
|
wneuper@59265
|
578 |
in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
|
neuper@37906
|
579 |
|
neuper@37906
|
580 |
fun overwrite_ppc thy itm ppc =
|
neuper@37906
|
581 |
let
|
wneuper@59265
|
582 |
fun repl _ (_, _, _, _, itm_) [] =
|
wneuper@59265
|
583 |
error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ " not found")
|
wneuper@59265
|
584 |
| repl ppc' itm (p :: ppc) =
|
wneuper@59265
|
585 |
if (#1 itm) = (#1 (p: itm))
|
wneuper@59265
|
586 |
then ppc' @ [itm] @ ppc
|
wneuper@59265
|
587 |
else repl (ppc' @ [p]) itm ppc
|
wneuper@59265
|
588 |
in repl [] itm ppc end
|
neuper@37906
|
589 |
|
wneuper@59265
|
590 |
(* 10.3.00: insert the already compiled itm into model;
|
neuper@37906
|
591 |
ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
|
neuper@37906
|
592 |
fun insert_ppc thy itm ppc =
|
wneuper@59265
|
593 |
let
|
wneuper@59265
|
594 |
fun eq_untouched d ((0, _, _, _, itm_): itm) = (d = d_in itm_)
|
wneuper@59265
|
595 |
| eq_untouched _ _ = false
|
wneuper@59265
|
596 |
val ppc' = case seek_ppc (#1 itm) ppc of
|
wneuper@59265
|
597 |
SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
|
wneuper@59265
|
598 |
| NONE => (ppc @ [itm])
|
wneuper@59265
|
599 |
in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end
|
neuper@37906
|
600 |
|
wneuper@59265
|
601 |
fun eq_dsc ((_, _, _, _, itm_): itm, (_, _, _, _, iitm_): itm) = (d_in itm_ = d_in iitm_)
|
neuper@37906
|
602 |
|
wneuper@59265
|
603 |
(* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
|
wneuper@59265
|
604 |
handles superfluous items carelessly *)
|
wneuper@59265
|
605 |
fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
|
neuper@37906
|
606 |
|
wneuper@59265
|
607 |
(* output the headline to a ppc *)
|
wneuper@59265
|
608 |
fun header p_ pI mI =
|
wneuper@59271
|
609 |
case p_ of Pbl => Generate.Problem (if pI = e_pblID then [] else pI)
|
wneuper@59271
|
610 |
| Met => Generate.Method mI
|
wneuper@59265
|
611 |
| pos => error ("header called with "^ pos_2str pos)
|
neuper@37906
|
612 |
|
wneuper@59265
|
613 |
fun specify_additem sel (ct, _) (p, Met) _ pt =
|
wneuper@59265
|
614 |
let
|
wneuper@59265
|
615 |
val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
616 |
(PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
|
wneuper@59265
|
617 |
=> (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
|
wneuper@59265
|
618 |
| _ => error "specify_additem: uncovered case of get_obj I pt p"
|
wneuper@59265
|
619 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
|
wneuper@59265
|
620 |
val cpI = if pI = e_pblID then pI' else pI
|
wneuper@59265
|
621 |
val cmI = if mI = e_metID then mI' else mI
|
wneuper@59269
|
622 |
val {ppc, pre, prls, ...} = Specify.get_met cmI
|
wneuper@59265
|
623 |
in
|
wneuper@59265
|
624 |
case appl_add ctxt sel oris met ppc ct of
|
wneuper@59265
|
625 |
Add itm => (*..union old input *)
|
wneuper@59265
|
626 |
let
|
wneuper@59265
|
627 |
val met' = insert_ppc thy itm met
|
wneuper@59265
|
628 |
val arg = case sel of
|
wneuper@59265
|
629 |
"#Given" => Add_Given' (ct, met')
|
wneuper@59265
|
630 |
| "#Find" => Add_Find' (ct, met')
|
wneuper@59265
|
631 |
| "#Relate"=> Add_Relation'(ct, met')
|
wneuper@59265
|
632 |
| str => error ("specify_additem: uncovered case with " ^ str)
|
wneuper@59271
|
633 |
val (p, Met, pt') = case Generate.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
|
wneuper@59265
|
634 |
((p, Met), _, _, pt') => (p, Met, pt')
|
wneuper@59265
|
635 |
| _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
|
wneuper@59265
|
636 |
val pre' = check_preconds thy prls pre met'
|
wneuper@59265
|
637 |
val pb = foldl and_ (true, map fst pre')
|
wneuper@59265
|
638 |
val (p_, nxt) =
|
wneuper@59265
|
639 |
nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
|
wneuper@59269
|
640 |
((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
|
wneuper@59265
|
641 |
in ((p, p_), ((p, p_), Uistate),
|
wneuper@59271
|
642 |
Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
|
wneuper@59265
|
643 |
end
|
wneuper@59265
|
644 |
| Err msg =>
|
wneuper@59265
|
645 |
let
|
wneuper@59265
|
646 |
val pre' = check_preconds thy prls pre met
|
wneuper@59265
|
647 |
val pb = foldl and_ (true, map fst pre')
|
wneuper@59265
|
648 |
val (p_, nxt) =
|
wneuper@59265
|
649 |
nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
|
wneuper@59269
|
650 |
((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
|
wneuper@59271
|
651 |
in ((p,p_), ((p,p_),Uistate), Generate.Error' msg, nxt, Safe,pt) end
|
wneuper@59265
|
652 |
end
|
wneuper@59265
|
653 |
| specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
|
neuper@41993
|
654 |
let
|
wneuper@59265
|
655 |
val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
656 |
(PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
|
wneuper@59265
|
657 |
=> (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
|
wneuper@59265
|
658 |
| _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
|
wneuper@59265
|
659 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
|
wneuper@59265
|
660 |
val cpI = if pI = e_pblID then pI' else pI
|
wneuper@59265
|
661 |
val cmI = if mI = e_metID then mI' else mI
|
wneuper@59269
|
662 |
val {ppc, where_, prls, ...} = Specify.get_pbt cpI
|
neuper@41993
|
663 |
in
|
neuper@41993
|
664 |
case appl_add ctxt sel oris pbl ppc ct of
|
wneuper@59265
|
665 |
Add itm => (*..union old input *)
|
neuper@41993
|
666 |
let
|
neuper@41993
|
667 |
val pbl' = insert_ppc thy itm pbl
|
wneuper@59265
|
668 |
val arg = case sel of
|
wneuper@59265
|
669 |
"#Given" => Add_Given' (ct, pbl')
|
wneuper@59265
|
670 |
| "#Find" => Add_Find' (ct, pbl')
|
wneuper@59265
|
671 |
| "#Relate"=> Add_Relation'(ct, pbl')
|
wneuper@59265
|
672 |
| str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
|
wneuper@59271
|
673 |
val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
|
neuper@41993
|
674 |
val pre = check_preconds thy prls where_ pbl'
|
neuper@41993
|
675 |
val pb = foldl and_ (true, map fst pre)
|
neuper@41993
|
676 |
val (p_, nxt) =
|
wneuper@59269
|
677 |
nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
|
wneuper@59265
|
678 |
val ppc = if p_= Pbl then pbl' else met
|
wneuper@59265
|
679 |
in
|
wneuper@59265
|
680 |
((p, p_), ((p, p_), Uistate),
|
wneuper@59271
|
681 |
Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
|
neuper@41993
|
682 |
end
|
neuper@41993
|
683 |
| Err msg =>
|
neuper@41993
|
684 |
let
|
neuper@41993
|
685 |
val pre = check_preconds thy prls where_ pbl
|
neuper@41993
|
686 |
val pb = foldl and_ (true, map fst pre)
|
neuper@41993
|
687 |
val (p_, nxt) =
|
wneuper@59265
|
688 |
nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
|
wneuper@59269
|
689 |
(ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
|
wneuper@59271
|
690 |
in ((p, p_), ((p, p_), Uistate), Generate.Error' msg, nxt, Safe,pt) end
|
wneuper@59265
|
691 |
end
|
neuper@37906
|
692 |
|
wneuper@59265
|
693 |
fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
|
neuper@41994
|
694 |
let (* either """"""""""""""" all empty or complete *)
|
wneuper@59265
|
695 |
val thy = assoc_thy dI'
|
neuper@41994
|
696 |
val (oris, ctxt) =
|
neuper@41994
|
697 |
if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
|
neuper@41994
|
698 |
then ([], e_ctxt)
|
wneuper@59269
|
699 |
else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
|
wneuper@59265
|
700 |
val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
|
neuper@42092
|
701 |
(oris, (dI',pI',mI'), e_term)
|
neuper@41994
|
702 |
val pt = update_ctxt pt [] ctxt
|
wneuper@59265
|
703 |
val (pbl, pre) = ([], [])
|
neuper@41994
|
704 |
in
|
neuper@41994
|
705 |
case mI' of
|
neuper@41994
|
706 |
["no_met"] =>
|
neuper@41994
|
707 |
(([], Pbl), (([], Pbl), Uistate),
|
wneuper@59271
|
708 |
Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
|
neuper@41994
|
709 |
Refine_Tacitly pI', Safe, pt)
|
neuper@41994
|
710 |
| _ =>
|
neuper@41994
|
711 |
(([], Pbl), (([], Pbl), Uistate),
|
wneuper@59271
|
712 |
Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
|
neuper@41994
|
713 |
Model_Problem, Safe, pt)
|
wneuper@59265
|
714 |
end
|
wneuper@59265
|
715 |
(* ONLY for STARTING modeling phase *)
|
wneuper@59265
|
716 |
| specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
|
wneuper@59265
|
717 |
let
|
wneuper@59265
|
718 |
val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
719 |
PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
|
wneuper@59265
|
720 |
(oris, dI',pI',mI', dI, ctxt)
|
wneuper@59265
|
721 |
| _ => error "specify (Model_Problem': uncovered case get_obj"
|
wneuper@59265
|
722 |
val thy' = if dI = e_domID then dI' else dI
|
wneuper@59265
|
723 |
val thy = assoc_thy thy'
|
wneuper@59269
|
724 |
val {ppc, prls, where_, ...} = Specify.get_pbt pI'
|
wneuper@59265
|
725 |
val pre = check_preconds thy prls where_ pbl
|
wneuper@59265
|
726 |
val pb = foldl and_ (true, map fst pre)
|
wneuper@59265
|
727 |
val ((p, _), _, _, pt) =
|
wneuper@59271
|
728 |
Generate.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
|
wneuper@59265
|
729 |
val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
|
wneuper@59269
|
730 |
(ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
|
wneuper@59265
|
731 |
in
|
wneuper@59265
|
732 |
((p, Pbl), ((p, p_), Uistate),
|
wneuper@59271
|
733 |
Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
|
wneuper@59265
|
734 |
nxt, Safe, pt)
|
wneuper@59265
|
735 |
end
|
wneuper@59265
|
736 |
(* called only if no_met is specified *)
|
wneuper@59265
|
737 |
| specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
|
neuper@41980
|
738 |
let
|
wneuper@59265
|
739 |
val (dI', ctxt) = case get_obj I pt p of
|
wneuper@59265
|
740 |
PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
|
wneuper@59265
|
741 |
| _ => error "specify (Refine_Tacitly': uncovered case get_obj"
|
wneuper@59269
|
742 |
val {met, thy,...} = Specify.get_pbt pIre
|
wneuper@59265
|
743 |
val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
|
wneuper@59265
|
744 |
val ((p,_), _, _, pt) =
|
wneuper@59271
|
745 |
Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
|
wneuper@59265
|
746 |
val (pbl, pre, _) = ([], [], false)
|
neuper@41980
|
747 |
in ((p, Pbl), (pos, Uistate),
|
wneuper@59271
|
748 |
Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
|
neuper@41980
|
749 |
Model_Problem, Safe, pt)
|
neuper@41980
|
750 |
end
|
wneuper@59265
|
751 |
| specify (Refine_Problem' rfd) pos _ pt =
|
neuper@42005
|
752 |
let
|
neuper@42005
|
753 |
val ctxt = get_ctxt pt pos
|
wneuper@59265
|
754 |
val (pos, _, _, pt) =
|
wneuper@59271
|
755 |
Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
|
wneuper@59265
|
756 |
in
|
wneuper@59271
|
757 |
(pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Generate.RefinedKF rfd, Model_Problem, Safe, pt)
|
neuper@41980
|
758 |
end
|
neuper@41994
|
759 |
(*WN110515 initialise ctxt again from itms and add preconds*)
|
wneuper@59265
|
760 |
| specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
|
neuper@41994
|
761 |
let
|
wneuper@59265
|
762 |
val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
|
wneuper@59265
|
763 |
PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
|
wneuper@59265
|
764 |
(oris, dI', pI', mI', dI, mI, ctxt, met)
|
wneuper@59265
|
765 |
| _ => error "specify (Specify_Problem': uncovered case get_obj"
|
neuper@41994
|
766 |
val thy = assoc_thy dI
|
wneuper@59265
|
767 |
val (p, Pbl, pt) =
|
wneuper@59271
|
768 |
case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
|
wneuper@59265
|
769 |
((p, Pbl), _, _, pt) => (p, Pbl, pt)
|
wneuper@59265
|
770 |
| _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
|
wneuper@59265
|
771 |
val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
|
wneuper@59265
|
772 |
val mI'' = if mI=e_metID then mI' else mI
|
wneuper@59269
|
773 |
val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
|
wneuper@59269
|
774 |
(#ppc o Specify.get_met) mI'') (dI, pI, mI);
|
wneuper@59265
|
775 |
in
|
wneuper@59265
|
776 |
((p,Pbl), (pos,Uistate),
|
wneuper@59271
|
777 |
Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
|
wneuper@59265
|
778 |
nxt, Safe, pt)
|
neuper@41994
|
779 |
end
|
neuper@41994
|
780 |
(*WN110515 initialise ctxt again from itms and add preconds*)
|
wneuper@59265
|
781 |
| specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt =
|
neuper@41994
|
782 |
let
|
wneuper@59265
|
783 |
val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
784 |
PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
|
wneuper@59265
|
785 |
(oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
|
wneuper@59265
|
786 |
| _ => error "specify (Specify_Problem': uncovered case get_obj"
|
wneuper@59269
|
787 |
val {ppc,pre,prls,...} = Specify.get_met mID
|
neuper@41994
|
788 |
val thy = assoc_thy dI
|
wneuper@59269
|
789 |
val oris = Specify.add_field' thy ppc oris
|
wneuper@59265
|
790 |
val dI'' = if dI=e_domID then dI' else dI
|
wneuper@59265
|
791 |
val pI'' = if pI = e_pblID then pI' else pI
|
wneuper@59265
|
792 |
val met = if met = [] then pbl else met
|
wneuper@59269
|
793 |
val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
|
neuper@41994
|
794 |
val (pos, _, _, pt) =
|
wneuper@59271
|
795 |
Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
|
wneuper@59265
|
796 |
val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
|
wneuper@59269
|
797 |
((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
|
wneuper@59265
|
798 |
in
|
wneuper@59265
|
799 |
(pos, (pos,Uistate),
|
wneuper@59271
|
800 |
Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
|
wneuper@59265
|
801 |
nxt, Safe, pt)
|
neuper@41994
|
802 |
end
|
neuper@37906
|
803 |
| specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
|
neuper@37906
|
804 |
| specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
|
neuper@37906
|
805 |
| specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
|
wneuper@59265
|
806 |
| specify (Specify_Theory' domID) (pos as (p,p_)) _ pt =
|
neuper@41994
|
807 |
let
|
neuper@41994
|
808 |
val p_ = case p_ of Met => Met | _ => Pbl
|
wneuper@59265
|
809 |
val thy = assoc_thy domID
|
wneuper@59265
|
810 |
val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
811 |
PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
|
wneuper@59265
|
812 |
(oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
|
wneuper@59265
|
813 |
| _ => error "specify (Specify_Theory': uncovered case get_obj"
|
wneuper@59265
|
814 |
val mppc = case p_ of Met => met | _ => pbl
|
wneuper@59265
|
815 |
val cpI = if pI = e_pblID then pI' else pI
|
wneuper@59269
|
816 |
val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
|
wneuper@59265
|
817 |
val cmI = if mI = e_metID then mI' else mI
|
wneuper@59269
|
818 |
val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
|
wneuper@59265
|
819 |
val pre = case p_ of
|
wneuper@59265
|
820 |
Met => (check_preconds thy mer mwh met)
|
wneuper@59265
|
821 |
| _ => (check_preconds thy per pwh pbl)
|
neuper@41994
|
822 |
val pb = foldl and_ (true, map fst pre)
|
neuper@41994
|
823 |
in
|
neuper@41994
|
824 |
if domID = dI
|
neuper@41994
|
825 |
then
|
wneuper@59265
|
826 |
let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
|
wneuper@59265
|
827 |
in
|
wneuper@59265
|
828 |
((p, p_), (pos, Uistate),
|
wneuper@59271
|
829 |
Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
|
wneuper@59265
|
830 |
nxt, Safe, pt)
|
neuper@41994
|
831 |
end
|
neuper@41994
|
832 |
else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
|
neuper@41994
|
833 |
let
|
wneuper@59271
|
834 |
val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
|
wneuper@59265
|
835 |
val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
|
wneuper@59265
|
836 |
in
|
wneuper@59265
|
837 |
((p,p_), (pos,Uistate),
|
wneuper@59271
|
838 |
Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
|
wneuper@59265
|
839 |
nxt, Safe, pt)
|
neuper@41994
|
840 |
end
|
neuper@41994
|
841 |
end
|
wneuper@59265
|
842 |
| specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m')
|
neuper@37906
|
843 |
|
neuper@41994
|
844 |
(*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
|
neuper@41994
|
845 |
-- for input from scratch*)
|
neuper@38051
|
846 |
fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
|
wneuper@59265
|
847 |
let
|
wneuper@59265
|
848 |
val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
849 |
PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
|
wneuper@59265
|
850 |
(oris, dI', pI', dI, pI, pbl, ctxt)
|
wneuper@59265
|
851 |
| _ => error "specify (Specify_Theory': uncovered case get_obj"
|
wneuper@59265
|
852 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
|
wneuper@59265
|
853 |
val cpI = if pI = e_pblID then pI' else pI;
|
wneuper@59265
|
854 |
in
|
wneuper@59269
|
855 |
case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
|
wneuper@59265
|
856 |
Add itm (*..union old input *) =>
|
wneuper@59265
|
857 |
let
|
wneuper@59265
|
858 |
val pbl' = insert_ppc thy itm pbl
|
wneuper@59265
|
859 |
val (tac, tac_) = case sel of
|
wneuper@59265
|
860 |
"#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
|
wneuper@59265
|
861 |
| "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
|
wneuper@59265
|
862 |
| "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
|
wneuper@59265
|
863 |
| sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
|
wneuper@59271
|
864 |
val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
|
wneuper@59265
|
865 |
((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
|
wneuper@59265
|
866 |
| _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
|
wneuper@59265
|
867 |
in
|
wneuper@59265
|
868 |
([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
|
wneuper@59265
|
869 |
end
|
wneuper@59265
|
870 |
| Err msg => (*TODO.WN03 pass error-msgs to the frontend..
|
wneuper@59265
|
871 |
FIXME ..and dont abuse a tactic for that purpose*)
|
wneuper@59265
|
872 |
([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
|
wneuper@59265
|
873 |
(e_pos', (e_istate, e_ctxt)))], [], ptp)
|
wneuper@59265
|
874 |
end
|
wneuper@59265
|
875 |
| nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
|
wneuper@59265
|
876 |
let
|
wneuper@59265
|
877 |
val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
878 |
PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
|
wneuper@59265
|
879 |
(oris, dI', mI', dI, mI, met, ctxt)
|
wneuper@59265
|
880 |
| _ => error "nxt_specif_additem Met: uncovered case get_obj"
|
wneuper@59265
|
881 |
val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
|
wneuper@59265
|
882 |
val cmI = if mI = e_metID then mI' else mI;
|
wneuper@59265
|
883 |
in
|
wneuper@59269
|
884 |
case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
|
wneuper@59265
|
885 |
Add itm (*..union old input *) =>
|
wneuper@59265
|
886 |
let
|
wneuper@59265
|
887 |
val met' = insert_ppc thy itm met;
|
wneuper@59265
|
888 |
val (tac,tac_) = case sel of
|
wneuper@59265
|
889 |
"#Given" => (Add_Given ct, Add_Given' (ct, met'))
|
wneuper@59265
|
890 |
| "#Find" => (Add_Find ct, Add_Find' (ct, met'))
|
wneuper@59265
|
891 |
| "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
|
wneuper@59265
|
892 |
| sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
|
wneuper@59271
|
893 |
val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
|
wneuper@59265
|
894 |
((p, Met), c, _, pt') => (p, Met, c, pt')
|
wneuper@59265
|
895 |
| _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
|
wneuper@59265
|
896 |
in
|
wneuper@59265
|
897 |
([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))
|
wneuper@59265
|
898 |
end
|
wneuper@59265
|
899 |
| Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
|
wneuper@59265
|
900 |
end
|
wneuper@59265
|
901 |
| nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
|
neuper@41994
|
902 |
|
wneuper@59265
|
903 |
fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) =
|
wneuper@59265
|
904 |
((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm)
|
wneuper@59265
|
905 |
handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm)
|
wneuper@59265
|
906 |
(*dsc in oris, but not in pbl pat list: keep this dsc*)
|
neuper@37906
|
907 |
|
wneuper@59265
|
908 |
(* filter out oris which have same description in itms *)
|
neuper@37906
|
909 |
fun filter_outs oris [] = oris
|
neuper@37906
|
910 |
| filter_outs oris (i::itms) =
|
wneuper@59265
|
911 |
let
|
wneuper@59265
|
912 |
val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris
|
wneuper@59265
|
913 |
in
|
wneuper@59265
|
914 |
filter_outs ors itms
|
wneuper@59265
|
915 |
end
|
neuper@37906
|
916 |
|
wneuper@59265
|
917 |
(* filter oris which are in pbt, too *)
|
neuper@37906
|
918 |
fun filter_pbt oris pbt =
|
wneuper@59265
|
919 |
let
|
wneuper@59265
|
920 |
val dscs = map (fst o snd) pbt
|
wneuper@59265
|
921 |
in
|
wneuper@59265
|
922 |
filter ((member op= dscs) o (#4 : ori -> term)) oris
|
wneuper@59265
|
923 |
end
|
neuper@37906
|
924 |
|
wneuper@59265
|
925 |
(* combine itms from pbl + met and complete them wrt. pbt *)
|
wneuper@59265
|
926 |
(* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
|
wneuper@59265
|
927 |
fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met =
|
wneuper@59265
|
928 |
let
|
wneuper@59265
|
929 |
val vat = max_vt pits;
|
wneuper@59265
|
930 |
val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits)
|
wneuper@59265
|
931 |
val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris
|
wneuper@59265
|
932 |
val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
|
wneuper@59265
|
933 |
in
|
wneuper@59265
|
934 |
itms @ (map (ori2Coritm met) os)
|
wneuper@59265
|
935 |
end
|
neuper@37906
|
936 |
|
wneuper@59265
|
937 |
(* complete model and guard of a calc-head *)
|
wneuper@59265
|
938 |
fun complete_mod_ (oris, mpc, ppc, probl) =
|
wneuper@59265
|
939 |
let
|
wneuper@59265
|
940 |
val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl
|
wneuper@59265
|
941 |
val vat = if probl = [] then 1 else max_vt probl
|
wneuper@59265
|
942 |
val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris
|
wneuper@59265
|
943 |
val pors = filter_outs pors pits (*which are in pbl already*)
|
wneuper@59265
|
944 |
val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
|
wneuper@59265
|
945 |
val pits = pits @ (map (ori2Coritm ppc) pors)
|
wneuper@59265
|
946 |
val mits = complete_metitms oris pits [] mpc
|
wneuper@59265
|
947 |
in (pits, mits) end
|
neuper@37906
|
948 |
|
wneuper@59265
|
949 |
fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =
|
wneuper@59265
|
950 |
(if dI = e_domID then odI else dI,
|
wneuper@59265
|
951 |
if pI = e_pblID then opI else pI,
|
wneuper@59265
|
952 |
if mI = e_metID then omI else mI) : spec
|
neuper@37906
|
953 |
|
wneuper@59265
|
954 |
(* find a next applicable tac (for calcstate) and update ptree
|
wneuper@59265
|
955 |
(for ev. finding several more tacs due to hide) *)
|
wneuper@59265
|
956 |
(* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
|
wneuper@59265
|
957 |
(* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
|
wneuper@59265
|
958 |
(* WN.24.10.03 fun nxt_solv = ...................................?? *)
|
wneuper@59265
|
959 |
fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) =
|
neuper@41982
|
960 |
let
|
wneuper@59265
|
961 |
val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
962 |
PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
|
wneuper@59265
|
963 |
| _ => error "nxt_specif Model_Problem; uncovered case get_obj"
|
neuper@41982
|
964 |
val (dI, pI, mI) = some_spec ospec spec
|
neuper@41982
|
965 |
val thy = assoc_thy dI
|
wneuper@59269
|
966 |
val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
|
wneuper@59269
|
967 |
val {cas, ppc, ...} = Specify.get_pbt pI
|
wneuper@59271
|
968 |
val pbl = Generate.init_pbl ppc (* fill in descriptions *)
|
neuper@41982
|
969 |
(*----------------if you think, this should be done by the Dialog
|
neuper@41982
|
970 |
in the java front-end, search there for WN060225-modelProblem----*)
|
wneuper@59265
|
971 |
val (pbl, met) = case cas of
|
wneuper@59265
|
972 |
NONE => (pbl, [])
|
wneuper@59265
|
973 |
| _ => complete_mod_ (oris, mpc, ppc, probl)
|
neuper@41982
|
974 |
(*----------------------------------------------------------------*)
|
neuper@41982
|
975 |
val tac_ = Model_Problem' (pI, pbl, met)
|
wneuper@59271
|
976 |
val (pos,c,_,pt) = Generate.generate1 thy tac_ (Uistate, ctxt) pos pt
|
wneuper@59265
|
977 |
in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
|
neuper@37906
|
978 |
| nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
|
neuper@37906
|
979 |
| nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
|
neuper@37906
|
980 |
| nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
|
neuper@41975
|
981 |
(*. called only if no_met is specified .*)
|
neuper@37906
|
982 |
| nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
|
wneuper@59265
|
983 |
let
|
wneuper@59265
|
984 |
val (oris, dI, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
985 |
(PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
|
wneuper@59265
|
986 |
| _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
|
wneuper@59269
|
987 |
val opt = Specify.refine_ori oris pI
|
wneuper@59265
|
988 |
in
|
wneuper@59265
|
989 |
case opt of
|
wneuper@59265
|
990 |
SOME pI' =>
|
wneuper@59265
|
991 |
let
|
wneuper@59269
|
992 |
val {met, ...} = Specify.get_pbt pI'
|
wneuper@59265
|
993 |
(*val pt = update_pbl pt p pbl ..done by Model_Problem*)
|
wneuper@59265
|
994 |
val mI = if length met = 0 then e_metID else hd met
|
wneuper@59265
|
995 |
val thy = assoc_thy dI
|
wneuper@59265
|
996 |
val (pos, c, _, pt) =
|
wneuper@59271
|
997 |
Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
|
wneuper@59265
|
998 |
in
|
wneuper@59265
|
999 |
([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
|
wneuper@59265
|
1000 |
(pos, (Uistate, e_ctxt)))], c, (pt,pos))
|
wneuper@59265
|
1001 |
end
|
wneuper@59265
|
1002 |
| NONE => ([], [], ptp)
|
wneuper@59265
|
1003 |
end
|
neuper@37906
|
1004 |
| nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
|
wneuper@59265
|
1005 |
let
|
wneuper@59265
|
1006 |
val (dI, dI', probl, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
1007 |
PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
|
wneuper@59265
|
1008 |
(dI, dI', probl, ctxt)
|
wneuper@59265
|
1009 |
| _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
|
wneuper@59265
|
1010 |
val thy = if dI' = e_domID then dI else dI'
|
wneuper@59265
|
1011 |
in
|
wneuper@59269
|
1012 |
case Specify.refine_pbl (assoc_thy thy) pI probl of
|
wneuper@59265
|
1013 |
NONE => ([], [], ptp)
|
wneuper@59265
|
1014 |
| SOME rfd =>
|
wneuper@59265
|
1015 |
let
|
wneuper@59271
|
1016 |
val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
|
wneuper@59265
|
1017 |
in
|
wneuper@59265
|
1018 |
([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
|
wneuper@59265
|
1019 |
end
|
wneuper@59265
|
1020 |
end
|
neuper@37906
|
1021 |
| nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
|
wneuper@59265
|
1022 |
let
|
wneuper@59265
|
1023 |
val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
1024 |
PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>
|
wneuper@59265
|
1025 |
(oris, dI, dI', pI', probl, ctxt)
|
wneuper@59265
|
1026 |
| _ => error ""
|
wneuper@59265
|
1027 |
val thy = assoc_thy (if dI' = e_domID then dI else dI');
|
wneuper@59269
|
1028 |
val {ppc,where_,prls,...} = Specify.get_pbt pI
|
wneuper@59265
|
1029 |
val pbl =
|
wneuper@59265
|
1030 |
if pI' = e_pblID andalso pI = e_pblID
|
wneuper@59271
|
1031 |
then (false, (Generate.init_pbl ppc, []))
|
wneuper@59269
|
1032 |
else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
|
wneuper@59265
|
1033 |
(*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
|
wneuper@59271
|
1034 |
val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
|
wneuper@59265
|
1035 |
((_, Pbl), c, _, pt) => (c, pt)
|
wneuper@59265
|
1036 |
| _ => error ""
|
wneuper@59265
|
1037 |
in
|
wneuper@59265
|
1038 |
([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))
|
wneuper@59265
|
1039 |
end
|
wneuper@59265
|
1040 |
(* transfers oris (not required in pbl) to met-model for script-env
|
wneuper@59265
|
1041 |
FIXME.WN.8.03: application of several mIDs to SAME model? *)
|
wneuper@59265
|
1042 |
| nxt_specif (Specify_Method mID) (pt, pos as (p,_)) =
|
wneuper@59265
|
1043 |
let
|
wneuper@59265
|
1044 |
val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
|
wneuper@59265
|
1045 |
PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
|
wneuper@59265
|
1046 |
=> (oris, pbl, dI, met, ctxt)
|
wneuper@59265
|
1047 |
| _ => error "nxt_specif Specify_Method: uncovered case get_obj"
|
wneuper@59269
|
1048 |
val {ppc,pre,prls,...} = Specify.get_met mID
|
wneuper@59265
|
1049 |
val thy = assoc_thy dI
|
wneuper@59269
|
1050 |
val oris = Specify.add_field' thy ppc oris
|
wneuper@59265
|
1051 |
val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
|
wneuper@59269
|
1052 |
val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
|
wneuper@59265
|
1053 |
val (pos, c, _, pt) =
|
wneuper@59271
|
1054 |
Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
|
wneuper@59265
|
1055 |
in
|
wneuper@59265
|
1056 |
([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
|
wneuper@59265
|
1057 |
end
|
wneuper@59265
|
1058 |
| nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =
|
wneuper@59265
|
1059 |
let
|
wneuper@59265
|
1060 |
val ctxt = get_ctxt pt pos
|
wneuper@59265
|
1061 |
val (pos, c, _, pt) =
|
wneuper@59271
|
1062 |
Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
|
wneuper@59265
|
1063 |
in (*FIXXXME: check if pbl can still be parsed*)
|
wneuper@59265
|
1064 |
([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
|
wneuper@59265
|
1065 |
(pt, pos))
|
wneuper@59265
|
1066 |
end
|
wneuper@59265
|
1067 |
| nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
|
wneuper@59265
|
1068 |
let
|
wneuper@59265
|
1069 |
val ctxt = get_ctxt pt pos
|
wneuper@59271
|
1070 |
val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
|
wneuper@59265
|
1071 |
in (*FIXXXME: check if met can still be parsed*)
|
wneuper@59265
|
1072 |
([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
|
wneuper@59265
|
1073 |
end
|
wneuper@59265
|
1074 |
| nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')
|
neuper@37906
|
1075 |
|
neuper@41982
|
1076 |
(* get the values from oris; handle the term list w.r.t. penv *)
|
neuper@37906
|
1077 |
fun vals_of_oris oris =
|
wneuper@59265
|
1078 |
((map (mkval' o (#5 : ori -> term list))) o
|
wneuper@59265
|
1079 |
(filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris
|
neuper@37906
|
1080 |
|
neuper@38056
|
1081 |
(* create a calc-tree with oris via an cas.refined pbl *)
|
neuper@38056
|
1082 |
fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
|
wneuper@59265
|
1083 |
if pI <> []
|
wneuper@59265
|
1084 |
then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
|
wneuper@59265
|
1085 |
let
|
wneuper@59269
|
1086 |
val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
|
wneuper@59265
|
1087 |
val dI = if dI = "" then theory2theory' thy else dI
|
wneuper@59265
|
1088 |
val mI = if mI = [] then hd met else mI
|
wneuper@59265
|
1089 |
val hdl = case cas of NONE => pblterm dI pI | SOME t => t
|
wneuper@59265
|
1090 |
val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
|
wneuper@59265
|
1091 |
([], (dI,pI,mI), hdl)
|
wneuper@59265
|
1092 |
val pt = update_spec pt [] (dI, pI, mI)
|
wneuper@59271
|
1093 |
val pits = Generate.init_pbl' ppc
|
wneuper@59265
|
1094 |
val pt = update_pbl pt [] pits
|
wneuper@59265
|
1095 |
in ((pt, ([] , Pbl)), []) : calcstate end
|
wneuper@59265
|
1096 |
else
|
wneuper@59265
|
1097 |
if mI <> []
|
wneuper@59265
|
1098 |
then (* from met-browser *)
|
neuper@41976
|
1099 |
let
|
wneuper@59269
|
1100 |
val {ppc, ...} = Specify.get_met mI
|
wneuper@59265
|
1101 |
val dI = if dI = "" then "Isac" else dI
|
wneuper@59265
|
1102 |
val (pt, _) =
|
wneuper@59265
|
1103 |
cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
|
wneuper@59265
|
1104 |
val pt = update_spec pt [] (dI, pI, mI)
|
wneuper@59271
|
1105 |
val mits = Generate.init_pbl' ppc
|
wneuper@59265
|
1106 |
val pt = update_met pt [] mits
|
wneuper@59265
|
1107 |
in ((pt, ([], Met)), []) end
|
wneuper@59265
|
1108 |
else (* new example, pepare for interactive modeling *)
|
wneuper@59265
|
1109 |
let
|
wneuper@59265
|
1110 |
val (pt, _) =
|
wneuper@59265
|
1111 |
cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
|
wneuper@59265
|
1112 |
in ((pt, ([], Pbl)), []) end
|
wneuper@59265
|
1113 |
| nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
|
wneuper@59265
|
1114 |
let (* both """"""""""""""""""""""""" either empty or complete *)
|
wneuper@59265
|
1115 |
val thy = assoc_thy dI
|
wneuper@59265
|
1116 |
val (pI, (pors, pctxt), mI) =
|
wneuper@59265
|
1117 |
if mI = ["no_met"]
|
wneuper@59265
|
1118 |
then
|
wneuper@59265
|
1119 |
let
|
wneuper@59269
|
1120 |
val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
|
wneuper@59269
|
1121 |
val pI' = Specify.refine_ori' pors pI;
|
wneuper@59265
|
1122 |
in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
|
wneuper@59269
|
1123 |
(hd o #met o Specify.get_pbt) pI')
|
wneuper@59265
|
1124 |
end
|
wneuper@59269
|
1125 |
else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
|
wneuper@59269
|
1126 |
val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
|
wneuper@59265
|
1127 |
val dI = theory2theory' (maxthy thy thy')
|
wneuper@59265
|
1128 |
val hdl = case cas of
|
wneuper@59265
|
1129 |
NONE => pblterm dI pI
|
wneuper@59265
|
1130 |
| SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
|
wneuper@59265
|
1131 |
val (pt, _) =
|
wneuper@59265
|
1132 |
cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
|
wneuper@59265
|
1133 |
val pt = update_ctxt pt [] pctxt
|
wneuper@59265
|
1134 |
in
|
wneuper@59265
|
1135 |
((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
|
wneuper@59265
|
1136 |
end
|
neuper@41976
|
1137 |
|
wneuper@59265
|
1138 |
fun get_spec_form m ((p, p_) : pos') pt =
|
wneuper@59265
|
1139 |
let val (_, _, f, _, _, _) = specify m (p, p_) [] pt
|
wneuper@59265
|
1140 |
in f end
|
neuper@37906
|
1141 |
|
wneuper@59265
|
1142 |
(* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
|
wneuper@59265
|
1143 |
(((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
|
neuper@37934
|
1144 |
fun tag_form thy (formal, given) =
|
neuper@52070
|
1145 |
(let
|
neuper@52070
|
1146 |
val gf = (head_of given) $ formal;
|
wneuper@59184
|
1147 |
val _ = Thm.global_cterm_of thy gf
|
neuper@52070
|
1148 |
in gf end)
|
neuper@52070
|
1149 |
handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
|
wneuper@59265
|
1150 |
" .. " ^ term_to_string''' thy formal ^ " ..types do not match")
|
neuper@38053
|
1151 |
|
neuper@37906
|
1152 |
fun chktyp thy (n, fs, gs) =
|
neuper@52070
|
1153 |
((writeln o (term_to_string''' thy) o (nth n)) fs;
|
neuper@52070
|
1154 |
(writeln o (term_to_string''' thy) o (nth n)) gs;
|
wneuper@59265
|
1155 |
tag_form thy (nth n fs, nth n gs))
|
wneuper@59265
|
1156 |
fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
|
neuper@37906
|
1157 |
|
neuper@37906
|
1158 |
(* check pbltypes, announces one failure a time *)
|
neuper@37930
|
1159 |
fun chk_vars ctppc =
|
wneuper@59265
|
1160 |
let
|
wneuper@59269
|
1161 |
val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
|
wneuper@59265
|
1162 |
val chked = subtract op = gi wh
|
wneuper@59265
|
1163 |
in
|
wneuper@59265
|
1164 |
if chked <> [] then ("wh\\gi", chked)
|
wneuper@59265
|
1165 |
else
|
wneuper@59265
|
1166 |
let val chked = subtract op = (union op = gi fi) re
|
wneuper@59265
|
1167 |
in
|
wneuper@59265
|
1168 |
if chked <> []
|
wneuper@59265
|
1169 |
then ("re\\(gi union fi)", chked)
|
wneuper@59265
|
1170 |
else ("ok", [])
|
wneuper@59265
|
1171 |
end
|
wneuper@59265
|
1172 |
end
|
neuper@37906
|
1173 |
|
neuper@37906
|
1174 |
(* check a new pbltype: variables (Free) unbound by given, find*)
|
neuper@37906
|
1175 |
fun unbound_ppc ctppc =
|
wneuper@59265
|
1176 |
let
|
wneuper@59269
|
1177 |
val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
|
wneuper@59265
|
1178 |
in
|
wneuper@59265
|
1179 |
distinct (subtract op = (union op = gi fi) re)
|
wneuper@59265
|
1180 |
end
|
neuper@37906
|
1181 |
|
wneuper@59265
|
1182 |
(* f, a binary operator, is nested right associative *)
|
neuper@37906
|
1183 |
fun foldr1 f xs =
|
neuper@37906
|
1184 |
let
|
wneuper@59265
|
1185 |
fun fld _ (x :: []) = x
|
wneuper@59265
|
1186 |
| fld f (x :: x' :: []) = f (x', x)
|
wneuper@59265
|
1187 |
| fld f (x :: x' :: xs) = f (fld f (x' :: xs), x)
|
wneuper@59265
|
1188 |
| fld _ _ = error "foldr1 uncovered definition"
|
wneuper@59265
|
1189 |
in ((fld f) o rev) xs end
|
neuper@37906
|
1190 |
|
neuper@37906
|
1191 |
(* f, a binary operator, is nested leftassociative *)
|
wneuper@59265
|
1192 |
fun foldl1 _ (x :: []) = x
|
wneuper@59265
|
1193 |
| foldl1 f (x :: x' :: []) = f (x, x')
|
wneuper@59265
|
1194 |
| foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs))
|
wneuper@59265
|
1195 |
| foldl1 _ _ = error "foldl1 uncovered definition"
|
neuper@37906
|
1196 |
|
neuper@37906
|
1197 |
(* called only once, if a Subproblem has been located in the script*)
|
wneuper@59265
|
1198 |
fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
|
wneuper@59265
|
1199 |
(case metID of
|
wneuper@59265
|
1200 |
["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
|
wneuper@59265
|
1201 |
| _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
|
wneuper@59265
|
1202 |
(*all stored in tac_ itms^^^^^^^^^^*)
|
wneuper@59265
|
1203 |
| nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_)
|
neuper@37906
|
1204 |
|
wneuper@59265
|
1205 |
(* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *)
|
wneuper@59265
|
1206 |
fun eq4 v (_, vts, _, _, _) = member op = vts v
|
wneuper@59265
|
1207 |
fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d
|
neuper@37906
|
1208 |
|
wneuper@59265
|
1209 |
(* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
|
wneuper@59265
|
1210 |
+ met from fmz; assumes pos on PblObj, meth = [] *)
|
wneuper@59265
|
1211 |
fun complete_mod (pt, pos as (p, p_) : pos') =
|
wneuper@59265
|
1212 |
let
|
wneuper@59265
|
1213 |
val _ = if p_ <> Pbl
|
wneuper@59265
|
1214 |
then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
|
wneuper@59265
|
1215 |
else ()
|
wneuper@59265
|
1216 |
val (oris, ospec, probl, spec) = case get_obj I pt p of
|
wneuper@59265
|
1217 |
PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
|
wneuper@59265
|
1218 |
| _ => error "complete_mod: unvered case get_obj"
|
wneuper@59265
|
1219 |
val (_, pI, mI) = some_spec ospec spec
|
wneuper@59269
|
1220 |
val mpc = (#ppc o Specify.get_met) mI
|
wneuper@59269
|
1221 |
val ppc = (#ppc o Specify.get_pbt) pI
|
wneuper@59265
|
1222 |
val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
|
wneuper@59265
|
1223 |
val pt = update_pblppc pt p pits
|
wneuper@59265
|
1224 |
val pt = update_metppc pt p mits
|
wneuper@59265
|
1225 |
in (pt, (p, Met) : pos') end
|
neuper@37906
|
1226 |
|
neuper@37906
|
1227 |
(*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
|
neuper@37906
|
1228 |
oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
|
wneuper@59265
|
1229 |
fun all_modspec (pt, (p, _) : pos') =
|
wneuper@59265
|
1230 |
let
|
wneuper@59265
|
1231 |
val (pors, dI, pI, mI) = case get_obj I pt p of
|
wneuper@59265
|
1232 |
PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
|
wneuper@59265
|
1233 |
| _ => error "all_modspec: uncovered case get_obj"
|
wneuper@59269
|
1234 |
val {ppc, ...} = Specify.get_met mI
|
wneuper@59265
|
1235 |
val (_, vals) = oris2fmz_vals pors
|
neuper@48761
|
1236 |
val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
|
neuper@42092
|
1237 |
|> declare_constraints' vals
|
wneuper@59265
|
1238 |
val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
|
wneuper@59265
|
1239 |
val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
|
wneuper@59265
|
1240 |
val pt = update_spec pt p (dI, pI, mI)
|
neuper@42092
|
1241 |
val pt = update_ctxt pt p ctxt
|
wneuper@59265
|
1242 |
in
|
wneuper@59265
|
1243 |
(pt, (p, Met) : pos')
|
wneuper@59265
|
1244 |
end
|
neuper@37906
|
1245 |
|
wneuper@59265
|
1246 |
(* WN0312: use in nxt_spec, too ? what about variants ??? *)
|
wneuper@59265
|
1247 |
fun is_complete_mod_ ([] : itm list) = false
|
wneuper@59265
|
1248 |
| is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
|
neuper@41976
|
1249 |
|
wneuper@59265
|
1250 |
fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
|
wneuper@59265
|
1251 |
if (is_pblobj o (get_obj I pt)) p
|
wneuper@59265
|
1252 |
then (is_complete_mod_ o (get_obj g_pbl pt)) p
|
wneuper@59265
|
1253 |
else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
|
neuper@37906
|
1254 |
| is_complete_mod (pt, pos as (p, Met)) =
|
wneuper@59265
|
1255 |
if (is_pblobj o (get_obj I pt)) p
|
wneuper@59265
|
1256 |
then (is_complete_mod_ o (get_obj g_met pt)) p
|
wneuper@59265
|
1257 |
else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
|
neuper@37906
|
1258 |
| is_complete_mod (_, pos) =
|
wneuper@59265
|
1259 |
error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
|
neuper@37906
|
1260 |
|
wneuper@59265
|
1261 |
(* have (thy, pbl, met) _all_ been specified explicitly ? *)
|
wneuper@59265
|
1262 |
fun is_complete_spec (pt, pos as (p, _) : pos') =
|
wneuper@59265
|
1263 |
if (not o is_pblobj o (get_obj I pt)) p
|
wneuper@59265
|
1264 |
then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
|
wneuper@59265
|
1265 |
else
|
wneuper@59265
|
1266 |
let val (dI,pI,mI) = get_obj g_spec pt p
|
wneuper@59265
|
1267 |
in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end
|
neuper@37906
|
1268 |
|
wneuper@59265
|
1269 |
(* complete empty items in specification from origin (pbl, met ev.refined);
|
wneuper@59265
|
1270 |
assumes 'is_complete_mod' *)
|
wneuper@59265
|
1271 |
fun complete_spec (pt, pos as (p, _) : pos') =
|
wneuper@59265
|
1272 |
let
|
wneuper@59265
|
1273 |
val (ospec, spec) = case get_obj I pt p of
|
wneuper@59265
|
1274 |
PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
|
wneuper@59265
|
1275 |
| _ => error "complete_spec: uncovered case get_obj"
|
wneuper@59265
|
1276 |
val pt = update_spec pt p (some_spec ospec spec)
|
wneuper@59265
|
1277 |
in
|
wneuper@59265
|
1278 |
(pt, pos)
|
wneuper@59265
|
1279 |
end
|
neuper@37906
|
1280 |
|
wneuper@59265
|
1281 |
fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
|
neuper@37906
|
1282 |
|
wneuper@59265
|
1283 |
fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
|
wneuper@59265
|
1284 |
let
|
wneuper@59265
|
1285 |
val (_, _, metID) = get_somespec' spec spec'
|
wneuper@59265
|
1286 |
val pre = if metID = e_metID then []
|
wneuper@59265
|
1287 |
else
|
wneuper@59265
|
1288 |
let
|
wneuper@59269
|
1289 |
val {prls, pre= where_, ...} = Specify.get_met metID
|
wneuper@59265
|
1290 |
val pre = check_preconds' prls where_ meth 0
|
wneuper@59265
|
1291 |
in pre end
|
wneuper@59265
|
1292 |
val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
|
wneuper@59265
|
1293 |
in
|
wneuper@59265
|
1294 |
ModSpec (allcorrect, Met, hdl, meth, pre, spec)
|
wneuper@59265
|
1295 |
end
|
wneuper@59265
|
1296 |
| pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
|
wneuper@59265
|
1297 |
let
|
wneuper@59265
|
1298 |
val (_, pI, _) = get_somespec' spec spec'
|
wneuper@59265
|
1299 |
val pre = if pI = e_pblID then []
|
wneuper@59265
|
1300 |
else
|
wneuper@59265
|
1301 |
let
|
wneuper@59269
|
1302 |
val {prls, where_, ...} = Specify.get_pbt pI
|
wneuper@59265
|
1303 |
val pre = check_preconds' prls where_ probl 0
|
wneuper@59265
|
1304 |
in pre end
|
wneuper@59265
|
1305 |
val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
|
wneuper@59265
|
1306 |
in
|
wneuper@59265
|
1307 |
ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
|
wneuper@59265
|
1308 |
end
|
wneuper@59265
|
1309 |
| pt_model _ _ = error "pt_model: uncovered definition"
|
neuper@37906
|
1310 |
|
wneuper@59265
|
1311 |
fun pt_form (PrfObj {form, ...}) = Form form
|
wneuper@59265
|
1312 |
| pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
|
wneuper@59265
|
1313 |
let
|
wneuper@59265
|
1314 |
val (dI, pI, _) = get_somespec' spec spec'
|
wneuper@59269
|
1315 |
val {cas, ...} = Specify.get_pbt pI
|
wneuper@59265
|
1316 |
in case cas of
|
wneuper@59265
|
1317 |
NONE => Form (pblterm dI pI)
|
wneuper@59265
|
1318 |
| SOME t => Form (subst_atomic (mk_env probl) t)
|
wneuper@59265
|
1319 |
end
|
neuper@37906
|
1320 |
|
wneuper@59265
|
1321 |
(* pt_extract returns
|
neuper@37906
|
1322 |
# the formula at pos
|
neuper@37906
|
1323 |
# the tactic applied to this formula
|
neuper@37906
|
1324 |
# the list of assumptions generated at this formula
|
neuper@37906
|
1325 |
(by application of another tac to the preceding formula !)
|
wneuper@59265
|
1326 |
pos is assumed to come from the frontend, ie. generated by moveDown.
|
wneuper@59265
|
1327 |
Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
|
wneuper@59265
|
1328 |
TODO 110417 get assumptions from ctxt !?
|
wneuper@59265
|
1329 |
*)
|
wneuper@59265
|
1330 |
fun pt_extract (pt, ([], Res)) =
|
wneuper@59265
|
1331 |
(* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
|
wneuper@59265
|
1332 |
let
|
wneuper@59265
|
1333 |
val (f, asm) = get_obj g_result pt []
|
wneuper@59265
|
1334 |
in (Form f, NONE, asm) end
|
neuper@37906
|
1335 |
| pt_extract (pt,(p,Res)) =
|
wneuper@59265
|
1336 |
let
|
wneuper@59265
|
1337 |
val (f, asm) = get_obj g_result pt p
|
wneuper@59265
|
1338 |
val tac =
|
wneuper@59265
|
1339 |
if last_onlev pt p
|
wneuper@59265
|
1340 |
then
|
wneuper@59265
|
1341 |
if is_pblobj' pt (lev_up p)
|
neuper@42437
|
1342 |
then
|
wneuper@59265
|
1343 |
let
|
wneuper@59265
|
1344 |
val pI = case get_obj I pt (lev_up p) of
|
wneuper@59265
|
1345 |
PblObj{spec = (_, pI, _), ...} => pI
|
wneuper@59265
|
1346 |
| _ => error "pt_extract last_onlev: uncovered case get_obj"
|
wneuper@59265
|
1347 |
in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
|
wneuper@59265
|
1348 |
else SOME End_Trans (* WN0502 TODO for other branches *)
|
wneuper@59265
|
1349 |
else
|
wneuper@59265
|
1350 |
let val p' = lev_on p
|
wneuper@59265
|
1351 |
in
|
wneuper@59265
|
1352 |
if is_pblobj' pt p'
|
wneuper@59265
|
1353 |
then
|
wneuper@59265
|
1354 |
let
|
wneuper@59265
|
1355 |
val (dI ,pI) = case get_obj I pt p' of
|
wneuper@59265
|
1356 |
PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
|
wneuper@59265
|
1357 |
| _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
|
wneuper@59265
|
1358 |
in SOME (Subproblem (dI, pI)) end
|
wneuper@59265
|
1359 |
else
|
wneuper@59265
|
1360 |
if f = get_obj g_form pt p'
|
wneuper@59265
|
1361 |
then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
|
wneuper@59265
|
1362 |
else SOME (Take (term2str (get_obj g_form pt p')))
|
wneuper@59265
|
1363 |
end
|
wneuper@59265
|
1364 |
in (Form f, tac, asm) end
|
wneuper@59265
|
1365 |
| pt_extract (pt, (p,p_(*Frm,Pbl*))) =
|
neuper@42437
|
1366 |
let
|
neuper@42437
|
1367 |
val ppobj = get_obj I pt p
|
neuper@42437
|
1368 |
val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
|
neuper@42437
|
1369 |
val tac = g_tac ppobj
|
wneuper@59265
|
1370 |
in (f, SOME tac, []) end
|
neuper@37906
|
1371 |
|
wneuper@59265
|
1372 |
(** get the formula from a ctree-node:
|
wneuper@59265
|
1373 |
take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
|
wneuper@59265
|
1374 |
take res from all other PrfObj's
|
wneuper@59265
|
1375 |
Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
|
wneuper@59265
|
1376 |
fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
|
wneuper@59265
|
1377 |
[("headline", (p, Frm), h), ("stepform", (p, Res), r)]
|
wneuper@59265
|
1378 |
| formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
|
wneuper@59265
|
1379 |
[("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
|
wneuper@59265
|
1380 |
| formres _ _ = error "formres: uncovered definition"
|
wneuper@59265
|
1381 |
fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
|
wneuper@59265
|
1382 |
[("stepform", (p, Res), r)]
|
wneuper@59265
|
1383 |
| form _ _ = error "form: uncovered definition"
|
neuper@37906
|
1384 |
|
wneuper@59265
|
1385 |
(* assumes to take whole level, in particular hd -- for use in interSteps *)
|
wneuper@59265
|
1386 |
fun get_formress fs _ [] = flat fs
|
neuper@37906
|
1387 |
| get_formress fs p (nd::nds) =
|
neuper@37906
|
1388 |
(* start with 'form+res' and continue with trying 'res' only*)
|
neuper@37906
|
1389 |
get_forms (fs @ [formres p nd]) (lev_on p) nds
|
wneuper@59265
|
1390 |
and get_forms fs _ [] = flat fs
|
neuper@37906
|
1391 |
| get_forms fs p (nd::nds) =
|
neuper@37906
|
1392 |
if is_pblnd nd
|
neuper@37906
|
1393 |
(* start again with 'form+res' ///ugly repeat with Check_elementwise
|
neuper@37906
|
1394 |
then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
|
neuper@37906
|
1395 |
then get_forms (fs @ [formres p nd]) (lev_on p) nds
|
neuper@37906
|
1396 |
(* continue with trying 'res' only*)
|
neuper@37906
|
1397 |
else get_forms (fs @ [form p nd]) (lev_on p) nds;
|
neuper@37906
|
1398 |
|
wneuper@59265
|
1399 |
(** get an 'interval' 'from' 'to' of formulae from a ptree **)
|
wneuper@59265
|
1400 |
(* WN0401 this functionality belongs to ctree.sml *)
|
wneuper@59265
|
1401 |
fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
|
wneuper@59265
|
1402 |
| eq_pos' (p1, Res) (p2, Res) = p1 = p2
|
wneuper@59265
|
1403 |
| eq_pos' (p1, Pbl) (p2, p2_) =
|
wneuper@59265
|
1404 |
p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
|
wneuper@59265
|
1405 |
| eq_pos' (p1, Met) (p2, p2_) =
|
wneuper@59265
|
1406 |
p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
|
neuper@37906
|
1407 |
| eq_pos' _ _ = false;
|
neuper@37906
|
1408 |
|
wneuper@59265
|
1409 |
(* get an 'interval' from the ctree; 'interval' is w.r.t. the
|
neuper@37906
|
1410 |
total ordering Position#compareTo(Position p) in the java-code
|
neuper@37906
|
1411 |
val get_interval = fn
|
neuper@37906
|
1412 |
: pos' -> : from is "move_up 1st-element" to return
|
neuper@37906
|
1413 |
pos' -> : to the last element to be returned; from < to
|
neuper@37906
|
1414 |
int -> : level: 0 gets the flattest sub-tree possible
|
neuper@37906
|
1415 |
>999 gets the deepest sub-tree possible
|
neuper@37906
|
1416 |
ptree -> :
|
neuper@37906
|
1417 |
(pos' * : of the formula
|
neuper@37906
|
1418 |
Term.term) : the formula
|
wneuper@59265
|
1419 |
list *)
|
neuper@37906
|
1420 |
fun get_interval from to level pt =
|
neuper@42432
|
1421 |
let
|
wneuper@59265
|
1422 |
fun get_inter c (from : pos') (to : pos') lev pt =
|
wneuper@59265
|
1423 |
if eq_pos' from to orelse from = ([], Res)
|
neuper@42432
|
1424 |
then
|
wneuper@59265
|
1425 |
let val (f, _, _) = pt_extract (pt, from)
|
wneuper@59265
|
1426 |
in case f of
|
wneuper@59265
|
1427 |
ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)]
|
wneuper@59265
|
1428 |
| Form t => c @ [(from, t)]
|
neuper@42432
|
1429 |
end
|
neuper@37906
|
1430 |
else
|
neuper@42432
|
1431 |
if lev < lev_of from
|
neuper@42432
|
1432 |
then (get_inter c (move_dn [] pt from) to lev pt)
|
neuper@42432
|
1433 |
handle (PTREE _(*from move_dn too far*)) => c
|
neuper@42432
|
1434 |
else
|
neuper@42432
|
1435 |
let
|
wneuper@59265
|
1436 |
val (f, _, _) = pt_extract (pt, from)
|
neuper@42432
|
1437 |
val term = case f of
|
neuper@42432
|
1438 |
ModSpec (_,_,headline,_,_,_) => headline
|
neuper@42432
|
1439 |
| Form t => t
|
neuper@42432
|
1440 |
in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
|
neuper@42432
|
1441 |
handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
|
neuper@42432
|
1442 |
end
|
wneuper@59265
|
1443 |
in get_inter [] from to level pt end
|
neuper@37906
|
1444 |
|
wneuper@59265
|
1445 |
(* for tests *)
|
wneuper@59265
|
1446 |
fun posform2str (pos : pos', form) =
|
wneuper@59265
|
1447 |
"(" ^ pos'2str pos ^ ", " ^
|
wneuper@59265
|
1448 |
(case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^
|
wneuper@59265
|
1449 |
")"
|
wneuper@59265
|
1450 |
fun posforms2str pfs =
|
wneuper@59265
|
1451 |
(strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs
|
wneuper@59265
|
1452 |
fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"
|
wneuper@59265
|
1453 |
fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
|
neuper@37906
|
1454 |
|
wneuper@59265
|
1455 |
(* WN050225 omits the last step, if pt is incomplete *)
|
wneuper@59265
|
1456 |
fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
|
neuper@37906
|
1457 |
|
wneuper@59265
|
1458 |
(* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
|
wneuper@59265
|
1459 |
fun get_ocalhd (pt, (p, Pbl) : pos') =
|
wneuper@59265
|
1460 |
let
|
wneuper@59265
|
1461 |
val (ospec, hdf', spec, probl) = case get_obj I pt p of
|
wneuper@59265
|
1462 |
PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
|
wneuper@59265
|
1463 |
| _ => error "get_ocalhd Pbl: uncovered case get_obj"
|
wneuper@59269
|
1464 |
val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
|
wneuper@59265
|
1465 |
val pre = check_preconds (assoc_thy"Isac") prls where_ probl
|
wneuper@59265
|
1466 |
in
|
wneuper@59265
|
1467 |
(ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
|
wneuper@59265
|
1468 |
end
|
wneuper@59265
|
1469 |
| get_ocalhd (pt, (p, Met)) =
|
wneuper@59265
|
1470 |
let
|
wneuper@59265
|
1471 |
val (ospec, hdf', spec, meth) = case get_obj I pt p of
|
wneuper@59265
|
1472 |
PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
|
wneuper@59265
|
1473 |
| _ => error "get_ocalhd Met: uncovered case get_obj"
|
wneuper@59269
|
1474 |
val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
|
wneuper@59265
|
1475 |
val pre = check_preconds (assoc_thy"Isac") prls pre meth
|
wneuper@59265
|
1476 |
in
|
wneuper@59265
|
1477 |
(ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
|
wneuper@59265
|
1478 |
end
|
wneuper@59265
|
1479 |
| get_ocalhd _ = error "get_ocalhd: uncovered definition"
|
neuper@37906
|
1480 |
|
wneuper@59265
|
1481 |
(* at the activeFormula set the Model, the Guard and the Specification
|
wneuper@59265
|
1482 |
to empty and return a CalcHead;
|
wneuper@59265
|
1483 |
the 'origin' remains (for reconstructing all that) *)
|
wneuper@59265
|
1484 |
fun reset_calchead (pt, (p,_) : pos') =
|
wneuper@59265
|
1485 |
let
|
wneuper@59265
|
1486 |
val () = case get_obj I pt p of
|
wneuper@59265
|
1487 |
PblObj _ => ()
|
wneuper@59265
|
1488 |
| _ => error "reset_calchead: uncovered case get_obj"
|
wneuper@59265
|
1489 |
val pt = update_pbl pt p []
|
wneuper@59265
|
1490 |
val pt = update_met pt p []
|
wneuper@59265
|
1491 |
val pt = update_spec pt p e_spec
|
wneuper@59265
|
1492 |
in (pt, (p, Pbl) : pos') end
|
neuper@37906
|
1493 |
|
wneuper@59265
|
1494 |
end |