1.1 --- a/src/Tools/isac/IsacKnowledge/Test.ML Thu Aug 19 15:41:56 2010 +0200
1.2 +++ b/src/Tools/isac/IsacKnowledge/Test.ML Fri Aug 20 12:25:37 2010 +0200
1.3 @@ -538,13 +538,13 @@
1.4 if atom t then true else bin_ops_only t;
1.5
1.6 fun polynomial opl t bdVar = (* bdVar TODO *)
1.7 - (bin_op t) subset opl andalso (bin_ops_only t);
1.8 + subset op = (bin_op t, opl) andalso (bin_ops_only t);
1.9
1.10 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
1.11 andalso polynomial opl (equ_lhs t) bdVar
1.12 andalso polynomial opl (equ_rhs t) bdVar
1.13 - andalso ((varids bdVar) subset (varids (equ_lhs t))
1.14 - orelse(varids bdVar) subset (varids (equ_lhs t)));
1.15 + andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
1.16 + subset op = (varids bdVar, varids (equ_lhs t)));
1.17
1.18 (*fun max is =
1.19 let fun max_ m [] = m
1.20 @@ -563,7 +563,7 @@
1.21 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
1.22 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
1.23 | deg addl mul v (h $ t1 $ t2) =
1.24 - if(bin_op h)subset addl
1.25 + if subset op = (bin_op h, addl)
1.26 then max (deg addl mul v t1 ,deg addl mul v t2)
1.27 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
1.28 in if polynomial (addl @ [mul]) t bdVar
2.1 --- a/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:41:56 2010 +0200
2.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Fri Aug 20 12:25:37 2010 +0200
2.3 @@ -39,16 +39,16 @@
2.4
2.5
2.6 ML {*
2.7 -thy2ctxt;
2.8 -thy2ctxt';
2.9 -SOME 111;
2.10 +111;
2.11 +member op = [1,2,3] 2;
2.12 *}
2.13
2.14 use "ME/calchead.sml"
2.15
2.16 ML {*
2.17 -thy2ctxt;
2.18 -SOME 111;
2.19 +theory2theory';
2.20 +(assoc_thy "Script");
2.21 +(assoc_thy "Script.thy");
2.22 *}
2.23
2.24 (*
3.1 --- a/src/Tools/isac/ME/appl.sml Thu Aug 19 15:41:56 2010 +0200
3.2 +++ b/src/Tools/isac/ME/appl.sml Fri Aug 20 12:25:37 2010 +0200
3.3 @@ -113,7 +113,7 @@
3.4 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
3.5 > val p = [];
3.6 > val (sss,ttt) = mk_set thy pt p consts pred;
3.7 -> (Syntax.string_of_term (thy2ctxt thy) sss,Sign.string_of_term(sign_of thy) ttt);
3.8 +> (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt);
3.9 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
3.10
3.11 val consts = str2term "UniversalList";
4.1 --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:41:56 2010 +0200
4.2 +++ b/src/Tools/isac/ME/calchead.sml Fri Aug 20 12:25:37 2010 +0200
4.3 @@ -6,6 +6,8 @@
4.4
4.5 use"ME/calchead.sml";
4.6 use"calchead.sml";
4.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
4.8 + 10 20 30 40 50 60 70 80
4.9 *)
4.10
4.11 (* TODO interne Funktionen aus sig entfernen *)
4.12 @@ -23,11 +25,11 @@
4.13 (string * (Term.term * Term.term)) list -> cterm' -> additm
4.14 type calcstate
4.15 type calcstate'
4.16 - val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
4.17 + val chk_vars : term ppc -> string * Term.term list
4.18 val chktyp :
4.19 - theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
4.20 + theory -> int * term list * term list -> term
4.21 val chktyps :
4.22 - theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
4.23 + theory -> term list * term list -> term list
4.24 val complete_metitms :
4.25 SpecifyTools.ori list ->
4.26 SpecifyTools.itm list ->
4.27 @@ -193,10 +195,10 @@
4.28 'b ->
4.29 ptree ->
4.30 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
4.31 - val tag_form : theory -> Thm.cterm * Thm.cterm -> Thm.cterm
4.32 + val tag_form : theory -> term * term -> term
4.33 val test_types : theory -> Term.term * Term.term list -> string
4.34 val typeless : Term.term -> Term.term
4.35 - val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
4.36 + val unbound_ppc : term SpecifyTools.ppc -> Term.term list
4.37 val vals_of_oris : SpecifyTools.ori list -> Term.term list
4.38 val variants_in : Term.term list -> int
4.39 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
4.40 @@ -279,31 +281,38 @@
4.41 (*.to an input (d,ts) find the according ori and insert the ts.*)
4.42 (*WN.11.03: + dont take first inter<>[]*)
4.43 fun seek_oridts thy sel (d,ts) [] =
4.44 - ("'"^(Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy (d,ts)))^
4.45 - (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
4.46 + ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
4.47 "' not found (typed)", (0,[],sel,d,ts):ori, [])
4.48 (* val (id,vat,sel',d',ts')::oris = ori;
4.49 val (id,vat,sel',d',ts') = ori;
4.50 *)
4.51 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
4.52 - if sel = sel' andalso d=d' andalso (ts inter ts') <> []
4.53 - then if sel = sel'
4.54 - then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
4.55 - else ((Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy(d,ts)))^
4.56 - " not for "^sel, e_ori_, [])
4.57 + if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
4.58 + then if sel = sel'
4.59 + then ("",
4.60 + (id,vat,sel,d, inter op = ts ts'):ori,
4.61 + ts')
4.62 + else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))
4.63 + ^ " not for " ^ sel,
4.64 + e_ori_,
4.65 + [])
4.66 else seek_oridts thy sel (d,ts) oris;
4.67
4.68 (*.to an input (_,ts) find the according ori and insert the ts.*)
4.69 fun seek_orits thy sel ts [] =
4.70 ("'"^
4.71 - (strs2str (map (Syntax.string_of_term (thy2ctxt' thy)) ts))^
4.72 + (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
4.73 "' not found (typed)", e_ori_, [])
4.74 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
4.75 - if sel = sel' andalso (ts inter ts') <> []
4.76 + if sel = sel' andalso (inter op = ts ts') <> []
4.77 then if sel = sel'
4.78 - then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
4.79 - else (((strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) ts)^
4.80 - " not for "^sel, e_ori_, [])
4.81 + then ("",
4.82 + (id,vat,sel,d, inter op = ts ts'):ori,
4.83 + ts')
4.84 + else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
4.85 + ^ " not for "^sel,
4.86 + e_ori_,
4.87 + [])
4.88 else seek_orits thy sel ts oris;
4.89 (* false
4.90 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
4.91 @@ -345,7 +354,7 @@
4.92 | coll eq xs (y::ys) =
4.93 let val (n,ys') = cnt eq (y::ys) y 0;
4.94 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
4.95 - val vts = (distinct (coll eq [] ts))\\[1];
4.96 + val vts = subtract op = [1] (distinct (coll eq [] ts));
4.97 in case vts of [] => 1 | [n] => n
4.98 | _ => error "different variants in formalization" end;
4.99 (*
4.100 @@ -397,35 +406,6 @@
4.101 > has_list_type (term_of ct);
4.102 val it = false : bool *)
4.103
4.104 -
4.105 -
4.106 -
4.107 -(*fdcrs = descriptions in formalization
4.108 - unused 22.11.00
4.109 -fun is_already_input thy fdcrs ts t =
4.110 - let
4.111 - val tss = flat (map isalist2list ts);
4.112 -(*28.1. val (dcr,t') = split_dsc_t fdcrs t; *)
4.113 - val (dcr,[t']) = split_dts t;
4.114 - in if (typeless t') mem (map typeless tss)
4.115 - then ("term '"^(Syntax.string_of_term (thy2ctxt' thy) t')^
4.116 - "' already input")
4.117 - else "" end;
4.118 -
4.119 -> val pts = appc (map (term_of o the o (parse thy))) pbl;
4.120 -> val ts = #Relate pts;
4.121 -> val t = (term_of o the o (parse thy))"(A=#2*a*b - a^^^#2)";
4.122 -> is_already_input thy ts t;
4.123 -val it = "term 'A = #2 * a * b - a ^^^ #2' already input" : string
4.124 -> val t = (term_of o the o (parse thy))"a=#2*R*sin alpha";
4.125 -> is_already_input thy ts t;
4.126 -val it = "term 'a = #2 * R * sin alpha' already input" : string
4.127 -> val t = (term_of o the o (parse thy))"a=R*sin alpha";
4.128 -> is_already_input thy ts t;
4.129 -val it = "" : string
4.130 -*)
4.131 -
4.132 -
4.133 fun is_parsed (Syn _) = false
4.134 | is_parsed _ = true;
4.135 fun parse_ok its = foldl and_ (true, map is_parsed its);
4.136 @@ -502,13 +482,15 @@
4.137 (* val (_,_,fd,d,ts) = hd miss;
4.138 *)
4.139 fun getr_ct thy ((_,_,fd,d,ts):ori) =
4.140 - (fd, (string_of_cterm o (comp_dts thy)) (d,[hd ts]):cterm');
4.141 + (fd, ((Syntax.string_of_term (thy2ctxt thy)) o
4.142 + (comp_dts thy)) (d,[hd ts]):cterm');
4.143 (* val t = comp_dts thy (d,[hd ts]);
4.144 *)
4.145
4.146 (* get a term from ori, notyet input in itm *)
4.147 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
4.148 - (fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');
4.149 + (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
4.150 + (d, subtract op = (ts_in itm_) ts):cterm');
4.151 (* test-maximum.sml fmy <> [], Init_Proof ...
4.152 val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
4.153 val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
4.154 @@ -516,8 +498,8 @@
4.155 atomty d';
4.156 atomty (hd ts);
4.157 atomty ts';
4.158 - cterm_of (sign_of thy) (d $ (hd ts));
4.159 - cterm_of (sign_of thy) (d' $ ts');
4.160 + Thm.cterm_of thy (d $ (hd ts));
4.161 + Thm.cterm_of thy (d' $ ts');
4.162
4.163 comp_dts thy (d,ts);
4.164 *)
4.165 @@ -530,6 +512,11 @@
4.166
4.167 (* select an item in oris, notyet input in itms
4.168 (precondition: in itms are only Cor, Sup, Inc) *)
4.169 +local
4.170 +infix mem;
4.171 +fun x mem [] = false
4.172 + | x mem (y :: ys) = x = y orelse x mem ys;
4.173 +in
4.174 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
4.175 let
4.176 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
4.177 @@ -540,7 +527,7 @@
4.178 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
4.179 *)
4.180 (f,(d,_))::itms =>
4.181 - SOME (f:string, (string_of_cterm o comp_dts thy) (d,[]):cterm')
4.182 + SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
4.183 | _ => NONE end
4.184
4.185 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
4.186 @@ -554,7 +541,7 @@
4.187 (* val itm = hd icl; val (_,_,_,d,ts) = v6;
4.188 *)
4.189 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
4.190 - (d_in (#5 itm)) = d andalso (ts_in (#5 itm)) subset ts;
4.191 + (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
4.192 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
4.193 | false_and_not_Sup (i,v,false,f, _) = true
4.194 | false_and_not_Sup _ = false;
4.195 @@ -576,7 +563,8 @@
4.196 *)
4.197 NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
4.198 | SOME ori => SOME (geti_ct thy ori (hd icl))
4.199 - end;
4.200 + end
4.201 +end;
4.202
4.203
4.204
4.205 @@ -699,10 +687,10 @@
4.206 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
4.207 (id,vt,cl,sl,Cor (d,ts)):itm
4.208 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
4.209 - raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
4.210 + raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
4.211 " not not for Syn (s:cterm')")
4.212 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
4.213 - raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
4.214 + raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
4.215 " not not for Typ (s:cterm')")
4.216 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
4.217 (id,vt,cl,sl,Fal (d,ts))
4.218 @@ -718,7 +706,7 @@
4.219 fun is_field_correct sel d dscpbt =
4.220 case assoc (dscpbt, sel) of
4.221 NONE => false
4.222 - | SOME ds => d mem ds;
4.223 + | SOME ds => member op = ds d;
4.224
4.225 (*. update the itm_ already input, all..from ori .*)
4.226 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
4.227 @@ -729,7 +717,7 @@
4.228 val pval = pbl_ids' thy d ts'
4.229 (*WN.9.5.03: FIXXXME [#0, epsilon]
4.230 here would upd_penv be called for [#0, epsilon] etc. *)
4.231 - val complete = if eq_set (ts', all) then true else false;
4.232 + val complete = if eq_set op = (ts', all) then true else false;
4.233 in case itm_ of
4.234 (Cor _) =>
4.235 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
4.236 @@ -774,42 +762,20 @@
4.237 (case find_first (eq3 f d) itms of
4.238 SOME (_,_,_,_,itm_) =>
4.239 let
4.240 - val ts' = (ts_in itm_) inter ts;
4.241 - in if ts subset ts'
4.242 + val ts' = inter op = (ts_in itm_) ts;
4.243 + in if subset op = (ts, ts')
4.244 then (((strs2str' o
4.245 - map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
4.246 + map (Syntax.string_of_term (thy2ctxt thy))) ts')^
4.247 " already input", e_itm) (*2*)
4.248 - else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts')) (*3,4*)
4.249 + else ("",
4.250 + ori_2itm thy itm_ pid all (i,v,f,d,
4.251 + subtract op = ts' ts)) (*3,4*)
4.252 end
4.253 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
4.254 pid all (i,v,f,d,ts)) (*1*)
4.255 )
4.256 | NONE => ("", ori_2itm thy (Sup (d,ts))
4.257 e_term all (i,v,f,d,ts));
4.258 -(*------------------------------------------------
4.259 -fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
4.260 -fun is_notyet_input thy itms pval all ((id,vt,fd,d,ts):ori) pbt =
4.261 - case find_first (eq1 d) pbt of
4.262 - SOME (_,(_,pid)) => (* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
4.263 - *)
4.264 - (case seek_ppc id itms of
4.265 - SOME (id',_,_,_,itm_) =>
4.266 - let
4.267 - val ts' = (ts_in itm_) inter ts;
4.268 - in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all
4.269 - (id,vt,fd,d,(ts_in itm_)@ts))
4.270 - else (((strs2str' o
4.271 - map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
4.272 - " already input", e_itm) end
4.273 - | NONE =>
4.274 - if all = ts
4.275 - then ("", ori_2itm (Cor ((e_term,[]),(pid,[])))
4.276 - (pid, pval) all (id,vt,fd,d,ts))
4.277 - else ("", ori_2itm (Inc ((e_term,[]),(e_term,[])))
4.278 - (pid, pval) all (id,vt,fd,d,ts))
4.279 - )
4.280 - | NONE => ("", ori_2itm (Sup (e_term,[]))
4.281 - (e_term, []) all (id,vt,fd,d,ts));----*)
4.282
4.283 fun test_types thy (d,ts) =
4.284 let
4.285 @@ -817,9 +783,9 @@
4.286 val opt = (try (comp_dts thy)) (d,ts);
4.287 val msg = case opt of
4.288 SOME _ => ""
4.289 - | NONE => ((Sign.string_of_term (sign_of thy) d)^" "^
4.290 - ((strs2str' o map (Sign.string_of_term(sign_of thy)))ts)
4.291 - ^" is illtyped");
4.292 + | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
4.293 + ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
4.294 + ^ " is illtyped");
4.295 val _ = show_types:= s
4.296 in msg end;
4.297
4.298 @@ -846,16 +812,16 @@
4.299 val (d,ts(*,pval*)) = split_dts thy t;
4.300 val ids = map (fst o dest_Free)
4.301 ((distinct o (flat o (map vars))) ts);
4.302 - in if (ids \\ oids) <> []
4.303 - then (("identifiers "^(strs2str' (ids \\ oids))^
4.304 + in if (subtract op = oids ids) <> []
4.305 + then (("identifiers "^(strs2str' (subtract op = oids ids))^
4.306 " not in example"), e_ori_, [])
4.307 else
4.308 if d = e_term
4.309 then
4.310 - if not ((map typeless ts) subset (map typeless ots))
4.311 + if not (subset op = (map typeless ts, map typeless ots))
4.312 then (("terms '"^
4.313 - ((strs2str' o (map (Sign.string_of_term
4.314 - (sign_of thy)))) ts)^
4.315 + ((strs2str' o (map (Syntax.string_of_term
4.316 + (thy2ctxt thy)))) ts)^
4.317 "' not in example (typeless)"), e_ori_, [])
4.318 else (case seek_orits thy sel ts ori of
4.319 ("", ori_ as (_,_,_,d,ts), all) =>
4.320 @@ -864,9 +830,9 @@
4.321 | msg => (msg, e_ori_, []))
4.322 | (msg,_,_) => (msg, e_ori_, []))
4.323 else
4.324 - if d mem (map #4 ori)
4.325 + if member op = (map #4 ori) d
4.326 then seek_oridts thy sel (d,ts) ori
4.327 - else ((Syntax.string_of_term (thy2ctxt' thy) d)^
4.328 + else ((Syntax.string_of_term (thy2ctxt thy) d)^
4.329 (*" not in example", e_ori_, []) ///11.11.03*)
4.330 " not in example", (0,[],sel,d,ts), [])
4.331 end;
4.332 @@ -999,11 +965,11 @@
4.333 (*.split type-wrapper from scr-arg and build part of an ori;
4.334 an type-error is reported immediately, raises an exn,
4.335 subsequent handling of exn provides 2nd part of error message.*)
4.336 -fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
4.337 +(*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term
4.338 (* val (thy, (str, (dsc, _)), (ty $ var)) =
4.339 (thy, p, a);
4.340 *)
4.341 - (cterm_of (sign_of thy) (dsc $ var);(*type check*)
4.342 + (Thm.cterm_of thy (dsc $ var);(*type check*)
4.343 SOME ((([1], str, dsc, (*[var]*)
4.344 split_dts' (dsc, var))): preori)(*:ori without leading #*))
4.345 handle e as TYPE _ =>
4.346 @@ -1017,6 +983,25 @@
4.347 ^"*** checked by theory: "^(theory2str thy)^"\n"
4.348 ^"*** "^dots 66);
4.349 print_exn e; (*raises exn again*)
4.350 + NONE);*)
4.351 +fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
4.352 + (* val (thy, (str, (dsc, _)), (ty $ var)) =
4.353 + (thy, p, a);
4.354 + *)
4.355 + (Thm.cterm_of thy (dsc $ var);(*type check*)
4.356 + SOME ((([1], str, dsc, (*[var]*)
4.357 + split_dts' (dsc, var))): preori)(*:ori without leading #*))
4.358 + handle e as TYPE _ =>
4.359 + (writeln (dashs 70^"\n"
4.360 + ^"*** ERROR while creating the items for the model of the ->problem\n"
4.361 + ^"*** from the ->stac with ->typeconstructor in arglist:\n"
4.362 + ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
4.363 + ^"*** description: "^(term_detail2str dsc)
4.364 + ^"*** value: "^(term_detail2str var)
4.365 + ^"*** typeconstructor in script: "^(term_detail2str ty)
4.366 + ^"*** checked by theory: "^(theory2str thy)^"\n"
4.367 + ^"*** "^dots 66);
4.368 + (*WN100820 postponed: print_exn e; raises exn again*)
4.369 NONE);
4.370 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
4.371 > val Const ("Script.SubProblem",_) $
4.372 @@ -1139,7 +1124,8 @@
4.373 fun overwrite_ppc thy itm ppc =
4.374 let
4.375 fun repl ppc' (_,_,_,_,itm_) [] =
4.376 - raise error ("overwrite_ppc: "^(itm__2str thy itm_)^" not found")
4.377 + raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
4.378 + " not found")
4.379 | repl ppc' itm (p::ppc) =
4.380 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
4.381 else repl (ppc' @ [p]) itm ppc
4.382 @@ -1186,9 +1172,9 @@
4.383
4.384
4.385 (* test-printouts ---
4.386 -val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
4.387 +val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
4.388 val _=writeln("### insert_ppc: pts= "^
4.389 -(strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) pts);
4.390 +(strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
4.391
4.392
4.393 val sel = "#Given"; val Add_Given' ct = m;
4.394 @@ -1384,6 +1370,7 @@
4.395 meth=met, ...}) = get_obj I pt p;
4.396 (*val pt = update_pbl pt p itms;
4.397 val pt = update_pblID pt p pI;*)
4.398 + val thy = assoc_thy dI
4.399 val ((p,Pbl),_,_,pt)=
4.400 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
4.401 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
4.402 @@ -1500,7 +1487,7 @@
4.403 (*TODO.WN03 pass error-msgs to the frontend..
4.404 FIXME ..and dont abuse a tactic for that purpose*)
4.405 ([(Tac msg,
4.406 - Tac_ (ProtoPure.thy, msg,msg,msg),
4.407 + Tac_ (theory "Pure", msg,msg,msg),
4.408 (e_pos', e_istate))], [], ptp)
4.409 end
4.410
4.411 @@ -1558,7 +1545,7 @@
4.412 (#4:ori -> term)) oris;
4.413 in filter_outs ors itms end;
4.414
4.415 -fun memI a b = b mem a;
4.416 +fun memI a b = member op = a b;
4.417 (*filter oris which are in pbt, too*)
4.418 fun filter_pbt oris pbt =
4.419 let val dscs = map (fst o snd) pbt
4.420 @@ -1566,6 +1553,11 @@
4.421
4.422 (*.combine itms from pbl + met and complete them wrt. pbt.*)
4.423 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
4.424 +local
4.425 +infix mem;
4.426 +fun x mem [] = false
4.427 + | x mem (y :: ys) = x = y orelse x mem ys;
4.428 +in
4.429 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
4.430 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
4.431 *)
4.432 @@ -1575,11 +1567,17 @@
4.433 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
4.434 val os = filter_outs ors itms;
4.435 (*WN.12.03?: does _NOT_ add itms from met ?!*)
4.436 - in itms @ (map (ori2Coritm met) os) end;
4.437 + in itms @ (map (ori2Coritm met) os) end
4.438 +end;
4.439
4.440
4.441
4.442 (*.complete model and guard of a calc-head .*)
4.443 +local
4.444 +infix mem;
4.445 +fun x mem [] = false
4.446 + | x mem (y :: ys) = x = y orelse x mem ys;
4.447 +in
4.448 fun complete_mod_ (oris, mpc, ppc, probl) =
4.449 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
4.450 val vat = if probl = [] then 1 else max_vt probl
4.451 @@ -1589,7 +1587,8 @@
4.452
4.453 val pits = pits @ (map (ori2Coritm ppc) pors)
4.454 val mits = complete_metitms oris pits [] mpc
4.455 - in (pits, mits) end;
4.456 + in (pits, mits) end
4.457 +end;
4.458
4.459 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
4.460 (if dI = e_domID then odI else dI,
4.461 @@ -1606,6 +1605,7 @@
4.462 let
4.463 val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
4.464 val (dI,pI,mI) = some_spec ospec spec
4.465 + val thy = assoc_thy dI
4.466 val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
4.467 val {cas,ppc,...} = get_pbt pI
4.468 val pbl = init_pbl ppc (*fill in descriptions*)
4.469 @@ -1634,6 +1634,7 @@
4.470 val pbl = init_pbl ppc
4.471 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
4.472 val mI = if length met = 0 then e_metID else hd met
4.473 + val thy = assoc_thy dI
4.474 val (pos,c,_,pt) =
4.475 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
4.476 Uistate pos pt
4.477 @@ -1710,9 +1711,16 @@
4.478 raise error ("nxt_specif: not impl. for "^tac2str m');
4.479
4.480 (*.get the values from oris; handle the term list w.r.t. penv.*)
4.481 +
4.482 +local
4.483 +infix mem;
4.484 +fun x mem [] = false
4.485 + | x mem (y :: ys) = x = y orelse x mem ys;
4.486 +in
4.487 fun vals_of_oris oris =
4.488 ((map (mkval' o (#5:ori -> term list))) o
4.489 - (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris;
4.490 + (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
4.491 +end;
4.492
4.493
4.494
4.495 @@ -1782,21 +1790,25 @@
4.496 in f end;
4.497
4.498
4.499 -
4.500 -
4.501 -
4.502 -
4.503 -(* --------------------- ME --------------------- *)
4.504 -fun tag_form thy (formal, given) = cterm_of (sign_of thy)
4.505 - (((head_of o term_of) given) $ (term_of formal));
4.506 +(*fun tag_form thy (formal, given) = Thm.cterm_of thy
4.507 + (((head_of o term_of) given) $ (term_of formal)); WN100819*)
4.508 +fun tag_form thy (formal, given) =
4.509 + (let val gf = (head_of given) $ formal;
4.510 + val _ = Thm.cterm_of thy gf
4.511 + in gf end)
4.512 + handle _ => raise error ("calchead.tag_form: " ^
4.513 + Syntax.string_of_term (thy2ctxt thy) given ^
4.514 + " .. " ^
4.515 + Syntax.string_of_term (thy2ctxt thy) formal ^
4.516 + " ..types do not match");
4.517 (* val formal = (the o (parse thy)) "[R::real]";
4.518 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
4.519 > tag_form thy (formal, given);
4.520 val it = "fixed_values [R]" : cterm
4.521 *)
4.522 fun chktyp thy (n, fs, gs) =
4.523 - ((writeln o string_of_cterm o (nth n)) fs;
4.524 - (writeln o string_of_cterm o (nth n)) gs;
4.525 + ((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
4.526 + (writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
4.527 tag_form thy (nth n fs, nth n gs));
4.528
4.529 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
4.530 @@ -1844,7 +1856,7 @@
4.531 else ("ok",[]) end;*)
4.532 fun chk_vars ctppc =
4.533 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
4.534 - appc flat (mappc (vars o term_of) ctppc)
4.535 + appc flat (mappc vars ctppc)
4.536 val chked = subtract op = gi wh
4.537 in if chked <> [] then ("wh\\gi", chked)
4.538 else let val chked = subtract op = (union op = gi fi) re
4.539 @@ -1857,7 +1869,7 @@
4.540 (* check a new pbltype: variables (Free) unbound by given, find*)
4.541 fun unbound_ppc ctppc =
4.542 let val {Given=gi,Find=fi,Relate=re,...} =
4.543 - appc flat (mappc (vars o term_of) ctppc)
4.544 + appc flat (mappc vars ctppc)
4.545 in distinct (*re\\(gi union fi)*)
4.546 (subtract op = (union op = gi fi) re) end;
4.547 (*
4.548 @@ -1880,9 +1892,9 @@
4.549 in ((fld f) o rev) xs end;
4.550 (*
4.551 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
4.552 -> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
4.553 +> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
4.554 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
4.555 -> cterm_of (sign_of thy) conj;
4.556 +> Thm.cterm_of thy conj;
4.557 val it = "(a = b & c = d) & e = f" : cterm
4.558 *)
4.559
4.560 @@ -1892,9 +1904,9 @@
4.561 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
4.562 (*
4.563 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
4.564 -> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
4.565 +> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
4.566 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
4.567 -> cterm_of (sign_of thy) conj;
4.568 +> Thm.cterm_of thy conj;
4.569 val it = "a = b & c = d & e = f & g = h" : cterm
4.570 *)
4.571
4.572 @@ -1920,8 +1932,7 @@
4.573 *)
4.574
4.575 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
4.576 -fun eq4 v (_,vts,_,_,_) = v mem vts;
4.577 -(*((curry (op mem)) (vat:int)) o (#2:ori -> int list);*)
4.578 +fun eq4 v (_,vts,_,_,_) = member op = vts v;
4.579 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
4.580
4.581
5.1 --- a/src/Tools/isac/ME/ctree.sml Thu Aug 19 15:41:56 2010 +0200
5.2 +++ b/src/Tools/isac/ME/ctree.sml Fri Aug 20 12:25:37 2010 +0200
5.3 @@ -227,11 +227,6 @@
5.4
5.5 fun subte2sube ss = map term2str ss;
5.6
5.7 -(*fun subst2str' thy' (s:subst) =
5.8 - (strs2str o
5.9 - (map (pair2str o
5.10 - (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
5.11 - (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
5.12 fun subst2subs s = map (pair2str o
5.13 (apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o
5.14 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;
6.1 --- a/src/Tools/isac/ME/inform.sml Thu Aug 19 15:41:56 2010 +0200
6.2 +++ b/src/Tools/isac/ME/inform.sml Fri Aug 20 12:25:37 2010 +0200
6.3 @@ -227,7 +227,7 @@
6.4 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
6.5 *)
6.6 (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
6.7 - val s = Sign.string_of_term (sign_of dI) t;
6.8 + val s = Syntax.string_of_term (thy2ctxt dI) t;
6.9 (*this ^ should raise the exn on unability of re-parsing dts*)
6.10 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
6.11 | parsitm dI (itm as (i,v,b,f, Syn str)) =
6.12 @@ -238,17 +238,17 @@
6.13 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
6.14 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
6.15 (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
6.16 - val s = Sign.string_of_term (sign_of dI) t;
6.17 + val s = Syntax.string_of_term (thy2ctxt dI) t;
6.18 (*this ^ should raise the exn on unability of re-parsing dts*)
6.19 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
6.20 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
6.21 (let val t = (term_of o comp_dts (Isac"delay" )) (d,ts);
6.22 - val s = Sign.string_of_term (sign_of dI) t;
6.23 + val s = Syntax.string_of_term (thy2ctxt dI) t;
6.24 (*this ^ should raise the exn on unability of re-parsing dts*)
6.25 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
6.26 | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
6.27 (let val t = d $ t';
6.28 - val s = Sign.string_of_term (sign_of dI) t;
6.29 + val s = Syntax.string_of_term (thy2ctxt dI) t;
6.30 (*this ^ should raise the exn on unability of re-parsing dts*)
6.31 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
6.32 | parsitm dI (itm as (i,v,_,f, Par _)) =
7.1 --- a/src/Tools/isac/ME/script.sml Thu Aug 19 15:41:56 2010 +0200
7.2 +++ b/src/Tools/isac/ME/script.sml Fri Aug 20 12:25:37 2010 +0200
7.3 @@ -105,13 +105,6 @@
7.4 > val des = de_esc_underscore esc;
7.5 val des = de_esc_underscore esc;*)
7.6
7.7 -
7.8 -(*WN.12.5.03 not used any more,
7.9 - tacs are more stable than listepxr: subst_tacexpr
7.10 -fun is_listexpr t =
7.11 - (((ids_of o head_of) t) inter (!listexpr)) <> [];
7.12 -----*)
7.13 -
7.14 (*go at a location in a script and fetch the contents*)
7.15 fun go [] t = t
7.16 | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
7.17 @@ -246,7 +239,7 @@
7.18 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
7.19 | itr_arg thy t = raise error
7.20 ("itr_arg not impl. for "^
7.21 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));
7.22 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
7.23 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
7.24 > itr_arg "Script.thy" t;
7.25 val it = Free ("e_","RealDef.real") : term
7.26 @@ -595,9 +588,9 @@
7.27 (case stac of
7.28 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
7.29 ((*writeln("3### assod: stac = "^
7.30 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));
7.31 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
7.32 writeln("3### assod: f(m)= "^
7.33 - (Sign.string_of_term (sign_of (assoc_thy thy)) f));*)
7.34 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) f));*)
7.35 if thmID = thmID_ then
7.36 if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
7.37 else ((*writeln"### assod ..AssWeak";
7.38 @@ -1563,7 +1556,7 @@
7.39 | appy thy ptp E (*env*) l
7.40 (Const ("Script.Repeat"(*2*),_) $ e) a v =
7.41 ((*writeln("3### appy Repeat: a= "^
7.42 - (Sign.string_of_term (sign_of (assoc_thy thy)) a));*)
7.43 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) a));*)
7.44 appy thy ptp E (*env*) (l@[R]) e a v)
7.45 (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e $ a), _, v)=
7.46 (thy, ptp, E, (l@[R]), e2, a, v);
7.47 @@ -1572,7 +1565,7 @@
7.48 (t as Const ("Script.Try",_) $ e $ a) _ v =
7.49 (case appy thy ptp E (l@[L,R]) e (SOME a) v of
7.50 Napp E => ((*writeln("### appy Try "^
7.51 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
7.52 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
7.53 Skip (v, E))
7.54 | ay => ay)
7.55 (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e), _, v)=
7.56 @@ -1584,7 +1577,7 @@
7.57 (t as Const ("Script.Try",_) $ e) a v =
7.58 (case appy thy ptp E (l@[R]) e a v of
7.59 Napp E => ((*writeln("### appy Try "^
7.60 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
7.61 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
7.62 Skip (v, E))
7.63 | ay => ay)
7.64
7.65 @@ -1688,7 +1681,7 @@
7.66 | nxt_up thy ptp scr E l ay
7.67 (t as Abs (_,_,_)) a v =
7.68 ((*writeln("### nxt_up Abs: "^
7.69 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
7.70 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
7.71 nstep_up thy ptp scr E (*enr*) l ay a v)
7.72
7.73 | nxt_up thy ptp scr E l ay
7.74 @@ -1696,7 +1689,7 @@
7.75 ((*writeln("### nxt_up Let$e$Abs: is=");
7.76 writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
7.77 (*writeln("### nxt_up Let e Abs: "^
7.78 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
7.79 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
7.80 nstep_up thy ptp scr (*upd_env*) E (*a,v)*)
7.81 (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v)
7.82
7.83 @@ -1751,7 +1744,7 @@
7.84 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
7.85 (t as Const ("Script.Try",_) $ e $ _) a v =
7.86 ((*writeln("### nxt_up Try "^
7.87 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
7.88 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
7.89 nstep_up thy ptp scr E l Skip_ a v )
7.90 (* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e), a, v) =
7.91 (thy, ptp, (Script sc),
7.92 @@ -1760,7 +1753,7 @@
7.93 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
7.94 (t as Const ("Script.Try"(*2*),_) $ e) a v =
7.95 ((*writeln("### nxt_up Try "^
7.96 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
7.97 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
7.98 nstep_up thy ptp scr E l Skip_ a v)
7.99
7.100
7.101 @@ -1805,7 +1798,7 @@
7.102
7.103 | nxt_up (thy,_) ptp scr E l ay t a v =
7.104 raise error ("nxt_up not impl for "^
7.105 - (Sign.string_of_term (sign_of (assoc_thy thy)) t))
7.106 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t))
7.107
7.108 (* val (thy, ptp, (Script sc), E, l, ay, a, v)=
7.109 (thy, ptp, scr, E, l, Skip_, a, v);
7.110 @@ -1815,13 +1808,13 @@
7.111 and nstep_up thy ptp (Script sc) E l ay a v =
7.112 ((*writeln("### nstep_up from: "^(loc_2str l));
7.113 writeln("### nstep_up from: "^
7.114 - (Sign.string_of_term (sign_of (assoc_thy thy)) (go l sc)));*)
7.115 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go l sc)));*)
7.116 if 1 < length l
7.117 then
7.118 let
7.119 val up = drop_last l;
7.120 in ((*writeln("### nstep_up to: "^
7.121 - (Sign.string_of_term (sign_of (assoc_thy thy)) (go up sc)));*)
7.122 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go up sc)));*)
7.123 nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
7.124 else (*interpreted to end*)
7.125 if ay = Skip_ then Skip (v, E) else Napp E
8.1 --- a/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 15:41:56 2010 +0200
8.2 +++ b/src/Tools/isac/Scripts/term_G.sml Fri Aug 20 12:25:37 2010 +0200
8.3 @@ -9,13 +9,13 @@
8.4 > cterm_of (sign_of thy) a_term;
8.5 val it = "empty" : cterm *)
8.6
8.7 -(*1003 fun match thy t pat =
8.8 +(*2003 fun match thy t pat =
8.9 (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
8.10 handle _ => [];
8.11 fn : theory ->
8.12 Term.term -> Term.term -> (Term.indexname * Term.term) list*)
8.13 (*see src/Tools/eqsubst.ML fun clean_match*)
8.14 -(*1003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
8.15 +(*2003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
8.16 fun matches thy tm pa =
8.17 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
8.18 handle _ => false
9.1 --- a/src/Tools/isac/calcelems.sml Thu Aug 19 15:41:56 2010 +0200
9.2 +++ b/src/Tools/isac/calcelems.sml Fri Aug 20 12:25:37 2010 +0200
9.3 @@ -233,8 +233,6 @@
9.4 type domID = string; (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
9.5 type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
9.6
9.7 -(*2002 fun string_of_thy thy =
9.8 -((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory';*)
9.9 fun string_of_thy thy = Context.theory_name thy: theory';
9.10 val theory2domID = string_of_thy;
9.11 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
9.12 @@ -596,16 +594,12 @@
9.13 else ass ids
9.14 in ass (!calclist') : calcID end;
9.15
9.16 -(*fun termopt2str (SOME t) =
9.17 - "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
9.18 - | termopt2str NONE = "NONE";*)
9.19 fun termopt2str (SOME t) =
9.20 "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
9.21 | termopt2str NONE = "NONE";
9.22 fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
9.23 fun terms2str ts= (strs2str o (map (Syntax.string_of_term
9.24 (thy2ctxt' "Isac")))) ts;
9.25 -(*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
9.26 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
9.27 val string_of_typ = type2str;
9.28
10.1 --- a/test/Tools/isac/IsacKnowledge/atools.sml Thu Aug 19 15:41:56 2010 +0200
10.2 +++ b/test/Tools/isac/IsacKnowledge/atools.sml Fri Aug 20 12:25:37 2010 +0200
10.3 @@ -24,7 +24,7 @@
10.4 "----------- occurs_in -------------------------------------------";
10.5 "----------- occurs_in -------------------------------------------";
10.6 fun str2term str = (term_of o the o (parse thy )) str;
10.7 -fun term2s t = Sign.string_of_term (sign_of thy) t;
10.8 +fun term2s t = Syntax.string_of_term (thy2ctxt thy) t;
10.9 val t = str2term "x";
10.10 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
10.11
11.1 --- a/test/Tools/isac/IsacKnowledge/biegelinie.sml Thu Aug 19 15:41:56 2010 +0200
11.2 +++ b/test/Tools/isac/IsacKnowledge/biegelinie.sml Fri Aug 20 12:25:37 2010 +0200
11.3 @@ -31,7 +31,7 @@
11.4 "----------- the rules -------------------------------------------";
11.5 "----------- the rules -------------------------------------------";
11.6 fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
11.7 -fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
11.8 +fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
11.9 fun rewrit thm str =
11.10 fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
11.11
12.1 --- a/test/Tools/isac/IsacKnowledge/integrate.sml Thu Aug 19 15:41:56 2010 +0200
12.2 +++ b/test/Tools/isac/IsacKnowledge/integrate.sml Fri Aug 20 12:25:37 2010 +0200
12.3 @@ -37,7 +37,7 @@
12.4 "----------- parsing ---------------------------------------------";
12.5 "----------- parsing ---------------------------------------------";
12.6 fun str2term str = (term_of o the o (parse Integrate.thy)) str;
12.7 -fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;
12.8 +fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t;
12.9
12.10 val t = str2term "Integral x D x";
12.11 val t = str2term "Integral x^^^2 D x";
12.12 @@ -576,4 +576,4 @@
12.13 (* WN070703 does not work like Diff due to error in next-pos
12.14 if p = ([], Res) andalso term2str res = "5 * a" then ()
12.15 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
12.16 -*)
12.17 \ No newline at end of file
12.18 +*)
13.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Thu Aug 19 15:41:56 2010 +0200
13.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri Aug 20 12:25:37 2010 +0200
13.3 @@ -33,7 +33,7 @@
13.4 > val t = (term_of o the o (parse thy)) "#2^^^#3";
13.5 > val eval_fn = the (assoc (!eval_list, "pow"));
13.6 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
13.7 -> Sign.string_of_term (sign_of thy) t';
13.8 +> Syntax.string_of_term (thy2ctxt thy) t';
13.9 *)
13.10 (******************************************************************)
13.11 (* ------------------------------------- *)
14.1 --- a/test/Tools/isac/OLDTESTS/script.sml Thu Aug 19 15:41:56 2010 +0200
14.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Fri Aug 20 12:25:37 2010 +0200
14.3 @@ -92,19 +92,19 @@
14.4 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
14.5 loc_2str l1;
14.6 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
14.7 -Sign.string_of_term (sign_of DiffApp.thy) t1;
14.8 +Syntax.string_of_term (thy2ctxt' "DiffApp") t1;
14.9 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
14.10
14.11 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
14.12 loc_2str l2;
14.13 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
14.14 -Sign.string_of_term (sign_of DiffApp.thy) t2;
14.15 +Syntax.string_of_term (thy2ctxt' "DiffApp") t2;
14.16 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
14.17
14.18 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
14.19 loc_2str l3;
14.20 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
14.21 -Sign.string_of_term (sign_of DiffApp.thy) t3;
14.22 +Syntax.string_of_term (thy2ctxt' "DiffApp") t3;
14.23 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
14.24
14.25
15.1 --- a/test/Tools/isac/Scripts/calculate.sml Thu Aug 19 15:41:56 2010 +0200
15.2 +++ b/test/Tools/isac/Scripts/calculate.sml Fri Aug 20 12:25:37 2010 +0200
15.3 @@ -36,19 +36,19 @@
15.4 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
15.5 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
15.6 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.7 -Sign.string_of_term (sign_of thy) t;
15.8 +Syntax.string_of_term (thy2ctxt thy) t;
15.9 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
15.10 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
15.11 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.12 -Sign.string_of_term (sign_of thy) t;
15.13 +Syntax.string_of_term (thy2ctxt thy) t;
15.14 (*val it = "(#12 // #3) ^^^ #2" : string*)
15.15 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
15.16 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.17 -Sign.string_of_term (sign_of thy) t;
15.18 +Syntax.string_of_term (thy2ctxt thy) t;
15.19 (*it = "#4 ^^^ #2" : string*)
15.20 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
15.21 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.22 -Sign.string_of_term (sign_of thy) t;
15.23 +Syntax.string_of_term (thy2ctxt thy) t;
15.24 (*val it = "#16" : string*)
15.25 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
15.26 else ();
15.27 @@ -388,22 +388,22 @@
15.28 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
15.29 "1 + 2 = 3";
15.30 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.31 - Sign.string_of_term (sign_of thy) t;
15.32 + Syntax.string_of_term (thy2ctxt thy) t;
15.33 "(3 * 4 / 3) ^^^ 2";
15.34 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
15.35 "3 * 4 = 12";
15.36 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.37 - Sign.string_of_term (sign_of thy) t;
15.38 + Syntax.string_of_term (thy2ctxt thy) t;
15.39 "(12 / 3) ^^^ 2";
15.40 val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
15.41 "12 / 3 = 4";
15.42 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.43 - Sign.string_of_term (sign_of thy) t;
15.44 + Syntax.string_of_term (thy2ctxt thy) t;
15.45 "4 ^^^ 2";
15.46 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
15.47 "4 ^^^ 2 = 16";
15.48 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
15.49 - Sign.string_of_term (sign_of thy) t;
15.50 + Syntax.string_of_term (thy2ctxt thy) t;
15.51 "16";
15.52 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
15.53 else ();