1.1 --- a/src/Tools/isac/Interpret/calchead.sml Fri Oct 08 18:58:24 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sat Oct 09 16:03:49 2010 +0200
1.3 @@ -278,38 +278,38 @@
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 - ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
1.8 - "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.9 - (* val (id,vat,sel',d',ts')::oris = ori;
1.10 - val (id,vat,sel',d',ts') = ori;
1.11 - *)
1.12 + ("'" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
1.13 + (comp_dts thy (d,ts))) ^
1.14 + "' not found (typed)", (0, [], sel, d, ts) : ori,
1.15 + [])
1.16 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.17 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.18 then if sel = sel'
1.19 then ("",
1.20 (id,vat,sel,d, inter op = ts ts'):ori,
1.21 ts')
1.22 - else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))
1.23 - ^ " not for " ^ sel,
1.24 + else ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
1.25 + (comp_dts thy (d,ts))) ^ " not for " ^ sel,
1.26 e_ori_,
1.27 [])
1.28 else seek_oridts thy sel (d,ts) oris;
1.29
1.30 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.31 fun seek_orits thy sel ts [] =
1.32 - ("'"^
1.33 - (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
1.34 + ("'" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
1.35 + (thy2ctxt thy))) ts) ^
1.36 "' not found (typed)", e_ori_, [])
1.37 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.38 if sel = sel' andalso (inter op = ts ts') <> []
1.39 - then if sel = sel'
1.40 - then ("",
1.41 - (id,vat,sel,d, inter op = ts ts'):ori,
1.42 - ts')
1.43 - else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
1.44 - ^ " not for "^sel,
1.45 - e_ori_,
1.46 - [])
1.47 + then if sel = sel'
1.48 + then ("",
1.49 + (id,vat,sel,d, inter op = ts ts'):ori,
1.50 + ts')
1.51 + else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.52 + (thy2ctxt thy)))) ts)
1.53 + ^ " not for " ^ sel,
1.54 + e_ori_,
1.55 + [])
1.56 else seek_orits thy sel ts oris;
1.57 (* false
1.58 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.59 @@ -479,7 +479,7 @@
1.60 (* val (_,_,fd,d,ts) = hd miss;
1.61 *)
1.62 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.63 - (fd, ((Syntax.string_of_term (thy2ctxt thy)) o
1.64 + (fd, (Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy))) o
1.65 (comp_dts thy)) (d,[hd ts]) : cterm');
1.66 (* val t = comp_dts thy (d,[hd ts]);
1.67 *)
1.68 @@ -488,8 +488,9 @@
1.69 the term from ori is thrown back to a string in order to reuse
1.70 machinery for immediate input by the user. *)
1.71 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.72 - (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
1.73 - (d, subtract op = (ts_in itm_) ts) : cterm');
1.74 + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.75 + (comp_dts thy))
1.76 + (d, subtract op = (ts_in itm_) ts) : cterm');
1.77 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.78 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.79 (comp_dts thy))
1.80 @@ -516,7 +517,9 @@
1.81 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
1.82 *)
1.83 (f,(d,_))::itms =>
1.84 - SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
1.85 + SOME (f : string,
1.86 + ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.87 + comp_dts thy) (d, []) : cterm')
1.88 | _ => NONE end
1.89
1.90 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.91 @@ -631,32 +634,6 @@
1.92 (2,[2],true,"#Find",Syn("empty"))];
1.93 *)
1.94
1.95 -
1.96 -(* ^^^--- aus nnewcode.sml am 30.1.00 ---^^^ *)
1.97 -(*#############################################################*)
1.98 -(*#############################################################*)
1.99 -(* vvv--- aus nnewcode.sml vor 29.1.00 ---vvv *)
1.100 -
1.101 -(*3.3.--
1.102 -fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
1.103 - (id,vt,cl,sl,Cor (d,ts)):itm
1.104 - | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
1.105 - error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.106 - " not not for Syn (s:cterm')")
1.107 - | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
1.108 - error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.109 - " not not for Typ (s:cterm')")
1.110 - | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
1.111 - (id,vt,cl,sl,Fal (d,ts))
1.112 - | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =
1.113 - (id,vt,cl,sl,Inc (d,ts))
1.114 - | update_itm (cl,d,ts) (id,vt,_,sl,Sup (_,_)) =
1.115 - (id,vt,cl,sl,Sup (d,ts));
1.116 -*)
1.117 -
1.118 -
1.119 -
1.120 -
1.121 fun is_field_correct sel d dscpbt =
1.122 case assoc (dscpbt, sel) of
1.123 NONE => false
1.124 @@ -719,7 +696,8 @@
1.125 val ts' = inter op = (ts_in itm_) ts;
1.126 in if subset op = (ts, ts')
1.127 then (((strs2str' o
1.128 - map (Syntax.string_of_term (thy2ctxt thy))) ts')^
1.129 + map (Print_Mode.setmp [] (Syntax.string_of_term
1.130 + (thy2ctxt thy)))) ts') ^
1.131 " already input", e_itm) (*2*)
1.132 else ("",
1.133 ori_2itm thy itm_ pid all (i,v,f,d,
1.134 @@ -737,8 +715,10 @@
1.135 val opt = (try (comp_dts thy)) (d,ts);
1.136 val msg = case opt of
1.137 SOME _ => ""
1.138 - | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
1.139 - ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
1.140 + | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d) ^
1.141 + " " ^
1.142 + ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.143 + (thy2ctxt thy)))) ts)
1.144 ^ " is illtyped");
1.145 val _ = show_types:= s
1.146 in msg end;
1.147 @@ -774,8 +754,9 @@
1.148 then
1.149 if not (subset op = (map typeless ts, map typeless ots))
1.150 then (("terms '"^
1.151 - ((strs2str' o (map (Syntax.string_of_term
1.152 - (thy2ctxt thy)))) ts)^
1.153 + ((strs2str' o
1.154 + (map (Print_Mode.setmp [] (Syntax.string_of_term
1.155 + (thy2ctxt thy))))) ts)^
1.156 "' not in example (typeless)"), e_ori_, [])
1.157 else (case seek_orits thy sel ts ori of
1.158 ("", ori_ as (_,_,_,d,ts), all) =>
1.159 @@ -786,9 +767,9 @@
1.160 else
1.161 if member op = (map #4 ori) d
1.162 then seek_oridts thy sel (d,ts) ori
1.163 - else ((Syntax.string_of_term (thy2ctxt thy) d)^
1.164 - (*" not in example", e_ori_, []) ///11.11.03*)
1.165 - " not in example", (0,[],sel,d,ts), [])
1.166 + else ((Print_Mode.setmp [] (Syntax.string_of_term
1.167 + (thy2ctxt thy)) d) ^
1.168 + " not in example", (0, [], sel, d, ts), [])
1.169 end;
1.170
1.171
1.172 @@ -1051,21 +1032,6 @@
1.173 | pos => error ("header called with "^ pos_2str pos);
1.174
1.175
1.176 -
1.177 -(* test-printouts ---
1.178 -val _=tracing("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
1.179 - val _=tracing("### insert_ppc: pts= "^
1.180 -(strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
1.181 -
1.182 -
1.183 - val sel = "#Given"; val Add_Given' ct = m;
1.184 -
1.185 - val sel = "#Find"; val Add_Find' (ct,_) = m;
1.186 - val (p,_) = p;
1.187 - val (_,_,f,nxt',_,pt')= specify_additem sel (ct,[]) (p,Pbl(*!!!!!!!*)) c pt;
1.188 ---------------
1.189 - val sel = "#Given"; val Add_Given' (ct,_) = nxt; val (p,_) = p;
1.190 - *)
1.191 fun specify_additem sel (ct,_) (p,Met) c pt =
1.192 let
1.193 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.194 @@ -1671,21 +1637,25 @@
1.195 (let val gf = (head_of given) $ formal;
1.196 val _ = cterm_of thy gf
1.197 in gf end)
1.198 - handle _ => error ("calchead.tag_form: " ^
1.199 - Syntax.string_of_term (thy2ctxt thy) given ^
1.200 - " .. " ^
1.201 - Syntax.string_of_term (thy2ctxt thy) formal ^
1.202 - " ..types do not match");
1.203 + handle _ =>
1.204 + error ("calchead.tag_form: " ^
1.205 + Print_Mode.setmp [] (Syntax.string_of_term
1.206 + (thy2ctxt thy)) given ^ " .. " ^
1.207 + Print_Mode.setmp [] (Syntax.string_of_term
1.208 + (thy2ctxt thy)) formal ^
1.209 + " ..types do not match");
1.210 (* val formal = (the o (parse thy)) "[R::real]";
1.211 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1.212 > tag_form thy (formal, given);
1.213 val it = "fixed_values [R]" : cterm
1.214 *)
1.215 +
1.216 fun chktyp thy (n, fs, gs) =
1.217 - ((tracing o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
1.218 - (tracing o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
1.219 + ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.220 + (nth n)) fs;
1.221 + (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.222 + (nth n)) gs;
1.223 tag_form thy (nth n fs, nth n gs));
1.224 -
1.225 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1.226
1.227 (* #####################################################
1.228 @@ -1811,15 +1781,6 @@
1.229 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1.230
1.231
1.232 -
1.233 -(*
1.234 - tracing (oris2str pors);
1.235 -
1.236 - tracing (itms2str_ thy pits);
1.237 - tracing (itms2str_ thy mits);
1.238 - *)
1.239 -
1.240 -
1.241 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1.242 + met from fmz; assumes pos on PblObj, meth = [].*)
1.243 fun complete_mod (pt, pos as (p, p_):pos') =