1.1 --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:20:53 2010 +0200
1.2 +++ b/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:36:02 2010 +0200
1.3 @@ -279,7 +279,7 @@
1.4 (*.to an input (d,ts) find the according ori and insert the ts.*)
1.5 (*WN.11.03: + dont take first inter<>[]*)
1.6 fun seek_oridts thy sel (d,ts) [] =
1.7 - ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
1.8 + ("'"^(Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy (d,ts)))^
1.9 (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
1.10 "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.11 (* val (id,vat,sel',d',ts')::oris = ori;
1.12 @@ -289,42 +289,20 @@
1.13 if sel = sel' andalso d=d' andalso (ts inter ts') <> []
1.14 then if sel = sel'
1.15 then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
1.16 - else ((string_of_cterm (comp_dts thy(d,ts)))^
1.17 + else ((Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy(d,ts)))^
1.18 " not for "^sel, e_ori_, [])
1.19 else seek_oridts thy sel (d,ts) oris;
1.20
1.21 -(*FIXXXME.WN.11.03: + dont take first inter<>[] .. ev. variants are following:
1.22 - thus take largest intersection !!!
1.23 - if sel NOTok .. then the correct itm should NOT be overwritten by insert_ppc*)
1.24 -(*fun eq7 d (_,_,_,d',_) = d = d';
1.25 -fun inter_length ((_,_,_,_,ts), (_,_,_,_,ts')) = (length ts) < (length ts');
1.26 -fun seek_oridts _ sel (d,ts) [] =
1.27 - ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
1.28 - (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
1.29 - "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.30 - (* val (id,vat,sel',d',ts')::oris = ori;
1.31 - val (id,vat,sel',d',ts') = ori;
1.32 - *)
1.33 - | seek_oridts _ sel (d,ts) oris =
1.34 - let val dscOK = filter (eq7 d) oris;
1.35 - in if dscOK = [] then ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
1.36 - "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.37 - else let val (id,vat,sel',d',ts') = gen_max inter_length dscOK;
1.38 - in if sel = sel' then ("",(id,vat,sel,d,ts inter ts'), [])
1.39 - else ("wrong field",(id,vat,sel,d,ts inter ts'), []) end
1.40 - end;
1.41 ---------------------didnt work with Add_Given/_Find/_Relation 11.03*)
1.42 -
1.43 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.44 fun seek_orits thy sel ts [] =
1.45 ("'"^
1.46 - (strs2str (map (Sign.string_of_term (sign_of thy)) ts))^
1.47 + (strs2str (map (Syntax.string_of_term (thy2ctxt' thy)) ts))^
1.48 "' not found (typed)", e_ori_, [])
1.49 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.50 if sel = sel' andalso (ts inter ts') <> []
1.51 then if sel = sel'
1.52 then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
1.53 - else (((strs2str' o map (Sign.string_of_term (sign_of thy))) ts)^
1.54 + else (((strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) ts)^
1.55 " not for "^sel, e_ori_, [])
1.56 else seek_orits thy sel ts oris;
1.57 (* false
1.58 @@ -430,7 +408,7 @@
1.59 (*28.1. val (dcr,t') = split_dsc_t fdcrs t; *)
1.60 val (dcr,[t']) = split_dts t;
1.61 in if (typeless t') mem (map typeless tss)
1.62 - then ("term '"^(Sign.string_of_term (sign_of thy) t')^
1.63 + then ("term '"^(Syntax.string_of_term (thy2ctxt' thy) t')^
1.64 "' already input")
1.65 else "" end;
1.66
1.67 @@ -799,7 +777,7 @@
1.68 val ts' = (ts_in itm_) inter ts;
1.69 in if ts subset ts'
1.70 then (((strs2str' o
1.71 - map (Sign.string_of_term (sign_of thy))) ts')^
1.72 + map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
1.73 " already input", e_itm) (*2*)
1.74 else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts')) (*3,4*)
1.75 end
1.76 @@ -821,7 +799,7 @@
1.77 in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all
1.78 (id,vt,fd,d,(ts_in itm_)@ts))
1.79 else (((strs2str' o
1.80 - map (Sign.string_of_term (sign_of thy))) ts')^
1.81 + map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
1.82 " already input", e_itm) end
1.83 | NONE =>
1.84 if all = ts
1.85 @@ -888,7 +866,7 @@
1.86 else
1.87 if d mem (map #4 ori)
1.88 then seek_oridts thy sel (d,ts) ori
1.89 - else ((Sign.string_of_term (sign_of thy) d)^
1.90 + else ((Syntax.string_of_term (thy2ctxt' thy) d)^
1.91 (*" not in example", e_ori_, []) ///11.11.03*)
1.92 " not in example", (0,[],sel,d,ts), [])
1.93 end;
1.94 @@ -1210,7 +1188,7 @@
1.95 (* test-printouts ---
1.96 val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
1.97 val _=writeln("### insert_ppc: pts= "^
1.98 -(strs2str' o map (Sign.string_of_term (sign_of thy))) pts);
1.99 +(strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) pts);
1.100
1.101
1.102 val sel = "#Given"; val Add_Given' ct = m;
1.103 @@ -1867,12 +1845,14 @@
1.104 fun chk_vars ctppc =
1.105 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1.106 appc flat (mappc (vars o term_of) ctppc)
1.107 - in let val chked = subtract op = gi wh
1.108 - if chked <> [] then ("wh\\gi", chked)
1.109 + val chked = subtract op = gi wh
1.110 + in if chked <> [] then ("wh\\gi", chked)
1.111 else let val chked = subtract op = (union op = gi fi) re
1.112 - if chked <> []
1.113 - then ("re\\(gi union fi)", chked)
1.114 - else ("ok", []) end;
1.115 + in if chked <> []
1.116 + then ("re\\(gi union fi)", chked)
1.117 + else ("ok", [])
1.118 + end
1.119 + end;
1.120
1.121 (* check a new pbltype: variables (Free) unbound by given, find*)
1.122 fun unbound_ppc ctppc =