/*
	Tables are useful for storing finite maps from closed terms
	to closed terms and can be accessed in almost constant
	time by means of hashing. In many program transformation
	applications a table is used to keep track of a scoped 
	finite map in which the bindings have to be removed after
	leaving the scope. Adding and removing entries in the
	finite map has to be done according to the scope structure
	and thus interferes with traversal. This module introduces
	operators that separate the declaration of a scope
	and the addition of bindings. Removing bindings at the
	end of a scope is completely transparent.
*/

module lang/scoped-finite-map
imports 
  collection/hash-table/common
  collection/list/-
  strategy/conditional

signature
  constructors
    Scopes : Key

strategies

  init-name-space(ns) = 
    where(ns; table-create)

  exit-name-space(ns) =  
    where(ns; table-destroy)

  begin-scope(ns) = //debug(!"begin-scope: ");
  where(ns => ns
  ; <table-put>(ns, Scopes(), [[] | <table-get <+ ![]>(ns, Scopes())])
  )

  end-scope(ns) = //debug(!"end-scope: ");
  where(ns => ns
  ; (<table-get; not(?[])>(ns, Scopes()) <+ ![[]]) => [scope | scopes]
  ; <table-put> (ns, Scopes(), scopes)
  ; <map( \ key -> <table-pop-rm>(ns, key) \ )> scope
  )

//  scope(ns, s) =
//    begin-scope(ns); (s; end-scope(ns) <+ end-scope(ns); fail)

  scope(ns, s) =
    begin-scope(ns); restore-always(s, end-scope(ns))

  assert(ns) = ?(key, val); //debug(!"assert: ");
  where(ns => ns
  ; <table-push>(ns, key, val)
  ; (<table-get; not(?[])>(ns, Scopes()) <+ ![[]]) => [scope | scopes]
  ; <table-put>(ns, Scopes(), [[key | scope] | scopes])
  //; debug(!"asserted: ")
  )

  override-key(ns) = ?(key, val); //debug(!"override-key: ");
  where(ns => ns
  ; <table-replace>(ns, key, val)
  //; debug(!"overriden: ")
  )

  rewrite(ns) = //debug(!"rewrite: "); 
    \ key -> <table-lookup>(<ns>(), key) \
  //; debug(!"rewriten: ")


// for extend [overide] rules

  extend-assert(ns) = ?(key, val); //debug(!"assert: ");
  where(ns => ns
  ; (<table-get; not(?[])>(ns, Scopes()) <+ ![[]]) => [scope | scopes]
  ; (<elem>(key, scope)
     ; <table-get>(ns, key) => [prevvals | morevals]
     ; <table-put>(ns, key, [[val | prevvals] | morevals])
    <+ <table-push>(ns, key, [val])
       ; <table-put>(ns, Scopes(), [[key | scope] | scopes])
     )
  //; debug(!"asserted: ")
  )

  extend-override-key(ns) = ?(key, val); //debug(!"override-key: ");
  where(ns => ns
    ; <table-get>(ns, key) => [prevvals | morevals]
    ; <table-put>(ns, key, [[val | prevvals] | morevals])
  //; debug(!"overriden: ")
  )

  extend-assert-undefined(ns) = ?key; //debug(!"assert: ");
  where(ns => ns
  ; (<table-get; not(?[])>(ns, Scopes()) <+ ![[]]) => [scope | scopes]
  ; (<elem>(key, scope)
     ; <table-get>(ns, key) => [prevvals | morevals]
     ; <table-put>(ns, key, [[] | morevals])
    <+ <table-push>(ns, key, [])
       ; <table-put>(ns, Scopes(), [[key | scope] | scopes])
     )
  //; debug(!"asserted: ")
  )

  extend-override-key-undefined(ns) = ?key; //debug(!"override-key: ");
  where(ns => ns
    ; <table-get>(ns, key) => [prevvals | morevals]
    ; <table-put>(ns, key, [[] | morevals])
  //; debug(!"overriden: ")
  )

   extend-rewrite(ns) = rewrite(ns)

/*

\paragraph{Usage}

\begin{itemize}

\item \verb|init-name-space(!"fun")| initializes a name space for
function symbols, say.

\item \verb|exit-name-space(!"fun")| destroys the name space.

\item \verb|begin-scope(!"fun")| starts a new scope

\item \verb|end-scope(!"fun")| ends a scope

\item \verb|scope(!"fun", inline)| applies inline to the subject term
in a new scope, which is exited after inline returns, even if inline
fails.

\item \verb|<assert(!"fun")>("foldr", Fdec("foldr", xs, e))| binds a
value (e.g., a function declaration), to a key (e.g., the name of the
function)

\item \verb|<rewrite(!"fun")> "foldr"| retrieves the declaration

\end{itemize}

\paragraph{Example}

For an example see module \verb|scoped-finite-map-test|.

\paragraph{Backtracking}

Be aware that, in general, side-effects are not undone after a
failure.  The \verb|scope| strategy deals with this by catching a
possible failure of the scoped strategy, exiting the scope and then
failing again.

*/