wneuper@59572
|
1 |
(* Title: interpreter-state for Lucas-Interpretation
|
wneuper@59572
|
2 |
Author: Walther Neuper 190724
|
wneuper@59572
|
3 |
(c) due to copyright terms
|
wneuper@59572
|
4 |
*)
|
wneuper@59572
|
5 |
signature INTERPRETER_STATE =
|
wneuper@59572
|
6 |
sig
|
wneuper@59572
|
7 |
|
walther@59737
|
8 |
datatype asap = datatype Istate_Def.asap
|
walther@59777
|
9 |
val asap2str: asap -> string
|
walther@59737
|
10 |
type pstate = Istate_Def.pstate
|
walther@59777
|
11 |
val e_pstate: pstate
|
walther@59777
|
12 |
val pstate2str: pstate -> string
|
wneuper@59572
|
13 |
|
walther@59737
|
14 |
datatype T = datatype Istate_Def.T
|
walther@59846
|
15 |
val empty: T
|
walther@59844
|
16 |
val string_of: T -> string
|
walther@59844
|
17 |
val string_of': T -> string
|
walther@59664
|
18 |
val istates2str: T option * T option -> string
|
walther@59685
|
19 |
val the_pstate: T -> pstate
|
wneuper@59572
|
20 |
|
walther@59667
|
21 |
val get_act_env: pstate -> (term * Env.T)
|
walther@59667
|
22 |
val get_subst: pstate -> (Env.T * (term option * term))
|
walther@59660
|
23 |
|
walther@59784
|
24 |
val trans_scan_dn: pstate -> pstate
|
walther@59783
|
25 |
val trans_scan_up: pstate -> pstate
|
walther@59667
|
26 |
val trans_ass: pstate -> pstate -> pstate
|
walther@59667
|
27 |
val trans_env_act: pstate -> pstate -> pstate
|
walther@59659
|
28 |
|
walther@59767
|
29 |
val path_down: TermC.path -> pstate -> pstate
|
walther@59767
|
30 |
val path_down_form: (TermC.path * term) -> pstate -> pstate
|
walther@59767
|
31 |
val path_up': TermC.path -> TermC.path
|
walther@59667
|
32 |
val path_up: pstate -> pstate
|
walther@59767
|
33 |
val path_up_down: TermC.path -> pstate -> pstate
|
walther@59660
|
34 |
|
walther@59698
|
35 |
val set_form: term -> pstate -> pstate
|
walther@59767
|
36 |
val set_path: TermC.path -> pstate -> pstate
|
walther@59851
|
37 |
val set_eval: Rule_Set.T -> pstate -> pstate
|
walther@59698
|
38 |
val set_act: term -> pstate -> pstate
|
walther@59698
|
39 |
val set_or: asap -> pstate -> pstate
|
walther@59785
|
40 |
val set_found: pstate -> pstate
|
walther@59698
|
41 |
|
walther@59698
|
42 |
val set_subst: Env.T -> (term * term) -> pstate -> pstate
|
walther@59709
|
43 |
val set_subst': (term * term) -> pstate -> pstate
|
walther@59698
|
44 |
val set_subst_true: (term option * term) -> pstate -> pstate
|
walther@59698
|
45 |
val set_subst_false: (term option * term) -> pstate -> pstate
|
walther@59782
|
46 |
val set_subst_found: (term option * term) -> pstate -> pstate
|
walther@59698
|
47 |
|
walther@59698
|
48 |
val set_env: Env.T -> pstate -> pstate
|
walther@59698
|
49 |
val set_env_true: Env.T -> pstate -> pstate
|
walther@59698
|
50 |
val set_form_env: (term * Env.T) -> pstate -> pstate
|
walther@59698
|
51 |
val set_act_env: (term * Env.T) -> pstate -> pstate
|
walther@59698
|
52 |
val upd_env: term -> pstate -> pstate
|
walther@59698
|
53 |
val upd_env': Env.T * (term * term) -> pstate -> pstate
|
walther@59709
|
54 |
val upd_env'': (term * term) -> pstate -> pstate
|
walther@59659
|
55 |
|
wneuper@59572
|
56 |
end
|
wneuper@59572
|
57 |
|
walther@59668
|
58 |
(**)
|
wneuper@59572
|
59 |
structure Istate(**): INTERPRETER_STATE(**) =
|
wneuper@59572
|
60 |
struct
|
walther@59659
|
61 |
(**)
|
wneuper@59572
|
62 |
|
walther@59737
|
63 |
datatype asap = datatype Istate_Def.asap
|
walther@59777
|
64 |
val asap2str = Istate_Def.asap2str
|
walther@59680
|
65 |
|
walther@59737
|
66 |
type pstate = Istate_Def.pstate
|
walther@59777
|
67 |
val e_pstate = Istate_Def.e_pstate
|
walther@59777
|
68 |
val pstate2str = Istate_Def.pstate2str
|
wneuper@59572
|
69 |
|
walther@59737
|
70 |
datatype T = datatype Istate_Def.T
|
walther@59846
|
71 |
val empty = Istate_Def.empty
|
walther@59685
|
72 |
fun the_pstate (Pstate pst) = pst
|
walther@59685
|
73 |
| the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
|
wneuper@59572
|
74 |
|
walther@59844
|
75 |
val string_of = Istate_Def.string_of
|
walther@59844
|
76 |
val string_of' = Istate_Def.string_of'
|
walther@59777
|
77 |
val istates2str = Istate_Def.istates2str
|
wneuper@59572
|
78 |
|
walther@59682
|
79 |
fun get_act_env {env, act_arg, ...} = (act_arg, env)
|
walther@59682
|
80 |
fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))
|
walther@59659
|
81 |
|
walther@59784
|
82 |
fun trans_scan_dn {env, eval, act_arg, or, found_accept, ...} =
|
walther@59767
|
83 |
{env = env, path = [TermC.R], eval = eval, form_arg = NONE, act_arg = act_arg,
|
walther@59784
|
84 |
or = or, found_accept = found_accept, assoc = false}
|
walther@59784
|
85 |
fun trans_scan_up {env, path, eval, form_arg, act_arg, or, found_accept, ...} =
|
walther@59682
|
86 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
87 |
or = or, found_accept = found_accept, assoc = false(*the only update*)}
|
walther@59784
|
88 |
fun trans_ass {assoc, ...} {env, path, eval, form_arg, act_arg, or, found_accept, ...} =
|
walther@59682
|
89 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
90 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
91 |
fun trans_env_act {env, act_arg, ...} {path, eval, form_arg, or, found_accept, assoc, ...} =
|
walther@59682
|
92 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
93 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59660
|
94 |
|
walther@59664
|
95 |
|
walther@59784
|
96 |
fun path_down p {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
|
walther@59682
|
97 |
{env = env, path = path @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
98 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
99 |
fun path_down_form (p, fa) {env, path, eval, act_arg, or, found_accept, assoc, ...} =
|
walther@59682
|
100 |
{env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,
|
walther@59784
|
101 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59723
|
102 |
fun path_up' [] = raise ERROR "path_up' []"
|
walther@59723
|
103 |
| path_up' path = drop_last path
|
walther@59784
|
104 |
fun path_up {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
|
walther@59723
|
105 |
{env = env, path = path_up' path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
106 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
107 |
fun path_up_down p {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
|
walther@59723
|
108 |
{env = env, path = (path_up' path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
109 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59664
|
110 |
|
walther@59784
|
111 |
fun set_form f {env, path, eval, act_arg, or, found_accept, assoc, ...} =
|
walther@59682
|
112 |
{env = env, path = path, eval = eval, form_arg = SOME f, act_arg = act_arg,
|
walther@59784
|
113 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
114 |
fun set_path p {env, eval, form_arg, act_arg, or, found_accept, assoc, ...} =
|
walther@59682
|
115 |
{env = env, path = p, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
116 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59737
|
117 |
val set_eval = Istate_Def.set_eval
|
walther@59737
|
118 |
val set_act = Istate_Def.set_act
|
walther@59784
|
119 |
fun set_or or {env, path, eval, form_arg, act_arg, found_accept, assoc, ...} =
|
walther@59684
|
120 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
121 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59785
|
122 |
fun set_found {env, path, eval, form_arg, act_arg, or, assoc, ...} =
|
walther@59682
|
123 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
124 |
or = or, found_accept = true, assoc = assoc}
|
walther@59664
|
125 |
|
walther@59784
|
126 |
fun set_subst env (form_arg, act_arg) {path, eval, or, found_accept, assoc, ...} =
|
walther@59698
|
127 |
{env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
|
walther@59784
|
128 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
129 |
fun set_subst' (form_arg, act_arg) {env, path, eval, or, found_accept, assoc, ...} =
|
walther@59709
|
130 |
{env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
|
walther@59784
|
131 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
132 |
fun set_subst_true (form_arg, act_arg) {env, path, eval, or, found_accept, ...} =
|
walther@59698
|
133 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
134 |
or = or, found_accept = found_accept, assoc = true}
|
walther@59784
|
135 |
fun set_subst_false (form_arg, act_arg) {env, path, eval, or, found_accept, ...} =
|
walther@59698
|
136 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
137 |
or = or, found_accept = found_accept, assoc = false}
|
walther@59782
|
138 |
fun set_subst_found (form_arg, act_arg) {env, path, eval, ...} =
|
walther@59698
|
139 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
140 |
or = ORundef, found_accept = true, assoc = false}
|
walther@59698
|
141 |
|
walther@59784
|
142 |
fun set_env env {path, eval, form_arg, act_arg, or, found_accept, assoc, ...} =
|
walther@59682
|
143 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
144 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59737
|
145 |
val set_env_true = Istate_Def.set_env_true
|
walther@59784
|
146 |
fun set_form_env (form_arg, env) {path, eval, act_arg, or, found_accept, assoc, ...} =
|
walther@59698
|
147 |
{env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
|
walther@59784
|
148 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
149 |
fun set_act_env (act_arg, env) {path, eval, form_arg, or, found_accept, assoc, ...} =
|
walther@59698
|
150 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
151 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
152 |
fun upd_env form {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
|
walther@59697
|
153 |
{env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
|
walther@59784
|
154 |
act_arg = act_arg, or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
155 |
fun upd_env' (env, (form, act)) {path, eval, or, found_accept, assoc, ...} =
|
walther@59697
|
156 |
{env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
|
walther@59784
|
157 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
158 |
fun upd_env'' (form, act) {env, path, eval, or, found_accept, assoc, ...} =
|
walther@59709
|
159 |
{env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
|
walther@59784
|
160 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59682
|
161 |
|
walther@59682
|
162 |
(*
|
walther@59682
|
163 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
164 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59682
|
165 |
*)
|
wneuper@59572
|
166 |
|
walther@59674
|
167 |
(**)end(**)
|
wneuper@59572
|
168 |
|