33 val SOME (thmID, thm) = get_calculation_ thy cal t; |
33 val SOME (thmID, thm) = get_calculation_ thy cal t; |
34 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop") |
34 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop") |
35 handle TERM _ => |
35 handle TERM _ => |
36 error "calculate.sml: get_calculation_ must return Trueprop"; |
36 error "calculate.sml: get_calculation_ must return Trueprop"; |
37 |
37 |
38 (*===== inhibit exn ?=========================================================== |
|
39 |
|
40 "----------- fun calculate_ -----------------------------"; |
38 "----------- fun calculate_ -----------------------------"; |
41 "----------- fun calculate_ -----------------------------"; |
39 "----------- fun calculate_ -----------------------------"; |
42 "----------- fun calculate_ -----------------------------"; |
40 "----------- fun calculate_ -----------------------------"; |
43 val thy = theory "Test"; |
41 val thy = theory "Test"; |
|
42 "===== test 1"; |
44 val t = (term_of o the o (parse thy)) "1+2"; |
43 val t = (term_of o the o (parse thy)) "1+2"; |
45 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
44 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
46 |
45 term2str (prop_of thm) = "1 + 2 = 3"; |
|
46 |
|
47 "===== test 2"; |
47 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; |
48 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; |
48 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
49 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
49 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
50 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
50 Sign.string_of_term (sign_of thy) t; |
51 term2str t = "(3 * 4 / 3) ^^^ 2"; |
51 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*) |
52 |
52 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t; |
53 "===== test 3: step into code"; |
53 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
54 |
54 Sign.string_of_term (sign_of thy) t; |
55 val ttt = str2term "2*3"; |
|
56 |
|
57 get_calculation_ thy (the(assoc(calclist, "TIMES"))) ttt; |
|
58 (*===== inhibit exn ?=========================================================== |
|
59 |
|
60 "===== test 3b -- 2 contiued"; |
|
61 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; |
|
62 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
63 term2str t; |
55 (*val it = "(#12 // #3) ^^^ #2" : string*) |
64 (*val it = "(#12 // #3) ^^^ #2" : string*) |
56 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
65 |
57 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
66 "===== test 4"; |
58 Sign.string_of_term (sign_of thy) t; |
67 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t; |
|
68 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
69 term2str t; |
59 (*it = "#4 ^^^ #2" : string*) |
70 (*it = "#4 ^^^ #2" : string*) |
60 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
71 |
61 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
72 "===== test 5"; |
62 Sign.string_of_term (sign_of thy) t; |
73 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t; |
|
74 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
75 term2str t; |
63 (*val it = "#16" : string*) |
76 (*val it = "#16" : string*) |
64 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
77 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
65 else (); |
78 else (); |
|
79 |
66 |
80 |
67 |
81 |
68 "----------- calculate from script ----------------------"; |
82 "----------- calculate from script ----------------------"; |
69 "----------- calculate from script ----------------------"; |
83 "----------- calculate from script ----------------------"; |
70 "----------- calculate from script ----------------------"; |
84 "----------- calculate from script ----------------------"; |
86 (["Test","test_calculate"]:metID, |
100 (["Test","test_calculate"]:metID, |
87 [("#Given" ,["realTestGiven t_"]), |
101 [("#Given" ,["realTestGiven t_"]), |
88 ("#Find" ,["realTestFind s_"]) |
102 ("#Find" ,["realTestFind s_"]) |
89 ], |
103 ], |
90 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, |
104 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, |
91 calc=[("plus" ,("op +" ,eval_binop "#add_")), |
105 calc=[("PLUS" ,("op +" ,eval_binop "#add_")), |
92 ("times" ,("op *" ,eval_binop "#mult_")), |
106 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
93 ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")), |
107 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), |
94 ("power_" ,("Atools.pow" ,eval_binop "#power_"))], |
108 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
95 crls=tval_rls, nrls=e_rls(*, |
109 crls=tval_rls, nrls=e_rls(*, |
96 asm_rls=[],asm_thm=[]*)}, |
110 asm_rls=[],asm_thm=[]*)}, |
97 "Script STest_simplify (t_::real) = \ |
111 "Script STest_simplify (t_::real) = \ |
98 \(Repeat \ |
112 \(Repeat \ |
99 \ ((Try (Repeat (Calculate plus))) @@ \ |
113 \ ((Try (Repeat (Calculate plus))) @@ \ |
121 (*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*) |
135 (*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*) |
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
123 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*) |
137 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*) |
124 |
138 |
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
126 (*nxt = ("Calculate",Calculate "plus")*) |
140 (*nxt = ("Calculate",Calculate "PLUS")*) |
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
128 (*nxt = ("Calculate",Calculate "times")*) |
142 (*nxt = ("Calculate",Calculate "TIMES")*) |
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
130 (*nxt = ("Calculate",Calculate "divide_")*) |
144 (*nxt = ("Calculate",Calculate "DIVIDE")*) |
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
132 (*nxt = ("Calculate",Calculate "power_")*) |
146 (*nxt = ("Calculate",Calculate "POWER")*) |
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
134 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) |
148 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) |
135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
136 (*nxt = ("End_Proof'",End_Proof')*) |
150 (*nxt = ("End_Proof'",End_Proof')*) |
137 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then () |
151 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then () |
383 " ================= calculate.sml: calculate_ 2002 =================== "; |
397 " ================= calculate.sml: calculate_ 2002 =================== "; |
384 " ================= calculate.sml: calculate_ 2002 =================== "; |
398 " ================= calculate.sml: calculate_ 2002 =================== "; |
385 |
399 |
386 val thy = Test.thy; |
400 val thy = Test.thy; |
387 val t = (term_of o the o (parse thy)) "12 / 3"; |
401 val t = (term_of o the o (parse thy)) "12 / 3"; |
388 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
402 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t; |
389 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
403 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
390 "12 / 3 = 4"; |
404 "12 / 3 = 4"; |
391 val thy = Test.thy; |
405 val thy = Test.thy; |
392 val t = (term_of o the o (parse thy)) "4 ^^^ 2"; |
406 val t = (term_of o the o (parse thy)) "4 ^^^ 2"; |
393 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t; |
407 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t; |
394 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
408 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
395 "4 ^ 2 = 16"; |
409 "4 ^ 2 = 16"; |
396 |
410 |
397 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
411 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
398 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
412 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
399 "1 + 2 = 3"; |
413 "1 + 2 = 3"; |
400 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
414 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
401 Sign.string_of_term (sign_of thy) t; |
415 term2str t; |
402 "(3 * 4 / 3) ^^^ 2"; |
416 "(3 * 4 / 3) ^^^ 2"; |
403 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t; |
417 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES")))t; |
404 "3 * 4 = 12"; |
418 "3 * 4 = 12"; |
405 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
419 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
406 Sign.string_of_term (sign_of thy) t; |
420 term2str t; |
407 "(12 / 3) ^^^ 2"; |
421 "(12 / 3) ^^^ 2"; |
408 val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
422 val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t; |
409 "12 / 3 = 4"; |
423 "12 / 3 = 4"; |
410 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
424 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
411 Sign.string_of_term (sign_of thy) t; |
425 term2str t; |
412 "4 ^^^ 2"; |
426 "4 ^^^ 2"; |
413 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
427 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t; |
414 "4 ^^^ 2 = 16"; |
428 "4 ^^^ 2 = 16"; |
415 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
429 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
416 Sign.string_of_term (sign_of thy) t; |
430 term2str t; |
417 "16"; |
431 "16"; |
418 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
432 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
419 else (); |
433 else (); |
420 |
434 |
421 (*13.9.02 *** calc: operator = pow not defined*) |
435 (*13.9.02 *** calc: operator = pow not defined*) |
422 val t = (term_of o the o (parse thy)) "3^^^2"; |
436 val t = (term_of o the o (parse thy)) "3^^^2"; |
423 val SOME (thmID,thm) = |
437 val SOME (thmID,thm) = |
424 get_calculation_ thy (the(assoc(calclist,"power_"))) t; |
438 get_calculation_ thy (the(assoc(calclist,"POWER"))) t; |
425 (*** calc: operator = pow not defined*) |
439 (*** calc: operator = pow not defined*) |
426 |
440 |
427 val (op_, eval_fn) = the (assoc(calclist,"power_")); |
441 val (op_, eval_fn) = the (assoc(calclist,"POWER")); |
428 (* |
442 (* |
429 val op_ = "Atools.pow" : string |
443 val op_ = "Atools.pow" : string |
430 val eval_fn = fn : string -> term -> theory -> (string * term) option*) |
444 val eval_fn = fn : string -> term -> theory -> (string * term) option*) |
431 |
445 |
432 val SOME (thmid,t') = get_pair thy op_ eval_fn t; |
446 val SOME (thmid,t') = get_pair thy op_ eval_fn t; |