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