(* Title:  interpreter-state for Lucas-Interpretation

   Author: Walther Neuper 191017

   (c) due to copyright terms

*)

signature ENVIRONMENT =

sig

  (*Celem*)

  type T

  val env2str: Rule.subst -> string

  val subst2str: Rule.subst -> string

  val subst2str': Rule.subst -> string

  val update: T -> term * term -> T

  val update': term -> term * T -> T

  val update_opt: T -> term option * term -> T

  val update_opt': T * (term option * term) -> T

  val update_opt'': ((term * T) * term option) -> T

end

(**)

structure Env(**): ENVIRONMENT(**) =

struct

(**)

type T = (term * term) list;

fun subst2str s =

    (strs2str o

      (map (

        Celem.linefeed o pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;

fun subst2str' s =

    (strs2str' o

     (map (

       pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;

val env2str = subst2str;

(* update environment; t <> empty if coming from listexpr *)

fun update env (id, vl) =

  let val env' = if vl = Rule.e_term then env else overwrite (env, (id, vl));

  in env' end;

fun update' id (vl, env) = update env (id, vl)

(*WN020526: not clear, when a is available in scan_up1 for eval_true*)

(*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS

  curried Rewrite) for CURRENT value (which may be different from PREVIOUS);

  thus "NONE" must be set at the end of currying (ill designed anyway)*)

fun update_opt env (SOME id, vl) = update env (id, vl)

  | update_opt env (NONE, vl) =

    ((**)tracing ("*** update_opt: (NONE," ^ Rule.term2str vl ^ ")");(**) env);

fun update_opt' (env, (id, vl)) = update_opt env (id, vl)

fun update_opt'' ((vl, env), id) = update_opt env (id, vl)

(**)end(**)