72 Uistate (*undefined in modspec, in '_deriv'ation*) |
72 Uistate (*undefined in modspec, in '_deriv'ation*) |
73 | Pstate of pstate (*for script interpreter*) |
73 | Pstate of pstate (*for script interpreter*) |
74 | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*) |
74 | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*) |
75 val empty = Pstate e_pstate; |
75 val empty = Pstate e_pstate; |
76 |
76 |
77 fun rta2str (r, (t, a)) = "\n(" ^ Rule_Set.rule2str r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"; |
77 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"; |
78 fun string_of Uistate = "Uistate" |
78 fun string_of Uistate = "Uistate" |
79 | string_of (Pstate pst) = |
79 | string_of (Pstate pst) = |
80 "Pstate " ^ pstate2str pst |
80 "Pstate " ^ pstate2str pst |
81 | string_of (RrlsState (t, t1, rss, rtas)) = |
81 | string_of (RrlsState (t, t1, rss, rtas)) = |
82 "RrlsState (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.term2str t1 ^ ", " ^ |
82 "RrlsState (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.term2str t1 ^ ", " ^ |
83 (strs2str o (map (strs2str o (map Rule_Set.rule2str)))) rss ^ ", " ^ |
83 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^ |
84 (strs2str o (map rta2str)) rtas ^ ")"; |
84 (strs2str o (map rta2str)) rtas ^ ")"; |
85 fun string_of' Uistate = "Uistate" |
85 fun string_of' Uistate = "Uistate" |
86 | string_of' (Pstate pst) = |
86 | string_of' (Pstate pst) = |
87 "Pstate " ^ pstate2str' pst |
87 "Pstate " ^ pstate2str' pst |
88 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState" |
88 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState" |