45 | asap2str AssGen = "AssGen" |
45 | asap2str AssGen = "AssGen" |
46 |
46 |
47 type pstate = |
47 type pstate = |
48 {env: Env.T, (* environment for variables in a program *) |
48 {env: Env.T, (* environment for variables in a program *) |
49 path: TermC.path, (* to the current location in a program *) |
49 path: TermC.path, (* to the current location in a program *) |
50 eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *) |
50 eval: Rule_Set.rls, (* rule-set for evaluating a Prog_Expr *) |
51 form_arg: term option,(* argument of a curried function *) |
51 form_arg: term option,(* argument of a curried function *) |
52 act_arg: term, (* value for the curried argument *) |
52 act_arg: term, (* value for the curried argument *) |
53 or: asap, (* flag for scanning tactical "Or" !shall be dropped *) |
53 or: asap, (* flag for scanning tactical "Or" !shall be dropped *) |
54 found_accept: bool, (* flag set after execution of a tactic !shall be dropped *) |
54 found_accept: bool, (* flag set after execution of a tactic !shall be dropped *) |
55 assoc: bool} (* is the tactic associated to input ?cont.search Unsafe_Step \<rightarrow> Safe_Step*) |
55 assoc: bool} (* is the tactic associated to input ?cont.search Unsafe_Step \<rightarrow> Safe_Step*) |
56 val e_pstate = |
56 val e_pstate = |
57 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term, |
57 {env = [], path = [], eval = Rule_Set.e_rls, form_arg = NONE, act_arg = Rule.e_term, |
58 or = ORundef, found_accept = false, assoc = false} |
58 or = ORundef, found_accept = false, assoc = false} |
59 fun topt2str NONE = "NONE" |
59 fun topt2str NONE = "NONE" |
60 | topt2str (SOME t) = "SOME " ^ Rule.term2str t; |
60 | topt2str (SOME t) = "SOME " ^ Rule.term2str t; |
61 fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *) |
61 fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *) |
62 "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule.id_rls eval ^ ", " ^ |
62 "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id_rls eval ^ ", " ^ |
63 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
63 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
64 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"; |
64 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"; |
65 fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *) |
65 fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *) |
66 "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule.id_rls eval ^ ", " ^ |
66 "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id_rls eval ^ ", " ^ |
67 topt2str form_arg ^ ", " ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
67 topt2str form_arg ^ ", " ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
68 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"; |
68 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"; |
69 |
69 |
70 (* for handling type T see fun resume_prog, +? *) |
70 (* for handling type T see fun resume_prog, +? *) |
71 datatype T = (*interpreter state*) |
71 datatype T = (*interpreter state*) |
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.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.rule2str r ^ ", (" ^ Rule.term2str t ^ ", " ^ Rule.terms2str a ^ "))"; |
77 fun rta2str (r, (t, a)) = "\n(" ^ Rule_Set.rule2str r ^ ", (" ^ Rule.term2str t ^ ", " ^ Rule.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 (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^ |
82 "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^ |
83 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^ |
83 (strs2str o (map (strs2str o (map Rule_Set.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" |