2 +++ outcommented tests *)
5 fun eval_var (thmid:string) (op_:string)
6 (t as (Const(op0,t0) $ arg)) thy =
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;
13 > val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";
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;
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
27 fun eval_Length (thmid:string) (op_:string)
28 (t as (Const(op0,t0) $ arg)) thy =
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;
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";
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]";
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
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;
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;
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
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
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
86 | eval_Nth _ _ _ _ = raise GO_ON;
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;
93 > val eval_fn = the (assoc (!eval_list, op_));
94 > val (SOME(id,t')) = get_pair op_ eval_fn t;
96 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
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_")
106 (*17.6.00: association list for calculate_, calculate*)
107 calc_list:= overwritel (! calc_list,
109 ("Var" ,("Var",eval_var "#Var_")),
110 ("Length",("Length",eval_Length "#Length_")),
111 ("Nth" ,("Nth",eval_Nth "#Nth_"))