(* Title:  interpreter-state for Lucas-Interpretation

    Author: Walther Neuper 190724

    (c) due to copyright terms

    Minimum of code required BEFORE Interpret/ 

 *)

 signature INTERPRETER_STATE_DEFINITION =

 sig

   datatype asap = ORundef | AssOnly | AssGen;

   val asap2str: asap -> string 

   type pstate

   val e_pstate: pstate

   val pstate2str: pstate -> string

   val pstate2str': pstate -> string

   datatype T = RrlsState of Rule_Set.rrlsstate | Pstate of pstate | Uistate

   val empty: T

   val string_of: Proof.context -> T -> string

   val string_of': T -> string

   val istates2str: Proof.context -> T option * T option -> string

   val set_eval: Rule_Set.T -> pstate -> pstate

   val set_act: term -> pstate -> pstate

   val set_env_true: Env.T -> pstate -> pstate

 end

 (**)                   

 structure Istate_Def(**): INTERPRETER_STATE_DEFINITION(**) =

 struct

 (**)

 datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or                 *)

   ORundef        (* undefined: set only by (topmost) Or                           *)

 | AssOnly       (* do not execute applicable Prog_Tac - there could be an associated

 	                 in parallel Or-branch                                         *)

 | AssGen;       (* no Associated(Weak) found within Or, thus continue scan

                    search for _applicable_ stacs, execute and generate pt        *)

 (*this constructions doesnt allow arbitrary nesting of Or !!!                    *)

 fun asap2str ORundef = "ORundef"

   | asap2str AssOnly = "AssOnly"

   | asap2str AssGen = "AssGen"

 type pstate =

   {env: Env.T,          (* environment for variables in a program *)

   path: TermC.path,     (* to the current location in a program   *)

   eval: Rule_Set.T,       (* rule-set for evaluating a Prog_Expr    *)

   form_arg: term option,(* argument of a curried function         *)

   act_arg: term,        (* value for the curried argument         *)

   or: asap,             (* flag for scanning tactical "Or"      !shall be dropped *)

   found_accept: bool,   (* flag set after execution of a tactic !shall be dropped *)

   assoc: bool}          (* is the tactic associated to input ?cont.search Unsafe_Step \<rightarrow> Safe_Step*)

 val e_pstate =

   {env = [], path = [], eval = Rule_Set.empty, form_arg = NONE, act_arg = TermC.empty,

     or = ORundef, found_accept = false, assoc = false}

 fun topt2str NONE = "NONE"

   | topt2str (SOME t) =

   let

     val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")

   in

     "SOME " ^ UnparseC.term_in_ctxt ctxt t

   end;

 fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =

   let

     val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")

   in

     "(" ^  Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^

     topt2str form_arg ^ ", \n" ^ UnparseC.term_in_ctxt ctxt act_arg ^ ", " ^ asap2str or ^ ", " ^

     bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"

   end;

 fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =

   let

     val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")

   in

     "(" ^  Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^

     topt2str form_arg ^ ", " ^ UnparseC.term_in_ctxt ctxt act_arg ^ ", " ^ asap2str or ^ ", " ^

     bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"

   end;

 (* for handling type T see fun resume_prog, +? *)

 datatype T =                 (*interpreter state*)

 	  Uistate                       (*undefined in modspec, in '_deriv'ation*)

   | Pstate of pstate          (*for script interpreter*)

   | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*)

 val empty = Pstate e_pstate;

 fun rta2str ctxt (r, (t, a)) =

   "\n(" ^ Rule.to_string ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^

   UnparseC.terms_in_ctxt ctxt a ^ "))";

 fun string_of _ Uistate = "Uistate"

   | string_of _ (Pstate pst) = 

     "Pstate " ^ pstate2str pst   

   | string_of ctxt (RrlsState (t, t1, rss, rtas)) =

     "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^

     (strs2str o (map (strs2str o (map (Rule.to_string ctxt))))) rss ^ ", " ^

     (strs2str o (map (rta2str ctxt))) rtas ^ ")";

 fun string_of' Uistate = "Uistate"

   | string_of' (Pstate pst) = 

     "Pstate " ^ pstate2str' pst

   | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState"

 fun istates2str _ (NONE, NONE) = "(#NONE, #NONE)"

   | istates2str ctxt (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ctxt ist ^ ")"

   | istates2str ctxt (SOME ist, NONE) = "(#SOME " ^ string_of ctxt ist ^ ",\n #NONE)"

   | istates2str ctxt (SOME i1, SOME i2) =

     "(#SOME " ^ string_of ctxt i1 ^ ",\n #SOME " ^ string_of ctxt i2 ^ ")";

 fun set_eval e {env, path, form_arg, act_arg, or, found_accept, assoc, ...} =

   {env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg,

     or = or, found_accept = found_accept, assoc = assoc}

 fun set_act act {env, path, eval, form_arg, or, found_accept, assoc, ...} =

   {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act,

     or = or, found_accept = found_accept, assoc = assoc}

 fun set_env_true env {path, eval, form_arg, act_arg, or, found_accept, ...} =

   {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,

     or = or, found_accept = found_accept, assoc = true}

 (**)end(**)