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