equal
deleted
inserted
replaced
98 handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite") |
98 handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite") |
99 | Rule.Rls_ rls => |
99 | Rule.Rls_ rls => |
100 (case Rewrite.rewrite_set_ ctxt true rls t of |
100 (case Rewrite.rewrite_set_ ctxt true rls t of |
101 NONE => rew_once lim rts t apno rs' |
101 NONE => rew_once lim rts t apno rs' |
102 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') |
102 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') |
103 | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string_PIDE ctxt rule)) |
103 | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string ctxt rule)) |
104 | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []" |
104 | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []" |
105 in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end |
105 in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end |
106 |
106 |
107 |
107 |
108 (** concatenate several steps in revers order **) |
108 (** concatenate several steps in revers order **) |