60 result: |
60 result: |
61 (string * term) option: found by the eval_* -function of type |
61 (string * term) option: found by the eval_* -function of type |
62 fn : string -> string -> term -> theory -> (string * term) option |
62 fn : string -> string -> term -> theory -> (string * term) option |
63 ^^^^^^... the selecting operator op_ (variable for eval_binop) |
63 ^^^^^^... the selecting operator op_ (variable for eval_binop) |
64 *) |
64 *) |
65 fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option) |
65 fun get_pair thy op_ (ef: eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *) |
66 (t as (Const(op0,t0) $ arg)) = (* unary fns *) |
|
67 (* val (thy, op_, (ef), (t as (Const(op0,t0) $ arg))) = |
|
68 (thy, op_, eval_fn, ct); |
|
69 *) |
|
70 if op_ = op0 then |
66 if op_ = op0 then |
71 let val popt = ef op_ t thy |
67 let val popt = ef op_ t thy |
72 in case popt of |
68 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end |
73 SOME _ => popt |
|
74 | NONE => get_pair thy op_ ef arg end |
|
75 else get_pair thy op_ ef arg |
69 else get_pair thy op_ ef arg |
76 |
70 | get_pair thy "Atools.ident" ef (t as (Const ("Atools.ident", _) $ _ $ _ )) = |
77 | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) = |
71 ef "Atools.ident" t thy (* not nested *) |
78 (* val (thy, "Atools.ident", ef, t as (Const(op0,_) $ t1 $ t2)) = |
72 | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *) |
79 (thy, op_, eval_fn, ct); |
73 ((* tracing ("1.. get_pair: binop = "^op_); *) |
80 *) |
74 if op_ = op0 then |
81 ef "Atools.ident" t thy (* not nested *) |
75 let val popt = ef op_ t thy |
82 |
76 (* val _ = tracing ("2.. get_pair: " ^ term2str t ^ " -> " ^ popt2str popt) *) |
83 | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) = (* binary funs*) |
77 in case popt of SOME _ => popt | NONE => |
84 (* val (thy, op_, ef, (t as (Const(op0,_) $ t1 $ t2))) = |
78 let val popt = get_pair thy op_ ef t1 |
85 (thy, op_, eval_fn, ct); |
79 (* val _ = tracing ("3.. get_pair: " ^ term2str t1 ^ " -> "^popt2str popt) *) |
86 *) |
80 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end |
87 ((*tracing("1.. get_pair: binop = "^op_);*) |
81 end |
88 if op_ = op0 then |
82 else (* search subterms *) |
89 let val popt = ef op_ t thy |
83 let val popt = get_pair thy op_ ef t1 |
90 (*val _ = tracing("2.. get_pair: "^term2str t^" -> "^popt2str popt)*) |
84 (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*) |
91 in case popt of |
85 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end) |
92 SOME (id,_) => popt |
86 | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *) |
93 | NONE => |
87 ((*tracing ("### get_pair 4a: t= " ^ term2str t); |
94 let val popt = get_pair thy op_ ef t1 |
88 tracing ("### get_pair 4a: op_= " ^ op_); |
95 (*val _ = tracing("3.. get_pair: "^term2str t1^ |
89 tracing ("### get_pair 4a: op0= " ^ op0); *) |
96 " -> "^popt2str popt)*) |
90 if op_ = op0 then |
97 in case popt of |
91 case ef op_ t thy of st as SOME _ => st | NONE => |
98 SOME (id,_) => popt |
92 (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3) |
99 | NONE => get_pair thy op_ ef t2 |
93 else |
100 end |
94 (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE => |
101 end |
95 (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3))) |
102 else (*search subterms*) |
96 | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body |
103 let val popt = get_pair thy op_ ef t1 |
97 | get_pair thy op_ ef (t1 $ t2) = |
104 (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*) |
98 let (* val _= tracing ("5.. get_pair t1 $ t2: " ^ term2str t1 ^ " $ " ^ term2str t2) *) |
105 in case popt of |
99 val popt = get_pair thy op_ ef t1 |
106 SOME (id,_) => popt |
100 in case popt of SOME _ => popt |
107 | NONE => get_pair thy op_ ef t2 |
101 | NONE => ((* tracing "### get_pair: t1 $ t2 -> NONE"; *) get_pair thy op_ ef t2) |
108 end) |
102 end |
109 | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*) |
103 | get_pair _ _ _ _ = NONE |
110 ((*tracing("### get_pair 4a: t= "^term2str t); |
104 |
111 tracing("### get_pair 4a: op_= "^op_); |
|
112 tracing("### get_pair 4a: op0= "^op0);*) |
|
113 if op_ = op0 then |
|
114 case ef op_ t thy of |
|
115 SOME tt => SOME tt |
|
116 | NONE => (case get_pair thy op_ ef t2 of |
|
117 SOME tt => SOME tt |
|
118 | NONE => get_pair thy op_ ef t3) |
|
119 else (case get_pair thy op_ ef t1 of |
|
120 SOME tt => SOME tt |
|
121 | NONE => (case get_pair thy op_ ef t2 of |
|
122 SOME tt => SOME tt |
|
123 | NONE => get_pair thy op_ ef t3))) |
|
124 | get_pair thy op_ ef (Const _) = NONE |
|
125 | get_pair thy op_ ef (Free _) = NONE |
|
126 | get_pair thy op_ ef (Var _) = NONE |
|
127 | get_pair thy op_ ef (Bound _) = NONE |
|
128 | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body |
|
129 | get_pair thy op_ ef (t1$t2) = |
|
130 let(*val _= tracing("5.. get_pair t1 $ t2: "^term2str t1^" |
|
131 $ "^term2str t2)*) |
|
132 val popt = get_pair thy op_ ef t1 |
|
133 in case popt of |
|
134 SOME _ => popt |
|
135 | NONE => ((*tracing"### get_pair: t1 $ t2 -> NONE";*) |
|
136 get_pair thy op_ ef t2) |
|
137 end; |
|
138 (* |
105 (* |
139 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
106 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
140 > val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus")); |
107 > val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus")); |
141 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; |
108 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; |
142 > term2str t'; |
109 > term2str t'; |
219 parse thy "" |
186 parse thy "" |
220 *) |
187 *) |
221 (*.get a thm from an op_ somewhere in the term; |
188 (*.get a thm from an op_ somewhere in the term; |
222 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*) |
189 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*) |
223 fun get_calculation_ thy (op_, eval_fn) ct = |
190 fun get_calculation_ thy (op_, eval_fn) ct = |
224 (* val (thy, (op_, eval_fn), ct) = |
|
225 (thy, (the (assoc(!calclist',"order_system"))), t); |
|
226 *) |
|
227 case get_pair thy op_ eval_fn ct of |
191 case get_pair thy op_ eval_fn ct of |
228 NONE => ((*tracing("@@@ get_calculation: NONE, op_="^op_); |
192 NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_); |
229 tracing("@@@ get_calculation: ct= ");atomty ct;*) |
193 tracing ("@@@ get_calculation: ct= "); atomty ct; *) |
230 NONE) |
194 NONE) |
231 | SOME (thmid,t) => |
195 | SOME (thmid, t) => SOME (thmid, (make_thm o (cterm_of thy)) t); |
232 SOME (thmid, (make_thm o (cterm_of thy)) t); |
|
233 (* |
196 (* |
234 > val ct = (the o (parse thy)) "#9 is_const"; |
197 > val ct = (the o (parse thy)) "#9 is_const"; |
235 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct; |
198 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct; |
236 val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]") |
199 val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]") |
237 |
200 |