1.1 --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:41:56 2010 +0200
1.2 +++ b/src/Tools/isac/ME/calchead.sml Fri Aug 20 12:25:37 2010 +0200
1.3 @@ -6,6 +6,8 @@
1.4
1.5 use"ME/calchead.sml";
1.6 use"calchead.sml";
1.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 + 10 20 30 40 50 60 70 80
1.9 *)
1.10
1.11 (* TODO interne Funktionen aus sig entfernen *)
1.12 @@ -23,11 +25,11 @@
1.13 (string * (Term.term * Term.term)) list -> cterm' -> additm
1.14 type calcstate
1.15 type calcstate'
1.16 - val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
1.17 + val chk_vars : term ppc -> string * Term.term list
1.18 val chktyp :
1.19 - theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
1.20 + theory -> int * term list * term list -> term
1.21 val chktyps :
1.22 - theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
1.23 + theory -> term list * term list -> term list
1.24 val complete_metitms :
1.25 SpecifyTools.ori list ->
1.26 SpecifyTools.itm list ->
1.27 @@ -193,10 +195,10 @@
1.28 'b ->
1.29 ptree ->
1.30 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
1.31 - val tag_form : theory -> Thm.cterm * Thm.cterm -> Thm.cterm
1.32 + val tag_form : theory -> term * term -> term
1.33 val test_types : theory -> Term.term * Term.term list -> string
1.34 val typeless : Term.term -> Term.term
1.35 - val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
1.36 + val unbound_ppc : term SpecifyTools.ppc -> Term.term list
1.37 val vals_of_oris : SpecifyTools.ori list -> Term.term list
1.38 val variants_in : Term.term list -> int
1.39 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
1.40 @@ -279,31 +281,38 @@
1.41 (*.to an input (d,ts) find the according ori and insert the ts.*)
1.42 (*WN.11.03: + dont take first inter<>[]*)
1.43 fun seek_oridts thy sel (d,ts) [] =
1.44 - ("'"^(Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy (d,ts)))^
1.45 - (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
1.46 + ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
1.47 "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.48 (* val (id,vat,sel',d',ts')::oris = ori;
1.49 val (id,vat,sel',d',ts') = ori;
1.50 *)
1.51 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.52 - if sel = sel' andalso d=d' andalso (ts inter ts') <> []
1.53 - then if sel = sel'
1.54 - then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
1.55 - else ((Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy(d,ts)))^
1.56 - " not for "^sel, e_ori_, [])
1.57 + if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.58 + then if sel = sel'
1.59 + then ("",
1.60 + (id,vat,sel,d, inter op = ts ts'):ori,
1.61 + ts')
1.62 + else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))
1.63 + ^ " not for " ^ sel,
1.64 + e_ori_,
1.65 + [])
1.66 else seek_oridts thy sel (d,ts) oris;
1.67
1.68 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.69 fun seek_orits thy sel ts [] =
1.70 ("'"^
1.71 - (strs2str (map (Syntax.string_of_term (thy2ctxt' thy)) ts))^
1.72 + (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
1.73 "' not found (typed)", e_ori_, [])
1.74 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.75 - if sel = sel' andalso (ts inter ts') <> []
1.76 + if sel = sel' andalso (inter op = ts ts') <> []
1.77 then if sel = sel'
1.78 - then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
1.79 - else (((strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) ts)^
1.80 - " not for "^sel, e_ori_, [])
1.81 + then ("",
1.82 + (id,vat,sel,d, inter op = ts ts'):ori,
1.83 + ts')
1.84 + else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
1.85 + ^ " not for "^sel,
1.86 + e_ori_,
1.87 + [])
1.88 else seek_orits thy sel ts oris;
1.89 (* false
1.90 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.91 @@ -345,7 +354,7 @@
1.92 | coll eq xs (y::ys) =
1.93 let val (n,ys') = cnt eq (y::ys) y 0;
1.94 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
1.95 - val vts = (distinct (coll eq [] ts))\\[1];
1.96 + val vts = subtract op = [1] (distinct (coll eq [] ts));
1.97 in case vts of [] => 1 | [n] => n
1.98 | _ => error "different variants in formalization" end;
1.99 (*
1.100 @@ -397,35 +406,6 @@
1.101 > has_list_type (term_of ct);
1.102 val it = false : bool *)
1.103
1.104 -
1.105 -
1.106 -
1.107 -(*fdcrs = descriptions in formalization
1.108 - unused 22.11.00
1.109 -fun is_already_input thy fdcrs ts t =
1.110 - let
1.111 - val tss = flat (map isalist2list ts);
1.112 -(*28.1. val (dcr,t') = split_dsc_t fdcrs t; *)
1.113 - val (dcr,[t']) = split_dts t;
1.114 - in if (typeless t') mem (map typeless tss)
1.115 - then ("term '"^(Syntax.string_of_term (thy2ctxt' thy) t')^
1.116 - "' already input")
1.117 - else "" end;
1.118 -
1.119 -> val pts = appc (map (term_of o the o (parse thy))) pbl;
1.120 -> val ts = #Relate pts;
1.121 -> val t = (term_of o the o (parse thy))"(A=#2*a*b - a^^^#2)";
1.122 -> is_already_input thy ts t;
1.123 -val it = "term 'A = #2 * a * b - a ^^^ #2' already input" : string
1.124 -> val t = (term_of o the o (parse thy))"a=#2*R*sin alpha";
1.125 -> is_already_input thy ts t;
1.126 -val it = "term 'a = #2 * R * sin alpha' already input" : string
1.127 -> val t = (term_of o the o (parse thy))"a=R*sin alpha";
1.128 -> is_already_input thy ts t;
1.129 -val it = "" : string
1.130 -*)
1.131 -
1.132 -
1.133 fun is_parsed (Syn _) = false
1.134 | is_parsed _ = true;
1.135 fun parse_ok its = foldl and_ (true, map is_parsed its);
1.136 @@ -502,13 +482,15 @@
1.137 (* val (_,_,fd,d,ts) = hd miss;
1.138 *)
1.139 fun getr_ct thy ((_,_,fd,d,ts):ori) =
1.140 - (fd, (string_of_cterm o (comp_dts thy)) (d,[hd ts]):cterm');
1.141 + (fd, ((Syntax.string_of_term (thy2ctxt thy)) o
1.142 + (comp_dts thy)) (d,[hd ts]):cterm');
1.143 (* val t = comp_dts thy (d,[hd ts]);
1.144 *)
1.145
1.146 (* get a term from ori, notyet input in itm *)
1.147 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
1.148 - (fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');
1.149 + (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
1.150 + (d, subtract op = (ts_in itm_) ts):cterm');
1.151 (* test-maximum.sml fmy <> [], Init_Proof ...
1.152 val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
1.153 val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
1.154 @@ -516,8 +498,8 @@
1.155 atomty d';
1.156 atomty (hd ts);
1.157 atomty ts';
1.158 - cterm_of (sign_of thy) (d $ (hd ts));
1.159 - cterm_of (sign_of thy) (d' $ ts');
1.160 + Thm.cterm_of thy (d $ (hd ts));
1.161 + Thm.cterm_of thy (d' $ ts');
1.162
1.163 comp_dts thy (d,ts);
1.164 *)
1.165 @@ -530,6 +512,11 @@
1.166
1.167 (* select an item in oris, notyet input in itms
1.168 (precondition: in itms are only Cor, Sup, Inc) *)
1.169 +local
1.170 +infix mem;
1.171 +fun x mem [] = false
1.172 + | x mem (y :: ys) = x = y orelse x mem ys;
1.173 +in
1.174 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
1.175 let
1.176 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
1.177 @@ -540,7 +527,7 @@
1.178 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
1.179 *)
1.180 (f,(d,_))::itms =>
1.181 - SOME (f:string, (string_of_cterm o comp_dts thy) (d,[]):cterm')
1.182 + SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
1.183 | _ => NONE end
1.184
1.185 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.186 @@ -554,7 +541,7 @@
1.187 (* val itm = hd icl; val (_,_,_,d,ts) = v6;
1.188 *)
1.189 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
1.190 - (d_in (#5 itm)) = d andalso (ts_in (#5 itm)) subset ts;
1.191 + (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
1.192 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
1.193 | false_and_not_Sup (i,v,false,f, _) = true
1.194 | false_and_not_Sup _ = false;
1.195 @@ -576,7 +563,8 @@
1.196 *)
1.197 NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
1.198 | SOME ori => SOME (geti_ct thy ori (hd icl))
1.199 - end;
1.200 + end
1.201 +end;
1.202
1.203
1.204
1.205 @@ -699,10 +687,10 @@
1.206 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
1.207 (id,vt,cl,sl,Cor (d,ts)):itm
1.208 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
1.209 - raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
1.210 + raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.211 " not not for Syn (s:cterm')")
1.212 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
1.213 - raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
1.214 + raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.215 " not not for Typ (s:cterm')")
1.216 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
1.217 (id,vt,cl,sl,Fal (d,ts))
1.218 @@ -718,7 +706,7 @@
1.219 fun is_field_correct sel d dscpbt =
1.220 case assoc (dscpbt, sel) of
1.221 NONE => false
1.222 - | SOME ds => d mem ds;
1.223 + | SOME ds => member op = ds d;
1.224
1.225 (*. update the itm_ already input, all..from ori .*)
1.226 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
1.227 @@ -729,7 +717,7 @@
1.228 val pval = pbl_ids' thy d ts'
1.229 (*WN.9.5.03: FIXXXME [#0, epsilon]
1.230 here would upd_penv be called for [#0, epsilon] etc. *)
1.231 - val complete = if eq_set (ts', all) then true else false;
1.232 + val complete = if eq_set op = (ts', all) then true else false;
1.233 in case itm_ of
1.234 (Cor _) =>
1.235 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
1.236 @@ -774,42 +762,20 @@
1.237 (case find_first (eq3 f d) itms of
1.238 SOME (_,_,_,_,itm_) =>
1.239 let
1.240 - val ts' = (ts_in itm_) inter ts;
1.241 - in if ts subset ts'
1.242 + val ts' = inter op = (ts_in itm_) ts;
1.243 + in if subset op = (ts, ts')
1.244 then (((strs2str' o
1.245 - map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
1.246 + map (Syntax.string_of_term (thy2ctxt thy))) ts')^
1.247 " already input", e_itm) (*2*)
1.248 - else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts')) (*3,4*)
1.249 + else ("",
1.250 + ori_2itm thy itm_ pid all (i,v,f,d,
1.251 + subtract op = ts' ts)) (*3,4*)
1.252 end
1.253 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
1.254 pid all (i,v,f,d,ts)) (*1*)
1.255 )
1.256 | NONE => ("", ori_2itm thy (Sup (d,ts))
1.257 e_term all (i,v,f,d,ts));
1.258 -(*------------------------------------------------
1.259 -fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
1.260 -fun is_notyet_input thy itms pval all ((id,vt,fd,d,ts):ori) pbt =
1.261 - case find_first (eq1 d) pbt of
1.262 - SOME (_,(_,pid)) => (* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
1.263 - *)
1.264 - (case seek_ppc id itms of
1.265 - SOME (id',_,_,_,itm_) =>
1.266 - let
1.267 - val ts' = (ts_in itm_) inter ts;
1.268 - in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all
1.269 - (id,vt,fd,d,(ts_in itm_)@ts))
1.270 - else (((strs2str' o
1.271 - map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
1.272 - " already input", e_itm) end
1.273 - | NONE =>
1.274 - if all = ts
1.275 - then ("", ori_2itm (Cor ((e_term,[]),(pid,[])))
1.276 - (pid, pval) all (id,vt,fd,d,ts))
1.277 - else ("", ori_2itm (Inc ((e_term,[]),(e_term,[])))
1.278 - (pid, pval) all (id,vt,fd,d,ts))
1.279 - )
1.280 - | NONE => ("", ori_2itm (Sup (e_term,[]))
1.281 - (e_term, []) all (id,vt,fd,d,ts));----*)
1.282
1.283 fun test_types thy (d,ts) =
1.284 let
1.285 @@ -817,9 +783,9 @@
1.286 val opt = (try (comp_dts thy)) (d,ts);
1.287 val msg = case opt of
1.288 SOME _ => ""
1.289 - | NONE => ((Sign.string_of_term (sign_of thy) d)^" "^
1.290 - ((strs2str' o map (Sign.string_of_term(sign_of thy)))ts)
1.291 - ^" is illtyped");
1.292 + | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
1.293 + ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
1.294 + ^ " is illtyped");
1.295 val _ = show_types:= s
1.296 in msg end;
1.297
1.298 @@ -846,16 +812,16 @@
1.299 val (d,ts(*,pval*)) = split_dts thy t;
1.300 val ids = map (fst o dest_Free)
1.301 ((distinct o (flat o (map vars))) ts);
1.302 - in if (ids \\ oids) <> []
1.303 - then (("identifiers "^(strs2str' (ids \\ oids))^
1.304 + in if (subtract op = oids ids) <> []
1.305 + then (("identifiers "^(strs2str' (subtract op = oids ids))^
1.306 " not in example"), e_ori_, [])
1.307 else
1.308 if d = e_term
1.309 then
1.310 - if not ((map typeless ts) subset (map typeless ots))
1.311 + if not (subset op = (map typeless ts, map typeless ots))
1.312 then (("terms '"^
1.313 - ((strs2str' o (map (Sign.string_of_term
1.314 - (sign_of thy)))) ts)^
1.315 + ((strs2str' o (map (Syntax.string_of_term
1.316 + (thy2ctxt thy)))) ts)^
1.317 "' not in example (typeless)"), e_ori_, [])
1.318 else (case seek_orits thy sel ts ori of
1.319 ("", ori_ as (_,_,_,d,ts), all) =>
1.320 @@ -864,9 +830,9 @@
1.321 | msg => (msg, e_ori_, []))
1.322 | (msg,_,_) => (msg, e_ori_, []))
1.323 else
1.324 - if d mem (map #4 ori)
1.325 + if member op = (map #4 ori) d
1.326 then seek_oridts thy sel (d,ts) ori
1.327 - else ((Syntax.string_of_term (thy2ctxt' thy) d)^
1.328 + else ((Syntax.string_of_term (thy2ctxt thy) d)^
1.329 (*" not in example", e_ori_, []) ///11.11.03*)
1.330 " not in example", (0,[],sel,d,ts), [])
1.331 end;
1.332 @@ -999,11 +965,11 @@
1.333 (*.split type-wrapper from scr-arg and build part of an ori;
1.334 an type-error is reported immediately, raises an exn,
1.335 subsequent handling of exn provides 2nd part of error message.*)
1.336 -fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
1.337 +(*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term
1.338 (* val (thy, (str, (dsc, _)), (ty $ var)) =
1.339 (thy, p, a);
1.340 *)
1.341 - (cterm_of (sign_of thy) (dsc $ var);(*type check*)
1.342 + (Thm.cterm_of thy (dsc $ var);(*type check*)
1.343 SOME ((([1], str, dsc, (*[var]*)
1.344 split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.345 handle e as TYPE _ =>
1.346 @@ -1017,6 +983,25 @@
1.347 ^"*** checked by theory: "^(theory2str thy)^"\n"
1.348 ^"*** "^dots 66);
1.349 print_exn e; (*raises exn again*)
1.350 + NONE);*)
1.351 +fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
1.352 + (* val (thy, (str, (dsc, _)), (ty $ var)) =
1.353 + (thy, p, a);
1.354 + *)
1.355 + (Thm.cterm_of thy (dsc $ var);(*type check*)
1.356 + SOME ((([1], str, dsc, (*[var]*)
1.357 + split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.358 + handle e as TYPE _ =>
1.359 + (writeln (dashs 70^"\n"
1.360 + ^"*** ERROR while creating the items for the model of the ->problem\n"
1.361 + ^"*** from the ->stac with ->typeconstructor in arglist:\n"
1.362 + ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
1.363 + ^"*** description: "^(term_detail2str dsc)
1.364 + ^"*** value: "^(term_detail2str var)
1.365 + ^"*** typeconstructor in script: "^(term_detail2str ty)
1.366 + ^"*** checked by theory: "^(theory2str thy)^"\n"
1.367 + ^"*** "^dots 66);
1.368 + (*WN100820 postponed: print_exn e; raises exn again*)
1.369 NONE);
1.370 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
1.371 > val Const ("Script.SubProblem",_) $
1.372 @@ -1139,7 +1124,8 @@
1.373 fun overwrite_ppc thy itm ppc =
1.374 let
1.375 fun repl ppc' (_,_,_,_,itm_) [] =
1.376 - raise error ("overwrite_ppc: "^(itm__2str thy itm_)^" not found")
1.377 + raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
1.378 + " not found")
1.379 | repl ppc' itm (p::ppc) =
1.380 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
1.381 else repl (ppc' @ [p]) itm ppc
1.382 @@ -1186,9 +1172,9 @@
1.383
1.384
1.385 (* test-printouts ---
1.386 -val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
1.387 +val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
1.388 val _=writeln("### insert_ppc: pts= "^
1.389 -(strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) pts);
1.390 +(strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
1.391
1.392
1.393 val sel = "#Given"; val Add_Given' ct = m;
1.394 @@ -1384,6 +1370,7 @@
1.395 meth=met, ...}) = get_obj I pt p;
1.396 (*val pt = update_pbl pt p itms;
1.397 val pt = update_pblID pt p pI;*)
1.398 + val thy = assoc_thy dI
1.399 val ((p,Pbl),_,_,pt)=
1.400 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1.401 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.402 @@ -1500,7 +1487,7 @@
1.403 (*TODO.WN03 pass error-msgs to the frontend..
1.404 FIXME ..and dont abuse a tactic for that purpose*)
1.405 ([(Tac msg,
1.406 - Tac_ (ProtoPure.thy, msg,msg,msg),
1.407 + Tac_ (theory "Pure", msg,msg,msg),
1.408 (e_pos', e_istate))], [], ptp)
1.409 end
1.410
1.411 @@ -1558,7 +1545,7 @@
1.412 (#4:ori -> term)) oris;
1.413 in filter_outs ors itms end;
1.414
1.415 -fun memI a b = b mem a;
1.416 +fun memI a b = member op = a b;
1.417 (*filter oris which are in pbt, too*)
1.418 fun filter_pbt oris pbt =
1.419 let val dscs = map (fst o snd) pbt
1.420 @@ -1566,6 +1553,11 @@
1.421
1.422 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1.423 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1.424 +local
1.425 +infix mem;
1.426 +fun x mem [] = false
1.427 + | x mem (y :: ys) = x = y orelse x mem ys;
1.428 +in
1.429 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1.430 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1.431 *)
1.432 @@ -1575,11 +1567,17 @@
1.433 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1.434 val os = filter_outs ors itms;
1.435 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1.436 - in itms @ (map (ori2Coritm met) os) end;
1.437 + in itms @ (map (ori2Coritm met) os) end
1.438 +end;
1.439
1.440
1.441
1.442 (*.complete model and guard of a calc-head .*)
1.443 +local
1.444 +infix mem;
1.445 +fun x mem [] = false
1.446 + | x mem (y :: ys) = x = y orelse x mem ys;
1.447 +in
1.448 fun complete_mod_ (oris, mpc, ppc, probl) =
1.449 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1.450 val vat = if probl = [] then 1 else max_vt probl
1.451 @@ -1589,7 +1587,8 @@
1.452
1.453 val pits = pits @ (map (ori2Coritm ppc) pors)
1.454 val mits = complete_metitms oris pits [] mpc
1.455 - in (pits, mits) end;
1.456 + in (pits, mits) end
1.457 +end;
1.458
1.459 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1.460 (if dI = e_domID then odI else dI,
1.461 @@ -1606,6 +1605,7 @@
1.462 let
1.463 val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
1.464 val (dI,pI,mI) = some_spec ospec spec
1.465 + val thy = assoc_thy dI
1.466 val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
1.467 val {cas,ppc,...} = get_pbt pI
1.468 val pbl = init_pbl ppc (*fill in descriptions*)
1.469 @@ -1634,6 +1634,7 @@
1.470 val pbl = init_pbl ppc
1.471 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.472 val mI = if length met = 0 then e_metID else hd met
1.473 + val thy = assoc_thy dI
1.474 val (pos,c,_,pt) =
1.475 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.476 Uistate pos pt
1.477 @@ -1710,9 +1711,16 @@
1.478 raise error ("nxt_specif: not impl. for "^tac2str m');
1.479
1.480 (*.get the values from oris; handle the term list w.r.t. penv.*)
1.481 +
1.482 +local
1.483 +infix mem;
1.484 +fun x mem [] = false
1.485 + | x mem (y :: ys) = x = y orelse x mem ys;
1.486 +in
1.487 fun vals_of_oris oris =
1.488 ((map (mkval' o (#5:ori -> term list))) o
1.489 - (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris;
1.490 + (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1.491 +end;
1.492
1.493
1.494
1.495 @@ -1782,21 +1790,25 @@
1.496 in f end;
1.497
1.498
1.499 -
1.500 -
1.501 -
1.502 -
1.503 -(* --------------------- ME --------------------- *)
1.504 -fun tag_form thy (formal, given) = cterm_of (sign_of thy)
1.505 - (((head_of o term_of) given) $ (term_of formal));
1.506 +(*fun tag_form thy (formal, given) = Thm.cterm_of thy
1.507 + (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1.508 +fun tag_form thy (formal, given) =
1.509 + (let val gf = (head_of given) $ formal;
1.510 + val _ = Thm.cterm_of thy gf
1.511 + in gf end)
1.512 + handle _ => raise error ("calchead.tag_form: " ^
1.513 + Syntax.string_of_term (thy2ctxt thy) given ^
1.514 + " .. " ^
1.515 + Syntax.string_of_term (thy2ctxt thy) formal ^
1.516 + " ..types do not match");
1.517 (* val formal = (the o (parse thy)) "[R::real]";
1.518 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1.519 > tag_form thy (formal, given);
1.520 val it = "fixed_values [R]" : cterm
1.521 *)
1.522 fun chktyp thy (n, fs, gs) =
1.523 - ((writeln o string_of_cterm o (nth n)) fs;
1.524 - (writeln o string_of_cterm o (nth n)) gs;
1.525 + ((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
1.526 + (writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
1.527 tag_form thy (nth n fs, nth n gs));
1.528
1.529 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1.530 @@ -1844,7 +1856,7 @@
1.531 else ("ok",[]) end;*)
1.532 fun chk_vars ctppc =
1.533 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1.534 - appc flat (mappc (vars o term_of) ctppc)
1.535 + appc flat (mappc vars ctppc)
1.536 val chked = subtract op = gi wh
1.537 in if chked <> [] then ("wh\\gi", chked)
1.538 else let val chked = subtract op = (union op = gi fi) re
1.539 @@ -1857,7 +1869,7 @@
1.540 (* check a new pbltype: variables (Free) unbound by given, find*)
1.541 fun unbound_ppc ctppc =
1.542 let val {Given=gi,Find=fi,Relate=re,...} =
1.543 - appc flat (mappc (vars o term_of) ctppc)
1.544 + appc flat (mappc vars ctppc)
1.545 in distinct (*re\\(gi union fi)*)
1.546 (subtract op = (union op = gi fi) re) end;
1.547 (*
1.548 @@ -1880,9 +1892,9 @@
1.549 in ((fld f) o rev) xs end;
1.550 (*
1.551 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1.552 -> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
1.553 +> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
1.554 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1.555 -> cterm_of (sign_of thy) conj;
1.556 +> Thm.cterm_of thy conj;
1.557 val it = "(a = b & c = d) & e = f" : cterm
1.558 *)
1.559
1.560 @@ -1892,9 +1904,9 @@
1.561 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1.562 (*
1.563 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1.564 -> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
1.565 +> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
1.566 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1.567 -> cterm_of (sign_of thy) conj;
1.568 +> Thm.cterm_of thy conj;
1.569 val it = "a = b & c = d & e = f & g = h" : cterm
1.570 *)
1.571
1.572 @@ -1920,8 +1932,7 @@
1.573 *)
1.574
1.575 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1.576 -fun eq4 v (_,vts,_,_,_) = v mem vts;
1.577 -(*((curry (op mem)) (vat:int)) o (#2:ori -> int list);*)
1.578 +fun eq4 v (_,vts,_,_,_) = member op = vts v;
1.579 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1.580
1.581