walther@59960
|
1 |
(* Title: Specify/refine.sml
|
walther@59960
|
2 |
Author: Walther Neuper 110226
|
walther@59960
|
3 |
(c) due to copyright terms
|
walther@59960
|
4 |
|
walther@59960
|
5 |
Operations on models.
|
walther@59960
|
6 |
*)
|
walther@59960
|
7 |
|
walther@59960
|
8 |
signature REFINE_PROBLEM =
|
walther@59960
|
9 |
sig
|
walther@59968
|
10 |
val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
|
walther@59968
|
11 |
|
walther@59968
|
12 |
val refine_ori : O_Model.T -> Problem.id -> Problem.id option
|
walther@59968
|
13 |
val refine_ori' : O_Model.T -> Problem.id -> Problem.id
|
walther@59960
|
14 |
|
walther@59960
|
15 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59968
|
16 |
val refine : Formalise.model -> Problem.id -> Model.match list
|
walther@59960
|
17 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59960
|
18 |
(*NONE*)
|
walther@59960
|
19 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59960
|
20 |
end
|
walther@59960
|
21 |
|
walther@59965
|
22 |
(**)
|
walther@59960
|
23 |
structure Refine(**) : REFINE_PROBLEM(**) =
|
walther@59960
|
24 |
struct
|
walther@59965
|
25 |
(**)
|
walther@59960
|
26 |
|
walther@59960
|
27 |
datatype match_ =
|
walther@59963
|
28 |
Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
|
walther@59960
|
29 |
| NoMatch_;
|
walther@59960
|
30 |
|
walther@59960
|
31 |
fun is_matches_ (Match_ _) = true
|
walther@59960
|
32 |
| is_matches_ _ = false;
|
walther@59960
|
33 |
|
walther@59960
|
34 |
fun refined_ ms = ((find_first is_matches_) o rev) ms;
|
walther@59960
|
35 |
|
walther@59960
|
36 |
fun eq1 d (_, (d', _)) = (d = d');
|
walther@59960
|
37 |
|
walther@59960
|
38 |
fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
|
walther@59960
|
39 |
(case find_first (eq1 d) pbt of
|
walther@59960
|
40 |
SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
|
walther@59960
|
41 |
| NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
|
walther@59960
|
42 |
| chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
|
walther@59960
|
43 |
(case find_first (eq1 d) pbt of
|
walther@59960
|
44 |
SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
|
walther@59960
|
45 |
| NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
|
walther@59960
|
46 |
| chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
|
walther@59960
|
47 |
| chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
|
walther@59960
|
48 |
| chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
|
walther@59960
|
49 |
(case find_first (eq1 d) pbt of
|
walther@59960
|
50 |
SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, I_Model.pbl_ids' d vs)))
|
walther@59960
|
51 |
| NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
|
walther@59960
|
52 |
| chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
|
walther@59960
|
53 |
(case find_first (eq1 d) pbt of
|
walther@59962
|
54 |
SOME (_, _) => raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, I_Model.pbl_ids' d vs))):itm)"
|
walther@59960
|
55 |
| NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
|
walther@59960
|
56 |
| chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
|
walther@59960
|
57 |
|
walther@59960
|
58 |
fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
|
walther@59960
|
59 |
fun eq0 (0, _, _, _, _) = true
|
walther@59960
|
60 |
| eq0 _ = false;
|
walther@59960
|
61 |
fun max_i i [] = i
|
walther@59960
|
62 |
| max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
|
walther@59960
|
63 |
fun max_id [] = 0
|
walther@59960
|
64 |
| max_id ((id, _, _, _, _) :: is) = max_i id is;
|
walther@59960
|
65 |
fun add_idvat itms _ _ [] = itms
|
walther@59960
|
66 |
| add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
|
walther@59960
|
67 |
add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
|
walther@59960
|
68 |
|
walther@59960
|
69 |
(* find elements of pbt not contained in itms;
|
walther@59960
|
70 |
if such one is untouched, return this one, otherwise create new itm *)
|
walther@59960
|
71 |
fun chk_m itms untouched (p as (f, (d, id))) =
|
walther@59960
|
72 |
case find_first (eq2 p) itms of
|
walther@59960
|
73 |
SOME _ => []
|
walther@59960
|
74 |
| NONE =>
|
walther@59960
|
75 |
(case find_first (eq2 p) untouched of
|
walther@59960
|
76 |
SOME itm => [itm]
|
walther@59960
|
77 |
| NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
|
walther@59960
|
78 |
|
walther@59960
|
79 |
fun chk_mis mvat itms untouched pbt =
|
walther@59960
|
80 |
let val mis = (flat o (map (chk_m itms untouched))) pbt;
|
walther@59960
|
81 |
val mid = max_id itms;
|
walther@59960
|
82 |
in add_idvat [] (mid + 1) mvat mis end;
|
walther@59960
|
83 |
|
walther@59960
|
84 |
(* check a problem (ie. itm list) for matching a problemtype,
|
walther@59960
|
85 |
takes the I_Model.max_vt for concluding completeness (could be another!) *)
|
walther@59960
|
86 |
fun match_itms thy itms (pbt, pre, prls) =
|
walther@59960
|
87 |
let
|
walther@59960
|
88 |
fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
|
walther@59960
|
89 |
val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
|
walther@59960
|
90 |
val mvat = I_Model.max_vt itms';
|
walther@59960
|
91 |
val itms'' = filter (okv mvat) itms';
|
walther@59960
|
92 |
val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
|
walther@59960
|
93 |
val mis = chk_mis mvat itms'' untouched pbt;
|
walther@59960
|
94 |
val pre' = Pre_Conds.check prls pre itms'' mvat
|
walther@59960
|
95 |
val pb = foldl and_ (true, map fst pre')
|
walther@59960
|
96 |
in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
|
walther@59960
|
97 |
|
walther@59960
|
98 |
(* refine a problem; version for tactic Refine_Problem *)
|
walther@59960
|
99 |
fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
|
walther@59960
|
100 |
let
|
walther@59960
|
101 |
val {thy, ppc, where_, prls, ...} = py
|
walther@59960
|
102 |
val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
|
walther@59960
|
103 |
in
|
walther@59960
|
104 |
if b
|
walther@59960
|
105 |
then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
|
walther@59960
|
106 |
else pbls @ [NoMatch_]
|
walther@59960
|
107 |
end
|
walther@59960
|
108 |
| refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
|
walther@59960
|
109 |
let
|
walther@59960
|
110 |
val {thy, ppc, where_, prls, ...} = py
|
walther@59960
|
111 |
val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
|
walther@59960
|
112 |
in if b
|
walther@59960
|
113 |
then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
|
walther@59960
|
114 |
in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
|
walther@59960
|
115 |
else (pbls @ [NoMatch_])
|
walther@59960
|
116 |
end
|
walther@59965
|
117 |
| refin'' _ _ _ _ _ = raise ERROR "refin'': uncovered fun def."
|
walther@59960
|
118 |
and refins'' _ _ _ pbls [] = pbls
|
walther@59960
|
119 |
| refins'' thy pblRD itms pbls ((p as Store.Node _) :: pts) =
|
walther@59960
|
120 |
let
|
walther@59960
|
121 |
val pbls' = refin'' thy pblRD itms pbls p
|
walther@59960
|
122 |
in case last_elem pbls' of
|
walther@59960
|
123 |
Match_ _ => pbls'
|
walther@59960
|
124 |
| NoMatch_ => refins'' thy pblRD itms pbls' pts
|
walther@59960
|
125 |
end;
|
walther@59960
|
126 |
|
walther@59960
|
127 |
fun problem thy pblID itms =
|
walther@59960
|
128 |
case refined_ ((Store.apply (get_ptyps ())) (refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) of
|
walther@59960
|
129 |
NONE => NONE
|
walther@59960
|
130 |
| SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
|
walther@59960
|
131 |
| _ => raise ERROR "Refine.problem: uncovered case refined_";
|
walther@59960
|
132 |
|
walther@59968
|
133 |
(* refine a problem; construct pblRD while scanning *)
|
walther@59968
|
134 |
fun refin pblRD ori (Store.Node (pI, [py], [])) =
|
walther@59968
|
135 |
if Model.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
|
walther@59968
|
136 |
then SOME (pblRD @ [pI])
|
walther@59968
|
137 |
else NONE
|
walther@59968
|
138 |
| refin pblRD ori (Store.Node (pI, [py], pys)) =
|
walther@59968
|
139 |
if Model.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
|
walther@59968
|
140 |
then (case refins (pblRD @ [pI]) ori pys of
|
walther@59968
|
141 |
SOME pblRD' => SOME pblRD'
|
walther@59968
|
142 |
| NONE => SOME (pblRD @ [pI]))
|
walther@59968
|
143 |
else NONE
|
walther@59968
|
144 |
| refin _ _ _ = raise ERROR "refin: uncovered fun def."
|
walther@59968
|
145 |
and refins _ _ [] = NONE
|
walther@59968
|
146 |
| refins pblRD ori ((p as Store.Node _) :: pts) =
|
walther@59968
|
147 |
(case refin pblRD ori p of
|
walther@59968
|
148 |
SOME pblRD' => SOME pblRD'
|
walther@59968
|
149 |
| NONE => refins pblRD ori pts);
|
walther@59968
|
150 |
|
walther@59968
|
151 |
(* refine a problem; version providing output for math-experts *)
|
walther@59968
|
152 |
fun refin' pblRD fmz pbls (Store.Node (pI, [py], [])) =
|
walther@59968
|
153 |
let
|
walther@59968
|
154 |
val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
|
walther@59968
|
155 |
val {thy, ppc, where_, prls, ...} = py
|
walther@59968
|
156 |
val oris = O_Model.init fmz thy ppc(* |> #1*);
|
walther@59968
|
157 |
(* WN020803: itms!: oris might _not_ be complete here *)
|
walther@59968
|
158 |
val (b, (itms, pre')) = Model.match_oris' thy oris (ppc, where_, prls)
|
walther@59968
|
159 |
in
|
walther@59968
|
160 |
if b
|
walther@59969
|
161 |
then pbls @ [Model.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
|
walther@59969
|
162 |
else pbls @ [Model.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
|
walther@59968
|
163 |
end
|
walther@59968
|
164 |
| refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
|
walther@59968
|
165 |
let
|
walther@59968
|
166 |
val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
|
walther@59968
|
167 |
val {thy, ppc, where_, prls, ...} = py
|
walther@59968
|
168 |
val oris = O_Model.init fmz thy ppc(* |> #1*);
|
walther@59968
|
169 |
(* WN020803: itms!: oris might _not_ be complete here *)
|
walther@59968
|
170 |
val(b, (itms, pre')) = Model.match_oris' thy oris (ppc,where_,prls);
|
walther@59968
|
171 |
in
|
walther@59968
|
172 |
if b
|
walther@59968
|
173 |
then
|
walther@59969
|
174 |
let val pbl = Model.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
|
walther@59968
|
175 |
in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
|
walther@59969
|
176 |
else (pbls @ [Model.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
|
walther@59968
|
177 |
end
|
walther@59968
|
178 |
| refin' _ _ _ _ = raise ERROR "refin': uncovered fun def."
|
walther@59968
|
179 |
and refins' _ _ pbls [] = pbls
|
walther@59968
|
180 |
| refins' pblRD fmz pbls ((p as Store.Node _) :: pts) =
|
walther@59968
|
181 |
let
|
walther@59968
|
182 |
val pbls' = refin' pblRD fmz pbls p
|
walther@59968
|
183 |
in
|
walther@59968
|
184 |
case last_elem pbls' of
|
walther@59968
|
185 |
Model.Matches _ => pbls'
|
walther@59968
|
186 |
| Model.NoMatch _ => refins' pblRD fmz pbls' pts
|
walther@59968
|
187 |
end;
|
walther@59968
|
188 |
|
walther@59968
|
189 |
(* apply a fun to a ptyps node *)
|
walther@59968
|
190 |
fun app_ptyp x = Store.apply (get_ptyps ()) x;
|
walther@59968
|
191 |
|
walther@59968
|
192 |
(* for tactic Refine_Tacitly
|
walther@59968
|
193 |
oris are already created wrt. some pbt; pbt contains thy for parsing *)
|
walther@59968
|
194 |
fun refine_ori oris pblID =
|
walther@59968
|
195 |
let
|
walther@59968
|
196 |
val opt = app_ptyp (refin ((rev o tl) pblID) oris) pblID (rev pblID);
|
walther@59968
|
197 |
in case opt of
|
walther@59968
|
198 |
SOME pblRD =>
|
walther@59968
|
199 |
let val pblID': Problem.id = rev pblRD
|
walther@59968
|
200 |
in if pblID' = pblID then NONE else SOME pblID' end
|
walther@59968
|
201 |
| NONE => NONE
|
walther@59968
|
202 |
end;
|
walther@59969
|
203 |
fun refine_ori' oris pI = perhaps (refine_ori oris) pI;
|
walther@59968
|
204 |
|
walther@59968
|
205 |
(* for math-authoring and test; TODO: needs thy for parsing fmz *)
|
walther@59968
|
206 |
fun refine fmz pblID =
|
walther@59968
|
207 |
app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID);
|
walther@59968
|
208 |
|
walther@59965
|
209 |
(**)end(**)
|