equal
deleted
inserted
replaced
45 val deriv2str = trtas2str |
45 val deriv2str = trtas2str |
46 |
46 |
47 |
47 |
48 (** make one triple towards the goal term **) |
48 (** make one triple towards the goal term **) |
49 |
49 |
50 fun msg_1 rts = |
50 fun msg_1 ctxt rts = |
51 (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n"); |
51 (tracing ("do_one exceeds " ^ int2str (Config.get ctxt rewrite_limit) ^ "with derivation =\n"); |
52 tracing (deriv2str rts)); |
52 tracing (deriv2str rts)); |
53 fun msg_2 ctxt thmid = |
53 fun msg_2 ctxt thmid = |
54 if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\""); |
54 if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\""); |
55 fun msg_3 ctxt t' = |
55 fun msg_3 ctxt t' = |
56 if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else (); |
56 if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else (); |
71 (case goal of |
71 (case goal of |
72 NONE => rew_or_calc lim rts t apno rs' |
72 NONE => rew_or_calc lim rts t apno rs' |
73 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs') |
73 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs') |
74 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) = |
74 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) = |
75 if lim < 0 |
75 if lim < 0 |
76 then (msg_1 rts; rts) |
76 then (msg_1 ctxt rts; rts) |
77 else |
77 else |
78 (case r of |
78 (case r of |
79 Rule.Thm (thmid, tm) => |
79 Rule.Thm (thmid, tm) => |
80 (msg_2 ctxt thmid; |
80 (msg_2 ctxt thmid; |
81 case Rewrite.rewrite_ ctxt ro erls true tm t of |
81 case Rewrite.rewrite_ ctxt ro erls true tm t of |
99 (case Rewrite.rewrite_set_ ctxt true rls t of |
99 (case Rewrite.rewrite_set_ ctxt true rls t of |
100 NONE => rew_once lim rts t apno rs' |
100 NONE => rew_once lim rts t apno rs' |
101 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') |
101 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') |
102 | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule)) |
102 | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule)) |
103 | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []" |
103 | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []" |
104 in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end |
104 in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end |
105 |
105 |
106 |
106 |
107 (** concatenate several steps in revers order **) |
107 (** concatenate several steps in revers order **) |
108 |
108 |
109 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a)); |
109 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a)); |