1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Thu Feb 02 10:41:09 2017 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sat Feb 04 07:20:39 2017 +0100
1.3 @@ -7,18 +7,18 @@
1.4 sig
1.5 type field
1.6 (* for calchead.sml, if below at left margin *)
1.7 - val prep_ori : Selem.fmz_ -> theory -> field list -> ori list * Proof.context
1.8 + val prep_ori : Selem.fmz_ -> theory -> field list -> Stool.ori list * Proof.context
1.9 val add_id : 'a list -> (int * 'a) list
1.10 - val add_field' : theory -> field list -> ori list -> ori list
1.11 - val match_itms_oris : theory -> itm list -> field list * term list * rls ->
1.12 - ori list -> bool * (itm list * (bool * term) list)
1.13 - val refine_ori : ori list -> pblID -> pblID option
1.14 - val refine_ori' : ori list -> pblID -> pblID
1.15 - val refine_pbl : theory -> pblID -> itm list -> (pblID * (itm list * (bool * term) list)) option
1.16 + val add_field' : theory -> field list -> Stool.ori list -> Stool.ori list
1.17 + val match_itms_oris : theory -> Stool.itm list -> field list * term list * rls ->
1.18 + Stool.ori list -> bool * (Stool.itm list * (bool * term) list)
1.19 + val refine_ori : Stool.ori list -> pblID -> pblID option
1.20 + val refine_ori' : Stool.ori list -> pblID -> pblID
1.21 + val refine_pbl : theory -> pblID -> Stool.itm list -> (pblID * (Stool.itm list * (bool * term) list)) option
1.22
1.23 - val appc : ('a list -> 'b list) -> 'a ppc -> 'b ppc
1.24 - val mappc : ('a -> 'b) -> 'a ppc -> 'b ppc
1.25 - val itms2itemppc : theory -> itm list -> (bool * term) list -> item ppc (* for generate.sml *)
1.26 + val appc : ('a list -> 'b list) -> 'a Stool.ppc -> 'b Stool.ppc
1.27 + val mappc : ('a -> 'b) -> 'a Stool.ppc -> 'b Stool.ppc
1.28 + val itms2itemppc : theory -> Stool.itm list -> (bool * term) list -> Stool.item Stool.ppc (* for generate.sml *)
1.29
1.30 val get_pbt : pblID -> pbt
1.31 val get_met : metID -> met (* for generate.sml *)
1.32 @@ -28,7 +28,7 @@
1.33 type pblRD = string list (* for pbl-met-hierarchy.sml *)
1.34 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
1.35 val scan : string list -> 'a ptyp list -> string list list (* for thy-hierarchy.sml *)
1.36 - val itm_out : theory -> itm_ -> string
1.37 + val itm_out : theory -> Stool.itm_ -> string
1.38 val dsc_unknown : term
1.39
1.40 val pblID2guh : pblID -> guh (* for datatypes.sml *)
1.41 @@ -45,9 +45,9 @@
1.42 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.43 val show_ptyps : unit -> unit
1.44 val show_mets : unit -> unit
1.45 - val refine : Selem.fmz_ -> pblID -> match list
1.46 + val refine : Selem.fmz_ -> pblID -> Stool.match list
1.47 val e_errpat : errpat
1.48 - datatype match' = Matches' of item ppc | NoMatch' of item ppc
1.49 + datatype match' = Matches' of Stool.item Stool.ppc | NoMatch' of Stool.item Stool.ppc
1.50 val match_pbl : Selem.fmz_ -> pbt -> match'
1.51 val show_pblguhs : unit -> unit
1.52 val sort_pblguhs : unit -> unit
1.53 @@ -62,29 +62,29 @@
1.54 type field = string * (term * term)
1.55 val dsc_unknown = (Thm.term_of o the o (parseold @{theory Script})) "unknown::'a => unknow";
1.56
1.57 -fun itm_2item (_: theory) (Cor ((d, ts), _)) = Correct (term2str (comp_dts (d, ts)))
1.58 - | itm_2item _ (Syn c) = SyntaxE c
1.59 - | itm_2item _ (Typ c) = TypeE c
1.60 - | itm_2item _ (Inc ((d, ts), _)) = Incompl (term2str (comp_dts (d, ts)))
1.61 - | itm_2item _ (Sup (d, ts)) = Superfl (term2str (comp_dts (d, ts)))
1.62 - | itm_2item _ (Mis (d, pid)) = Missing (term2str d ^ " " ^ term2str pid)
1.63 +fun itm_2item (_: theory) (Stool.Cor ((d, ts), _)) = Stool.Correct (term2str (Stool.comp_dts (d, ts)))
1.64 + | itm_2item _ (Stool.Syn c) = Stool.SyntaxE c
1.65 + | itm_2item _ (Stool.Typ c) = Stool.TypeE c
1.66 + | itm_2item _ (Stool.Inc ((d, ts), _)) = Stool.Incompl (term2str (Stool.comp_dts (d, ts)))
1.67 + | itm_2item _ (Stool.Sup (d, ts)) = Stool.Superfl (term2str (Stool.comp_dts (d, ts)))
1.68 + | itm_2item _ (Stool.Mis (d, pid)) = Stool.Missing (term2str d ^ " " ^ term2str pid)
1.69 | itm_2item _ _ = error "itm_2item: uncovered definition"
1.70
1.71 -fun mappc f ({Given = gi, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc) =
1.72 - {Given= map f gi, Where = map f wh, Find = map f fi, With = map f wi, Relate = map f re} :'b ppc
1.73 -fun appc f ({Given = gi, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc) =
1.74 - {Given = f gi, Where = f wh, Find = f fi, With = f wi, Relate = f re}: 'b ppc
1.75 +fun mappc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} =
1.76 + {Given= map f gi, Where = map f wh, Find = map f fi, With = map f wi, Relate = map f re}
1.77 +fun appc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} =
1.78 + {Given = f gi, Where = f wh, Find = f fi, With = f wi, Relate = f re}
1.79
1.80 -fun add_sel_ppc (_: theory) sel ({Given = gi, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc) x =
1.81 +fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
1.82 case sel of
1.83 - "#Given" => ({Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}: 'a ppc)
1.84 - | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
1.85 - | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
1.86 - | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
1.87 - | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
1.88 + "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
1.89 + | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
1.90 + | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
1.91 + | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
1.92 + | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
1.93 | _ => error ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
1.94 -fun add_where ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}: 'a ppc) wh =
1.95 - ({Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}: 'a ppc)
1.96 +fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
1.97 + {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
1.98
1.99 (* split a term into description and (id | structured variable) for pbt, met.ppc *)
1.100 fun split_did t =
1.101 @@ -95,23 +95,23 @@
1.102 in (hd, arg) end
1.103
1.104 (*create output-string for itm_*)
1.105 -fun itm_out _ (Cor ((d, ts), _)) = term2str (comp_dts (d, ts))
1.106 - | itm_out _ (Syn c) = c
1.107 - | itm_out _ (Typ c) = c
1.108 - | itm_out _ (Inc ((d, ts), _)) = term2str (comp_dts (d, ts))
1.109 - | itm_out _ (Sup (d, ts)) = term2str (comp_dts (d, ts))
1.110 - | itm_out _ (Mis (d, pid)) = term2str d ^ " " ^ term2str pid
1.111 +fun itm_out _ (Stool.Cor ((d, ts), _)) = term2str (Stool.comp_dts (d, ts))
1.112 + | itm_out _ (Stool.Syn c) = c
1.113 + | itm_out _ (Stool.Typ c) = c
1.114 + | itm_out _ (Stool.Inc ((d, ts), _)) = term2str (Stool.comp_dts (d, ts))
1.115 + | itm_out _ (Stool.Sup (d, ts)) = term2str (Stool.comp_dts (d, ts))
1.116 + | itm_out _ (Stool.Mis (d, pid)) = term2str d ^ " " ^ term2str pid
1.117 | itm_out _ _ = error "itm_out: uncovered definition"
1.118
1.119 -fun boolterm2item (true, term) = Correct (term2str term)
1.120 - | boolterm2item (false, term) = False (term2str term);
1.121 +fun boolterm2item (true, term) = Stool.Correct (term2str term)
1.122 + | boolterm2item (false, term) = Stool.False (term2str term);
1.123
1.124 -fun itms2itemppc thy (itms: itm list) (pre: (bool * term) list) =
1.125 +fun itms2itemppc thy itms pre =
1.126 let
1.127 fun coll ppc [] = ppc
1.128 | coll ppc ((_,_,_,field,itm_)::itms) =
1.129 coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
1.130 - val gfr = coll empty_ppc itms;
1.131 + val gfr = coll Stool.empty_ppc itms;
1.132 in add_where gfr (map boolterm2item pre) end;
1.133
1.134 (* compare d and dsc in pbt and transfer field to pre-ori *)
1.135 @@ -125,14 +125,14 @@
1.136
1.137 (* take over field from met.ppc at 'Specify_Method' into ori,
1.138 i.e. also removes "#undef" fields *)
1.139 -fun add_field' (_: theory) mpc (ori: ori list) =
1.140 +fun add_field' (_: theory) mpc ori =
1.141 let fun eq d pt = (d = (fst o snd) pt);
1.142 fun repl mpc (i, v, _, d, ts) =
1.143 case filter (eq d) mpc of
1.144 [(fi, (_, _))] => [(i, v, fi, d, ts)]
1.145 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
1.146 | _ => error ("add_field': " ^ term2str d ^ " more than once in met");
1.147 - in (flat ((map (repl mpc)) ori)): ori list end;
1.148 + in flat ((map (repl mpc)) ori) end;
1.149
1.150 (* mark an element with the position within a plateau;
1.151 a plateau with length 1 is marked with 0 *)
1.152 @@ -184,8 +184,8 @@
1.153 fun prep_ori [] _ _ = ([], Selem.e_ctxt)
1.154 | prep_ori fmz thy pbt =
1.155 let
1.156 - val ctxt = Proof_Context.init_global thy |> fold declare_constraints fmz;
1.157 - val ori = map (add_field thy pbt o split_dts o the o parseNEW ctxt) fmz |> add_variants;
1.158 + val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz;
1.159 + val ori = map (add_field thy pbt o Stool.split_dts o the o parseNEW ctxt) fmz |> add_variants;
1.160 val maxv = map fst ori |> max;
1.161 val maxv = if maxv = 0 then 1 else maxv;
1.162 val oris = coll_variants ori
1.163 @@ -358,61 +358,61 @@
1.164
1.165 (* transform oris *)
1.166
1.167 -fun coll_vats (vats, ((_, vs, _, _, _): ori)) = union op = vats vs;
1.168 -fun filter_vat oris i = filter ((member_swap op = i) o (#2 : ori -> int list)) oris;
1.169 +fun coll_vats (vats, (_, vs, _, _, _)) = union op = vats vs;
1.170 +fun filter_vat oris i = filter ((member_swap op = i) o (#2 : Stool.ori -> int list)) oris;
1.171
1.172 (** check a problem (ie. itm list) for matching a problemtype **)
1.173
1.174 fun eq1 d (_, (d', _)) = (d = d');
1.175 -fun ori2itmSup ((i, v, _, d, ts): ori) = ((i, v, true, "#Given", Sup (d, ts)): itm);
1.176 +fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", Stool.Sup (d, ts));
1.177 (*see + add_sel_ppc ~~~~~~~*)
1.178
1.179 -fun field_eq f ((_, _, f', _, _): ori) = f = f';
1.180 +fun field_eq f (_, _, f', _, _) = f = f';
1.181
1.182 (* check an item (with arbitrary itm_ from previous matchings)
1.183 for matching a problemtype; returns true only for itms found in pbt *)
1.184 -fun chk_ (_: theory) pbt ((i, vats, b, f, Cor ((d, vs), _)): itm) =
1.185 +fun chk_ (_: theory) pbt (i, vats, b, f, Stool.Cor ((d, vs), _)) =
1.186 (case find_first (eq1 d) pbt of
1.187 - SOME (_, (_, id)) => ((i, vats, b, f, Cor ((d, vs), (id, pbl_ids' d vs))): itm)
1.188 - | NONE => (i, vats, false, f, Sup (d, vs)))
1.189 - | chk_ _ pbt (i, vats, b, f, Inc ((d, vs), _)) =
1.190 + SOME (_, (_, id)) => (i, vats, b, f, Stool.Cor ((d, vs), (id, Stool.pbl_ids' d vs)))
1.191 + | NONE => (i, vats, false, f, Stool.Sup (d, vs)))
1.192 + | chk_ _ pbt (i, vats, b, f, Stool.Inc ((d, vs), _)) =
1.193 (case find_first (eq1 d) pbt of
1.194 - SOME (_, (_, id)) => (i, vats, b, f, Cor ((d, vs), (id, pbl_ids' d vs)))
1.195 - | NONE => (i, vats, false, f, Sup (d, vs)))
1.196 - | chk_ _ _ (itm as (_, _, _, _, Syn _)) = itm
1.197 - | chk_ _ _ (itm as (_, _, _, _, Typ _)) = itm
1.198 - | chk_ _ pbt (i, vats, b, f, Sup (d, vs)) =
1.199 + SOME (_, (_, id)) => (i, vats, b, f, Stool.Cor ((d, vs), (id, Stool.pbl_ids' d vs)))
1.200 + | NONE => (i, vats, false, f, Stool.Sup (d, vs)))
1.201 + | chk_ _ _ (itm as (_, _, _, _, Stool.Syn _)) = itm
1.202 + | chk_ _ _ (itm as (_, _, _, _, Stool.Typ _)) = itm
1.203 + | chk_ _ pbt (i, vats, b, f, Stool.Sup (d, vs)) =
1.204 (case find_first (eq1 d) pbt of
1.205 - SOME (_, (_, id)) => (i, vats, b, f, Cor ((d,vs), (id, pbl_ids' d vs)))
1.206 - | NONE => (i, vats, false, f, Sup (d, vs)))
1.207 - | chk_ _ pbt (i, vats, _, f, Mis (d, vs)) =
1.208 + SOME (_, (_, id)) => (i, vats, b, f, Stool.Cor ((d,vs), (id, Stool.pbl_ids' d vs)))
1.209 + | NONE => (i, vats, false, f, Stool.Sup (d, vs)))
1.210 + | chk_ _ pbt (i, vats, _, f, Stool.Mis (d, vs)) =
1.211 (case find_first (eq1 d) pbt of
1.212 - SOME (_, _) => error "chk_: ((i,vats,b,f,Cor ((d,vs),(id, pbl_ids' d vs))):itm)"
1.213 - | NONE => (i, vats, false, f, Sup (d, [vs])))
1.214 + SOME (_, _) => error "chk_: ((i,vats,b,f,Stool.Cor ((d,vs),(id, Stool.pbl_ids' d vs))):itm)"
1.215 + | NONE => (i, vats, false, f, Stool.Sup (d, [vs])))
1.216 | chk_ _ _ _ = error "chk_: uncovered fun def.";
1.217
1.218 -fun eq2 (_, (d, _)) ((_, _, _, _, itm_): itm) = d = d_in itm_;
1.219 -fun eq2' (_, (d, _)) ((_, _, _, d', _): ori) = d = d';
1.220 -fun eq0 ((0, _, _, _, _): itm) = true
1.221 +fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = Stool.d_in itm_;
1.222 +fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
1.223 +fun eq0 (0, _, _, _, _) = true
1.224 | eq0 _ = false;
1.225 fun max_i i [] = i
1.226 | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
1.227 -fun max_id ([]: itm list) = 0
1.228 +fun max_id [] = 0
1.229 | max_id ((id, _, _, _, _) :: is) = max_i id is;
1.230 -fun add_idvat itms _ _ ([]: itm list) = itms
1.231 - | add_idvat itms i mvat (((_, _, b, f, itm_): itm) :: its) =
1.232 - add_idvat (itms @ [(i,[],b,f,itm_):itm]) (i + 1) mvat its;
1.233 +fun add_idvat itms _ _ [] = itms
1.234 + | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
1.235 + add_idvat (itms @ [(i,[],b,f,itm_)]) (i + 1) mvat its;
1.236 (* ^^ mvat ...meaningless with pbl-identifier *)
1.237
1.238 (* find elements of pbt not contained in itms;
1.239 if such one is untouched, return this one, otherwise create new itm *)
1.240 -fun chk_m (itms: itm list) untouched (p as (f, (d, id))) =
1.241 +fun chk_m itms untouched (p as (f, (d, id))) =
1.242 case find_first (eq2 p) itms of
1.243 SOME _ => []
1.244 | NONE =>
1.245 (case find_first (eq2 p) untouched of
1.246 SOME itm => [itm]
1.247 - | NONE => [(0, [], false, f, Mis (d, id)): itm]);
1.248 + | NONE => [(0, [], false, f, Stool.Mis (d, id))]);
1.249
1.250 fun chk_mis mvat itms untouched pbt =
1.251 let val mis = (flat o (map (chk_m itms untouched))) pbt;
1.252 @@ -420,45 +420,45 @@
1.253 in add_idvat [] (mid + 1) mvat mis end;
1.254
1.255 (* check a problem (ie. itm list) for matching a problemtype,
1.256 - takes the max_vt for concluding completeness (could be another!) *)
1.257 + takes the Stool.max_vt for concluding completeness (could be another!) *)
1.258 fun match_itms thy itms (pbt, pre, prls) =
1.259 let
1.260 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
1.261 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
1.262 - val mvat = max_vt itms';
1.263 + val mvat = Stool.max_vt itms';
1.264 val itms'' = filter (okv mvat) itms';
1.265 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
1.266 val mis = chk_mis mvat itms'' untouched pbt;
1.267 - val pre' = check_preconds' prls pre itms'' mvat
1.268 + val pre' = Stool.check_preconds' prls pre itms'' mvat
1.269 val pb = foldl and_ (true, map fst pre')
1.270 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
1.271
1.272 (* check a problem pbl (ie. itm list) for matching a problemtype pbt,
1.273 for missing items get data from formalization (ie. ori list);
1.274 - takes the max_vt for concluding completeness (could be another!)
1.275 + takes the Stool.max_vt for concluding completeness (could be another!)
1.276
1.277 (0) determine the most frequent variant mv in pbl
1.278 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1.279 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
1.280 (3) newitms = filter (mv mem vat(news)) news
1.281 (4) pbt @ newitms *)
1.282 -fun match_itms_oris (_: theory) (pbl: itm list) (pbt, pre, prls) oris =
1.283 +fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
1.284 let
1.285 - (*0*)val mv = max_vt pbl;
1.286 + (*0*)val mv = Stool.max_vt pbl;
1.287
1.288 - fun eqdsc_pbt_itm ((_,(d,_))) ((_, _, _, _, itm_): itm) = d = d_in itm_;
1.289 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = Stool.d_in itm_;
1.290 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1.291 SOME _ => false | NONE => true;
1.292 (*1*)val mis = (filter (notmem pbl)) pbt;
1.293
1.294 - fun eqdsc_ori (_,(d,_)) ((_, _, _, d', _): ori) = d = d';
1.295 - fun ori2itmMis (f, (d, pid)) ((i, v, _, _, _): ori) = (i, v, false, f, Mis (d, pid)): itm;
1.296 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
1.297 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, Stool.Mis (d, pid));
1.298 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
1.299 val news = (flat o (map (oris2itms oris))) mis;
1.300 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
1.301 val newitms = filter mem_vat news;
1.302 (*4*)val itms' = pbl @ newitms;
1.303 - val pre' = check_preconds' prls pre itms' mv;
1.304 + val pre' = Stool.check_preconds' prls pre itms' mv;
1.305 val pb = foldl and_ (true, map fst pre');
1.306 in (length mis = 0 andalso pb, (itms', pre')) end;
1.307
1.308 @@ -467,30 +467,30 @@
1.309
1.310 (* check an ori for matching a problemtype by description;
1.311 returns true only for itms found in pbt *)
1.312 -fun chk1_ (_: theory) pbt ((i, vats, f, d, vs): ori) =
1.313 +fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
1.314 case find_first (eq1 d) pbt of
1.315 - SOME (_, (_, id)) => [(i, vats, true, f, Cor ((d, vs), (id, pbl_ids' d vs))): itm]
1.316 + SOME (_, (_, id)) => [(i, vats, true, f, Stool.Cor ((d, vs), (id, Stool.pbl_ids' d vs)))]
1.317 | NONE => [];
1.318
1.319 (* elem 'p' of pbt contained in itms ? *)
1.320 -fun chk1_m (itms:itm list) p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
1.321 -fun chk1_m' (oris: ori list) (p as (f, (d, t))) =
1.322 +fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
1.323 +fun chk1_m' oris (p as (f, (d, t))) =
1.324 case find_first (eq2' p) oris of
1.325 SOME _ => []
1.326 - | NONE => [(f, Mis (d, t))];
1.327 -fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_): itm;
1.328 + | NONE => [(f, Stool.Mis (d, t))];
1.329 +fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
1.330
1.331 fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
1.332 fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
1.333
1.334 (* check a problem (ie. ori list) for matching a problemtype,
1.335 - takes the max_vt for concluding completeness (FIXME could be another!) *)
1.336 + takes the Stool.max_vt for concluding completeness (FIXME could be another!) *)
1.337 fun match_oris thy prls oris (pbt,pre) =
1.338 let
1.339 val itms = (flat o (map (chk1_ thy pbt))) oris;
1.340 - val mvat = max_vt itms;
1.341 + val mvat = Stool.max_vt itms;
1.342 val complete = chk1_mis mvat itms pbt;
1.343 - val pre' = check_preconds' prls pre itms mvat;
1.344 + val pre' = Stool.check_preconds' prls pre itms mvat;
1.345 val pb = foldl and_ (true, map fst pre');
1.346 in if complete andalso pb then true else false end;
1.347
1.348 @@ -500,15 +500,15 @@
1.349 let
1.350 val itms = (flat o (map (chk1_ thy ppc))) oris;
1.351 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
1.352 - val mvat = max_vt itms;
1.353 + val mvat = Stool.max_vt itms;
1.354 val miss = chk1_mis' oris ppc;
1.355 - val pre' = check_preconds' prls pre itms mvat;
1.356 + val pre' = Stool.check_preconds' prls pre itms mvat;
1.357 val pb = foldl and_ (true, map fst pre');
1.358 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
1.359
1.360 datatype match' = (* for the user *)
1.361 - Matches' of item ppc
1.362 -| NoMatch' of item ppc;
1.363 + Matches' of Stool.item Stool.ppc
1.364 +| NoMatch' of Stool.item Stool.ppc;
1.365
1.366 (* match a formalization with a problem type, for tests *)
1.367 fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: pbt) =
1.368 @@ -549,8 +549,8 @@
1.369 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
1.370 in
1.371 if b
1.372 - then pbls @ [Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
1.373 - else pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
1.374 + then pbls @ [Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
1.375 + else pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
1.376 end
1.377 | refin' pblRD fmz pbls (Ptyp (pI, [py], pys)) =
1.378 let
1.379 @@ -562,9 +562,9 @@
1.380 in
1.381 if b
1.382 then
1.383 - let val pbl = Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')
1.384 + let val pbl = Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')
1.385 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
1.386 - else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
1.387 + else (pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
1.388 end
1.389 | refin' _ _ _ _ = error "refin': uncovered fun def."
1.390 and refins' _ _ pbls [] = pbls
1.391 @@ -573,8 +573,8 @@
1.392 val pbls' = refin' pblRD fmz pbls p
1.393 in
1.394 case last_elem pbls' of
1.395 - Matches _ => pbls'
1.396 - | NoMatch _ => refins' pblRD fmz pbls' pts
1.397 + Stool.Matches _ => pbls'
1.398 + | Stool.NoMatch _ => refins' pblRD fmz pbls' pts
1.399 end;
1.400
1.401 (* refine a problem; version for tactic Refine_Problem *)
1.402 @@ -584,17 +584,17 @@
1.403 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
1.404 in
1.405 if b
1.406 - then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
1.407 - else pbls @ [NoMatch_]
1.408 + then pbls @ [Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))]
1.409 + else pbls @ [Stool.NoMatch_]
1.410 end
1.411 | refin'' _ pblRD itms pbls (Ptyp (pI, [py], pys)) =
1.412 let
1.413 val {thy, ppc, where_, prls, ...} = py
1.414 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
1.415 in if b
1.416 - then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
1.417 + then let val pbl = Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))
1.418 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
1.419 - else (pbls @ [NoMatch_])
1.420 + else (pbls @ [Stool.NoMatch_])
1.421 end
1.422 | refin'' _ _ _ _ _ = error "refin': uncovered fun def."
1.423 and refins'' _ _ _ pbls [] = pbls
1.424 @@ -602,8 +602,8 @@
1.425 let
1.426 val pbls' = refin'' thy pblRD itms pbls p
1.427 in case last_elem pbls' of
1.428 - Match_ _ => pbls'
1.429 - | NoMatch_ => refins'' thy pblRD itms pbls' pts
1.430 + Stool.Match_ _ => pbls'
1.431 + | Stool.NoMatch_ => refins'' thy pblRD itms pbls' pts
1.432 end;
1.433
1.434 (* for tactic Refine_Tacitly
1.435 @@ -622,9 +622,9 @@
1.436 (* for tactic Refine_Problem
1.437 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
1.438 fun refine_pbl thy (pblID: pblID) itms =
1.439 - case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) of
1.440 + case Stool.refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) of
1.441 NONE => NONE
1.442 - | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
1.443 + | SOME (Stool.Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
1.444 | _ => error "refine_pbl: uncovered case refined_";
1.445
1.446