(* Title:  interpreter-state for Lucas-Interpretation

   Author: Walther Neuper 190724

   (c) due to copyright terms

*)

signature INTERPRETER_STATE =

sig

  datatype asap = Aundef | AssOnly | AssGen;

  datatype appy_ = AppUndef_ | Napp_ | Skip_

  type pstate

  val e_scrstate: pstate

  val scrstate2str: pstate -> string

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

  val istate2str: T -> string

  val istates2str: T option * T option -> string

  val e_istate: T

  val the_pstate: T -> pstate

  val get_act_env: pstate -> (term * Env.T)

  val get_subst: pstate -> (Env.T * (term option * term))

  val trans_scan_down2: pstate -> pstate

  val trans_scan_up2: pstate -> pstate

  val trans_ass: pstate -> pstate -> pstate

  val trans_env_act: pstate -> pstate -> pstate

  val path_down: Celem.path -> pstate -> pstate

  val path_down_form: (Celem.path * term) -> pstate -> pstate

  val path_up': Celem.path -> Celem.path

  val path_up: pstate -> pstate

  val path_up_down: Celem.path -> pstate -> pstate

  val set_form: term -> pstate -> pstate

  val set_path: Celem.path -> pstate -> pstate

  val set_eval: Rule.rls -> pstate -> pstate

  val set_act: term -> pstate -> pstate

  val set_or: asap -> pstate -> pstate

  val set_appy: appy_ -> pstate -> pstate

  val set_subst: Env.T -> (term * term) -> pstate -> pstate

  val set_subst': (term * term) -> pstate -> pstate

  val set_subst_true: (term option * term) -> pstate -> pstate

  val set_subst_false: (term option * term) -> pstate -> pstate

  val set_subst_reset: (term option * term) -> pstate -> pstate

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

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

  val set_form_env: (term * Env.T) -> pstate -> pstate

  val set_act_env: (term * Env.T) -> pstate -> pstate

  val upd_env: term -> pstate -> pstate

  val upd_env': Env.T * (term * term) -> pstate -> pstate

  val upd_env'': (term * term) -> pstate -> pstate

end

(**)                   

structure Istate(**): INTERPRETER_STATE(**) =

struct

(**)

open Celem                           

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

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

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

	                 in parallel Or-branch                                         *)

| AssGen;       (* no Ass(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 Aundef = "Aundef"

  | asap2str AssOnly = "AssOnly"

  | asap2str AssGen = "AssGen"

datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2      *)

(*Ackn_Tac2         is only (final) returnvalue, not argument during search  *)

  AppUndef_

| Napp_          (* ev. detects 'script is not appropriate for this example' *)

| Skip_;         (* detects 'script successfully finished'

		                also used as init-value for resuming; this works,

	                  because 'nxt_up Or e1' treats as Ackn_Tac2               *)

fun appy_2str AppUndef_ = "AppUndef_"

  | appy_2str Napp_ = "Napp_"

  | appy_2str Skip_ = "Skip_"

type pstate =

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

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

  eval: Rule.rls,       (* 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"        *)

  finish: appy_,        (* flag set after execution of a tactic   *)

  assoc: bool}          (* is the tactic associated to input      *)

val e_scrstate =

  {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,

    or = Aundef, finish = AppUndef_, assoc = false}

fun topt2str NONE = "NONE"

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

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

  "(" ^  Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^

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

  appy_2str finish ^ ", " ^ bool2str assoc ^ ")";

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

datatype T =                 (*interpreter state*)

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

  | Pstate of pstate          (*for script interpreter*)

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

val e_istate = Pstate e_scrstate;

fun the_pstate (Pstate pst) = pst

  | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")

fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";

fun istate2str Uistate = "Uistate"

  | istate2str (Pstate pst) = 

    "Pstate " ^ scrstate2str pst

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

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

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

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

fun istates2str (NONE, NONE) = "(#NONE, #NONE)"  (* for tests only *)

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

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

  | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";

fun get_act_env {env, act_arg, ...} = (act_arg, env)

fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))

fun trans_scan_down2 {env, eval, act_arg, or, ...}  = 

  {env = env, path = [R], eval = eval, form_arg = NONE, act_arg = act_arg,

    or = or, finish = AppUndef_, assoc = false}

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

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

    or = or, finish = AppUndef_, assoc = false}

fun trans_ass {assoc, ...} {env, path, eval, form_arg, act_arg, or, finish, ...} = 

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

    or = or, finish = finish, assoc = assoc}

fun trans_env_act {env, act_arg, ...} {path, eval, form_arg, or, finish, assoc, ...} = 

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

    or = or, finish = finish, assoc = assoc}

fun path_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =

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

    or = or, finish = finish, assoc = assoc}

fun path_down_form (p, fa) {env, path, eval, act_arg, or, finish, assoc, ...} =

  {env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,

    or = or, finish = finish, assoc = assoc}

fun path_up' path = drop_last path

fun path_up {env, path, eval, form_arg, act_arg, or, finish, assoc} =

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

    or = or, finish = finish, assoc = assoc}

fun path_up_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =

  {env = env, path = (drop_last path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,

    or = or, finish = finish, assoc = assoc}

fun set_form f {env, path, eval, act_arg, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

fun set_path p {env, eval, form_arg, act_arg, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

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

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

    or = or, finish = finish, assoc = assoc}

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

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

    or = or, finish = finish, assoc = assoc}

fun set_or or {env, path, eval, form_arg, act_arg, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

fun set_appy fin {env, path, eval, form_arg, act_arg, or, assoc, ...} =

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

    or = or, finish = fin, assoc = assoc}

fun set_subst env (form_arg, act_arg) {path, eval, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

fun set_subst' (form_arg, act_arg) {env, path, eval, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

fun set_subst_true (form_arg, act_arg) {env, path, eval, or, finish, ...} =

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

    or = or, finish = finish, assoc = true}

fun set_subst_false (form_arg, act_arg) {env, path, eval, or, finish, ...} =

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

    or = or, finish = finish, assoc = false}

fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*)

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

    or = Aundef, finish = AppUndef_, assoc = false}

fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

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

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

    or = or, finish = finish, assoc = true}

fun set_form_env (form_arg, env) {path, eval, act_arg, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

fun set_act_env (act_arg, env) {path, eval, form_arg, or, finish, assoc, ...} =

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

    or = or, finish = finish, assoc = assoc}

fun upd_env form {env, path, eval, form_arg, act_arg, or, finish, assoc} =

  {env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,

    act_arg = act_arg, or = or, finish = finish, assoc = assoc}

fun upd_env' (env, (form, act)) {path, eval, or, finish, assoc, ...} =

  {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,

    or = or, finish = finish, assoc = assoc}

fun upd_env'' (form, act) {env, path, eval, or, finish, assoc, ...} =

  {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,

    or = or, finish = finish, assoc = assoc}

(*

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

    or = or, finish = finish, assoc = assoc}

*)

(**)end(**)