14 val pstate2str: pstate -> string |
14 val pstate2str: pstate -> string |
15 val pstate2str': pstate -> string |
15 val pstate2str': pstate -> string |
16 |
16 |
17 datatype T = RrlsState of Rule_Set.rrlsstate | Pstate of pstate | Uistate |
17 datatype T = RrlsState of Rule_Set.rrlsstate | Pstate of pstate | Uistate |
18 val empty: T |
18 val empty: T |
19 val string_of: T -> string |
19 val string_of: Proof.context -> T -> string |
20 val string_of': T -> string |
20 val string_of': T -> string |
21 val istates2str: T option * T option -> string |
21 val istates2str: Proof.context -> T option * T option -> string |
22 |
22 |
23 val set_eval: Rule_Set.T -> pstate -> pstate |
23 val set_eval: Rule_Set.T -> pstate -> pstate |
24 val set_act: term -> pstate -> pstate |
24 val set_act: term -> pstate -> pstate |
25 val set_env_true: Env.T -> pstate -> pstate |
25 val set_env_true: Env.T -> pstate -> pstate |
26 |
26 |
83 Uistate (*undefined in modspec, in '_deriv'ation*) |
83 Uistate (*undefined in modspec, in '_deriv'ation*) |
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 (r, (t, a)) = "\n(" ^ Rule.to_string r ^ ", (" ^ UnparseC.term t ^ ", " ^ UnparseC.terms a ^ "))"; |
88 fun rta2str ctxt (r, (t, a)) = |
89 fun string_of Uistate = "Uistate" |
89 "\n(" ^ Rule.to_string_PIDE ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^ |
90 | string_of (Pstate pst) = |
90 UnparseC.terms_in_ctxt ctxt a ^ "))"; |
91 "Pstate " ^ pstate2str pst |
91 fun string_of _ Uistate = "Uistate" |
92 | string_of (RrlsState (t, t1, rss, rtas)) = |
92 | string_of _ (Pstate pst) = |
93 "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term t1 ^ ", " ^ |
93 "Pstate " ^ pstate2str pst |
94 (strs2str o (map (strs2str o (map Rule.to_string)))) rss ^ ", " ^ |
94 | string_of ctxt (RrlsState (t, t1, rss, rtas)) = |
95 (strs2str o (map rta2str)) rtas ^ ")"; |
95 "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^ |
|
96 (strs2str o (map (strs2str o (map (Rule.to_string_PIDE ctxt))))) rss ^ ", " ^ |
|
97 (strs2str o (map (rta2str ctxt))) rtas ^ ")"; |
96 fun string_of' Uistate = "Uistate" |
98 fun string_of' Uistate = "Uistate" |
97 | string_of' (Pstate pst) = |
99 | string_of' (Pstate pst) = |
98 "Pstate " ^ pstate2str' pst |
100 "Pstate " ^ pstate2str' pst |
99 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState" |
101 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState" |
100 fun istates2str (NONE, NONE) = "(#NONE, #NONE)" |
102 fun istates2str _ (NONE, NONE) = "(#NONE, #NONE)" |
101 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ist ^ ")" |
103 | istates2str ctxt (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ctxt ist ^ ")" |
102 | istates2str (SOME ist, NONE) = "(#SOME " ^ string_of ist ^ ",\n #NONE)" |
104 | istates2str ctxt (SOME ist, NONE) = "(#SOME " ^ string_of ctxt ist ^ ",\n #NONE)" |
103 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ string_of i1 ^ ",\n #SOME " ^ string_of i2 ^ ")"; |
105 | istates2str ctxt (SOME i1, SOME i2) = |
|
106 "(#SOME " ^ string_of ctxt i1 ^ ",\n #SOME " ^ string_of ctxt i2 ^ ")"; |
104 |
107 |
105 |
108 |
106 fun set_eval e {env, path, form_arg, act_arg, or, found_accept, assoc, ...} = |
109 fun set_eval e {env, path, form_arg, act_arg, or, found_accept, assoc, ...} = |
107 {env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg, |
110 {env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg, |
108 or = or, found_accept = found_accept, assoc = assoc} |
111 or = or, found_accept = found_accept, assoc = assoc} |