84 | Pstate of pstate (*for script interpreter*) |
84 | Pstate of pstate (*for script interpreter*) |
85 | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*) |
85 | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*) |
86 val empty = Pstate e_pstate; |
86 val empty = Pstate e_pstate; |
87 |
87 |
88 fun rta2str ctxt (r, (t, a)) = |
88 fun rta2str ctxt (r, (t, a)) = |
89 "\n(" ^ Rule.to_string_PIDE ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^ |
89 "\n(" ^ Rule.to_string ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^ |
90 UnparseC.terms_in_ctxt ctxt a ^ "))"; |
90 UnparseC.terms_in_ctxt ctxt a ^ "))"; |
91 fun string_of _ Uistate = "Uistate" |
91 fun string_of _ Uistate = "Uistate" |
92 | string_of _ (Pstate pst) = |
92 | string_of _ (Pstate pst) = |
93 "Pstate " ^ pstate2str pst |
93 "Pstate " ^ pstate2str pst |
94 | string_of ctxt (RrlsState (t, t1, rss, rtas)) = |
94 | string_of ctxt (RrlsState (t, t1, rss, rtas)) = |
95 "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^ |
95 "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^ |
96 (strs2str o (map (strs2str o (map (Rule.to_string_PIDE ctxt))))) rss ^ ", " ^ |
96 (strs2str o (map (strs2str o (map (Rule.to_string ctxt))))) rss ^ ", " ^ |
97 (strs2str o (map (rta2str ctxt))) rtas ^ ")"; |
97 (strs2str o (map (rta2str ctxt))) rtas ^ ")"; |
98 fun string_of' Uistate = "Uistate" |
98 fun string_of' Uistate = "Uistate" |
99 | string_of' (Pstate pst) = |
99 | string_of' (Pstate pst) = |
100 "Pstate " ^ pstate2str' pst |
100 "Pstate " ^ pstate2str' pst |
101 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState" |
101 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState" |