1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Sun Dec 18 16:27:41 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Dec 19 09:02:41 2016 +0100
1.3 @@ -5,42 +5,37 @@
1.4
1.5 signature MODEL_SPECIFY =
1.6 sig
1.7 - (* for generate.sml *)
1.8 - val itms2itemppc : theory -> itm list -> (bool * term) list -> item ppc
1.9 - val get_met : metID -> met
1.10 - (* for calchead.sml *)
1.11 - val itm_out : 'a -> itm_ -> string
1.12 - val dsc_unknown : term
1.13 + type field
1.14 + (* for calchead.sml, if below at left margin *)
1.15 + val prep_ori : fmz_ -> theory -> field list -> ori list * Proof.context
1.16 val add_id : 'a list -> (int * 'a) list
1.17 - val get_pbt : pblID -> pbt
1.18 - val prep_ori : string list -> theory -> (string * (term * 'a)) list ->
1.19 - (int * int list * string * term * term list) list * Proof.context
1.20 - val add_field' : theory -> (string * (term * 'a)) list -> ori list -> ori list
1.21 - val match_itms_oris : theory -> itm list -> (string * (term * term)) list * term list * rls ->
1.22 + val add_field' : theory -> field list -> ori list -> ori list
1.23 + val match_itms_oris : theory -> itm list -> field list * term list * rls ->
1.24 ori list -> bool * (itm list * (bool * term) list)
1.25 val refine_ori : ori list -> pblID -> pblID option
1.26 + val refine_ori' : ori list -> pblID -> pblID
1.27 val refine_pbl : theory -> pblID -> itm list -> (pblID * (itm list * (bool * term) list)) option
1.28 - val refine_ori' : ori list -> pblID -> pblID
1.29 +
1.30 val appc : ('a list -> 'b list) -> 'a ppc -> 'b ppc
1.31 val mappc : ('a -> 'b) -> 'a ppc -> 'b ppc
1.32 - (* for appl.sml *)
1.33 - (* for rewtools.sml *)
1.34 - (* for script.sml *)
1.35 - (* for inform.sml *)
1.36 - val get_the : theID -> thydata
1.37 - (* for datatypes.sml *)
1.38 - val kestoreID2guh : ketype -> kestoreID -> guh
1.39 - val pblID2guh : pblID -> guh
1.40 - val metID2guh : metID -> guh
1.41 - (* for pbl-met-hierarchy.sml *)
1.42 - type pblRD = string list
1.43 - val get_met' : theory -> metID -> met
1.44 - (* for thy-hierarchy.sml *)
1.45 - val format_pblIDl : string list list -> string
1.46 - val scan : string list -> 'a ptyp list -> string list list
1.47 - (* for interface.sml *)
1.48 - val guh2kestoreID : guh -> string list
1.49 - (* for Knowledge/ *)
1.50 + val itms2itemppc : theory -> itm list -> (bool * term) list -> item ppc (* for generate.sml *)
1.51 +
1.52 + val get_pbt : pblID -> pbt
1.53 + val get_met : metID -> met (* for generate.sml *)
1.54 + val get_met' : theory -> metID -> met (* for pbl-met-hierarchy.sml *)
1.55 + val get_the : theID -> thydata (* for inform.sml *)
1.56 +
1.57 + type pblRD = string list (* for pbl-met-hierarchy.sml *)
1.58 + val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
1.59 + val scan : string list -> 'a ptyp list -> string list list (* for thy-hierarchy.sml *)
1.60 + val itm_out : theory -> itm_ -> string
1.61 + val dsc_unknown : term
1.62 +
1.63 + val pblID2guh : pblID -> guh (* for datatypes.sml *)
1.64 + val metID2guh : metID -> guh (* for datatypes.sml *)
1.65 + val kestoreID2guh : ketype -> kestoreID -> guh (* for datatypes.sml *)
1.66 + val guh2kestoreID : guh -> string list (* for interface.sml *)
1.67 + (* for Knowledge/, if below at left margin *)
1.68 val prep_pbt : theory -> guh -> string list -> pblID ->
1.69 string list * (string * string list) list * rls * string option * metID list -> pbt * pblID
1.70 val prep_met : theory -> string -> string list -> pblID ->
1.71 @@ -64,6 +59,7 @@
1.72 struct
1.73 (**)
1.74
1.75 +type field = string * (term * term)
1.76 val dsc_unknown = (Thm.term_of o the o (parseold @{theory Script})) "unknown::'a => unknow";
1.77
1.78 fun itm_2item (_: theory) (Cor ((d, ts), _)) = Correct (term2str (comp_dts (d, ts)))
1.79 @@ -79,25 +75,6 @@
1.80 fun appc f ({Given = gi, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc) =
1.81 {Given = f gi, Where = f wh, Find = f fi, With = f wi, Relate = f re}: 'b ppc
1.82
1.83 -(* for ppc of changing type *)
1.84 -fun sel_ppc sel ppc =
1.85 - case sel of
1.86 - "#Given" => #Given (ppc: 'a ppc)
1.87 - | "#Where" => #Where (ppc: 'a ppc)
1.88 - | "#Find" => #Find (ppc: 'a ppc)
1.89 - | "#With" => #With (ppc: 'a ppc)
1.90 - | "#Relate" => #Relate (ppc: 'a ppc)
1.91 - | _ => error ("sel_ppc tried to select by \"" ^ sel ^ "\"");
1.92 -
1.93 -fun repl_sel_ppc sel ({Given = gi, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc) x =
1.94 - case sel of
1.95 - "#Given" => ({Given = x, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc)
1.96 - | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
1.97 - | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
1.98 - | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
1.99 - | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
1.100 - | _ => error ("repl_sel_ppc tried to select by \"" ^ sel ^ "\"");
1.101 -
1.102 fun add_sel_ppc (_: theory) sel ({Given = gi, Where = wh, Find = fi, With = wi, Relate = re}: 'a ppc) x =
1.103 case sel of
1.104 "#Given" => ({Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}: 'a ppc)
1.105 @@ -109,28 +86,13 @@
1.106 fun add_where ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}: 'a ppc) wh =
1.107 ({Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}: 'a ppc)
1.108
1.109 -(* decompose a problem-type into description and identifier
1.110 - FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
1.111 -fun split_dsc _ t =
1.112 - (let val (hd, args) = strip_comb t
1.113 - in
1.114 - if is_dsc hd
1.115 - then (hd, args)
1.116 - else (e_term, [t]) (*??? 9.01 just copied*)
1.117 - end)
1.118 - handle _ => error ("split_dsc: called with " ^ term2str t);
1.119 -
1.120 -(* take the first two return-values; for prep_ori *)
1.121 -fun split_dsc' t =
1.122 - (let val dsc $ var = t
1.123 - in var end)
1.124 - handle _ => error ("split_dsc': called with " ^ term2str t)
1.125 -
1.126 (* split a term into description and (id | structured variable) for pbt, met.ppc *)
1.127 fun split_did t =
1.128 - (let val (hd, [arg]) = strip_comb t
1.129 - in (hd, arg) end)
1.130 - handle _ => error ("split_did: doesn't match (hd,[arg]) for t = " ^ term2str t)
1.131 + let
1.132 + val (hd, [arg]) = case strip_comb t of
1.133 + (hd, [arg]) => (hd, [arg])
1.134 + | _ => error ("split_did: doesn't match (hd,[arg]) for t = " ^ term2str t)
1.135 + in (hd, arg) end
1.136
1.137 (*create output-string for itm_*)
1.138 fun itm_out _ (Cor ((d, ts), _)) = term2str (comp_dts (d, ts))
1.139 @@ -192,23 +154,11 @@
1.140 fun eq (a, b) = curry op= (snd3 a) (snd3 b);
1.141 in mark eq fdts end;
1.142
1.143 -(* collect equal elements: the model for coll_variants *)
1.144 -fun coll eq xs =
1.145 - let
1.146 - fun col xs _ x [] = xs @ [x]
1.147 - | col xs eq x (y :: ys) = if eq(x, y) then col xs eq x ys else col (xs @ [x]) eq y ys;
1.148 - in col [] eq (hd xs) xs end;
1.149 -
1.150 fun max [] = error "max of []"
1.151 | max (y :: ys) =
1.152 let fun mx x [] = x
1.153 | mx x (y :: ys) = if x < y then mx y ys else mx x ys;
1.154 in mx y ys end;
1.155 -fun gen_max _ [] = error "gen_max of []"
1.156 - | gen_max ord (y::ys) =
1.157 - let fun mx x [] = x
1.158 - | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
1.159 -in mx y ys end;
1.160
1.161 fun coll_variants (((v,x) :: vxs)) =
1.162 let
1.163 @@ -230,8 +180,6 @@
1.164 in add 1 xs end;
1.165
1.166 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
1.167 -fun flattup' (a, (b, ((c,d), e))) = (a, b, c, d, e);
1.168 -fun flat3 (a, (b, c)) = (a, b, c);
1.169
1.170 fun prep_ori [] _ _ = ([], e_ctxt)
1.171 | prep_ori fmz thy pbt =
1.172 @@ -267,14 +215,6 @@
1.173 fun get_met' thy (metID : metID) = get_py (KEStore_Elems.get_mets thy) metID metID;
1.174 fun get_the (theID : theID) = get_py (get_thes ()) theID theID;
1.175
1.176 -fun del_eq k ptyps =
1.177 - let
1.178 - fun del _ ptyps [] = ptyps
1.179 - | del k ptyps ((Ptyp (k', [p], ps)) :: pys) =
1.180 - if k = k' then del k ptyps pys else del k (ptyps @ [Ptyp (k', [p], ps)]) pys
1.181 - | del _ _ _ = error "del_eq: uncovered fun def."
1.182 - in del k [] ptyps end;
1.183 -
1.184 (* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)
1.185 fun guh2kestoreID (guh: guh) =
1.186 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.187 @@ -410,8 +350,8 @@
1.188 | scan id ((Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
1.189 | scan id ((Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
1.190
1.191 -fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ());
1.192 -fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ());
1.193 +fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ()); (* for tests *)
1.194 +fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)
1.195
1.196
1.197 (** instantiate a problem-type **)
1.198 @@ -420,18 +360,10 @@
1.199
1.200 fun coll_vats (vats, ((_, vs, _, _, _): ori)) = union op = vats vs;
1.201 fun filter_vat oris i = filter ((member_swap op = i) o (#2 : ori -> int list)) oris;
1.202 -fun separate_vats oris =
1.203 - let
1.204 - val vats = foldl coll_vats ([] : int list, oris);
1.205 - in
1.206 - map (filter_vat oris) vats
1.207 - end;
1.208
1.209 (** check a problem (ie. itm list) for matching a problemtype **)
1.210
1.211 fun eq1 d (_, (d', _)) = (d = d');
1.212 -fun itm_id ((i, _, _, _, _): itm) = i;
1.213 -fun ori_id ((i, _, _, _, _): ori) = i;
1.214 fun ori2itmSup ((i, v, _, d, ts): ori) = ((i, v, true, "#Given", Sup (d, ts)): itm);
1.215 (*see + add_sel_ppc ~~~~~~~*)
1.216
1.217 @@ -578,7 +510,7 @@
1.218 Matches' of item ppc
1.219 | NoMatch' of item ppc;
1.220
1.221 -(* match a formalization with a problem type *)
1.222 +(* match a formalization with a problem type, for tests *)
1.223 fun match_pbl (fmz: fmz_) ({thy = thy, where_ = pre, ppc, prls = er, ...}: pbt) =
1.224 let
1.225 val oris = prep_ori fmz thy ppc |> #1;
1.226 @@ -696,7 +628,7 @@
1.227 | _ => error "refine_pbl: uncovered case refined_";
1.228
1.229
1.230 -(* for math-experts
1.231 +(* for math-experts and test;
1.232 FIXME.WN021019: needs thy for parsing fmz *)
1.233 fun refine (fmz: fmz_) (pblID: pblID) =
1.234 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID);
1.235 @@ -712,20 +644,20 @@
1.236 | kestoreID2guh ketype kestoreID =
1.237 error ("kestoreID2guh: \"" ^ ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
1.238
1.239 -fun show_pblguhs () =
1.240 +fun show_pblguhs () = (* for tests *)
1.241 (default_print_depth 999;
1.242 (tracing o strs2str o (map linefeed)) (coll_pblguhs (get_ptyps ()));
1.243 default_print_depth 3);
1.244 -fun sort_pblguhs () =
1.245 +fun sort_pblguhs () = (* for tests *)
1.246 (default_print_depth 999;
1.247 (tracing o strs2str o (map linefeed)) (((sort string_ord) o coll_pblguhs) (get_ptyps ()));
1.248 default_print_depth 3);
1.249
1.250 -fun show_metguhs () =
1.251 +fun show_metguhs () = (* for tests *)
1.252 (default_print_depth 999;
1.253 (tracing o strs2str o (map linefeed)) (coll_metguhs (get_mets ()));
1.254 default_print_depth 3);
1.255 -fun sort_metguhs () =
1.256 +fun sort_metguhs () = (* for tests *)
1.257 (default_print_depth 999;
1.258 (tracing o strs2str o (map linefeed)) (((sort string_ord) o coll_metguhs) (get_mets ()));
1.259 default_print_depth 3);
2.1 --- a/test/Tools/isac/Interpret/ptyps.sml Sun Dec 18 16:27:41 2016 +0100
2.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Mon Dec 19 09:02:41 2016 +0100
2.3 @@ -14,7 +14,6 @@
2.4 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
2.5 "----------- fun coll_guhs ---------------------------------------";
2.6 "----------- fun guh2kestoreID -----------------------------------";
2.7 -"----------- fun split_dsc ---------------------------------------";
2.8 "----------- fun mark --------------------------------------------";
2.9 "----------- fun coll --------------------------------------------";
2.10 "----------- fun coll_variants -----------------------------------";
2.11 @@ -469,18 +468,6 @@
2.12 nodes [] guh3 (get_ptyps ());
2.13 nodes [] guh21 (get_ptyps ());
2.14 *)
2.15 -"----------- fun split_dsc ---------------------------------------";
2.16 -"----------- fun split_dsc ---------------------------------------";
2.17 -"----------- fun split_dsc ---------------------------------------";
2.18 -(*
2.19 -> val t1 = (Thm.term_of o the o (parse thy)) "errorBound err_";
2.20 -> split_dsc t1;
2.21 -(Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
2.22 - : term * term
2.23 -> val t3 = (Thm.term_of o the o (parse thy)) "valuesFor vs_";
2.24 -> split_dsc t3;
2.25 -(Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
2.26 - Free ("vs_","bool List.list")) : term * term*)
2.27
2.28 "----------- fun mark --------------------------------------------";
2.29 "----------- fun mark --------------------------------------------";