|
1 (* = Atools.ML 9.3.01 |
|
2 +++ outcommented tests *) |
|
3 |
|
4 (** eval_ |
|
5 precondition: head_of t is the constant to be evaluated |
|
6 (had been filtered by get_pair before call) **) |
|
7 (* eval_const was the reason for introducing exception GO_ON: |
|
8 patterns on arg incomparable to other unary functions. |
|
9 |
|
10 ugly consequence: |
|
11 eval_... need to have the same result type as get_pair |
|
12 *) |
|
13 fun eval_const (thmid:string) _ (t as (Const(op0,t0) $ arg)) (thy:theory) = |
|
14 (case arg of |
|
15 Const(n1,_) => |
|
16 Some (mk_thmid thmid op0 n1 "", |
|
17 Trueprop $ (mk_equality (t, false_as_term))) |
|
18 | Free(n1,_) => |
|
19 if (hd o explode) n1 = "#" |
|
20 then Some (mk_thmid thmid op0 n1 "", |
|
21 Trueprop $ (mk_equality (t, true_as_term))) |
|
22 else Some (mk_thmid thmid op0 n1 "", |
|
23 Trueprop $ (mk_equality (t, false_as_term))) |
|
24 | _ => raise GO_ON) |
|
25 | eval_const _ _ _ _ = raise GO_ON; |
|
26 (* necessary for recursion over (t1$t2) in get_pair *) |
|
27 (* use"Isa99/knowl-base/RatArith.ML"; |
|
28 |
|
29 > val ct = (the o (parse thy)) "#3 is_const"; |
|
30 > calc_thm thy "is'_const" ct; |
|
31 val it = Some ("is_const_3_","(is_const 3 ) = True [(is_const 3 ) = True]") |
|
32 *) |
|
33 |
|
34 (* fn : string -> string -> term -> string * term |
|
35 TODO clumsy: 2-fold pattern matching |
|
36 3 patterns for binops used for equ, too |
|
37 although only the 1st pattern matches ... *) |
|
38 fun eval_binop (thmid:string) (op_:string) (t as |
|
39 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
|
40 (* binary . n1.n2 *) |
|
41 let |
|
42 val n1' = int_of_str n1; |
|
43 val n2' = int_of_str n2; |
|
44 val (T1,T2,Trange) = dest_binop_typ t0; |
|
45 val res = calc (strip_thy op0) (n1',n2'); |
|
46 val rhs = term_of_num Trange res; |
|
47 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
48 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
49 | eval_binop (thmid:string) (op_:string) (t as ( Const(op0,t0) $ |
|
50 ( Const(op0',t0') $ v $ Free(n1,t1)) $ |
|
51 Free(n2,t2))) thy = |
|
52 let (* binary . (v.n1).n2 *) |
|
53 val n1' = int_of_str n1; |
|
54 val n2' = int_of_str n2; |
|
55 val (T1,T2,Trange) = dest_binop_typ t0; |
|
56 val res = calc (strip_thy op0) (n1',n2'); |
|
57 val rhs = var_op_num v op_ t0 T1 res; |
|
58 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
59 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
60 | eval_binop (thmid:string) (op_:string) (t as |
|
61 ( Const(op0,t0) $ Free(n1,t1) $ |
|
62 ( Const(op0',t0') $ Free(n2,t2) $ v))) thy = |
|
63 let (* binary . n1.(n2.v) *) |
|
64 val n1' = int_of_str n1; |
|
65 val n2' = int_of_str n2; |
|
66 val (T1,T2,Trange) = dest_binop_typ t0; |
|
67 val res = calc (strip_thy op0) (n1',n2'); |
|
68 val rhs = num_op_var v op_ t0 T1 res; |
|
69 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
70 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
71 | eval_binop _ _ _ _ = raise GO_ON; |
|
72 |
|
73 fun eval_equ (thmid:string) (op_:string) (t as |
|
74 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
|
75 if calc_equ (strip_thy op0) ((int_of_str n1),(int_of_str n2)) |
|
76 then Some (mk_thmid thmid op0 n1 n2, |
|
77 Trueprop $ (mk_equality (t, true_as_term))) |
|
78 else Some (mk_thmid thmid op0 n1 n2, |
|
79 Trueprop $ (mk_equality (t, false_as_term))) |
|
80 | eval_equ _ _ _ _ = raise GO_ON; |
|
81 |
|
82 |
|
83 fun eval_ident (thmid:string) (op_:string) (t as |
|
84 (Const (op0,t0) $ t1 $ t2 )) thy = |
|
85 if t1 = t2 |
|
86 then Some (mk_thmid thmid op0 |
|
87 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
88 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
89 Trueprop $ (mk_equality (t, true_as_term))) |
|
90 else Some (mk_thmid thmid op0 |
|
91 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
92 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
93 Trueprop $ (mk_equality (t, false_as_term))) |
|
94 | eval_ident _ _ _ _ = raise GO_ON; |
|
95 (* |
|
96 (string_of_cterm o (cterm_of (sign_of thy))); |
|
97 *) |
|
98 |
|
99 val simprls = |
|
100 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
|
101 rules = [Calc ("ident",eval_ident "#ident_"), |
|
102 Calc ("Var",eval_var "#Var_"), |
|
103 Calc ("Length",eval_Length "#Length_"), |
|
104 Calc ("Nth",eval_Nth "#Nth_"), |
|
105 Calc ("op <",eval_equ "#less_"), |
|
106 Calc ("op <=",eval_equ "#less_equal_"), |
|
107 Calc ("ident",eval_ident "#ident_"), |
|
108 |
|
109 Thm ("if_True",num_str if_True), |
|
110 Thm ("if_False",num_str if_False) |
|
111 ], |
|
112 scr = Script ((term_of o the o (parse thy)) |
|
113 "empty_script") |
|
114 }:rls; |
|
115 |