(* Title:  interpreter-state for Lucas-Interpretation

   Author: Walther Neuper 190724

   (c) due to copyright terms

*)

signature INTERPRETER_STATE =

sig

  datatype asap = datatype Istate_Def.asap

  val asap2str: asap -> string 

  type pstate = Istate_Def.pstate

  val e_pstate: pstate

  val pstate2str: pstate -> string

  datatype T = datatype Istate_Def.T

  val empty: T

  val string_of: T -> string

  val string_of': T -> string

  val istates2str: T option * T option -> string

  val the_pstate: T -> pstate

  val init_detail: Tactic.input -> term -> Istate_Def.T

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

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

  val trans_scan_dn: pstate -> pstate

  val trans_scan_up: pstate -> pstate

  val trans_ass: pstate -> pstate -> pstate

  val trans_env_act: pstate -> pstate -> pstate

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

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

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

  val path_up: pstate -> pstate

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

  val set_form: term -> pstate -> pstate

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

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

  val set_act: term -> pstate -> pstate

  val set_or: asap -> pstate -> pstate

  val set_found: 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_found: (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

(**)

(** types **)

datatype asap = datatype Istate_Def.asap

val asap2str = Istate_Def.asap2str

type pstate = Istate_Def.pstate

val e_pstate = Istate_Def.e_pstate

val pstate2str = Istate_Def.pstate2str

datatype T = datatype Istate_Def.T

val empty = Istate_Def.empty

fun the_pstate (Pstate pst) = pst

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

(** access functions **)

val string_of = Istate_Def.string_of

val string_of' = Istate_Def.string_of'

val istates2str = Istate_Def.istates2str

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_dn {env, eval, act_arg, or, found_accept, ...}  = 

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

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

fun trans_scan_up {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 = false(*the only update*)}

fun trans_ass {assoc, ...} {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 = assoc}

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

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

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

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

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

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

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

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

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

fun path_up' [] = raise ERROR "path_up' []"

  | path_up' path = drop_last path

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

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

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

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

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

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

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

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

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

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

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

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

val set_eval = Istate_Def.set_eval

val set_act = Istate_Def.set_act

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

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

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

fun set_found {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, found_accept = true, assoc = assoc}

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

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

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

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

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

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

fun set_subst_true (form_arg, act_arg) {env, path, eval, 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}

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

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

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

fun set_subst_found (form_arg, act_arg) {env, path, eval, ...} =

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

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

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

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

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

val set_env_true = Istate_Def.set_env_true

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* initialize istate for Detail_Set *)

fun init_detail (Tactic.Rewrite_Set rls) t =

    let

      val thy = ThyC.get_theory "Isac_Knowledge"

      val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args

    in

      Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])

    end

  | init_detail (Tactic.Rewrite_Set_Inst (subs, rls)) t =

    let

      val ctxt = Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge")

      val rls' = assoc_rls rls

      val v = case Subst.T_from_input ctxt subs of

        (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)

      | _ => raise ERROR "init_detail: uncovered case"

      val prog = Auto_Prog.gen (Proof_Context.theory_of ctxt) t rls'

      val args = Program.formal_args prog

    in

      Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))

    end

  | init_detail tac _ = raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac)

(** initialisation **)

(**)end(**)