1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sun Jul 21 15:15:50 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Jul 22 13:52:18 2013 +0200
1.3 @@ -284,8 +284,7 @@
1.4 (*WN.11.03: + dont take first inter<>[]*)
1.5 fun seek_oridts ctxt sel (d,ts) [] =
1.6 ("seek_oridts: input ('" ^
1.7 - (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^
1.8 - "') not found in oris (typed)",
1.9 + (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",
1.10 (0, [], sel, d, ts),
1.11 [])
1.12 | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
1.13 @@ -295,20 +294,13 @@
1.14
1.15 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.16 fun seek_orits ctxt sel ts [] =
1.17 - ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
1.18 - ctxt)) ts) ^
1.19 - "') not found in oris (typed)", e_ori_, [])
1.20 + ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
1.21 + "') not found in oris (typed)", e_ori_, [])
1.22 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.23 if sel = sel' andalso (inter op = ts ts') <> []
1.24 then if sel = sel'
1.25 - then ("",
1.26 - (id,vat,sel,d, inter op = ts ts'):ori,
1.27 - ts')
1.28 - else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.29 - ctxt))) ts)
1.30 - ^ " not for " ^ sel,
1.31 - e_ori_,
1.32 - [])
1.33 + then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts')
1.34 + else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
1.35 else seek_orits ctxt sel ts oris;
1.36 (* false
1.37 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.38 @@ -478,20 +470,15 @@
1.39 (* val (_,_,fd,d,ts) = hd miss;
1.40 *)
1.41 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.42 - (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
1.43 - comp_dts) (d,[hd ts]) : cterm');
1.44 + (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');
1.45 (* val t = comp_dts (d,[hd ts]);
1.46 *)
1.47
1.48 (* get a term from ori, notyet input in itm.
1.49 the term from ori is thrown back to a string in order to reuse
1.50 machinery for immediate input by the user. *)
1.51 -fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.52 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.53 - (d, subtract op = (ts_in itm_) ts) : cterm');
1.54 -fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.55 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.56 - (d, subtract op = (ts_in itm_) ts) : cterm');
1.57 +fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.58 + (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
1.59
1.60 (* in FE dsc, not dat: this is in itms ...*)
1.61 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
1.62 @@ -514,9 +501,7 @@
1.63 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
1.64 *)
1.65 (f,(d,_))::itms =>
1.66 - SOME (f : string,
1.67 - ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.68 - comp_dts) (d, []) : cterm')
1.69 + SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
1.70 | _ => NONE end
1.71
1.72 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.73 @@ -684,43 +669,28 @@
1.74 *)
1.75 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.76 case find_first (eq1 d) pbt of
1.77 - SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
1.78 - val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
1.79 - *)
1.80 + SOME (_,(_,pid)) =>
1.81 (case find_first (eq3 f d) itms of
1.82 - SOME (_,_,_,_,itm_) =>
1.83 - let
1.84 - val ts' = inter op = (ts_in itm_) ts;
1.85 - in if subset op = (ts, ts')
1.86 - then (((strs2str' o
1.87 - map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
1.88 - " already input", e_itm) (*2*)
1.89 - else ("",
1.90 - ori_2itm itm_ pid all (i,v,f,d,
1.91 - subtract op = ts' ts)) (*3,4*)
1.92 - end
1.93 - | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
1.94 - pid all (i,v,f,d,ts)) (*1*)
1.95 - )
1.96 - | NONE => ("", ori_2itm (Sup (d,ts))
1.97 - e_term all (i,v,f,d,ts));
1.98 + SOME (_,_,_,_,itm_) =>
1.99 + let
1.100 + val ts' = inter op = (ts_in itm_) ts;
1.101 + in
1.102 + if subset op = (ts, ts')
1.103 + then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)
1.104 + else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
1.105 + end
1.106 + | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts))) (*1*)
1.107 + | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));
1.108
1.109 fun test_types ctxt (d,ts) =
1.110 let
1.111 - (*val s = !show_types; val _ = show_types:= true;*)
1.112 val opt = (try comp_dts) (d,ts);
1.113 val msg = case opt of
1.114 SOME _ => ""
1.115 - | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.116 - " " ^
1.117 - ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.118 - ctxt))) ts)
1.119 - ^ " is illtyped");
1.120 - (*val _ = show_types:= s*)
1.121 + | NONE => (term_to_string' ctxt d ^ " " ^
1.122 + (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");
1.123 in msg end;
1.124
1.125 -
1.126 -
1.127 fun maxl [] = error "maxl of []"
1.128 | maxl (y::ys) =
1.129 let fun mx x [] = x
1.130 @@ -747,9 +717,8 @@
1.131 if d = e_term
1.132 then
1.133 if not (subset op = (map typeless ts, map typeless ots))
1.134 - then (("terms '" ^ ((strs2str' o
1.135 - (map (Print_Mode.setmp [] (Syntax.string_of_term ctxt)))) ts) ^
1.136 - "' not in example (typeless)"), e_ori_, [])
1.137 + then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
1.138 + "' not in example (typeless)", e_ori_, [])
1.139 else
1.140 (case seek_orits ctxt sel ts ori of
1.141 ("", ori_ as (_,_,_,d,ts), all) =>
1.142 @@ -760,11 +729,9 @@
1.143 else
1.144 if member op = (map #4 ori) d
1.145 then seek_oridts ctxt sel (d,ts) ori
1.146 - else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.147 - " not in example", (0, [], sel, d, ts), [])
1.148 + else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
1.149 end;
1.150
1.151 -
1.152 (*. for return-value of appl_add .*)
1.153 datatype additm =
1.154 Add of itm
1.155 @@ -1568,16 +1535,12 @@
1.156 (*fun tag_form thy (formal, given) = cterm_of thy
1.157 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1.158 fun tag_form thy (formal, given) =
1.159 - (let val gf = (head_of given) $ formal;
1.160 - val _ = cterm_of thy gf
1.161 - in gf end)
1.162 - handle _ =>
1.163 - error ("calchead.tag_form: " ^
1.164 - Print_Mode.setmp [] (Syntax.string_of_term
1.165 - (thy2ctxt thy)) given ^ " .. " ^
1.166 - Print_Mode.setmp [] (Syntax.string_of_term
1.167 - (thy2ctxt thy)) formal ^
1.168 - " ..types do not match");
1.169 + (let
1.170 + val gf = (head_of given) $ formal;
1.171 + val _ = cterm_of thy gf
1.172 + in gf end)
1.173 + handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1.174 + " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
1.175 (* val formal = (the o (parse thy)) "[R::real]";
1.176 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1.177 > tag_form thy (formal, given);
1.178 @@ -1585,10 +1548,8 @@
1.179 *)
1.180
1.181 fun chktyp thy (n, fs, gs) =
1.182 - ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.183 - (nth n)) fs;
1.184 - (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.185 - (nth n)) gs;
1.186 + ((writeln o (term_to_string''' thy) o (nth n)) fs;
1.187 + (writeln o (term_to_string''' thy) o (nth n)) gs;
1.188 tag_form thy (nth n fs, nth n gs));
1.189 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1.190