1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -256,9 +256,9 @@
1.4 | SOME ori => SOME (geti_ct thy ori (hd icl))
1.5 end
1.6
1.7 -fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
1.8 - | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
1.9 - | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
1.10 +fun mk_delete thy "#Given" itm_ = Del_Given (Specify.itm_out thy itm_)
1.11 + | mk_delete thy "#Find" itm_ = Del_Find (Specify.itm_out thy itm_)
1.12 + | mk_delete thy "#Relate" itm_ = Del_Relation(Specify.itm_out thy itm_)
1.13 | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
1.14 fun mk_additem "#Given" ct = Add_Given ct
1.15 | mk_additem "#Find" ct = Add_Find ct
1.16 @@ -433,7 +433,7 @@
1.17 let val (d, ts) = split_dts t
1.18 in
1.19 if d = e_term
1.20 - then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
1.21 + then Add (i, [], false, sel, Mis (Specify.dsc_unknown, hd ts))
1.22 else
1.23 (case find_first (eq1 d) pbt of
1.24 NONE => Add (i, [], true, sel, Sup (d,ts))
1.25 @@ -551,13 +551,13 @@
1.26 val cy = filter is_copy_named pbt
1.27 val oris' = matc thy pbt' ags []
1.28 val cy' = map (cpy_nam pbt' oris') cy
1.29 - val ors = add_id (oris' @ cy') (*...appended in order to get into the model-items *)
1.30 + val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
1.31 in (map flattup ors): ori list end
1.32
1.33 (* report part of the error-msg which is not available in match_args *)
1.34 fun match_ags_msg pI stac ags =
1.35 let
1.36 - val pats = (#ppc o get_pbt) pI
1.37 + val pats = (#ppc o Specify.get_pbt) pI
1.38 val msg = (dots 70^"\n"
1.39 ^ "*** problem "^strs2str pI ^ " has the ...\n"
1.40 ^ "*** model-pattern "^pats2str pats ^ "\n"
1.41 @@ -619,7 +619,7 @@
1.42 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
1.43 val cpI = if pI = e_pblID then pI' else pI
1.44 val cmI = if mI = e_metID then mI' else mI
1.45 - val {ppc, pre, prls, ...} = get_met cmI
1.46 + val {ppc, pre, prls, ...} = Specify.get_met cmI
1.47 in
1.48 case appl_add ctxt sel oris met ppc ct of
1.49 Add itm => (*..union old input *)
1.50 @@ -637,9 +637,9 @@
1.51 val pb = foldl and_ (true, map fst pre')
1.52 val (p_, nxt) =
1.53 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.54 - ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.55 + ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
1.56 in ((p, p_), ((p, p_), Uistate),
1.57 - Ctree.PpcKF (Ctree.Method cmI, itms2itemppc thy met' pre'), nxt, Safe, pt')
1.58 + Ctree.PpcKF (Ctree.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
1.59 end
1.60 | Err msg =>
1.61 let
1.62 @@ -647,7 +647,7 @@
1.63 val pb = foldl and_ (true, map fst pre')
1.64 val (p_, nxt) =
1.65 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.66 - ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.67 + ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
1.68 in ((p,p_), ((p,p_),Uistate), Ctree.Error' msg, nxt, Safe,pt) end
1.69 end
1.70 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
1.71 @@ -659,7 +659,7 @@
1.72 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
1.73 val cpI = if pI = e_pblID then pI' else pI
1.74 val cmI = if mI = e_metID then mI' else mI
1.75 - val {ppc, where_, prls, ...} = get_pbt cpI
1.76 + val {ppc, where_, prls, ...} = Specify.get_pbt cpI
1.77 in
1.78 case appl_add ctxt sel oris pbl ppc ct of
1.79 Add itm => (*..union old input *)
1.80 @@ -674,11 +674,11 @@
1.81 val pre = check_preconds thy prls where_ pbl'
1.82 val pb = foldl and_ (true, map fst pre)
1.83 val (p_, nxt) =
1.84 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.85 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.86 val ppc = if p_= Pbl then pbl' else met
1.87 in
1.88 ((p, p_), ((p, p_), Uistate),
1.89 - Ctree.PpcKF (header p_ pI cmI, itms2itemppc thy ppc pre), nxt, Safe, pt')
1.90 + Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
1.91 end
1.92 | Err msg =>
1.93 let
1.94 @@ -686,7 +686,7 @@
1.95 val pb = foldl and_ (true, map fst pre)
1.96 val (p_, nxt) =
1.97 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.98 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.99 + (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.100 in ((p, p_), ((p, p_), Uistate), Ctree.Error' msg, nxt, Safe,pt) end
1.101 end
1.102
1.103 @@ -696,7 +696,7 @@
1.104 val (oris, ctxt) =
1.105 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1.106 then ([], e_ctxt)
1.107 - else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1.108 + else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
1.109 val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
1.110 (oris, (dI',pI',mI'), e_term)
1.111 val pt = update_ctxt pt [] ctxt
1.112 @@ -705,11 +705,11 @@
1.113 case mI' of
1.114 ["no_met"] =>
1.115 (([], Pbl), (([], Pbl), Uistate),
1.116 - Ctree.PpcKF (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre),
1.117 + Ctree.PpcKF (Ctree.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.118 Refine_Tacitly pI', Safe, pt)
1.119 | _ =>
1.120 (([], Pbl), (([], Pbl), Uistate),
1.121 - Ctree.PpcKF (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre),
1.122 + Ctree.PpcKF (Ctree.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.123 Model_Problem, Safe, pt)
1.124 end
1.125 (* ONLY for STARTING modeling phase *)
1.126 @@ -721,16 +721,16 @@
1.127 | _ => error "specify (Model_Problem': uncovered case get_obj"
1.128 val thy' = if dI = e_domID then dI' else dI
1.129 val thy = assoc_thy thy'
1.130 - val {ppc, prls, where_, ...} = get_pbt pI'
1.131 + val {ppc, prls, where_, ...} = Specify.get_pbt pI'
1.132 val pre = check_preconds thy prls where_ pbl
1.133 val pb = foldl and_ (true, map fst pre)
1.134 val ((p, _), _, _, pt) =
1.135 Ctree.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.136 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.137 - (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.138 + (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
1.139 in
1.140 ((p, Pbl), ((p, p_), Uistate),
1.141 - Ctree.PpcKF (Ctree.Problem pI', itms2itemppc (assoc_thy dI') pbl pre),
1.142 + Ctree.PpcKF (Ctree.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.143 nxt, Safe, pt)
1.144 end
1.145 (* called only if no_met is specified *)
1.146 @@ -739,13 +739,13 @@
1.147 val (dI', ctxt) = case get_obj I pt p of
1.148 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
1.149 | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
1.150 - val {met, thy,...} = get_pbt pIre
1.151 + val {met, thy,...} = Specify.get_pbt pIre
1.152 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.153 val ((p,_), _, _, pt) =
1.154 Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.155 val (pbl, pre, _) = ([], [], false)
1.156 in ((p, Pbl), (pos, Uistate),
1.157 - Ctree.PpcKF (Ctree.Problem pIre, itms2itemppc (assoc_thy dI') pbl pre),
1.158 + Ctree.PpcKF (Ctree.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.159 Model_Problem, Safe, pt)
1.160 end
1.161 | specify (Refine_Problem' rfd) pos _ pt =
1.162 @@ -770,11 +770,11 @@
1.163 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.164 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
1.165 val mI'' = if mI=e_metID then mI' else mI
1.166 - val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o get_pbt) pI,
1.167 - (#ppc o get_met) mI'') (dI, pI, mI);
1.168 + val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
1.169 + (#ppc o Specify.get_met) mI'') (dI, pI, mI);
1.170 in
1.171 ((p,Pbl), (pos,Uistate),
1.172 - Ctree.PpcKF (Ctree.Problem pI, itms2itemppc dI'' itms pre),
1.173 + Ctree.PpcKF (Ctree.Problem pI, Specify.itms2itemppc dI'' itms pre),
1.174 nxt, Safe, pt)
1.175 end
1.176 (*WN110515 initialise ctxt again from itms and add preconds*)
1.177 @@ -784,20 +784,20 @@
1.178 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
1.179 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
1.180 | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.181 - val {ppc,pre,prls,...} = get_met mID
1.182 + val {ppc,pre,prls,...} = Specify.get_met mID
1.183 val thy = assoc_thy dI
1.184 - val oris = add_field' thy ppc oris
1.185 + val oris = Specify.add_field' thy ppc oris
1.186 val dI'' = if dI=e_domID then dI' else dI
1.187 val pI'' = if pI = e_pblID then pI' else pI
1.188 val met = if met = [] then pbl else met
1.189 - val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris
1.190 + val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
1.191 val (pos, _, _, pt) =
1.192 Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.193 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
1.194 - ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
1.195 + ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
1.196 in
1.197 (pos, (pos,Uistate),
1.198 - Ctree.PpcKF (Ctree.Method mID, itms2itemppc (assoc_thy dI'') itms pre'),
1.199 + Ctree.PpcKF (Ctree.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
1.200 nxt, Safe, pt)
1.201 end
1.202 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.203 @@ -813,9 +813,9 @@
1.204 | _ => error "specify (Specify_Theory': uncovered case get_obj"
1.205 val mppc = case p_ of Met => met | _ => pbl
1.206 val cpI = if pI = e_pblID then pI' else pI
1.207 - val {prls = per, ppc, where_ = pwh, ...} = get_pbt cpI
1.208 + val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
1.209 val cmI = if mI = e_metID then mI' else mI
1.210 - val {prls = mer, ppc = mpc, pre= mwh, ...} = get_met cmI
1.211 + val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
1.212 val pre = case p_ of
1.213 Met => (check_preconds thy mer mwh met)
1.214 | _ => (check_preconds thy per pwh pbl)
1.215 @@ -826,7 +826,7 @@
1.216 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.217 in
1.218 ((p, p_), (pos, Uistate),
1.219 - Ctree.PpcKF (header p_ pI cmI, itms2itemppc thy mppc pre),
1.220 + Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.221 nxt, Safe, pt)
1.222 end
1.223 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.224 @@ -835,7 +835,7 @@
1.225 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.226 in
1.227 ((p,p_), (pos,Uistate),
1.228 - Ctree.PpcKF (header p_ pI cmI, itms2itemppc thy mppc pre),
1.229 + Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.230 nxt, Safe, pt)
1.231 end
1.232 end
1.233 @@ -852,7 +852,7 @@
1.234 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.235 val cpI = if pI = e_pblID then pI' else pI;
1.236 in
1.237 - case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.238 + case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
1.239 Add itm (*..union old input *) =>
1.240 let
1.241 val pbl' = insert_ppc thy itm pbl
1.242 @@ -881,7 +881,7 @@
1.243 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.244 val cmI = if mI = e_metID then mI' else mI;
1.245 in
1.246 - case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1.247 + case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
1.248 Add itm (*..union old input *) =>
1.249 let
1.250 val met' = insert_ppc thy itm met;
1.251 @@ -963,8 +963,8 @@
1.252 | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
1.253 val (dI, pI, mI) = some_spec ospec spec
1.254 val thy = assoc_thy dI
1.255 - val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.256 - val {cas, ppc, ...} = get_pbt pI
1.257 + val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
1.258 + val {cas, ppc, ...} = Specify.get_pbt pI
1.259 val pbl = Ctree.init_pbl ppc (* fill in descriptions *)
1.260 (*----------------if you think, this should be done by the Dialog
1.261 in the java front-end, search there for WN060225-modelProblem----*)
1.262 @@ -984,12 +984,12 @@
1.263 val (oris, dI, ctxt) = case get_obj I pt p of
1.264 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
1.265 | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
1.266 - val opt = refine_ori oris pI
1.267 + val opt = Specify.refine_ori oris pI
1.268 in
1.269 case opt of
1.270 SOME pI' =>
1.271 let
1.272 - val {met, ...} = get_pbt pI'
1.273 + val {met, ...} = Specify.get_pbt pI'
1.274 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.275 val mI = if length met = 0 then e_metID else hd met
1.276 val thy = assoc_thy dI
1.277 @@ -1009,7 +1009,7 @@
1.278 | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
1.279 val thy = if dI' = e_domID then dI else dI'
1.280 in
1.281 - case refine_pbl (assoc_thy thy) pI probl of
1.282 + case Specify.refine_pbl (assoc_thy thy) pI probl of
1.283 NONE => ([], [], ptp)
1.284 | SOME rfd =>
1.285 let
1.286 @@ -1025,11 +1025,11 @@
1.287 (oris, dI, dI', pI', probl, ctxt)
1.288 | _ => error ""
1.289 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.290 - val {ppc,where_,prls,...} = get_pbt pI
1.291 + val {ppc,where_,prls,...} = Specify.get_pbt pI
1.292 val pbl =
1.293 if pI' = e_pblID andalso pI = e_pblID
1.294 then (false, (Ctree.init_pbl ppc, []))
1.295 - else match_itms_oris thy probl (ppc,where_,prls) oris
1.296 + else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
1.297 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.298 val (c, pt) = case Ctree.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.299 ((_, Pbl), c, _, pt) => (c, pt)
1.300 @@ -1045,11 +1045,11 @@
1.301 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
1.302 => (oris, pbl, dI, met, ctxt)
1.303 | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
1.304 - val {ppc,pre,prls,...} = get_met mID
1.305 + val {ppc,pre,prls,...} = Specify.get_met mID
1.306 val thy = assoc_thy dI
1.307 - val oris = add_field' thy ppc oris
1.308 + val oris = Specify.add_field' thy ppc oris
1.309 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1.310 - val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris
1.311 + val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
1.312 val (pos, c, _, pt) =
1.313 Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.314 in
1.315 @@ -1083,7 +1083,7 @@
1.316 if pI <> []
1.317 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1.318 let
1.319 - val {cas, met, ppc, thy, ...} = get_pbt pI
1.320 + val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
1.321 val dI = if dI = "" then theory2theory' thy else dI
1.322 val mI = if mI = [] then hd met else mI
1.323 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.324 @@ -1097,7 +1097,7 @@
1.325 if mI <> []
1.326 then (* from met-browser *)
1.327 let
1.328 - val {ppc, ...} = get_met mI
1.329 + val {ppc, ...} = Specify.get_met mI
1.330 val dI = if dI = "" then "Isac" else dI
1.331 val (pt, _) =
1.332 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1.333 @@ -1117,13 +1117,13 @@
1.334 if mI = ["no_met"]
1.335 then
1.336 let
1.337 - val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1.338 - val pI' = refine_ori' pors pI;
1.339 + val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
1.340 + val pI' = Specify.refine_ori' pors pI;
1.341 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1.342 - (hd o #met o get_pbt) pI')
1.343 + (hd o #met o Specify.get_pbt) pI')
1.344 end
1.345 - else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1.346 - val {cas, ppc, thy = thy', ...} = get_pbt pI (*take dI from _refined_ pbl*)
1.347 + else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
1.348 + val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
1.349 val dI = theory2theory' (maxthy thy thy')
1.350 val hdl = case cas of
1.351 NONE => pblterm dI pI
1.352 @@ -1158,7 +1158,7 @@
1.353 (* check pbltypes, announces one failure a time *)
1.354 fun chk_vars ctppc =
1.355 let
1.356 - val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
1.357 + val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
1.358 val chked = subtract op = gi wh
1.359 in
1.360 if chked <> [] then ("wh\\gi", chked)
1.361 @@ -1174,7 +1174,7 @@
1.362 (* check a new pbltype: variables (Free) unbound by given, find*)
1.363 fun unbound_ppc ctppc =
1.364 let
1.365 - val {Given = gi, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
1.366 + val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
1.367 in
1.368 distinct (subtract op = (union op = gi fi) re)
1.369 end
1.370 @@ -1217,8 +1217,8 @@
1.371 PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
1.372 | _ => error "complete_mod: unvered case get_obj"
1.373 val (_, pI, mI) = some_spec ospec spec
1.374 - val mpc = (#ppc o get_met) mI
1.375 - val ppc = (#ppc o get_pbt) pI
1.376 + val mpc = (#ppc o Specify.get_met) mI
1.377 + val ppc = (#ppc o Specify.get_pbt) pI
1.378 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1.379 val pt = update_pblppc pt p pits
1.380 val pt = update_metppc pt p mits
1.381 @@ -1231,7 +1231,7 @@
1.382 val (pors, dI, pI, mI) = case get_obj I pt p of
1.383 PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
1.384 | _ => error "all_modspec: uncovered case get_obj"
1.385 - val {ppc, ...} = get_met mI
1.386 + val {ppc, ...} = Specify.get_met mI
1.387 val (_, vals) = oris2fmz_vals pors
1.388 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1.389 |> declare_constraints' vals
1.390 @@ -1286,7 +1286,7 @@
1.391 val pre = if metID = e_metID then []
1.392 else
1.393 let
1.394 - val {prls, pre= where_, ...} = get_met metID
1.395 + val {prls, pre= where_, ...} = Specify.get_met metID
1.396 val pre = check_preconds' prls where_ meth 0
1.397 in pre end
1.398 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
1.399 @@ -1299,7 +1299,7 @@
1.400 val pre = if pI = e_pblID then []
1.401 else
1.402 let
1.403 - val {prls, where_, ...} = get_pbt pI
1.404 + val {prls, where_, ...} = Specify.get_pbt pI
1.405 val pre = check_preconds' prls where_ probl 0
1.406 in pre end
1.407 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
1.408 @@ -1312,7 +1312,7 @@
1.409 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
1.410 let
1.411 val (dI, pI, _) = get_somespec' spec spec'
1.412 - val {cas, ...} = get_pbt pI
1.413 + val {cas, ...} = Specify.get_pbt pI
1.414 in case cas of
1.415 NONE => Form (pblterm dI pI)
1.416 | SOME t => Form (subst_atomic (mk_env probl) t)
1.417 @@ -1461,7 +1461,7 @@
1.418 val (ospec, hdf', spec, probl) = case get_obj I pt p of
1.419 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1.420 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1.421 - val {prls, where_, ...} = get_pbt (#2 (some_spec ospec spec))
1.422 + val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
1.423 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1.424 in
1.425 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1.426 @@ -1471,7 +1471,7 @@
1.427 val (ospec, hdf', spec, meth) = case get_obj I pt p of
1.428 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1.429 | _ => error "get_ocalhd Met: uncovered case get_obj"
1.430 - val {prls, pre, ...} = get_met (#3 (some_spec ospec spec))
1.431 + val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
1.432 val pre = check_preconds (assoc_thy"Isac") prls pre meth
1.433 in
1.434 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)