72 |
72 |
73 "----------- calculate from Prog --------------------------------- -----------------------------"; |
73 "----------- calculate from Prog --------------------------------- -----------------------------"; |
74 "----------- calculate from Prog --------------------------------- -----------------------------"; |
74 "----------- calculate from Prog --------------------------------- -----------------------------"; |
75 "----------- calculate from Prog --------------------------------- -----------------------------"; |
75 "----------- calculate from Prog --------------------------------- -----------------------------"; |
76 val thy = @{theory "Test"}; |
76 val thy = @{theory "Test"}; |
77 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"]; |
77 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)", "realTestFind s"]; |
78 val (dI',pI',mI') = |
78 val (dI',pI',mI') = |
79 ("Test",["calculate","test"],["Test","test_calculate"]); |
79 ("Test",["calculate", "test"],["Test", "test_calculate"]); |
80 |
80 |
81 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
81 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
83 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*) |
83 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*) |
84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
85 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*) |
85 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*) |
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
87 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*) |
87 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*) |
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
89 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*) |
89 (*nxt = ("Specify_Problem",Specify_Problem ["calculate", "test"])*) |
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
91 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*) |
91 (*nxt = ("Specify_Method",Specify_Method ("Test", "test_calculate"))*) |
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
93 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*) |
93 (*nxt = ("Apply_Method",Apply_Method ("Test", "test_calculate"))*) |
94 |
94 |
95 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*) |
95 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*) |
96 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*) |
96 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*) |
97 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*) |
97 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*) |
98 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*) |
98 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*) |
99 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) |
99 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate", "test"])*) |
100 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*) |
100 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*) |
101 case f of Test_Out.FormKF "16" => () | _ => |
101 case f of Test_Out.FormKF "16" => () | _ => |
102 error "evaluate.sml: script test_calculate changed behaviour"; |
102 error "evaluate.sml: script test_calculate changed behaviour"; |
103 |
103 |
104 |
104 |
129 (*--------------(2): does divide work in Test_simplify ?: ------*) |
129 (*--------------(2): does divide work in Test_simplify ?: ------*) |
130 val thy = @{theory Test}; |
130 val thy = @{theory Test}; |
131 val t = (Thm.term_of o the o (parse thy)) "6 / 2"; |
131 val t = (Thm.term_of o the o (parse thy)) "6 / 2"; |
132 val rls = Test_simplify; |
132 val rls = Test_simplify; |
133 val (t,_) = the (rewrite_set_ thy false rls t); |
133 val (t,_) = the (rewrite_set_ thy false rls t); |
134 (*val t = Free ("3","Real.real") : term*) |
134 (*val t = Free ("3", "Real.real") : term*) |
135 |
135 |
136 (*--------------(3): is_const works ?: -------------------------------------*) |
136 (*--------------(3): is_const works ?: -------------------------------------*) |
137 val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const"; |
137 val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const"; |
138 atomty t; |
138 atomty t; |
139 rewrite_set_ @{theory Test} false tval_rls t; |
139 rewrite_set_ @{theory Test} false tval_rls t; |
140 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*) |
140 (*val it = SOME (Const ("HOL.True", "bool"),[]) ... works*) |
141 |
141 |
142 val t = str2term "2 * x is_const"; |
142 val t = str2term "2 * x is_const"; |
143 val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"}); |
143 val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"}); |
144 UnparseC.term t'; |
144 UnparseC.term t'; |
145 |
145 |