1 (* Title: interpreter-state for Lucas-Interpretation
2 Author: Walther Neuper 190724
3 (c) due to copyright terms
5 signature INTERPRETER_STATE =
8 datatype asap = datatype Istate_Def.asap
9 datatype appy_ = datatype Istate_Def.appy_
10 type pstate = Istate_Def.pstate
11 val e_scrstate: pstate
12 val scrstate2str: pstate -> string
14 datatype T = datatype Istate_Def.T
16 val istate2str: T -> string
17 val istates2str: T option * T option -> string
19 val the_pstate: T -> pstate
21 val get_act_env: pstate -> (term * Env.T)
22 val get_subst: pstate -> (Env.T * (term option * term))
24 val trans_scan_down2: pstate -> pstate
25 val trans_scan_up2: pstate -> pstate
26 val trans_ass: pstate -> pstate -> pstate
27 val trans_env_act: pstate -> pstate -> pstate
29 val path_down: Celem.path -> pstate -> pstate
30 val path_down_form: (Celem.path * term) -> pstate -> pstate
31 val path_up': Celem.path -> Celem.path
32 val path_up: pstate -> pstate
33 val path_up_down: Celem.path -> pstate -> pstate
35 val set_form: term -> pstate -> pstate
36 val set_path: Celem.path -> pstate -> pstate
37 val set_eval: Rule.rls -> pstate -> pstate
38 val set_act: term -> pstate -> pstate
39 val set_or: asap -> pstate -> pstate
40 val set_appy: appy_ -> pstate -> pstate
42 val set_subst: Env.T -> (term * term) -> pstate -> pstate
43 val set_subst': (term * term) -> pstate -> pstate
44 val set_subst_true: (term option * term) -> pstate -> pstate
45 val set_subst_false: (term option * term) -> pstate -> pstate
46 val set_subst_reset: (term option * term) -> pstate -> pstate
48 val set_env: Env.T -> pstate -> pstate
49 val set_env_true: Env.T -> pstate -> pstate
50 val set_form_env: (term * Env.T) -> pstate -> pstate
51 val set_act_env: (term * Env.T) -> pstate -> pstate
52 val upd_env: term -> pstate -> pstate
53 val upd_env': Env.T * (term * term) -> pstate -> pstate
54 val upd_env'': (term * term) -> pstate -> pstate
59 structure Istate(**): INTERPRETER_STATE(**) =
65 datatype asap = datatype Istate_Def.asap
66 (*this constructions doesnt allow arbitrary nesting of Or !!! *)
67 fun asap2str ORundef = "ORundef"
68 | asap2str AssOnly = "AssOnly"
69 | asap2str AssGen = "AssGen"
71 datatype appy_ = datatype Istate_Def.appy_
72 fun appy_2str AppUndef_ = "AppUndef_"
73 | appy_2str Napp_ = "Napp_"
74 | appy_2str Skip_ = "Skip_"
76 type pstate = Istate_Def.pstate
78 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,
79 or = ORundef, finish = AppUndef_, assoc = false}
80 fun topt2str NONE = "NONE"
81 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
82 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
83 "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
84 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
85 appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
87 (* for handling type T see fun from_pblobj_or_detail', +? *)
88 datatype T = datatype Istate_Def.T
89 val e_istate = Pstate e_scrstate;
90 fun the_pstate (Pstate pst) = pst
91 | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
93 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
94 fun istate2str Uistate = "Uistate"
95 | istate2str (Pstate pst) =
96 "Pstate " ^ scrstate2str pst
97 | istate2str (RrlsState (t, t1, rss, rtas)) =
98 "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
99 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
100 (strs2str o (map rta2str)) rtas ^ ")";
101 fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
102 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
103 | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
104 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
106 fun get_act_env {env, act_arg, ...} = (act_arg, env)
107 fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))
109 fun trans_scan_down2 {env, eval, act_arg, or, ...} =
110 {env = env, path = [R], eval = eval, form_arg = NONE, act_arg = act_arg,
111 or = or, finish = AppUndef_, assoc = false}
112 fun trans_scan_up2 {env, path, eval, form_arg, act_arg, or, ...} =
113 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
114 or = or, finish = AppUndef_, assoc = false}
115 fun trans_ass {assoc, ...} {env, path, eval, form_arg, act_arg, or, finish, ...} =
116 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
117 or = or, finish = finish, assoc = assoc}
118 fun trans_env_act {env, act_arg, ...} {path, eval, form_arg, or, finish, assoc, ...} =
119 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
120 or = or, finish = finish, assoc = assoc}
123 fun path_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
124 {env = env, path = path @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
125 or = or, finish = finish, assoc = assoc}
126 fun path_down_form (p, fa) {env, path, eval, act_arg, or, finish, assoc, ...} =
127 {env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,
128 or = or, finish = finish, assoc = assoc}
129 fun path_up' [] = raise ERROR "path_up' []"
130 | path_up' path = drop_last path
131 fun path_up {env, path, eval, form_arg, act_arg, or, finish, assoc} =
132 {env = env, path = path_up' path, eval = eval, form_arg = form_arg, act_arg = act_arg,
133 or = or, finish = finish, assoc = assoc}
134 fun path_up_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
135 {env = env, path = (path_up' path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
136 or = or, finish = finish, assoc = assoc}
138 fun set_form f {env, path, eval, act_arg, or, finish, assoc, ...} =
139 {env = env, path = path, eval = eval, form_arg = SOME f, act_arg = act_arg,
140 or = or, finish = finish, assoc = assoc}
141 fun set_path p {env, eval, form_arg, act_arg, or, finish, assoc, ...} =
142 {env = env, path = p, eval = eval, form_arg = form_arg, act_arg = act_arg,
143 or = or, finish = finish, assoc = assoc}
144 val set_eval = Istate_Def.set_eval
145 val set_act = Istate_Def.set_act
146 fun set_or or {env, path, eval, form_arg, act_arg, finish, assoc, ...} =
147 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
148 or = or, finish = finish, assoc = assoc}
149 fun set_appy fin {env, path, eval, form_arg, act_arg, or, assoc, ...} =
150 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
151 or = or, finish = fin, assoc = assoc}
153 fun set_subst env (form_arg, act_arg) {path, eval, or, finish, assoc, ...} =
154 {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
155 or = or, finish = finish, assoc = assoc}
156 fun set_subst' (form_arg, act_arg) {env, path, eval, or, finish, assoc, ...} =
157 {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
158 or = or, finish = finish, assoc = assoc}
159 fun set_subst_true (form_arg, act_arg) {env, path, eval, or, finish, ...} =
160 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
161 or = or, finish = finish, assoc = true}
162 fun set_subst_false (form_arg, act_arg) {env, path, eval, or, finish, ...} =
163 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
164 or = or, finish = finish, assoc = false}
165 fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*)
166 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
167 or = ORundef, finish = AppUndef_, assoc = false}
169 fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} =
170 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
171 or = or, finish = finish, assoc = assoc}
172 val set_env_true = Istate_Def.set_env_true
173 fun set_form_env (form_arg, env) {path, eval, act_arg, or, finish, assoc, ...} =
174 {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
175 or = or, finish = finish, assoc = assoc}
176 fun set_act_env (act_arg, env) {path, eval, form_arg, or, finish, assoc, ...} =
177 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
178 or = or, finish = finish, assoc = assoc}
179 fun upd_env form {env, path, eval, form_arg, act_arg, or, finish, assoc} =
180 {env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
181 act_arg = act_arg, or = or, finish = finish, assoc = assoc}
182 fun upd_env' (env, (form, act)) {path, eval, or, finish, assoc, ...} =
183 {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
184 or = or, finish = finish, assoc = assoc}
185 fun upd_env'' (form, act) {env, path, eval, or, finish, assoc, ...} =
186 {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
187 or = or, finish = finish, assoc = assoc}
190 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
191 or = or, finish = finish, assoc = assoc}