1 (* Title: Specify/refine.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close>
6 better fitting the respective where_-condition.
8 The search on the tree given by @{term Know_Store.get_pbls} is costly such that
9 \<open>ML_structure Know_Store\<close> holds terms pre-parsed with a most generally type.
11 On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type
12 (and users of this function in \<open>ML_structure Error_Pattern, MethodC, Problem\<close>)
13 according to the current context.
15 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
16 are adapted for "adapt_to_type on the fly" until further clarification.
18 timing (from evaluating imports to use-cases.sml) for Test_Isac_Short
19 before adapt_to_type: 01:05 sec:sec
21 timing for test/../refine.sml --- equation with CalcTree [ = 6 / 5] for timing: ...
22 before adapt_to_type: 1.5 sec
24 timing for test/../refine.sml --- refine ad-hoc equation for timing: ...
25 before adapt_to_type: 0.05 sec
29 signature REFINE_PROBLEM =
32 val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
34 val by_o_model : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
35 val by_o_model' : Proof.context -> O_Model.T -> Problem.id -> Problem.id
36 val by_formalise: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list
38 (*from isac_test for Minisubpbl*)
39 datatype match_model_prec = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_;
40 val find_match: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node -> match_model_prec list
41 val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
42 val check_match: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
45 val match_found: match_model_prec list -> match_model_prec option
46 val find_matchs: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node list -> match_model_prec list
51 structure Refine(**) : REFINE_PROBLEM(**) =
55 datatype match_model_prec =
56 Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
59 fun is_matches_ (Match_ _) = true
60 | is_matches_ _ = false;
62 fun match_found ms = ((find_first is_matches_) o rev) ms;
64 fun eq1 d (_, (d', _)) = (d = d');
66 (* chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)
68 fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
69 (case find_first (eq1 d) pbt of
70 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
71 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
72 | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
73 (case find_first (eq1 d) pbt of
74 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
75 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
76 | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
77 | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
78 | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
79 (case find_first (eq1 d) pbt of
80 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
81 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
82 | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
83 (case find_first (eq1 d) pbt of
85 raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"
86 | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
87 | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
89 fun chk_TEST (_: theory) pbt (i, vats, b, f, I_Model.Cor_TEST (d, vs)) =
90 (case find_first (eq1 d) pbt of
91 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
92 | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
93 | chk_TEST _ pbt (i, vats, b, f, I_Model.Inc_TEST (d, vs)) =
94 (case find_first (eq1 d) pbt of
95 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
96 | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
97 | chk_TEST _ pbt (i, vats, b, f, I_Model.Sup_TEST (d, vs)) =
98 (case find_first (eq1 d) pbt of
99 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
100 | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
103 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
104 fun eq0 (0, _, _, _, _) = true
107 | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
109 | max_id ((id, _, _, _, _) :: is) = max_i id is;
110 fun add_idvat itms _ _ [] = itms
111 | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
112 add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
114 (* find elements of pbt not contained in itms;
115 if such one is untouched, return this one, otherwise create new itm *)
116 fun chk_m itms untouched (p as (f, (d, id))) =
117 case find_first (eq2 p) itms of
120 (case find_first (eq2 p) untouched of
122 | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
124 fun chk_mis mvat itms untouched pbt =
125 let val mis = (flat o (map (chk_m itms untouched))) pbt;
126 val mid = max_id itms;
127 in add_idvat [] (mid + 1) mvat mis end;
129 (* check a problem (ie. itm list) for matching a problemtype,
130 takes the Pre_Conds.max_variant for concluding completeness (could be another!) *)
131 (* match_itms: theory -> I_Model.T -> Model_Pattern.T * unchecked * Rule_Def.rule_set ->
132 bool * (I_Model.T * (bool * term) list)*)
133 fun match_itms thy itms (pbt, where_, where_rls) =
135 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
136 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
137 val mvat = Pre_Conds.max_variant itms';
138 val itms'' = filter (okv mvat) itms';
139 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
140 val mis = chk_mis mvat itms'' untouched pbt;
141 val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_
142 (pbt, I_Model.OLD_to_TEST itms'')
143 in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
145 (* refine a problem; version for tactic Refine_Problem *)
146 fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
148 val {thy, model, where_, where_rls, ...} = py
149 (*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*)
150 val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
153 then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', where_'))]
154 else pbls @ [NoMatch_]
156 | find_match _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
158 val {thy, model, where_, where_rls, ...} = py
159 val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
161 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', where_'))
162 in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
163 else (pbls @ [NoMatch_])
165 | find_match _ _ _ _ _ = raise ERROR "find_match: uncovered fun def."
166 and find_matchs _ _ _ pbls [] = pbls
167 | find_matchs thy pblRD itms pbls ((p as Store.Node _) :: pts) =
169 val pbls' = find_match thy pblRD itms pbls p
170 in case last_elem pbls' of
172 | NoMatch_ => find_matchs thy pblRD itms pbls' pts
175 fun problem thy pblID itms =
176 case match_found ((Store.apply (get_pbls ())) (find_match thy ((rev o tl) pblID) itms [])
177 pblID (rev pblID)) of
179 | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd;
182 refine a problem; construct pblRD while scanning Problem.T Store.T
183 TODO: as \<open>check_match: 'a -> .. -> 'b option\<close> could be ignorant of Store.T structure.
185 fun check_match ctxt pblRD ori (Store.Node (pI, [py], [])) =
187 val _ = writeln ("check_match 1: " ^ strs2str pblRD)
188 val {where_rls, model, where_, ...} = py: Problem.T
189 val model = map (Model_Pattern.adapt_to_type ctxt) model
190 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
192 if M_Match.match_oris ctxt where_rls ori (model, where_)
193 then SOME (pblRD(**) @ [pI](**))
196 | check_match ctxt pblRD ori (Store.Node (pI, [py], pys)) =
198 val _ = writeln ("check_match 2: " ^ strs2str pblRD)
199 val {where_rls, model, where_, ...} = py: Problem.T
200 val model = map (Model_Pattern.adapt_to_type ctxt) model
201 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
203 if M_Match.match_oris ctxt where_rls ori (model, where_)
204 then (case refins ctxt (pblRD @ [pI]) ori pys of
205 SOME pblRD' => SOME pblRD'
206 | NONE => SOME (pblRD (**)@ [pI](**)))
209 | check_match _ _ _ _ = raise ERROR "check_match: uncovered fun def."
210 and refins _ _ _ [] = NONE
211 | refins ctxt pblRD ori ((p as Store.Node _) :: pts) =
212 (writeln ("refins: " ^ strs2str pblRD);
213 (case check_match ctxt pblRD ori p of
214 SOME pblRD' => SOME (pblRD')
215 | NONE => refins ctxt pblRD ori pts)
222 (* refine a problem; version providing output for math authors *)
223 (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list ->
224 Probl_Def.T Store.node -> M_Match.T list*)
225 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
227 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
228 val {thy, model, where_, where_rls, ...} = py
229 val model = map (Model_Pattern.adapt_to_type ctxt) model
230 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
231 val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
232 val (b, (itms, where_')) =
233 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
236 then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
237 else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
239 | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
241 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
242 val {thy, model, where_, where_rls, ...} = py
243 val model = map (Model_Pattern.adapt_to_type ctxt) model
244 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
245 val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
246 val (b, (itms, where_')) =
247 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
251 let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
252 in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
253 else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
255 | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
256 and refins' _ _ _ pbls [] = pbls
257 | refins' ctxt pblRD fmz pbls ((p as Store.Node _) :: pts) =
259 val pbls' = refin' ctxt pblRD fmz pbls p
261 case last_elem pbls' of
262 M_Match.Matches _ => pbls'
263 | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts
267 TODO: rename \<rightarrow> apply_to_node
268 apply a fun to a ptyps node.
269 val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
270 TODO: Store.apply scans Store.T only to the first hit; see Store.apply.
272 fun find_node_elem x = Store.apply (get_pbls ()) x;
274 (*for tactic Refine_Tacitly; oris are already created wrt. some pbt; ctxt overrides thy in pbt*)
275 fun by_o_model ctxt oris pblID =
277 val opt = find_node_elem (check_match ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
280 let val pblID': Problem.id = rev pblRD
281 in if pblID' = pblID then NONE else SOME pblID' end
284 fun by_o_model' ctxt oris pI = perhaps (by_o_model ctxt oris) pI;
286 (*specifically for tests*)
287 fun by_formalise ctxt fmz pblID =
288 find_node_elem (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);