1.1 --- a/test/Tools/isac/Interpret/appl.sml Tue Jul 26 14:35:06 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/appl.sml Tue Jul 26 15:52:07 2011 +0200
1.3 @@ -21,7 +21,6 @@
1.4 ("Test",["sqroot-test","univariate","equation","test"],
1.5 ["Test","squ-equ-test-subpbl1"]);
1.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.7 -(*========== inhibit exn 110415 -> 110506 ======================================
1.8 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.11 @@ -43,22 +42,23 @@
1.12
1.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.14 show_pt pt;
1.15 -============ inhibit exn 110415 ==============================================*)
1.16
1.17
1.18
1.19
1.20
1.21
1.22 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.23 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.24 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
1.25 val pIopt = get_pblID (pt,ip);
1.26 tacis; (*= []*)
1.27 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
1.28 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
1.29 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
1.30 -val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
1.31 - probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.32 +(*============ inhibit exn AK110726 ==============================================
1.33 +(* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
1.34 +val pblobj as (PblObj{meth, origin = origin as (oris,(dI', pI', mI'), _),
1.35 + probl, spec = (dI, pI, mI), ...}) = get_obj I pt p;
1.36 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
1.37 val cpI = if pI = e_pblID then pI' else pI;
1.38 val cmI = if mI = e_metID then mI' else mI;
1.39 @@ -67,6 +67,10 @@
1.40 val pb = foldl and_ (true, map fst pre);
1.41 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
1.42 (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
1.43 +============ inhibit exn AK110726 ==============================================*)
1.44 +
1.45 +(*============ inhibit exn AK110726 ==============================================
1.46 +(* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
1.47 "~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
1.48 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
1.49 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.50 @@ -81,5 +85,5 @@
1.51 if t = parseNEW "-1 + x = (0::real)" then ()
1.52 else error "TODO"
1.53 is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
1.54 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.55 -
1.56 +============ inhibit exn AK110726 ==============================================*)
1.57 +(*-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
2.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Jul 26 14:35:06 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 26 15:52:07 2011 +0200
2.3 @@ -584,7 +584,7 @@
2.4 "-------------- move_dn: Frm -> Res ------------------------------";
2.5 "-------------- move_dn: Frm -> Res ------------------------------";
2.6 "-------------- move_dn: Frm -> Res ------------------------------";
2.7 - (*states := [];
2.8 + states := [];
2.9 CalcTree (*start of calculation, return No.1*)
2.10 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.11 ("Test",
2.12 @@ -607,7 +607,7 @@
2.13 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
2.14 if get_pos 1 1 = ([1], Res) then ()
2.15 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
2.16 - moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)*)
2.17 + moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
2.18
2.19
2.20 "-------------- move_up ------------------------------------------";
2.21 @@ -1370,4 +1370,3 @@
2.22 show_pt pt;
2.23 *)
2.24 ========== inhibit exn AK110726 ==============================================*)
2.25 -
3.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Jul 26 14:35:06 2011 +0200
3.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Jul 26 15:52:07 2011 +0200
3.3 @@ -210,17 +210,20 @@
3.4 val ct = "x + (-4) / 2";
3.5
3.6 (*===== inhibit exn AK110725 ===========================================================
3.7 -(* ERROR: Value or constructor (thy') has not been declared *)
3.8 +(* ERROR: Value or constructor (thy') has not been declared
3.9 + AK: replacing with thy doesn't work either...*)
3.10 val (ct,_) = the (rewrite_set thy' false rls ct);
3.11 ===== inhibit exn AK110725 ===========================================================*)
3.12
3.13 "(-2) + x";
3.14 (*-------------- while ... *)
3.15 val ct = "(-4) / 2";
3.16 +
3.17 (*===== inhibit exn AK110725 ===========================================================
3.18 (* ERROR: Value or constructor (thy') has not been declared *)
3.19 val (ct,_) = the (rewrite_set thy' false rls ct);
3.20 ===== inhibit exn AK110725 ===========================================================*)
3.21 +
3.22 "-2";
3.23
3.24 (*--------------(5): reproduce (1) with simpler term: ------------*)
3.25 @@ -327,7 +330,7 @@
3.26 val thy = (@{theory "Isac"});
3.27 (*===== inhibit exn AK110725 ===========================================================
3.28 (* ERROR: real_divide_1 has not been declared
3.29 - - replace with real_divide_divide_1 or similar? *)
3.30 + - replace with Rings.division_ring_class.divide_1 - see line 387 *)
3.31 val prop = (#prop o rep_thm) real_divide_1;
3.32 atomty prop;
3.33
3.34 @@ -352,7 +355,7 @@
3.35 val t = (term_of o the o (parseold thy)) "aaa/1";
3.36 atomty t;
3.37 (*** -------------
3.38 -*** Const ( HOL.divide, ['a, 'a] => 'a)
3.39 +*** Csnst ( HOL.divide, ['a, 'a] => 'a)
3.40 *** . Free ( aaa, 'a)
3.41 *** . Free ( 1, 'a) *)
3.42 val t = (term_of o the o (parse thy)) "aaa/1";
3.43 @@ -361,12 +364,12 @@
3.44 *** Const ( HOL.divide, [real, real] => real)
3.45 *** . Free ( aaa, real)
3.46 *** . Free ( 1, real) *)
3.47 -(*===== inhibit exn AK110725 ===========================================================
3.48 - val thm = num_str @{thm real_divide_1};
3.49 +
3.50 + val thm = num_str @{thm divide_1};
3.51 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
3.52 (*val t = Free ("aaa","RealDef.real") : term*)
3.53
3.54 -
3.55 +(*===== inhibit exn AK110725 ===========================================================
3.56 val prop = (#prop o rep_thm) realpow_eq_one;
3.57 atomty prop;
3.58
4.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 26 14:35:06 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 15:52:07 2011 +0200
4.3 @@ -7,7 +7,7 @@
4.4
4.5 ML{* writeln "**** run the test ***************************************" *}
4.6
4.7 -use"../../../test/Tools/isac/Interpret/ctree.sml"
4.8 +use"../../../test/Tools/isac/Interpret/appl.sml"
4.9
4.10 ML {*
4.11
4.12 @@ -22,11 +22,6 @@
4.13
4.14
4.15
4.16 -
4.17 -
4.18 -
4.19 -
4.20 -
4.21 *}
4.22 ML{*
4.23 *}