|
1 (* = Tools.ML |
|
2 +++ outcommented tests *) |
|
3 |
|
4 |
|
5 fun eval_var (thmid:string) (op_:string) |
|
6 (t as (Const(op0,t0) $ arg)) thy = |
|
7 let |
|
8 val t' = ((list2isalist HOLogic.realT) o vars) t; |
|
9 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); |
|
10 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
|
11 | eval_var _ _ _ _ = raise GO_ON; |
|
12 (* |
|
13 > val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))"; |
|
14 > val op_ = "Var"; |
|
15 > val eval_fn = the (assoc (!eval_list, op_)); |
|
16 > get_pair op_ eval_fn t; |
|
17 > val (t as (Const(op0,t0) $ arg)) = t; |
|
18 > eval_fn op0 t; |
|
19 |
|
20 > val thmid = "#Var_"; |
|
21 > val (SOME(thmId,t')) = eval_var thmid op0 t; |
|
22 val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #)) |
|
23 : (string * term) option |
|
24 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
25 val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string |
|
26 *) |
|
27 fun eval_Length (thmid:string) (op_:string) |
|
28 (t as (Const(op0,t0) $ arg)) thy = |
|
29 let |
|
30 val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg; |
|
31 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); |
|
32 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
|
33 | eval_Length _ _ _ _ = raise GO_ON; |
|
34 (* |
|
35 > val thmid = "#Length_"; val op_ = "Length"; |
|
36 > val s = "Length [A = a * b, a // #2 = #2]"; |
|
37 > val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s; |
|
38 > val (SOME (id,t')) = eval_Length thmid op_ t; |
|
39 val id = "#Length_[A = a * b, a // #2 = #2]" : string |
|
40 val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
|
41 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
|
42 --------------------------------------------- |
|
43 > val thmid = "#Length_"; val op_ = "Length"; |
|
44 > val s = |
|
45 "if #1 < Length [A = a * b, a // #2 = #2] \ |
|
46 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\ |
|
47 \else hd [A = a * b, a // #2 = #2]"; |
|
48 |
|
49 > (cterm_of thy) t'; |
|
50 > val t = (term_of o the o (parse thy)) s; |
|
51 > val eval_fn = the (assoc (!eval_list, op_)); |
|
52 > val (SOME(_,t')) = get_pair op_ eval_fn t; |
|
53 val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
|
54 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
|
55 |
|
56 > val ct = (the o (parse thy)) s; |
|
57 > val (SOME(_,thm)) = get_calculation thy (op_, eval_fn) ct; |
|
58 val thm = "Length [A = a * b, a // #2 = #2] = #2" [[ Free ( #2, real) !!!]] |
|
59 > rewrite_ thy tless_true e_rls false thm ct; |
|
60 ("if #1 < #2 |
|
61 then make_fun (R, [make, function], no_met) |
|
62 A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]", |
|
63 []) : (cterm * cterm list) option |
|
64 > val ct = (the o (parse thy)) s; |
|
65 > rewrite_set_ thy e_rls false eval_script ct; |
|
66 ("if #1 < #2 |
|
67 then make_fun (R, [make, function], no_met) |
|
68 A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]", |
|
69 []) : (cterm * cterm list) option |
|
70 *) |
|
71 |
|
72 fun eval_Nth (thmid:string) (op_:string) (t as |
|
73 (Const (op0,t0) $ t1 $ t2 )) thy = |
|
74 (writeln"@@@ eval_Nth"; |
|
75 if is_num t1 andalso is_list t2 |
|
76 then |
|
77 let |
|
78 val t' = (nth (num_of_term t1) (isalist2list t2)) |
|
79 handle _ => raise GO_ON; |
|
80 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^ |
|
81 "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^ |
|
82 " = "^(Syntax.string_of_term (thy2ctxt thy) t'); |
|
83 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
|
84 else raise GO_ON |
|
85 ) |
|
86 | eval_Nth _ _ _ _ = raise GO_ON; |
|
87 (* |
|
88 > val thmid = "#Nth_"; val op_ = "Nth"; |
|
89 > val s = "Nth #2 [A = a * b, a // #2 = #2]"; |
|
90 > val t = (term_of o the o (parse thy)) s; |
|
91 > eval_Nth thmid op_ t; |
|
92 |
|
93 > val eval_fn = the (assoc (!eval_list, op_)); |
|
94 > val (SOME(id,t')) = get_pair op_ eval_fn t; |
|
95 > (cterm_of thy) t'; |
|
96 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)" |
|
97 *) |
|
98 |
|
99 |
|
100 (*17.6.00: calc_list instead eval_list*) |
|
101 eval_list:= overwritel (! eval_list, |
|
102 [("Var",eval_var "#Var_"), |
|
103 ("Length",eval_Length "#Length_"), |
|
104 ("Nth",eval_Nth "#Nth_") |
|
105 ]); |
|
106 (*17.6.00: association list for calculate_, calculate*) |
|
107 calc_list:= overwritel (! calc_list, |
|
108 [ |
|
109 ("Var" ,("Var",eval_var "#Var_")), |
|
110 ("Length",("Length",eval_Length "#Length_")), |
|
111 ("Nth" ,("Nth",eval_Nth "#Nth_")) |
|
112 ]); |
|
113 |