1.1 --- a/doc-src/isac/akargl/ferialprakt.tex Mon Jul 25 14:19:50 2011 +0200
1.2 +++ b/doc-src/isac/akargl/ferialprakt.tex Tue Jul 26 09:09:49 2011 +0200
1.3 @@ -21,7 +21,7 @@
1.4 \section{Arbeitsprotokoll}
1.5 \begin{center}
1.6 \begin{tabular}{l|l|r}
1.7 -Datum & T\"atigkeit & Std. \\ \hline
1.8 +\textbf{Datum} &\textbf{T\"atigkeit} & \textbf{Std.} \\ \hline
1.9 12.7.2011
1.10 & Demonstration des ``educational math assistant \sisac'' & 1.0\\
1.11 & Demonstration des Theorem Provers Isabelle & 0.5\\
1.12 @@ -41,7 +41,7 @@
1.13 & Einf\"uhrung ML/\sisac\ IV & 1.0 \\
1.14 & ML- Programmierung & 2.5 \\
1.15 & Einf\"uhrung ML/\sisac\ V & 1.0 \\
1.16 - & ML- Programmierung & 3.0 \\ \hline
1.17 + & ML- Programmierung & 3.0 \\ \hline \hline
1.18 18.7.2011
1.19 & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.20 19.7.2011
1.21 @@ -52,7 +52,9 @@
1.22 & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.23 22.7.2011
1.24 & Information \"uber Studienrichtungen etc. & 1.0 \\
1.25 - & Fehlersuche/Debugging Isac-Tests & 6.5 \\ \hline
1.26 + & Fehlersuche/Debugging Isac-Tests & 6.5 \\ \hline \hline
1.27 +25.7.2011
1.28 + & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.29 \end{tabular}
1.30 \end{center}
1.31
2.1 --- a/test/Tools/isac/Interpret/mstools.sml Mon Jul 25 14:19:50 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/mstools.sml Tue Jul 26 09:09:49 2011 +0200
2.3 @@ -98,17 +98,24 @@
2.4 val (dI',pI',mI') =
2.5 ("Test", ["sqroot-test","univariate","equation","test"],
2.6 ["Test","squ-equ-test-subpbl1"]);
2.7 +
2.8 +(*========== inhibit exn AK110725 ================================================
2.9 +(* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)
2.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.11 +========== inhibit exn AK110725 ================================================*)
2.12
2.13 +(*========== inhibit exn AK110725 ================================================
2.14 +(* ERROR: pt and p are not declared due to above error *)
2.15 "=(1)= variables known from formalisation provide type-inference for further input";
2.16 val ctxt = get_ctxt pt p;
2.17 +
2.18 val SOME known_x = parseNEW ctxt "x+y+z";
2.19 val SOME unknown = parseNEW ctxt "xa+b+c";
2.20 +
2.21 if type_of known_x = Type ("RealDef.real",[]) then ()
2.22 else error "x+1=2 after start root-pbl wrong type-inference from known x";
2.23 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
2.24 else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
2.25 -
2.26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.29 @@ -126,6 +133,8 @@
2.30 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
2.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.32
2.33 +
2.34 +
2.35 "=(3)= variables known from arguments of (sub-)method provide type-inference for further input";
2.36 val ctxt = get_ctxt pt p;
2.37 val SOME known_x = parseNEW ctxt "x+y+z";
2.38 @@ -172,6 +181,7 @@
2.39 if terms2strs (get_assumptions_ pt p) = (*weak check: sub-result = root-result = [x = 1]*)
2.40 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
2.41 then () else error "x+1=2 transfer from sub-met to root-met changed";
2.42 +========== inhibit exn AK110725 ================================================*)
2.43
2.44
2.45 "----------- go through Model_Problem until nxt_tac -----";
2.46 @@ -182,7 +192,13 @@
2.47 val (dI',pI',mI') =
2.48 ("Test", ["sqroot-test","univariate","equation","test"],
2.49 ["Test","squ-equ-test-subpbl1"]);
2.50 +(*========== inhibit exn AK110725 ================================================
2.51 +(* ERROR: same as above, see lines 120- 123 *)
2.52 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.53 +========== inhibit exn AK110725 ================================================*)
2.54 +
2.55 +(*========== inhibit exn AK110725 ================================================
2.56 +(* ERROR: p, nxt, pt not declared due to above error *)
2.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.60 @@ -242,3 +258,4 @@
2.61 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
2.62 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS
2.63 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
2.64 +========== inhibit exn AK110725 ================================================*)
3.1 --- a/test/Tools/isac/Interpret/ptyps.sml Mon Jul 25 14:19:50 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Tue Jul 26 09:09:49 2011 +0200
3.3 @@ -1,6 +1,6 @@
3.4 -(* tests for ME/ptyps.sml
3.5 +(* Title: tests for ME/ptyps.sml
3.6 CAUTION: intermediately stores !ptyps THUS EVALUATE IN 1 GO
3.7 - author: Walther Neuper
3.8 + uthor: Walther Neuper
3.9 010916,
3.10 (c) due to copyright terms
3.11
3.12 @@ -24,7 +24,6 @@
3.13 "--------------------------------------------------------";
3.14 "--------------------------------------------------------";
3.15
3.16 -(*========== inhibit exn ?======================================================
3.17 "###### val intermediate_ptyps = !ptyps; #########################";
3.18 "###### val intermediate_ptyps = !ptyps; #########################";
3.19 "###### val intermediate_ptyps = !ptyps; #########################";
3.20 @@ -34,9 +33,9 @@
3.21 "----------- store test-pbtyps -----------------------------------";
3.22 "----------- store test-pbtyps -----------------------------------";
3.23 ptyps:= ([]:ptyps);
3.24 -
3.25 +(*========== inhibit exn AK110725 ======================================================
3.26 store_pbt
3.27 - (prep_pbt DiffApp.thy "pbl_pbla" [] e_pblID
3.28 + (prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID
3.29 (["pbla"],
3.30 [("#Given", ["fixedValues a_"])], e_rls, NONE, []));
3.31 store_pbt
3.32 @@ -69,13 +68,14 @@
3.33 e_rls, NONE, []));
3.34
3.35 show_ptyps();
3.36 +========== inhibit exn AK110725 ======================================================*)
3.37
3.38 (*case 1: no refinement *)
3.39 -val thy = (theory "Isac");
3.40 -val (d1,ts1) = split_dts thy ((term_of o the o (parse thy))
3.41 - "fixedValues [aaa=0]");
3.42 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
3.43 - "errorBound (ddd=0)");
3.44 +val thy = (@{theory "Isac"});
3.45 +(*========== inhibit exn AK110725 ======================================================
3.46 +val (d1,ts1) = split_dts thy ((term_of o the o (parse thy)) "fixedValues [aaa=0]");
3.47 +val (d2,ts2) = split_dts thy ((term_of o the o (parse thy)) "errorBound (ddd=0)");
3.48 +
3.49 val ori1 = [(1,[1],"#Given",d1,ts1),
3.50 (2,[1],"#Given",d2,ts2)]:ori list;
3.51
3.52 @@ -101,6 +101,7 @@
3.53 (2,[1],"#Given",d2,ts2),
3.54 (3,[1],"#Given",d3,ts3)]:ori list;
3.55
3.56 +
3.57 "----------- refin test-pbtyps -----------------------------------";
3.58 "----------- refin test-pbtyps -----------------------------------";
3.59 "----------- refin test-pbtyps -----------------------------------";
3.60 @@ -149,6 +150,7 @@
3.61 (*case 5: start refinement somewhere in ptyps*)
3.62 refine_ori ori4 ["pbla2","pbla"];
3.63 (*val it = SOME ["pbla2y","pbla2","pbla"] : pblID option*)
3.64 +========== inhibit exn AK110725 ======================================================*)
3.65
3.66
3.67 "----------- refine test-pbtyps ----------------------------------";
3.68 @@ -160,6 +162,7 @@
3.69 val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",
3.70 "boundVariable aaa222yyy"];
3.71
3.72 +(*========== inhibit exn AK110725 ======================================================
3.73 (*case 1: no refinement *)
3.74 refine fmz1 ["pbla"];
3.75 (*
3.76 @@ -190,6 +193,7 @@
3.77 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
3.78 : match list*)
3.79
3.80 +
3.81 (*case 2: refined to pbt without children *)
3.82 refine fmz2 ["pbla"];
3.83 (*
3.84 @@ -329,6 +333,8 @@
3.85 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
3.86 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
3.87 : match list*)
3.88 +========== inhibit exn AK110725 ======================================================*)
3.89 +
3.90
3.91 "###### ptyps:= intermediate_ptyps;###############################";
3.92 "###### ptyps:= intermediate_ptyps;###############################";
3.93 @@ -343,12 +349,16 @@
3.94 "errorBound (eps=0)","solutions L"];
3.95 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
3.96 ["Test","squ-equ-test-subpbl1"]);
3.97 +(*========== inhibit exn AK110725 ======================================================
3.98 +(* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)
3.99 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.100 +
3.101 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.102 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.103 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.104 (*nxt = ("Add_Find", Add_Find "solutions L")*)
3.105
3.106 +
3.107 val nxt = ("Specify_Problem",(*vvvv---specify a not-matching problem*)
3.108 Specify_Problem ["linear","univariate","equation","test"]);
3.109 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.110 @@ -386,6 +396,7 @@
3.111 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.112 (*Subproblem ("Test", ["linear", "univariate", "equation", "test"]*)
3.113
3.114 +
3.115 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.116 (*nxt = Model_Problem ["linear","univariate","equation","test"]*)
3.117 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.118 @@ -419,6 +430,7 @@
3.119 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;
3.120 if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()
3.121 else error "new behaviour in test:refine.sml:miniscript with mini-subpb";
3.122 +========== inhibit exn AK110725 ======================================================*)
3.123
3.124
3.125 "----------- fun coll_guhs ---------------------------------------";
3.126 @@ -453,8 +465,11 @@
3.127 "----------- fun guh2kestoreID -----------------------------------";
3.128 "----------- fun guh2kestoreID -----------------------------------";
3.129 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
3.130 +(*========== inhibit exn AK110725 ======================================================
3.131 +(* ERROR: Exception Bind raised *)
3.132 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
3.133 Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (!ptyps);
3.134 +
3.135 (*
3.136 nodes [] guh1 (!ptyps);
3.137 nodes [] guh2 (!ptyps);
3.138 @@ -471,8 +486,4 @@
3.139 nodes [] guh3 (!ptyps);
3.140 nodes [] guh21 (!ptyps);
3.141 *)
3.142 -============ inhibit exn ?====================================================*)
3.143 -
3.144 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.145 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
3.146 -
3.147 +============ inhibit exn AK110725 ====================================================*)
4.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Jul 25 14:19:50 2011 +0200
4.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Jul 26 09:09:49 2011 +0200
4.3 @@ -5,7 +5,6 @@
4.4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
4.5 10 20 30 40 50 60 70 80
4.6 *)
4.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
4.8
4.9 "--------------------------------------------------------";
4.10 "table of contents --------------------------------------";
4.11 @@ -74,7 +73,7 @@
4.12 "----------- calculate from script ----------------------";
4.13 "----------- calculate from script ----------------------";
4.14 "----------- calculate from script ----------------------";
4.15 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
4.16 +
4.17 store_pbt
4.18 (prep_pbt (@{theory "Test"}) "pbl_ttest" [] e_pblID
4.19 (["test"],
4.20 @@ -143,7 +142,6 @@
4.21 else error "calculate.sml: script test_calculate changed behaviour";
4.22
4.23
4.24 -(*===== inhibit exn ?===========================================================
4.25 "----------- calculate check test-root-equ --------------";
4.26 "----------- calculate check test-root-equ --------------";
4.27 "----------- calculate check test-root-equ --------------";
4.28 @@ -168,7 +166,7 @@
4.29 ............... does not work *)
4.30
4.31 (*--------------(2): does divide work in Test_simplify ?: ------*)
4.32 - val thy = Test.thy;
4.33 + val thy = @{theory Test};
4.34 val t = (term_of o the o (parse thy)) "6 / 2";
4.35 val rls = Test_simplify;
4.36 val (t,_) = the (rewrite_set_ thy false rls t);
4.37 @@ -183,13 +181,13 @@
4.38
4.39
4.40 (*--------------(3): is_const works ?: -------------------------------------*)
4.41 - val t = (term_of o the o (parse Test.thy)) "2 is_const";
4.42 + val t = (term_of o the o (parse @{theory Test})) "2 is_const";
4.43 atomty t;
4.44 - rewrite_set_ Test.thy false tval_rls t;
4.45 + rewrite_set_ @{theory Test} false tval_rls t;
4.46 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
4.47
4.48 val t = str2term "2 * x is_const";
4.49 - val SOME (str,t') = eval_const "" "" t (theory "Isac");
4.50 + val SOME (str,t') = eval_const "" "" t (@{theory "Isac"});
4.51 term2str t';
4.52
4.53
4.54 @@ -198,18 +196,31 @@
4.55 "----------- check calculate bottom up ------------------";
4.56 (*-------------- eval_cancel works: *)
4.57 trace_rewrite:=true;
4.58 - val thy = Test.thy;
4.59 + val thy = @{theory Test};
4.60 val t = (term_of o the o (parse thy)) "(-4) / 2";
4.61 - val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
4.62 +
4.63 +(*===== inhibit exn AK110725 ===========================================================
4.64 +(* ERROR: Exception Bind raised *)
4.65 +val SOME (_, t) = eval_cancel "xxx" "HOL.divide" t thy;
4.66 +===== inhibit exn AK110725 ===========================================================*)
4.67 +
4.68 term2str t;
4.69 "-4 / 2 = (-2)";
4.70 (*-------------- but ... *)
4.71 val ct = "x + (-4) / 2";
4.72 +
4.73 +(*===== inhibit exn AK110725 ===========================================================
4.74 +(* ERROR: Value or constructor (thy') has not been declared *)
4.75 val (ct,_) = the (rewrite_set thy' false rls ct);
4.76 +===== inhibit exn AK110725 ===========================================================*)
4.77 +
4.78 "(-2) + x";
4.79 (*-------------- while ... *)
4.80 val ct = "(-4) / 2";
4.81 +(*===== inhibit exn AK110725 ===========================================================
4.82 +(* ERROR: Value or constructor (thy') has not been declared *)
4.83 val (ct,_) = the (rewrite_set thy' false rls ct);
4.84 +===== inhibit exn AK110725 ===========================================================*)
4.85 "-2";
4.86
4.87 (*--------------(5): reproduce (1) with simpler term: ------------*)
4.88 @@ -231,7 +242,7 @@
4.89 trace_rewrite:=false;
4.90
4.91 trace_rewrite:=true; (*3.6.03*)
4.92 - val thy = Test.thy;
4.93 + val thy = @{theory Test};
4.94 val rls = Test_simplify;
4.95 val t = str2term "(3+(1+2*x))/2";
4.96 val SOME (t',asm) = rewrite_set_ thy false rls t;
4.97 @@ -270,7 +281,6 @@
4.98 -----------------------------------------------------------------*)
4.99
4.100
4.101 - toggle trace_rewrite;
4.102 (*===================*)
4.103 trace_rewrite:=true;
4.104 val thy' = "Test";
4.105 @@ -314,9 +324,13 @@
4.106 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
4.107 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
4.108 " ----------------- rewriting works ? -----------------------";
4.109 - val thy = (theory "Isac");
4.110 + val thy = (@{theory "Isac"});
4.111 +(*===== inhibit exn AK110725 ===========================================================
4.112 +(* ERROR: real_divide_1 has not been declared
4.113 + - replace with real_divide_divide_1 or similar? *)
4.114 val prop = (#prop o rep_thm) real_divide_1;
4.115 atomty prop;
4.116 +
4.117 (*** -------------
4.118 *** Const ( Trueprop, bool => prop)
4.119 *** . Const ( op =, [real, real] => bool)
4.120 @@ -326,6 +340,8 @@
4.121 *** . . Var ((x, 0), real) *)
4.122 val prop' = (#prop o rep_thm o num_str) real_divide_1;
4.123 atomty prop';
4.124 +===== inhibit exn AK110725 ===========================================================*)
4.125 +
4.126 (*** -------------
4.127 *** Const ( Trueprop, bool => prop)
4.128 *** . Const ( op =, [real, real] => bool)
4.129 @@ -345,6 +361,7 @@
4.130 *** Const ( HOL.divide, [real, real] => real)
4.131 *** . Free ( aaa, real)
4.132 *** . Free ( 1, real) *)
4.133 +(*===== inhibit exn AK110725 ===========================================================
4.134 val thm = num_str real_divide_1;
4.135 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
4.136 (*val t = Free ("aaa","RealDef.real") : term*)
4.137 @@ -352,6 +369,7 @@
4.138
4.139 val prop = (#prop o rep_thm) realpow_eq_one;
4.140 atomty prop;
4.141 +
4.142 (*** -------------
4.143 *** Const ( Trueprop, bool => prop)
4.144 *** . Const ( op =, [real, real] => bool)
4.145 @@ -361,6 +379,8 @@
4.146 *** . . Const ( 1, real) *)
4.147 val prop' = (#prop o rep_thm o num_str) realpow_eq_one;
4.148 atomty prop';
4.149 +===== inhibit exn AK110725 ===========================================================*)
4.150 +
4.151 (*** -------------
4.152 *** Const ( Trueprop, bool => prop)
4.153 *** . Const ( op =, [real, real] => bool)
4.154 @@ -380,20 +400,22 @@
4.155 *** Const ( Nat.power, [real, nat] => real)
4.156 *** . Free ( 1, real)
4.157 *** . Free ( aaa, nat) .......................... nat !!! *)
4.158 +(*===== inhibit exn AK110725 ===========================================================
4.159 val thm = num_str realpow_eq_one;
4.160 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
4.161 +===== inhibit exn AK110725 ===========================================================*)
4.162 (*val t = Free ("1","RealDef.real") : term*)
4.163
4.164 " ================= calculate.sml: calculate_ 2002 =================== ";
4.165 " ================= calculate.sml: calculate_ 2002 =================== ";
4.166 " ================= calculate.sml: calculate_ 2002 =================== ";
4.167
4.168 -val thy = Test.thy;
4.169 +val thy = @{theory Test};
4.170 val t = (term_of o the o (parse thy)) "12 / 3";
4.171 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
4.172 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
4.173 "12 / 3 = 4";
4.174 -val thy = Test.thy;
4.175 +val thy = @{theory Test};
4.176 val t = (term_of o the o (parse thy)) "4 ^^^ 2";
4.177 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;
4.178 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
4.179 @@ -444,7 +466,7 @@
4.180 val SOME (id,t') = eval_binop thmid op_ t thy;
4.181 (*** calc: operator = pow not defined*)
4.182
4.183 -
4.184 +
4.185 "----------- get_pair with 3 args --------------------------------";
4.186 "----------- get_pair with 3 args --------------------------------";
4.187 "----------- get_pair with 3 args --------------------------------";
4.188 @@ -452,11 +474,11 @@
4.189 (thy, "EqSystem.occur'_exactly'_in",
4.190 snd (the (assoc(!calclist',"occur_exactly_in"))),
4.191 str2term
4.192 - "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
4.193 + "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
4.194 );
4.195 val SOME (str, simpl) = get_pair thy op_ ef arg;
4.196 if str =
4.197 -"[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
4.198 +"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
4.199 then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";
4.200
4.201
4.202 @@ -464,12 +486,10 @@
4.203 "----------- calculate (2 * x is_const) -----------------";
4.204 "----------- calculate (2 * x is_const) -----------------";
4.205 val t = str2term "2 * x is_const";
4.206 -val SOME (str, t') = eval_const "" "" t Test.thy;
4.207 +val SOME (str, t') = eval_const "" "" t @{theory Test};
4.208 term2str t';
4.209 "(2 * x is_const) = False";
4.210
4.211 -val SOME (t',_) = rewrite_set_ Test.thy false tval_rls t;
4.212 +val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
4.213 term2str t';
4.214 "HOL.False";
4.215 -===== inhibit exn ?===========================================================*)
4.216 -
5.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Jul 25 14:19:50 2011 +0200
5.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Jul 26 09:09:49 2011 +0200
5.3 @@ -23,13 +23,13 @@
5.4 "--------------------------------------------------------";
5.5 "--------------------------------------------------------";
5.6
5.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
5.8
5.9 "----------- assemble rewrite ---------------------------";
5.10 "----------- assemble rewrite ---------------------------";
5.11 "----------- assemble rewrite ---------------------------";
5.12 "===== rewriting by thm with 'a";
5.13 (*show_types := true;*)
5.14 +
5.15 val thy = @{theory Complex_Main};
5.16 val ctxt = @{context};
5.17 val thm = @{thm add_commute};
5.18 @@ -73,7 +73,7 @@
5.19 (*is displayed on top of <response> buffer...*)
5.20 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
5.21 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
5.22 -(*}*)
5.23 +(**)
5.24
5.25 "----------- test rewriting without Isac's thys ---------";
5.26 "----------- test rewriting without Isac's thys ---------";
5.27 @@ -347,7 +347,6 @@
5.28 imports Main Complex
5.29 begin
5.30
5.31 -ML {*
5.32 let
5.33 val parser = Args.context -- Scan.lift Args.name_source
5.34 fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
5.35 @@ -355,20 +354,17 @@
5.36 in
5.37 ML_Antiquote.inline "term_pat" (parser >> term_pat)
5.38 end
5.39 -*}
5.40
5.41 -ML {*
5.42 val t = @{term "a + b * x = (0 ::real)"};
5.43 val pat = @{term_pat "?l = (?r ::real)"};
5.44 val precond = @{term_pat "is_polynomial (?l::real)"};
5.45 val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
5.46 -*}
5.47
5.48 -ML {*
5.49 Envir.subst_term inst precond
5.50 |> Syntax.string_of_term @{context}
5.51 |> writeln
5.52 -*}
5.53 +
5.54 +
5.55 end *)
5.56 val thy = @{theory "Isac"};
5.57 val t = @{term "a + b * x = (0 ::real)"};
5.58 @@ -522,5 +518,3 @@
5.59 case eval__true thy i asms bdv rls of
5.60 ([], true) => ()
5.61 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
5.62 -
5.63 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
6.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jul 25 14:19:50 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Jul 26 09:09:49 2011 +0200
6.3 @@ -99,7 +99,7 @@
6.4 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
6.5 use "library.sml"
6.6 use "calcelems.sml"
6.7 - use "ProgLang/termC.sml
6.8 + use "ProgLang/termC.sml"
6.9 use "ProgLang/calculate.sml" (*part.*)
6.10 use "ProgLang/rewrite.sml" (*part.*)
6.11 (*use "ProgLang/listg.sml" 2002*)
6.12 @@ -117,11 +117,11 @@
6.13 use "Minisubpbl/500-met-sub-to-root.sml"
6.14 use "Minisubpbl/530-error-Check_Elementwise.sml"
6.15 use "Minisubpbl/600-postcond.sml"
6.16 - ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
6.17 + ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
6.18 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
6.19 use "Interpret/mstools.sml" (*new 2010*)
6.20 use "Interpret/ctree.sml" (*!...!see(25)*)
6.21 - use "Interpret/ptyps.sml" (* *)
6.22 + use "Interpret/ptyps.sml" (*part.*)
6.23 (*use "Interpret/generate.sml" new 2011*)
6.24 use "Interpret/calchead.sml" (*part.*)
6.25 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
7.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 25 14:19:50 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 09:09:49 2011 +0200
7.3 @@ -9,7 +9,9 @@
7.4
7.5 use"../../../test/Tools/isac/Interpret/calchead.sml"
7.6
7.7 -ML{*
7.8 +ML {*
7.9 +
7.10 +
7.11
7.12
7.13
7.14 @@ -38,7 +40,7 @@
7.15 end
7.16
7.17
7.18 -(*========== inhibit exn AK110725 ================================================
7.19 +(*============ inhibit exn AK110725 ==============================================
7.20 ============ inhibit exn AK110725 ==============================================*)
7.21
7.22