prep. remove Specify/mstools.sml
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 ->
11 (Problem.id * (I_Model.T * Pre_Conds.T)) option
13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
17 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21 structure Refine(**) : REFINE_PROBLEM(**) =
26 Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
29 fun is_matches_ (Match_ _) = true
30 | is_matches_ _ = false;
32 fun refined_ ms = ((find_first is_matches_) o rev) ms;
34 fun eq1 d (_, (d', _)) = (d = d');
36 fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
37 (case find_first (eq1 d) pbt of
38 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
39 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
40 | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
41 (case find_first (eq1 d) pbt of
42 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
43 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
44 | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
45 | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
46 | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
47 (case find_first (eq1 d) pbt of
48 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, I_Model.pbl_ids' d vs)))
49 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
50 | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
51 (case find_first (eq1 d) pbt of
52 SOME (_, _) => raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, I_Model.pbl_ids' d vs))):itm)"
53 | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
54 | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
56 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
57 fun eq0 (0, _, _, _, _) = true
60 | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
62 | max_id ((id, _, _, _, _) :: is) = max_i id is;
63 fun add_idvat itms _ _ [] = itms
64 | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
65 add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
67 (* find elements of pbt not contained in itms;
68 if such one is untouched, return this one, otherwise create new itm *)
69 fun chk_m itms untouched (p as (f, (d, id))) =
70 case find_first (eq2 p) itms of
73 (case find_first (eq2 p) untouched of
75 | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
77 fun chk_mis mvat itms untouched pbt =
78 let val mis = (flat o (map (chk_m itms untouched))) pbt;
79 val mid = max_id itms;
80 in add_idvat [] (mid + 1) mvat mis end;
82 (* check a problem (ie. itm list) for matching a problemtype,
83 takes the I_Model.max_vt for concluding completeness (could be another!) *)
84 fun match_itms thy itms (pbt, pre, prls) =
86 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
87 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
88 val mvat = I_Model.max_vt itms';
89 val itms'' = filter (okv mvat) itms';
90 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
91 val mis = chk_mis mvat itms'' untouched pbt;
92 val pre' = Pre_Conds.check prls pre itms'' mvat
93 val pb = foldl and_ (true, map fst pre')
94 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
96 (* refine a problem; version for tactic Refine_Problem *)
97 fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
99 val {thy, ppc, where_, prls, ...} = py
100 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
103 then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
104 else pbls @ [NoMatch_]
106 | refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
108 val {thy, ppc, where_, prls, ...} = py
109 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
111 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
112 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
113 else (pbls @ [NoMatch_])
115 | refin'' _ _ _ _ _ = raise ERROR "refin'': uncovered fun def."
116 and refins'' _ _ _ pbls [] = pbls
117 | refins'' thy pblRD itms pbls ((p as Store.Node _) :: pts) =
119 val pbls' = refin'' thy pblRD itms pbls p
120 in case last_elem pbls' of
122 | NoMatch_ => refins'' thy pblRD itms pbls' pts
125 fun problem thy pblID itms =
126 case refined_ ((Store.apply (get_ptyps ())) (refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) of
128 | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
129 | _ => raise ERROR "Refine.problem: uncovered case refined_";