(* Title:  interpreter-state for Lucas-Interpretation

   Author: Walther Neuper 190724

   (c) due to copyright terms

*)

signature INTERPRETER_STATE =

sig

  datatype appy_ = AppUndef_ | Napp_ | Skip_

  type pstate

  val e_scrstate: pstate

  val scrstate2str: Rule.subst * Celem.loc_ * Rule.rls * term option * term * appy_ * bool -> 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 get_path: pstate -> Celem.loc_

  val get_path_up: pstate -> Celem.loc_

  val get_act: pstate -> term

  val get_rls: pstate -> Rule.rls

  val get_env: pstate -> Env.T

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

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

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

  val get_assoc: pstate -> bool

  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.loc_ -> pstate -> pstate

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

  val path_up: pstate -> pstate

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

  val upd_form: term -> pstate -> pstate

  val upd_path: Celem.loc_ -> pstate -> pstate

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

  val upd_act: term -> pstate -> pstate

  val upd_appy: appy_ -> pstate -> pstate

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

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

  val upd_env': term -> pstate -> pstate

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

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

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

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

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

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

end

(**)                   

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

struct

(**)

open Celem

datatype appy_ = (* as argument in nxt_up, nstep_up, from appy               *)

(*Appy              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 Appy                    *)

fun appy_2str AppUndef_ = "AppUndef_"

  | appy_2str Napp_ = "Napp_"

  | appy_2str Skip_ = "Skip_"

type pstate =  (* state for script interpreter                       *)

	 Env.T(*stack*)  (* used to instantiate tac for checking associate

		                12.03.noticed: e_ not updated during execution ?!? *)

	 * Celem.loc_  (* location of tac in script                          *)

	 * Rule.rls    (* for evaluating Prog_Expr                           *)

	 * term option (*id FORMal ARGument of curried functions               *)

	 * term        (*vl ACTual ARGument (value) for execution of Tactic.T

		                updated also after a derivation by 'new_val'       *)

	 * appy_        (* estimation of how result will be obtained          *)

	 * bool;       (* true = strongly .., false = weakly associated: 

					          only used during ass_dn/up                         *)

val e_scrstate =

  ([]: Env.T, []:Celem.loc_, Rule.e_rls, NONE, Rule.e_term, AppUndef_, false) : pstate

fun topt2str NONE = "NONE"

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

fun scrstate2str (env, loc_, rls, topt, t, safe, bool) = (* for tests only *)

  "(" ^  Env.env2str env ^ ", " ^ Celem.loc_2str loc_ ^ ", " ^ Rule.id_rls rls ^ ", " ^

  topt2str topt ^ ", \n" ^ Rule.term2str t ^ ", " ^ appy_2str safe ^ ", " ^ bool2str bool ^ ")";

(* 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 ([], [], Rule.e_rls, NONE, Rule.e_term, AppUndef_, false));

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_path (_, path, _, _,_, _, _) = path

fun get_path_up (ist as (_, path, _, _, _, _, _)) =

  if length path > 1 then drop_last path else raise ERROR ("get_path_up [] with " ^ scrstate2str ist)

fun get_act (_, _, _, _, act_arg, _, _) = act_arg

fun get_rls (_, _, rls, _, _, _, _) = rls

fun get_env (env, _, _, _, _, _, _) = env

fun get_act_env (env, _, _, _, act_arg, _, _) = (act_arg, env)

fun get_assoc (_, _, _, _, _, _, ass) = ass

fun get_subst (env, _, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))

fun trans_scan_down2 (env, _, rls, _, act_arg, _, _)  = 

  (env, [R], rls, NONE, act_arg, AppUndef_, false)

fun trans_scan_up2 (env, path, rls, form_arg, act_arg, _, _)  = 

  (env, path, rls, form_arg, act_arg, AppUndef_, false)

fun trans_ass (_, _, _,  _,_, _, ass) (env, path, rls, form_arg, act_arg, safe, _) = 

  (env, path, rls, form_arg, act_arg, safe, ass)

fun trans_env_act (env, _, _, _, act_arg, _, _) (_, path, rls, form_arg, _, safe, ass) = 

  (env, path, rls, form_arg, act_arg, safe, ass)

fun path_down path (env, p, rls, form_arg, act_arg, safe, ass) =

  (env, p @ path, rls, form_arg, act_arg, safe, ass)

fun path_down_form (path, form_arg) (env, p, rls, _, act_arg, safe, ass) =

  (env, p @ path, rls, SOME form_arg, act_arg, safe, ass)

fun path_up (env, path, rls, form_arg, act_arg, safe, ass) =

  (env, drop_last path, rls, form_arg, act_arg, safe, ass)

fun path_up_down path (env, p, rls, form_arg, act_arg, safe, ass) =

  (env, (drop_last p) @ path, rls, form_arg, act_arg, safe, ass)

fun upd_form form (env, path, rls, _, act_arg, safe, ass) =

  (env, path, rls, SOME form, act_arg, safe, ass)

fun upd_path path (env, _, rls, form_arg, act_arg, safe, ass) =

  (env, path, rls, form_arg, act_arg, safe, ass)

fun upd_rls rls (env, path, _, form_arg, act_arg, safe, ass) =

  (env, path, rls, form_arg, act_arg, safe, ass)

fun upd_act act (env, path, rls, form_arg, _, safe, ass) =

  (env, path, rls, form_arg, act, safe, ass)

fun upd_appy app (env, path, rls, form_arg, act_arg, _, ass) =

  (env, path, rls, form_arg, act_arg, app, ass)

fun upd_env env (_, path, rls, form_arg, act_arg, safe, ass) =

  (env, path, rls, form_arg, act_arg, safe, ass)

fun upd_env_true env (_, path, rls, form_arg, act_arg, safe, _) =

  (env, path, rls, form_arg, act_arg, safe, true)

fun upd_env' form (env, path, rls, form_arg, act_arg, safe, ass) =

  (Env.upd_env env (form, act_arg), path, rls, form_arg, act_arg, safe, ass)

fun upd_env'' (env, (form, act)) (_, path, rls, _, _, safe, ass) =

    (Env.upd_env env (form, act), path, rls, SOME form, act, safe, ass)

fun upd_form_env (form_arg, env) (_, path, rls, _, act_arg, safe, ass) =

  (env, path, rls, SOME form_arg, act_arg, safe, ass)

fun upd_act_env (act_arg, env) (_, path, rls, form_arg, _, safe, ass) =

  (env, path, rls, form_arg, act_arg, safe, ass)

fun upd_subst env (form_arg, act_arg) (_, path, rls, _, _, safe, ass) =

  (env, path, rls, SOME form_arg, act_arg, safe, ass)

fun upd_subst_true (form_arg, act_arg) (env, path, rls, _, _, safe, _) =

  (env, path, rls, form_arg, act_arg, safe, true)

fun upd_subst_false (form_arg, act_arg) (env, path, rls, _, _, safe, _) =

  (env, path, rls, form_arg, act_arg, safe, false)

(**)end(**)