(* 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: T -> string

  val string_of': T -> string

  val istates2str: 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

(**)

open Celem                           

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.e_rls, form_arg = NONE, act_arg = Rule.e_term,

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

fun topt2str NONE = "NONE"

  | topt2str (SOME t) = "SOME " ^ Rule.term2str t;

fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)

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

  topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^

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

fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)

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

  topt2str form_arg ^ ", " ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^

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

(* 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 (r, (t, a)) = "\n(" ^ Rule_Set.rule2str r ^ ", (" ^ Rule.term2str t ^ ", " ^ Rule.terms2str a ^ "))";

fun string_of Uistate = "Uistate"

  | string_of (Pstate pst) = 

    "Pstate " ^ pstate2str pst

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

    "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^

    (strs2str o (map (strs2str o (map Rule_Set.rule2str)))) rss ^ ", " ^

    (strs2str o (map rta2str)) 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)"  (* for tests only *)

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

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

  | istates2str (SOME i1, SOME i2) = "(#SOME " ^ string_of i1 ^ ",\n #SOME " ^ string_of 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(**)