1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Sep 13 16:36:14 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Sep 13 17:21:22 2010 +0200
1.3 @@ -63,6 +63,12 @@
1.4 use_thy "Knowledge/Atools"
1.5 use_thy "Knowledge/Simplify"
1.6 use_thy "Knowledge/Poly"
1.7 +
1.8 +ML {*
1.9 +val m = (1,[2]);
1.10 +#1 m;
1.11 +fst m;
1.12 +*}
1.13 use_thy "Knowledge/Rational"
1.14 use_thy "Knowledge/PolyMinus"
1.15 use_thy "Knowledge/Equation"
2.1 --- a/src/Tools/isac/Frontend/states.sml Mon Sep 13 16:36:14 2010 +0200
2.2 +++ b/src/Tools/isac/Frontend/states.sml Mon Sep 13 17:21:22 2010 +0200
2.3 @@ -146,7 +146,7 @@
2.4 (*pos' * set by the CalcIterator ---> for each user*)
2.5 calcstate; (*to which ev.included 'preview' tac_s could be applied*)
2.6 val e_state = (e_pos', e_calcstate):state;
2.7 -val states = ref ([]:(iterID * (calcID * state) list) list);
2.8 +val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
2.9 *)
2.10
2.11 val states =
3.1 --- a/src/Tools/isac/Interpret/ctree.sml Mon Sep 13 16:36:14 2010 +0200
3.2 +++ b/src/Tools/isac/Interpret/ctree.sml Mon Sep 13 17:21:22 2010 +0200
3.3 @@ -875,7 +875,7 @@
3.4 in pr_pt f [] pt end;
3.5 (*
3.6 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
3.7 -> val pt = ref EmptyPtree;
3.8 +> val pt = Unsynchronized.ref EmptyPtree;
3.9 > pt:=Nd("root'",
3.10 [Nd("xx1",[]),
3.11 Nd("xx2",
3.12 @@ -1064,7 +1064,7 @@
3.13 (*
3.14 > type ppobj = string;
3.15 > writeln (pr_ptree prfn (!pt));
3.16 - val pt = ref Empty;
3.17 + val pt = Unsynchronized.ref Empty;
3.18 pt:= insert ("root'":ppobj) EmptyPtree [];
3.19 pt:= insert ("xx1":ppobj) (!pt) [1];
3.20 pt:= insert ("xx2":ppobj) (!pt) [2];
4.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Sep 13 16:36:14 2010 +0200
4.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Sep 13 17:21:22 2010 +0200
4.3 @@ -149,7 +149,7 @@
4.4 list))) (*of elements in the formalization*)
4.5 list; (*of cas-entries in the association list*)
4.6
4.7 -val castab = ref ([]: castab);
4.8 +val castab = Unsynchronized.ref ([]: castab);
4.9
4.10
4.11 (*..*)
5.1 --- a/src/Tools/isac/Interpret/ptyps.sml Mon Sep 13 16:36:14 2010 +0200
5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Sep 13 17:21:22 2010 +0200
5.3 @@ -419,7 +419,7 @@
5.4
5.5 (** problem-types stored in format for usage in specify **)
5.6 (*25.8.01 ----
5.7 -val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
5.8 +val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
5.9 (term * (* description *)
5.10 term)) (* id | struct-var *)
5.11 list)
5.12 @@ -457,10 +457,10 @@
5.13 val e_Mets = Ptyp ("e_metID",[e_met],[]);
5.14
5.15 type ptyps = (pbt ptyp) list;
5.16 -val ptyps = ref ([e_Ptyp]:ptyps);
5.17 +val ptyps = Unsynchronized.ref ([e_Ptyp]:ptyps);
5.18
5.19 type mets = (met ptyp) list;
5.20 -val mets = ref ([e_Mets]:mets);
5.21 +val mets = Unsynchronized.ref ([e_Mets]:mets);
5.22
5.23
5.24 (**+ breadth-first search on hierarchy of problem-types +**)
6.1 --- a/src/Tools/isac/Interpret/script.sml Mon Sep 13 16:36:14 2010 +0200
6.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Sep 13 17:21:22 2010 +0200
6.3 @@ -43,7 +43,7 @@
6.4 found by next_tac.
6.5 a leaf is either a tactic or an 'exp' in 'let v = expr'
6.6 where 'exp' does not contain a tactic.*)
6.7 -val trace_script = ref false;
6.8 +val trace_script = Unsynchronized.ref false;
6.9
6.10 type step = (*data for creating a new node in the ptree;
6.11 designed for use:
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 13 16:36:14 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 13 17:21:22 2010 +0200
7.3 @@ -260,7 +260,7 @@
7.4 raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
7.5 | uv_mod_pdiv p1 [x] =
7.6 let
7.7 - val xs=ref [];
7.8 + val xs= Unsynchronized.ref [];
7.9 in
7.10 if x<>0 then
7.11 (
7.12 @@ -273,13 +273,13 @@
7.13 | uv_mod_pdiv p1 p2 =
7.14 let
7.15 val n= uv_mod_deg(p2);
7.16 - val m= ref (uv_mod_deg(p1));
7.17 - val p1'=ref (rev(p1));
7.18 + val m= Unsynchronized.ref (uv_mod_deg(p1));
7.19 + val p1'= Unsynchronized.ref (rev(p1));
7.20 val p2'=(rev(p2));
7.21 val lc2=hd(p2');
7.22 - val q=ref [];
7.23 - val c=ref 0;
7.24 - val output=ref ([],[]);
7.25 + val q= Unsynchronized.ref [];
7.26 + val c= Unsynchronized.ref 0;
7.27 + val output= Unsynchronized.ref ([],[]);
7.28 in
7.29 (
7.30 if (!m)=0 orelse p2=[0]
7.31 @@ -314,13 +314,13 @@
7.32 fun uv_mod_pdivp (p1:uv_poly) (p2:uv_poly) p =
7.33 let
7.34 val n=uv_mod_deg(p2);
7.35 - val m=ref (uv_mod_deg(uv_mod_list_modp p1 p));
7.36 - val p1'=ref (rev(p1));
7.37 + val m= Unsynchronized.ref (uv_mod_deg(uv_mod_list_modp p1 p));
7.38 + val p1'= Unsynchronized.ref (rev(p1));
7.39 val p2'=(rev(uv_mod_list_modp p2 p));
7.40 val lc2=hd(p2');
7.41 - val q=ref [];
7.42 - val c=ref 0;
7.43 - val output=ref ([],[]);
7.44 + val q= Unsynchronized.ref [];
7.45 + val c= Unsynchronized.ref 0;
7.46 + val output= Unsynchronized.ref ([],[]);
7.47 in
7.48 (
7.49 if (!m)=0 orelse p2=[0] then raise error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
7.50 @@ -376,7 +376,7 @@
7.51 fun uv_mod_pp ([]:uv_poly) = []:uv_poly
7.52 | uv_mod_pp p =
7.53 let
7.54 - val c=ref 0;
7.55 + val c= Unsynchronized.ref 0;
7.56 in
7.57 (
7.58 c:=uv_mod_cont(p);
7.59 @@ -393,9 +393,9 @@
7.60 (*. calculates the euklidean polynomial remainder sequence in Zp .*)
7.61 fun uv_mod_prs_euklid_p(p1:uv_poly,p2:uv_poly,p)=
7.62 let
7.63 - val f =ref [];
7.64 - val f'=ref p2;
7.65 - val fi=ref [];
7.66 + val f = Unsynchronized.ref [];
7.67 + val f'= Unsynchronized.ref p2;
7.68 + val fi= Unsynchronized.ref [];
7.69 in
7.70 (
7.71 f:=p2::p1::[];
7.72 @@ -419,12 +419,12 @@
7.73 | uv_mod_gcd_modp p1 [] p= p1
7.74 | uv_mod_gcd_modp p1 p2 p=
7.75 let
7.76 - val p1'=ref[];
7.77 - val p2'=ref[];
7.78 - val pc=ref[];
7.79 - val g=ref [];
7.80 - val d=ref 0;
7.81 - val prs=ref [];
7.82 + val p1'= Unsynchronized.ref [];
7.83 + val p2'= Unsynchronized.ref [];
7.84 + val pc= Unsynchronized.ref [];
7.85 + val g= Unsynchronized.ref [];
7.86 + val d= Unsynchronized.ref 0;
7.87 + val prs= Unsynchronized.ref [];
7.88 in
7.89 (
7.90 if uv_mod_deg(p1)>=uv_mod_deg(p2) then
7.91 @@ -480,9 +480,9 @@
7.92 (*. gets the first prime, which is greater than p and does not divide g .*)
7.93 fun uv_mod_nextprime(g,p)=
7.94 let
7.95 - val list=ref [2];
7.96 - val exit=ref 0;
7.97 - val i = ref 2
7.98 + val list= Unsynchronized.ref [2];
7.99 + val exit= Unsynchronized.ref 0;
7.100 + val i = Unsynchronized.ref 2
7.101 in
7.102 while (!i<p) do (* calculates the primes lower then p *)
7.103 (
7.104 @@ -527,10 +527,10 @@
7.105 (*. chinese remainder algorithm .*)
7.106 fun uv_mod_cra2(r1,r2,m1,m2)=
7.107 let
7.108 - val c=ref 0;
7.109 - val r1'=ref 0;
7.110 - val d=ref 0;
7.111 - val a=ref 0;
7.112 + val c= Unsynchronized.ref 0;
7.113 + val r1'= Unsynchronized.ref 0;
7.114 + val d= Unsynchronized.ref 0;
7.115 + val a= Unsynchronized.ref 0;
7.116 in
7.117 (
7.118 while (uv_mod_mod2((!c)*m1,m2))<>1 do
7.119 @@ -552,20 +552,20 @@
7.120 (*. calculates the gcd of two uv polynomials p1' and p2' with the modular algorithm .*)
7.121 fun uv_mod_gcd (p1':uv_poly) (p2':uv_poly) =
7.122 let
7.123 - val p1=ref (uv_mod_pp(p1'));
7.124 - val p2=ref (uv_mod_pp(p2'));
7.125 + val p1= Unsynchronized.ref (uv_mod_pp(p1'));
7.126 + val p2= Unsynchronized.ref (uv_mod_pp(p2'));
7.127 val c=gcd_int (uv_mod_cont(p1')) (uv_mod_cont(p2'));
7.128 - val temp=ref [];
7.129 - val cp=ref [];
7.130 - val qp=ref [];
7.131 - val q=ref[];
7.132 - val pn=ref 0;
7.133 - val d=ref 0;
7.134 - val g1=ref 0;
7.135 - val p=ref 0;
7.136 - val m=ref 0;
7.137 - val exit=ref 0;
7.138 - val i=ref 1;
7.139 + val temp= Unsynchronized.ref [];
7.140 + val cp= Unsynchronized.ref [];
7.141 + val qp= Unsynchronized.ref [];
7.142 + val q= Unsynchronized.ref [];
7.143 + val pn= Unsynchronized.ref 0;
7.144 + val d= Unsynchronized.ref 0;
7.145 + val g1= Unsynchronized.ref 0;
7.146 + val p= Unsynchronized.ref 0;
7.147 + val m= Unsynchronized.ref 0;
7.148 + val exit= Unsynchronized.ref 0;
7.149 + val i= Unsynchronized.ref 1;
7.150 in
7.151 if length(!p1)>length(!p2) then ()
7.152 else
7.153 @@ -705,7 +705,7 @@
7.154 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)
7.155 fun mv_geq order ((x1,x):mv_monom,(x2,y):mv_monom) =
7.156 let
7.157 - val temp=ref EQUAL;
7.158 + val temp= Unsynchronized.ref EQUAL;
7.159 in
7.160 if order=LEX_ then
7.161 (
7.162 @@ -765,9 +765,9 @@
7.163 | mv_lc([(x,y)],order) = mv_rev_to(mv_cut(mv_rev_to([(x,y)])))
7.164 | mv_lc(p1,order) =
7.165 let
7.166 - val p1o=ref (rev(sort (mv_geq order) (mv_rev_to(p1))));
7.167 + val p1o= Unsynchronized.ref (rev(sort (mv_geq order) (mv_rev_to(p1))));
7.168 val lp=hd(#2(hd(!p1o)));
7.169 - val lc=ref [];
7.170 + val lc= Unsynchronized.ref [];
7.171 in
7.172 (
7.173 while (length(!p1o)>0 andalso hd(#2(hd(!p1o)))=lp) do
7.174 @@ -851,8 +851,8 @@
7.175 | mv_mdiv(_,(0,[]))= raise error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
7.176 | mv_mdiv(p1:mv_monom,p2:mv_monom)=
7.177 let
7.178 - val c=ref (#1(p2));
7.179 - val pp=ref [];
7.180 + val c= Unsynchronized.ref (#1(p2));
7.181 + val pp= Unsynchronized.ref [];
7.182 in
7.183 (
7.184 if !c=0 then raise error("MV_MDIV_EXCEPTION Dividing by zero")
7.185 @@ -878,12 +878,12 @@
7.186 | mv_division(f,[],order)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
7.187 | mv_division(f,g,order)=
7.188 let
7.189 - val r=ref [];
7.190 - val q=ref [];
7.191 - val g'=ref [];
7.192 - val k=ref 0;
7.193 - val m=ref (0,[0]);
7.194 - val exit=ref 0;
7.195 + val r= Unsynchronized.ref [];
7.196 + val q= Unsynchronized.ref [];
7.197 + val g'= Unsynchronized.ref ([] : mv_monom list);
7.198 + val k= Unsynchronized.ref 0;
7.199 + val m= Unsynchronized.ref (0,[0]);
7.200 + val exit= Unsynchronized.ref 0;
7.201 in
7.202 r := rev(sort (mv_geq order) (mv_shorten(f,order)));
7.203 g':= rev(sort (mv_geq order) (mv_shorten(g,order)));
7.204 @@ -959,10 +959,10 @@
7.205 fun uv_to_list ([]:mv_poly)=[]:uv_poly
7.206 | uv_to_list ((c1,e1)::others) =
7.207 let
7.208 - val count=ref 0;
7.209 + val count= Unsynchronized.ref 0;
7.210 val max=mv_grad((c1,e1)::others);
7.211 - val help=ref ((c1,e1)::others);
7.212 - val list=ref [];
7.213 + val help= Unsynchronized.ref ((c1,e1)::others);
7.214 + val list= Unsynchronized.ref [];
7.215 in
7.216 if length(e1)>1 then raise error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
7.217 else if length(e1)=0 then [c1]
7.218 @@ -990,9 +990,9 @@
7.219 fun uv_to_poly ([]:uv_poly) = []:mv_poly
7.220 | uv_to_poly p1 =
7.221 let
7.222 - val count=ref 0;
7.223 - val help=ref p1;
7.224 - val list=ref [];
7.225 + val count= Unsynchronized.ref 0;
7.226 + val help= Unsynchronized.ref p1;
7.227 + val list= Unsynchronized.ref [];
7.228 in
7.229 while length(!help)>0 do
7.230 (
7.231 @@ -1009,14 +1009,14 @@
7.232 | uv_gcd p1 ([]:mv_poly) = p1
7.233 | uv_gcd p1 [(c,[e])] =
7.234 let
7.235 - val list=ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
7.236 + val list= Unsynchronized.ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
7.237 val min=uv_mod_min(e,(hd(#2(hd(rev(!list))))));
7.238 in
7.239 [(gcd_int (uv_content2(p1)) c,[min])]
7.240 end
7.241 | uv_gcd [(c,[e])] p2 =
7.242 let
7.243 - val list=ref (rev(sort (mv_geq LEX_) (mv_shorten(p2,LEX_))));
7.244 + val list= Unsynchronized.ref (rev(sort (mv_geq LEX_) (mv_shorten(p2,LEX_))));
7.245 val min=uv_mod_min(e,(hd(#2(hd(rev(!list))))));
7.246 in
7.247 [(gcd_int (uv_content2(p2)) c,[min])]
7.248 @@ -1027,11 +1027,11 @@
7.249 fun mv_newton_help ([]:mv_poly list,k:int) = []:mv_poly list
7.250 | mv_newton_help (pl:mv_poly list,k) =
7.251 let
7.252 - val x=ref (rev(pl));
7.253 - val t=ref [];
7.254 - val y=ref [];
7.255 - val n=ref 1;
7.256 - val n1=ref[];
7.257 + val x= Unsynchronized.ref (rev(pl));
7.258 + val t= Unsynchronized.ref [];
7.259 + val y= Unsynchronized.ref [];
7.260 + val n= Unsynchronized.ref 1;
7.261 + val n1= Unsynchronized.ref [];
7.262 in
7.263 (
7.264 while length(!x)>1 do
7.265 @@ -1052,8 +1052,8 @@
7.266 | mv_newton_add [x:mv_poly] t = x
7.267 | mv_newton_add (pl:mv_poly list) t =
7.268 let
7.269 - val expos=ref [];
7.270 - val pll=ref pl;
7.271 + val expos= Unsynchronized.ref [];
7.272 + val pll= Unsynchronized.ref pl;
7.273 in
7.274 (
7.275
7.276 @@ -1079,12 +1079,12 @@
7.277 | mv_newton ([mp]:(mv_poly) list) = mp:mv_poly
7.278 | mv_newton pl =
7.279 let
7.280 - val c=ref pl;
7.281 - val c1=ref [];
7.282 + val c= Unsynchronized.ref pl;
7.283 + val c1= Unsynchronized.ref [];
7.284 val n=length(pl);
7.285 - val k=ref 1;
7.286 - val i=ref n;
7.287 - val ppl=ref [];
7.288 + val k= Unsynchronized.ref 1;
7.289 + val i= Unsynchronized.ref n;
7.290 + val ppl= Unsynchronized.ref [];
7.291 in
7.292 c1:=hd(pl)::[];
7.293 c:=mv_newton_help(!c,!k);
7.294 @@ -1111,8 +1111,8 @@
7.295 fun mv_min_pp([]:mv_poly)=[]
7.296 | mv_min_pp((c,e)::xs)=
7.297 let
7.298 - val y=ref xs;
7.299 - val x=ref [];
7.300 + val y= Unsynchronized.ref xs;
7.301 + val x= Unsynchronized.ref [];
7.302 in
7.303 (
7.304 x:=e;
7.305 @@ -1136,9 +1136,9 @@
7.306 fun mv_content([]:mv_poly) = []:mv_poly
7.307 | mv_content(p1) =
7.308 let
7.309 - val list=ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
7.310 - val test=ref (hd(#2(hd(!list))));
7.311 - val result=ref [];
7.312 + val list= Unsynchronized.ref (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));
7.313 + val test= Unsynchronized.ref (hd(#2(hd(!list))));
7.314 + val result= Unsynchronized.ref [];
7.315 val min=(hd(#2(hd(rev(!list)))));
7.316 in
7.317 (
7.318 @@ -1170,8 +1170,8 @@
7.319 (*. calculates the primitiv part of a polynomial .*)
7.320 and mv_pp([]:mv_poly) = []:mv_poly
7.321 | mv_pp(p1) = let
7.322 - val cont=ref [];
7.323 - val pp=ref[];
7.324 + val cont= Unsynchronized.ref [];
7.325 + val pp= Unsynchronized.ref [];
7.326 in
7.327 cont:=mv_content(p1);
7.328 pp:=(#1(mv_division(p1,!cont,LEX_)));
7.329 @@ -1215,20 +1215,20 @@
7.330 );
7.331 val p1= #1(mv_division(p1',mv_content(p1'),LEX_));
7.332 val p2= #1(mv_division(p2',mv_content(p2'),LEX_));
7.333 - val gcd=ref [];
7.334 - val candidate=ref [];
7.335 - val interpolation_list=ref [];
7.336 - val delta=ref [];
7.337 - val p1r = ref [];
7.338 - val p2r = ref [];
7.339 - val p1r' = ref [];
7.340 - val p2r' = ref [];
7.341 - val factor=ref [];
7.342 - val r=ref 0;
7.343 - val gcd_r=ref [];
7.344 - val d=ref 0;
7.345 - val exit=ref 0;
7.346 - val current_degree=ref 99999; (*. FIXME: unlimited ! .*)
7.347 + val gcd= Unsynchronized.ref [];
7.348 + val candidate= Unsynchronized.ref [];
7.349 + val interpolation_list= Unsynchronized.ref [];
7.350 + val delta= Unsynchronized.ref [];
7.351 + val p1r = Unsynchronized.ref [];
7.352 + val p2r = Unsynchronized.ref [];
7.353 + val p1r' = Unsynchronized.ref [];
7.354 + val p2r' = Unsynchronized.ref [];
7.355 + val factor= Unsynchronized.ref [];
7.356 + val r= Unsynchronized.ref 0;
7.357 + val gcd_r= Unsynchronized.ref [];
7.358 + val d= Unsynchronized.ref 0;
7.359 + val exit= Unsynchronized.ref 0;
7.360 + val current_degree= Unsynchronized.ref 99999; (*. FIXME: unlimited ! .*)
7.361 in
7.362 (
7.363 if vc<2 then (* areUnivariate(p1',p2') *)
7.364 @@ -1349,11 +1349,11 @@
7.365 converts the term to a list of coefficients .*)
7.366 fun term2coef' (t as Free(str,_(*typ*))) v :mv_poly option =
7.367 let
7.368 - val x=ref NONE;
7.369 - val len=ref 0;
7.370 - val vl=ref [];
7.371 - val vh=ref [];
7.372 - val i=ref 0;
7.373 + val x= Unsynchronized.ref NONE;
7.374 + val len= Unsynchronized.ref 0;
7.375 + val vl= Unsynchronized.ref [];
7.376 + val vh= Unsynchronized.ref [];
7.377 + val i= Unsynchronized.ref 0;
7.378 in
7.379 if is_numeral str then
7.380 (
7.381 @@ -1381,10 +1381,10 @@
7.382 end
7.383 | term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
7.384 let
7.385 - val t1pp=ref [];
7.386 - val t2pp=ref [];
7.387 - val t1c=ref 0;
7.388 - val t2c=ref 0;
7.389 + val t1pp= Unsynchronized.ref [];
7.390 + val t2pp= Unsynchronized.ref [];
7.391 + val t1c= Unsynchronized.ref 0;
7.392 + val t2c= Unsynchronized.ref 0;
7.393 in
7.394 (
7.395 t1pp:=(#2(hd(the(term2coef' t1 v))));
7.396 @@ -1398,12 +1398,12 @@
7.397 end
7.398 | term2coef' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $ (t2 as Free (str2,_))) v :mv_poly option=
7.399 let
7.400 - val x=ref NONE;
7.401 - val len=ref 0;
7.402 - val vl=ref [];
7.403 - val vh=ref [];
7.404 - val vtemp=ref [];
7.405 - val i=ref 0;
7.406 + val x= Unsynchronized.ref NONE;
7.407 + val len= Unsynchronized.ref 0;
7.408 + val vl= Unsynchronized.ref [];
7.409 + val vh= Unsynchronized.ref [];
7.410 + val vtemp= Unsynchronized.ref [];
7.411 + val i= Unsynchronized.ref 0;
7.412 in
7.413 (
7.414 if (not o is_numeral) str1 andalso is_numeral str2 then
7.415 @@ -1462,11 +1462,11 @@
7.416
7.417 | term2poly' (Free(str,_)) v :mv_poly option =
7.418 let
7.419 - val x=ref NONE;
7.420 - val len=ref 0;
7.421 - val vl=ref [];
7.422 - val vh=ref [];
7.423 - val i=ref 0;
7.424 + val x= Unsynchronized.ref NONE;
7.425 + val len= Unsynchronized.ref 0;
7.426 + val vl= Unsynchronized.ref [];
7.427 + val vh= Unsynchronized.ref [];
7.428 + val i= Unsynchronized.ref 0;
7.429 in
7.430 if is_numeral str then
7.431 (
7.432 @@ -1494,10 +1494,10 @@
7.433 end
7.434 | term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
7.435 let
7.436 - val t1pp=ref [];
7.437 - val t2pp=ref [];
7.438 - val t1c=ref 0;
7.439 - val t2c=ref 0;
7.440 + val t1pp= Unsynchronized.ref [];
7.441 + val t2pp= Unsynchronized.ref [];
7.442 + val t1c= Unsynchronized.ref 0;
7.443 + val t2c= Unsynchronized.ref 0;
7.444 in
7.445 (
7.446 t1pp:=(#2(hd(the(term2poly' t1 v))));
7.447 @@ -1513,12 +1513,12 @@
7.448 | term2poly' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $
7.449 (t2 as Free (str2,_))) v :mv_poly option=
7.450 let
7.451 - val x=ref NONE;
7.452 - val len=ref 0;
7.453 - val vl=ref [];
7.454 - val vh=ref [];
7.455 - val vtemp=ref [];
7.456 - val i=ref 0;
7.457 + val x= Unsynchronized.ref NONE;
7.458 + val len= Unsynchronized.ref 0;
7.459 + val vl= Unsynchronized.ref [];
7.460 + val vh= Unsynchronized.ref [];
7.461 + val vtemp= Unsynchronized.ref [];
7.462 + val i= Unsynchronized.ref 0;
7.463 in
7.464 (
7.465 if (not o is_numeral) str1 andalso is_numeral str2 then
7.466 @@ -1580,8 +1580,8 @@
7.467 (*. converts a powerproduct into term representation .*)
7.468 fun powerproduct2term(xs,v) =
7.469 let
7.470 - val xss=ref xs;
7.471 - val vv=ref v;
7.472 + val xss= Unsynchronized.ref xs;
7.473 + val vv= Unsynchronized.ref v;
7.474 in
7.475 (
7.476 while hd(!xss)=0 do
7.477 @@ -1745,9 +1745,9 @@
7.478 (*. calculates the greatest common divisor of numerator and denominator and seperates it from each .*)
7.479 fun step_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) =
7.480 let
7.481 - val p1' = ref [];
7.482 - val p2' = ref [];
7.483 - val p3 = ref []
7.484 + val p1' = Unsynchronized.ref [];
7.485 + val p2' = Unsynchronized.ref [];
7.486 + val p3 = Unsynchronized.ref []
7.487 val vars = rev(get_vars(p1) union get_vars(p2));
7.488 in
7.489 (
7.490 @@ -1810,9 +1810,9 @@
7.491 (*. same as step_cancel, this time for expanded forms (input+output) .*)
7.492 fun step_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =
7.493 let
7.494 - val p1' = ref [];
7.495 - val p2' = ref [];
7.496 - val p3 = ref []
7.497 + val p1' = Unsynchronized.ref [];
7.498 + val p2' = Unsynchronized.ref [];
7.499 + val p3 = Unsynchronized.ref []
7.500 val vars = rev(get_vars(p1) union get_vars(p2));
7.501 in
7.502 (
7.503 @@ -1874,9 +1874,9 @@
7.504 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
7.505 fun direct_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) =
7.506 let
7.507 - val p1' = ref [];
7.508 - val p2' = ref [];
7.509 - val p3 = ref []
7.510 + val p1' = Unsynchronized.ref [];
7.511 + val p2' = Unsynchronized.ref [];
7.512 + val p3 = Unsynchronized.ref []
7.513 val vars = rev(get_vars(p1) union get_vars(p2));
7.514 in
7.515 (
7.516 @@ -1959,9 +1959,9 @@
7.517 (*. same es direct_cancel, this time for expanded forms (input+output).*)
7.518 fun direct_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =
7.519 let
7.520 - val p1' = ref [];
7.521 - val p2' = ref [];
7.522 - val p3 = ref []
7.523 + val p1' = Unsynchronized.ref [];
7.524 + val p2' = Unsynchronized.ref [];
7.525 + val p3 = Unsynchronized.ref []
7.526 val vars = rev(get_vars(p1) union get_vars(p2));
7.527 in
7.528 (
7.529 @@ -2046,18 +2046,18 @@
7.530 fun add_fract ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
7.531 let
7.532 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
7.533 - val t11'=ref (the(term2poly t11 vars));
7.534 + val t11'= Unsynchronized.ref (the(term2poly t11 vars));
7.535 val _= writeln"### add_fract: done t11"
7.536 - val t12'=ref (the(term2poly t12 vars));
7.537 + val t12'= Unsynchronized.ref (the(term2poly t12 vars));
7.538 val _= writeln"### add_fract: done t12"
7.539 - val t21'=ref (the(term2poly t21 vars));
7.540 + val t21'= Unsynchronized.ref (the(term2poly t21 vars));
7.541 val _= writeln"### add_fract: done t21"
7.542 - val t22'=ref (the(term2poly t22 vars));
7.543 + val t22'= Unsynchronized.ref (the(term2poly t22 vars));
7.544 val _= writeln"### add_fract: done t22"
7.545 - val den=ref [];
7.546 - val nom=ref [];
7.547 - val m1=ref [];
7.548 - val m2=ref [];
7.549 + val den= Unsynchronized.ref [];
7.550 + val nom= Unsynchronized.ref [];
7.551 + val m1= Unsynchronized.ref [];
7.552 + val m2= Unsynchronized.ref [];
7.553 in
7.554
7.555 (
7.556 @@ -2092,14 +2092,14 @@
7.557 fun add_fract_exp ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
7.558 let
7.559 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
7.560 - val t11'=ref (the(expanded2poly t11 vars));
7.561 - val t12'=ref (the(expanded2poly t12 vars));
7.562 - val t21'=ref (the(expanded2poly t21 vars));
7.563 - val t22'=ref (the(expanded2poly t22 vars));
7.564 - val den=ref [];
7.565 - val nom=ref [];
7.566 - val m1=ref [];
7.567 - val m2=ref [];
7.568 + val t11'= Unsynchronized.ref (the(expanded2poly t11 vars));
7.569 + val t12'= Unsynchronized.ref (the(expanded2poly t12 vars));
7.570 + val t21'= Unsynchronized.ref (the(expanded2poly t21 vars));
7.571 + val t22'= Unsynchronized.ref (the(expanded2poly t22 vars));
7.572 + val den= Unsynchronized.ref [];
7.573 + val nom= Unsynchronized.ref [];
7.574 + val m1= Unsynchronized.ref [];
7.575 + val m2= Unsynchronized.ref [];
7.576 in
7.577
7.578 (
7.579 @@ -2176,8 +2176,8 @@
7.580 fun termlist2denominators [] = ([],[])
7.581 | termlist2denominators xs =
7.582 let
7.583 - val xxs=ref xs;
7.584 - val var=ref [];
7.585 + val xxs= Unsynchronized.ref xs;
7.586 + val var= Unsynchronized.ref [];
7.587 in
7.588 var:=[];
7.589 while length(!xxs)>0 do
7.590 @@ -2210,8 +2210,8 @@
7.591 fun termlist2denominators [] = ([],[])
7.592 | termlist2denominators xs =
7.593 let
7.594 - val xxs=ref xs;
7.595 - val var=ref [];
7.596 + val xxs= Unsynchronized.ref xs;
7.597 + val var= Unsynchronized.ref [];
7.598 in
7.599 var:=[];
7.600 while length(!xxs)>0 do
7.601 @@ -2232,8 +2232,8 @@
7.602 fun termlist2denominators_exp [] = ([],[])
7.603 | termlist2denominators_exp xs =
7.604 let
7.605 - val xxs=ref xs;
7.606 - val var=ref [];
7.607 + val xxs= Unsynchronized.ref xs;
7.608 + val var= Unsynchronized.ref [];
7.609 in
7.610 var:=[];
7.611 while length(!xxs)>0 do
8.1 --- a/src/Tools/isac/ProgLang/Script.thy Mon Sep 13 16:36:14 2010 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Script.thy Mon Sep 13 17:21:22 2010 +0200
8.3 @@ -157,16 +157,16 @@
8.4 val IDTyp = Type("Script.ID",[]);
8.5
8.6
8.7 -val tacs = ref (distinct (remove op = ""
8.8 +val tacs = Unsynchronized.ref (distinct (remove op = ""
8.9 ["Calculate",
8.10 "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",
8.11 "Substitute","Tac","Check'_elementswise",
8.12 "Take","Subproblem","Or'_to'_List"]));
8.13
8.14 -val screxpr = ref (distinct (remove op = ""
8.15 +val screxpr = Unsynchronized.ref (distinct (remove op = ""
8.16 ["Let","If","Repeat","While","Try","Or"]));
8.17
8.18 -val listfuns = ref [(*_all_ functions in Isa99.List.thy *)
8.19 +val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
8.20 "@","filter","concat","foldl","hd","last","set","list_all",
8.21 "map","mem","nth","list_update","take","drop",
8.22 "takeWhile","dropWhile","tl","butlast",
8.23 @@ -174,16 +174,16 @@
8.24
8.25 "Cons","Nil"];
8.26
8.27 -val scrfuns = ref (distinct (remove op = ""
8.28 +val scrfuns = Unsynchronized.ref (distinct (remove op = ""
8.29 ["Testvar"]));
8.30
8.31 -val listexpr = ref (union op = (!listfuns) (!scrfuns));
8.32 +val listexpr = Unsynchronized.ref (union op = (!listfuns) (!scrfuns));
8.33
8.34 -val notsimp = ref
8.35 +val notsimp = Unsynchronized.ref
8.36 (distinct (remove op = ""
8.37 (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
8.38
8.39 -val negotiable = ref ((!tacs (*@ !subpbls*)));
8.40 +val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
8.41
8.42 val tacpbl = ref
8.43 (distinct (remove op = "" (!tacs (*@ !subpbls*))));
9.1 --- a/src/Tools/isac/calcelems.sml Mon Sep 13 16:36:14 2010 +0200
9.2 +++ b/src/Tools/isac/calcelems.sml Mon Sep 13 17:21:22 2010 +0200
9.3 @@ -336,11 +336,11 @@
9.4 | ketype2str' Met_ = "Method";
9.5
9.6 (*see 'How to manage theorys in subproblems' at 'type thyID'*)
9.7 -val theory' = ref ([]:(theory' * theory) list);
9.8 +val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
9.9
9.10 (*.all theories defined for Scripts, recorded in Scripts/Script.ML;
9.11 in order to distinguish them from general IsacKnowledge defined later on.*)
9.12 -val script_thys = ref ([] : (theory' * theory) list);
9.13 +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
9.14
9.15
9.16 (*rewrite orders, also stored in 'type met' and type 'and rls'
9.17 @@ -359,10 +359,10 @@
9.18 (*WN060120 a hack to get alltogether run again with minimal effort:
9.19 theory' is inserted for creating thy_hierarchy; calls for assoc_rls
9.20 need not be called*)
9.21 -val ruleset' = ref ([]:(rls' * (theory' * rls)) list);
9.22 +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
9.23
9.24 (*FIXME.040207 calclist': used by prep_rls, NOT in met*)
9.25 -val calclist'= ref ([]: calc list);
9.26 +val calclist'= Unsynchronized.ref ([]: calc list);
9.27
9.28 (*.the hierarchy of thydata.*)
9.29
9.30 @@ -403,10 +403,10 @@
9.31 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
9.32
9.33 type thehier = (thydata ptyp) list;
9.34 -val thehier = ref ([] : thehier);
9.35 +val thehier = Unsynchronized.ref ([] : thehier);
9.36
9.37 (*.an association list, gets the value once in Isac.ML.*)
9.38 -val isab_thm_thy = ref ([] : (thmID * (thyID * term)) list);
9.39 +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
9.40
9.41
9.42 type path = string;
9.43 @@ -632,18 +632,18 @@
9.44
9.45
9.46 (*.trace internal steps of isac's rewriter*)
9.47 -val trace_rewrite = ref false;
9.48 +val trace_rewrite = Unsynchronized.ref false;
9.49 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
9.50 -val depth = ref 99999;
9.51 +val depth = Unsynchronized.ref 99999;
9.52 (*.no of rewrites exceeding this int -> NO rewrite.*)
9.53 (*WN060829 still unused...*)
9.54 -val lim_rewrite = ref 99999;
9.55 +val lim_rewrite = Unsynchronized.ref 99999;
9.56 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
9.57 -val lim_deriv = ref 100;
9.58 +val lim_deriv = Unsynchronized.ref 100;
9.59 (*.switch for checking guhs unique before storing a pbl or met;
9.60 set true at startup (done at begin of ROOT.ML)
9.61 set false for editing IsacKnowledge (done at end of ROOT.ML).*)
9.62 -val check_guhs_unique = ref false;
9.63 +val check_guhs_unique = Unsynchronized.ref false;
9.64
9.65
9.66 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)