1 (* Title: interpreter-state for Lucas-Interpretation
2 Author: Walther Neuper 190724
3 (c) due to copyright terms
5 Minimum of code required BEFORE Interpret/
7 signature INTERPRETER_STATE_DEFINITION =
10 datatype asap = ORundef | AssOnly | AssGen;
11 val asap2str: asap -> string
12 datatype appy_ = AppUndef_(* | Napp_*) | Skip_
13 val appy_2str: appy_ -> string
16 val pstate2str: pstate -> string
18 datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
20 val istate2str: T -> string
21 val istates2str: T option * T option -> string
23 val set_eval: Rule.rls -> pstate -> pstate
24 val set_act: term -> pstate -> pstate
25 val set_env_true: Env.T -> pstate -> pstate
30 structure Istate_Def(**): INTERPRETER_STATE_DEFINITION(**) =
36 datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *)
37 ORundef (* undefined: set only by (topmost) Or *)
38 | AssOnly (* do not execute applicable Prog_Tac - there could be an associated
39 in parallel Or-branch *)
40 | AssGen; (* no Ass(Weak) found within Or, thus continue scan
41 search for _applicable_ stacs, execute and generate pt *)
42 (*this constructions doesnt allow arbitrary nesting of Or !!! *)
43 fun asap2str ORundef = "ORundef"
44 | asap2str AssOnly = "AssOnly"
45 | asap2str AssGen = "AssGen"
47 datatype appy_ = (* as argument in scan_up, go_scan_up, from scan_dn *)
48 (*Accept_Tac is only (final) return-value, not argument during search *)
51 | Napp_ (* ev. detects 'script is not appropriate for this example' *)
53 | Skip_; (* detects 'script successfully finished'
54 also used as init-value for resuming; this works,
55 because 'nxt_up Or e1' treats as Accept_Tac *)
56 fun appy_2str AppUndef_ = "AppUndef_"
58 | appy_2str Napp_ = "Napp_"
60 | appy_2str Skip_ = "Skip_"
63 {env: Env.T, (* environment for variables in a program *)
64 path: TermC.path, (* to the current location in a program *)
65 eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *)
66 form_arg: term option,(* argument of a curried function *)
67 act_arg: term, (* value for the curried argument *)
68 or: asap, (* flag for scanning tactical "Or" !shall be dropped *)
69 finish: appy_, (* flag set after execution of a tactic !shall be dropped *)
70 assoc: bool} (* is the tactic associated to input ?cont.search Unsafe_Step \<rightarrow> Safe_Step*)
72 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,
73 or = ORundef, finish = AppUndef_, assoc = false}
74 fun topt2str NONE = "NONE"
75 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
76 fun pstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
77 "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule.id_rls eval ^ ", " ^
78 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
79 appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
81 (* for handling type T see fun from_pblobj_or_detail', +? *)
82 datatype T = (*interpreter state*)
83 Uistate (*undefined in modspec, in '_deriv'ation*)
84 | Pstate of pstate (*for script interpreter*)
85 | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
86 val e_istate = Pstate e_pstate;
88 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
89 fun istate2str Uistate = "Uistate"
90 | istate2str (Pstate pst) =
91 "Pstate " ^ pstate2str pst
92 | istate2str (RrlsState (t, t1, rss, rtas)) =
93 "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
94 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
95 (strs2str o (map rta2str)) rtas ^ ")";
96 fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
97 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
98 | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
99 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
102 fun set_eval e {env, path, form_arg, act_arg, or, finish, assoc, ...} =
103 {env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg,
104 or = or, finish = finish, assoc = assoc}
105 fun set_act act {env, path, eval, form_arg, or, finish, assoc, ...} =
106 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act,
107 or = or, finish = finish, assoc = assoc}
108 fun set_env_true env {path, eval, form_arg, act_arg, or, finish, ...} =
109 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
110 or = or, finish = finish, assoc = true}