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 val asap2str: asap -> string
10 type pstate = Istate_Def.pstate
12 val pstate2str: pstate -> string
14 datatype T = datatype Istate_Def.T
16 val string_of: T -> string
17 val string_of': T -> string
18 val istates2str: T option * T option -> string
19 val the_pstate: T -> pstate
21 val init_detail: Tactic.input -> term -> Istate_Def.T
23 val get_act_env: pstate -> (term * Env.T)
24 val get_subst: pstate -> (Env.T * (term option * term))
26 val trans_scan_dn: pstate -> pstate
27 val trans_scan_up: pstate -> pstate
28 val trans_ass: pstate -> pstate -> pstate
29 val trans_env_act: pstate -> pstate -> pstate
31 val path_down: TermC.path -> pstate -> pstate
32 val path_down_form: (TermC.path * term) -> pstate -> pstate
33 val path_up': TermC.path -> TermC.path
34 val path_up: pstate -> pstate
35 val path_up_down: TermC.path -> pstate -> pstate
37 val set_form: term -> pstate -> pstate
38 val set_path: TermC.path -> pstate -> pstate
39 val set_eval: Rule_Set.T -> pstate -> pstate
40 val set_act: term -> pstate -> pstate
41 val set_or: asap -> pstate -> pstate
42 val set_found: pstate -> pstate
44 val set_subst: Env.T -> (term * term) -> pstate -> pstate
45 val set_subst': (term * term) -> pstate -> pstate
46 val set_subst_true: (term option * term) -> pstate -> pstate
47 val set_subst_false: (term option * term) -> pstate -> pstate
48 val set_subst_found: (term option * term) -> pstate -> pstate
50 val set_env: Env.T -> pstate -> pstate
51 val set_env_true: Env.T -> pstate -> pstate
52 val set_form_env: (term * Env.T) -> pstate -> pstate
53 val set_act_env: (term * Env.T) -> pstate -> pstate
54 val upd_env: term -> pstate -> pstate
55 val upd_env': Env.T * (term * term) -> pstate -> pstate
56 val upd_env'': (term * term) -> pstate -> pstate
61 structure Istate(**): INTERPRETER_STATE(**) =
67 datatype asap = datatype Istate_Def.asap
68 val asap2str = Istate_Def.asap2str
70 type pstate = Istate_Def.pstate
71 val e_pstate = Istate_Def.e_pstate
72 val pstate2str = Istate_Def.pstate2str
74 datatype T = datatype Istate_Def.T
75 val empty = Istate_Def.empty
76 fun the_pstate (Pstate pst) = pst
77 | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
80 (** access functions **)
82 val string_of = Istate_Def.string_of
83 val string_of' = Istate_Def.string_of'
84 val istates2str = Istate_Def.istates2str
86 fun get_act_env {env, act_arg, ...} = (act_arg, env)
87 fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))
89 fun trans_scan_dn {env, eval, act_arg, or, found_accept, ...} =
90 {env = env, path = [TermC.R], eval = eval, form_arg = NONE, act_arg = act_arg,
91 or = or, found_accept = found_accept, assoc = false}
92 fun trans_scan_up {env, path, eval, form_arg, act_arg, or, found_accept, ...} =
93 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
94 or = or, found_accept = found_accept, assoc = false(*the only update*)}
95 fun trans_ass {assoc, ...} {env, path, eval, form_arg, act_arg, or, found_accept, ...} =
96 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
97 or = or, found_accept = found_accept, assoc = assoc}
98 fun trans_env_act {env, act_arg, ...} {path, eval, form_arg, or, found_accept, assoc, ...} =
99 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
100 or = or, found_accept = found_accept, assoc = assoc}
102 fun path_down p {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
103 {env = env, path = path @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
104 or = or, found_accept = found_accept, assoc = assoc}
105 fun path_down_form (p, fa) {env, path, eval, act_arg, or, found_accept, assoc, ...} =
106 {env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,
107 or = or, found_accept = found_accept, assoc = assoc}
108 fun path_up' [] = raise ERROR "path_up' []"
109 | path_up' path = drop_last path
110 fun path_up {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
111 {env = env, path = path_up' path, eval = eval, form_arg = form_arg, act_arg = act_arg,
112 or = or, found_accept = found_accept, assoc = assoc}
113 fun path_up_down p {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
114 {env = env, path = (path_up' path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
115 or = or, found_accept = found_accept, assoc = assoc}
117 fun set_form f {env, path, eval, act_arg, or, found_accept, assoc, ...} =
118 {env = env, path = path, eval = eval, form_arg = SOME f, act_arg = act_arg,
119 or = or, found_accept = found_accept, assoc = assoc}
120 fun set_path p {env, eval, form_arg, act_arg, or, found_accept, assoc, ...} =
121 {env = env, path = p, eval = eval, form_arg = form_arg, act_arg = act_arg,
122 or = or, found_accept = found_accept, assoc = assoc}
123 val set_eval = Istate_Def.set_eval
124 val set_act = Istate_Def.set_act
125 fun set_or or {env, path, eval, form_arg, act_arg, found_accept, assoc, ...} =
126 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
127 or = or, found_accept = found_accept, assoc = assoc}
128 fun set_found {env, path, eval, form_arg, act_arg, or, assoc, ...} =
129 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
130 or = or, found_accept = true, assoc = assoc}
132 fun set_subst env (form_arg, act_arg) {path, eval, or, found_accept, assoc, ...} =
133 {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
134 or = or, found_accept = found_accept, assoc = assoc}
135 fun set_subst' (form_arg, act_arg) {env, path, eval, or, found_accept, assoc, ...} =
136 {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
137 or = or, found_accept = found_accept, assoc = assoc}
138 fun set_subst_true (form_arg, act_arg) {env, path, eval, or, found_accept, ...} =
139 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
140 or = or, found_accept = found_accept, assoc = true}
141 fun set_subst_false (form_arg, act_arg) {env, path, eval, or, found_accept, ...} =
142 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
143 or = or, found_accept = found_accept, assoc = false}
144 fun set_subst_found (form_arg, act_arg) {env, path, eval, ...} =
145 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
146 or = ORundef, found_accept = true, assoc = false}
148 fun set_env env {path, eval, form_arg, act_arg, or, found_accept, assoc, ...} =
149 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
150 or = or, found_accept = found_accept, assoc = assoc}
151 val set_env_true = Istate_Def.set_env_true
152 fun set_form_env (form_arg, env) {path, eval, act_arg, or, found_accept, assoc, ...} =
153 {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
154 or = or, found_accept = found_accept, assoc = assoc}
155 fun set_act_env (act_arg, env) {path, eval, form_arg, or, found_accept, assoc, ...} =
156 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
157 or = or, found_accept = found_accept, assoc = assoc}
158 fun upd_env form {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
159 {env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
160 act_arg = act_arg, or = or, found_accept = found_accept, assoc = assoc}
161 fun upd_env' (env, (form, act)) {path, eval, or, found_accept, assoc, ...} =
162 {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
163 or = or, found_accept = found_accept, assoc = assoc}
164 fun upd_env'' (form, act) {env, path, eval, or, found_accept, assoc, ...} =
165 {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
166 or = or, found_accept = found_accept, assoc = assoc}
168 (* initialize istate for Detail_Set *)
169 fun init_detail (Tactic.Rewrite_Set rls) t =
171 val thy = ThyC.get_theory "Isac_Knowledge"
172 val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args
174 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])
176 | init_detail (Tactic.Rewrite_Set_Inst (subs, rls)) t =
178 val ctxt = Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge")
179 val rls' = assoc_rls rls
180 val v = case Subst.T_from_input ctxt subs of
181 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
182 | _ => raise ERROR "init_detail: uncovered case"
183 val prog = Auto_Prog.gen (Proof_Context.theory_of ctxt) t rls'
184 val args = Program.formal_args prog
186 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))
188 | init_detail tac _ = raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac)
190 (** initialisation **)