equal
deleted
inserted
replaced
128 else if t = @{term False} then ([], false) |
128 else if t = @{term False} then ([], false) |
129 (*asm false .. thm not applied ^^^; continue until False vvv*) |
129 (*asm false .. thm not applied ^^^; continue until False vvv*) |
130 else chk (indets @ [t] @ a') asms); |
130 else chk (indets @ [t] @ a') asms); |
131 in chk [] asms end |
131 in chk [] asms end |
132 and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *) |
132 and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *) |
133 error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'") |
133 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'") |
134 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *) |
134 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *) |
135 let |
135 let |
136 val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t) |
136 val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t) |
137 val (t', asm, rew) = app_rev thy (i + 1) rrls t |
137 val (t', asm, rew) = app_rev thy (i + 1) rrls t |
138 in if rew then SOME (t', distinct asm) else NONE end |
138 in if rew then SOME (t', distinct asm) else NONE end |
163 NONE => rew_once ruls asm ct apno thms |
163 NONE => rew_once ruls asm ct apno thms |
164 | SOME (_, thm') => |
164 | SOME (_, thm') => |
165 let |
165 let |
166 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
166 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
167 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
167 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
168 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ |
168 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ |
169 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") |
169 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") |
170 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt)) |
170 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt)) |
171 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end |
171 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end |
172 end |
172 end |
173 | Rule.Cal1 (cc as (op_, _)) => |
173 | Rule.Cal1 (cc as (op_, _)) => |
177 NONE => (ct, asm) |
177 NONE => (ct, asm) |
178 | SOME (_, thm') => |
178 | SOME (_, thm') => |
179 let |
179 let |
180 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
180 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
181 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
181 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
182 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ |
182 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ |
183 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") |
183 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") |
184 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt)) |
184 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt)) |
185 in the pairopt end |
185 in the pairopt end |
186 end |
186 end |
187 | Rule.Rls_ rls' => |
187 | Rule.Rls_ rls' => |
278 | SOME (thmID, thm) => |
278 | SOME (thmID, thm) => |
279 (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of |
279 (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of |
280 SOME (rew, _) => rew |
280 SOME (rew, _) => rew |
281 | NONE => raise ERROR "" |
281 | NONE => raise ERROR "" |
282 in SOME (rew, (thmID, thm)) end) |
282 in SOME (rew, (thmID, thm)) end) |
283 handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite") |
283 handle _ (*TODO Pattern.MATCH ?del?*)=> raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite") |
284 end; |
284 end; |
285 |
285 |
286 fun eval_prog_expr thy srls t = |
286 fun eval_prog_expr thy srls t = |
287 let val rew = rewrite_set_ thy false srls t; |
287 let val rew = rewrite_set_ thy false srls t; |
288 in case rew of SOME (res,_) => res | NONE => t end; |
288 in case rew of SOME (res,_) => res | NONE => t end; |