walther@59737
|
1 |
(* Title: interpreter-state for Lucas-Interpretation
|
walther@59737
|
2 |
Author: Walther Neuper 190724
|
walther@59737
|
3 |
(c) due to copyright terms
|
walther@59777
|
4 |
|
walther@59777
|
5 |
Minimum of code required BEFORE Interpret/
|
walther@59737
|
6 |
*)
|
walther@59737
|
7 |
signature INTERPRETER_STATE_DEFINITION =
|
walther@59737
|
8 |
sig
|
walther@59737
|
9 |
|
walther@59737
|
10 |
datatype asap = ORundef | AssOnly | AssGen;
|
walther@59777
|
11 |
val asap2str: asap -> string
|
walther@59737
|
12 |
type pstate
|
walther@59777
|
13 |
val e_pstate: pstate
|
walther@59777
|
14 |
val pstate2str: pstate -> string
|
walther@59814
|
15 |
val pstate2str': pstate -> string
|
walther@59737
|
16 |
|
walther@59850
|
17 |
datatype T = RrlsState of Rule_Set.rrlsstate | Pstate of pstate | Uistate
|
walther@59846
|
18 |
val empty: T
|
Walther@60646
|
19 |
val string_of: Proof.context -> T -> string
|
walther@59844
|
20 |
val string_of': T -> string
|
Walther@60646
|
21 |
val istates2str: Proof.context -> T option * T option -> string
|
walther@59737
|
22 |
|
walther@59851
|
23 |
val set_eval: Rule_Set.T -> pstate -> pstate
|
walther@59737
|
24 |
val set_act: term -> pstate -> pstate
|
walther@59737
|
25 |
val set_env_true: Env.T -> pstate -> pstate
|
walther@59737
|
26 |
|
walther@59737
|
27 |
end
|
walther@59737
|
28 |
|
walther@59737
|
29 |
(**)
|
walther@59737
|
30 |
structure Istate_Def(**): INTERPRETER_STATE_DEFINITION(**) =
|
walther@59737
|
31 |
struct
|
walther@59737
|
32 |
(**)
|
walther@59737
|
33 |
|
walther@59737
|
34 |
datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *)
|
walther@59737
|
35 |
ORundef (* undefined: set only by (topmost) Or *)
|
walther@59737
|
36 |
| AssOnly (* do not execute applicable Prog_Tac - there could be an associated
|
walther@59737
|
37 |
in parallel Or-branch *)
|
walther@59844
|
38 |
| AssGen; (* no Associated(Weak) found within Or, thus continue scan
|
walther@59737
|
39 |
search for _applicable_ stacs, execute and generate pt *)
|
walther@59737
|
40 |
(*this constructions doesnt allow arbitrary nesting of Or !!! *)
|
walther@59737
|
41 |
fun asap2str ORundef = "ORundef"
|
walther@59737
|
42 |
| asap2str AssOnly = "AssOnly"
|
walther@59737
|
43 |
| asap2str AssGen = "AssGen"
|
walther@59737
|
44 |
|
walther@59737
|
45 |
type pstate =
|
walther@59737
|
46 |
{env: Env.T, (* environment for variables in a program *)
|
walther@59767
|
47 |
path: TermC.path, (* to the current location in a program *)
|
walther@59851
|
48 |
eval: Rule_Set.T, (* rule-set for evaluating a Prog_Expr *)
|
walther@59737
|
49 |
form_arg: term option,(* argument of a curried function *)
|
walther@59737
|
50 |
act_arg: term, (* value for the curried argument *)
|
walther@59779
|
51 |
or: asap, (* flag for scanning tactical "Or" !shall be dropped *)
|
walther@59784
|
52 |
found_accept: bool, (* flag set after execution of a tactic !shall be dropped *)
|
walther@59779
|
53 |
assoc: bool} (* is the tactic associated to input ?cont.search Unsafe_Step \<rightarrow> Safe_Step*)
|
walther@59777
|
54 |
val e_pstate =
|
walther@59861
|
55 |
{env = [], path = [], eval = Rule_Set.empty, form_arg = NONE, act_arg = TermC.empty,
|
walther@59784
|
56 |
or = ORundef, found_accept = false, assoc = false}
|
walther@59737
|
57 |
fun topt2str NONE = "NONE"
|
Walther@60618
|
58 |
| topt2str (SOME t) =
|
Walther@60618
|
59 |
let
|
Walther@60618
|
60 |
val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")
|
Walther@60618
|
61 |
in
|
Walther@60618
|
62 |
"SOME " ^ UnparseC.term_in_ctxt ctxt t
|
Walther@60618
|
63 |
end;
|
walther@60251
|
64 |
fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
|
Walther@60618
|
65 |
let
|
Walther@60618
|
66 |
val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")
|
Walther@60618
|
67 |
in
|
Walther@60618
|
68 |
"(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^
|
Walther@60618
|
69 |
topt2str form_arg ^ ", \n" ^ UnparseC.term_in_ctxt ctxt act_arg ^ ", " ^ asap2str or ^ ", " ^
|
Walther@60618
|
70 |
bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"
|
Walther@60618
|
71 |
end;
|
walther@60251
|
72 |
fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
|
Walther@60618
|
73 |
let
|
Walther@60618
|
74 |
val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")
|
Walther@60618
|
75 |
in
|
Walther@60618
|
76 |
"(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^
|
Walther@60618
|
77 |
topt2str form_arg ^ ", " ^ UnparseC.term_in_ctxt ctxt act_arg ^ ", " ^ asap2str or ^ ", " ^
|
Walther@60618
|
78 |
bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"
|
Walther@60618
|
79 |
end;
|
walther@59737
|
80 |
|
walther@59831
|
81 |
(* for handling type T see fun resume_prog, +? *)
|
walther@59737
|
82 |
datatype T = (*interpreter state*)
|
walther@59737
|
83 |
Uistate (*undefined in modspec, in '_deriv'ation*)
|
walther@59737
|
84 |
| Pstate of pstate (*for script interpreter*)
|
walther@59850
|
85 |
| RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*)
|
walther@59846
|
86 |
val empty = Pstate e_pstate;
|
walther@59737
|
87 |
|
Walther@60646
|
88 |
fun rta2str ctxt (r, (t, a)) =
|
Walther@60647
|
89 |
"\n(" ^ Rule.to_string ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^
|
Walther@60646
|
90 |
UnparseC.terms_in_ctxt ctxt a ^ "))";
|
Walther@60646
|
91 |
fun string_of _ Uistate = "Uistate"
|
Walther@60646
|
92 |
| string_of _ (Pstate pst) =
|
Walther@60646
|
93 |
"Pstate " ^ pstate2str pst
|
Walther@60646
|
94 |
| string_of ctxt (RrlsState (t, t1, rss, rtas)) =
|
Walther@60646
|
95 |
"RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^
|
Walther@60647
|
96 |
(strs2str o (map (strs2str o (map (Rule.to_string ctxt))))) rss ^ ", " ^
|
Walther@60646
|
97 |
(strs2str o (map (rta2str ctxt))) rtas ^ ")";
|
walther@59844
|
98 |
fun string_of' Uistate = "Uistate"
|
walther@59844
|
99 |
| string_of' (Pstate pst) =
|
walther@59814
|
100 |
"Pstate " ^ pstate2str' pst
|
walther@59844
|
101 |
| string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState"
|
Walther@60646
|
102 |
fun istates2str _ (NONE, NONE) = "(#NONE, #NONE)"
|
Walther@60646
|
103 |
| istates2str ctxt (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ctxt ist ^ ")"
|
Walther@60646
|
104 |
| istates2str ctxt (SOME ist, NONE) = "(#SOME " ^ string_of ctxt ist ^ ",\n #NONE)"
|
Walther@60646
|
105 |
| istates2str ctxt (SOME i1, SOME i2) =
|
Walther@60646
|
106 |
"(#SOME " ^ string_of ctxt i1 ^ ",\n #SOME " ^ string_of ctxt i2 ^ ")";
|
walther@59737
|
107 |
|
walther@59737
|
108 |
|
walther@59784
|
109 |
fun set_eval e {env, path, form_arg, act_arg, or, found_accept, assoc, ...} =
|
walther@59737
|
110 |
{env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
111 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
112 |
fun set_act act {env, path, eval, form_arg, or, found_accept, assoc, ...} =
|
walther@59737
|
113 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act,
|
walther@59784
|
114 |
or = or, found_accept = found_accept, assoc = assoc}
|
walther@59784
|
115 |
fun set_env_true env {path, eval, form_arg, act_arg, or, found_accept, ...} =
|
walther@59737
|
116 |
{env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
|
walther@59784
|
117 |
or = or, found_accept = found_accept, assoc = true}
|
walther@59737
|
118 |
|
walther@59737
|
119 |
(**)end(**)
|
walther@59737
|
120 |
|