1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:20:53 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:36:02 2010 +0200
1.3 @@ -37,12 +37,13 @@
1.4 use "ME/ptyps.sml"
1.5 use "ME/generate.sml"
1.6
1.7 +use "ME/calchead.sml"
1.8 +
1.9 ML {*
1.10 SOME 111;
1.11 *}
1.12
1.13 (*
1.14 -use "ME/calchead.sml"
1.15 use "ME/appl.sml"
1.16 use "ME/rewtools.sml"
1.17 use "ME/script.sml"
2.1 --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:20:53 2010 +0200
2.2 +++ b/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:36:02 2010 +0200
2.3 @@ -279,7 +279,7 @@
2.4 (*.to an input (d,ts) find the according ori and insert the ts.*)
2.5 (*WN.11.03: + dont take first inter<>[]*)
2.6 fun seek_oridts thy sel (d,ts) [] =
2.7 - ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
2.8 + ("'"^(Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy (d,ts)))^
2.9 (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
2.10 "' not found (typed)", (0,[],sel,d,ts):ori, [])
2.11 (* val (id,vat,sel',d',ts')::oris = ori;
2.12 @@ -289,42 +289,20 @@
2.13 if sel = sel' andalso d=d' andalso (ts inter ts') <> []
2.14 then if sel = sel'
2.15 then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
2.16 - else ((string_of_cterm (comp_dts thy(d,ts)))^
2.17 + else ((Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy(d,ts)))^
2.18 " not for "^sel, e_ori_, [])
2.19 else seek_oridts thy sel (d,ts) oris;
2.20
2.21 -(*FIXXXME.WN.11.03: + dont take first inter<>[] .. ev. variants are following:
2.22 - thus take largest intersection !!!
2.23 - if sel NOTok .. then the correct itm should NOT be overwritten by insert_ppc*)
2.24 -(*fun eq7 d (_,_,_,d',_) = d = d';
2.25 -fun inter_length ((_,_,_,_,ts), (_,_,_,_,ts')) = (length ts) < (length ts');
2.26 -fun seek_oridts _ sel (d,ts) [] =
2.27 - ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
2.28 - (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
2.29 - "' not found (typed)", (0,[],sel,d,ts):ori, [])
2.30 - (* val (id,vat,sel',d',ts')::oris = ori;
2.31 - val (id,vat,sel',d',ts') = ori;
2.32 - *)
2.33 - | seek_oridts _ sel (d,ts) oris =
2.34 - let val dscOK = filter (eq7 d) oris;
2.35 - in if dscOK = [] then ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
2.36 - "' not found (typed)", (0,[],sel,d,ts):ori, [])
2.37 - else let val (id,vat,sel',d',ts') = gen_max inter_length dscOK;
2.38 - in if sel = sel' then ("",(id,vat,sel,d,ts inter ts'), [])
2.39 - else ("wrong field",(id,vat,sel,d,ts inter ts'), []) end
2.40 - end;
2.41 ---------------------didnt work with Add_Given/_Find/_Relation 11.03*)
2.42 -
2.43 (*.to an input (_,ts) find the according ori and insert the ts.*)
2.44 fun seek_orits thy sel ts [] =
2.45 ("'"^
2.46 - (strs2str (map (Sign.string_of_term (sign_of thy)) ts))^
2.47 + (strs2str (map (Syntax.string_of_term (thy2ctxt' thy)) ts))^
2.48 "' not found (typed)", e_ori_, [])
2.49 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
2.50 if sel = sel' andalso (ts inter ts') <> []
2.51 then if sel = sel'
2.52 then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
2.53 - else (((strs2str' o map (Sign.string_of_term (sign_of thy))) ts)^
2.54 + else (((strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) ts)^
2.55 " not for "^sel, e_ori_, [])
2.56 else seek_orits thy sel ts oris;
2.57 (* false
2.58 @@ -430,7 +408,7 @@
2.59 (*28.1. val (dcr,t') = split_dsc_t fdcrs t; *)
2.60 val (dcr,[t']) = split_dts t;
2.61 in if (typeless t') mem (map typeless tss)
2.62 - then ("term '"^(Sign.string_of_term (sign_of thy) t')^
2.63 + then ("term '"^(Syntax.string_of_term (thy2ctxt' thy) t')^
2.64 "' already input")
2.65 else "" end;
2.66
2.67 @@ -799,7 +777,7 @@
2.68 val ts' = (ts_in itm_) inter ts;
2.69 in if ts subset ts'
2.70 then (((strs2str' o
2.71 - map (Sign.string_of_term (sign_of thy))) ts')^
2.72 + map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
2.73 " already input", e_itm) (*2*)
2.74 else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts')) (*3,4*)
2.75 end
2.76 @@ -821,7 +799,7 @@
2.77 in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all
2.78 (id,vt,fd,d,(ts_in itm_)@ts))
2.79 else (((strs2str' o
2.80 - map (Sign.string_of_term (sign_of thy))) ts')^
2.81 + map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
2.82 " already input", e_itm) end
2.83 | NONE =>
2.84 if all = ts
2.85 @@ -888,7 +866,7 @@
2.86 else
2.87 if d mem (map #4 ori)
2.88 then seek_oridts thy sel (d,ts) ori
2.89 - else ((Sign.string_of_term (sign_of thy) d)^
2.90 + else ((Syntax.string_of_term (thy2ctxt' thy) d)^
2.91 (*" not in example", e_ori_, []) ///11.11.03*)
2.92 " not in example", (0,[],sel,d,ts), [])
2.93 end;
2.94 @@ -1210,7 +1188,7 @@
2.95 (* test-printouts ---
2.96 val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
2.97 val _=writeln("### insert_ppc: pts= "^
2.98 -(strs2str' o map (Sign.string_of_term (sign_of thy))) pts);
2.99 +(strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) pts);
2.100
2.101
2.102 val sel = "#Given"; val Add_Given' ct = m;
2.103 @@ -1867,12 +1845,14 @@
2.104 fun chk_vars ctppc =
2.105 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
2.106 appc flat (mappc (vars o term_of) ctppc)
2.107 - in let val chked = subtract op = gi wh
2.108 - if chked <> [] then ("wh\\gi", chked)
2.109 + val chked = subtract op = gi wh
2.110 + in if chked <> [] then ("wh\\gi", chked)
2.111 else let val chked = subtract op = (union op = gi fi) re
2.112 - if chked <> []
2.113 - then ("re\\(gi union fi)", chked)
2.114 - else ("ok", []) end;
2.115 + in if chked <> []
2.116 + then ("re\\(gi union fi)", chked)
2.117 + else ("ok", [])
2.118 + end
2.119 + end;
2.120
2.121 (* check a new pbltype: variables (Free) unbound by given, find*)
2.122 fun unbound_ppc ctppc =