--------------------------------------------------------------------------------
-- T_NameReuse.tex

-- To investigate where the reuse of names in nested scopes is allowed in Circus,
-- but forbbiden in Java.
--------------------------------------------------------------------------------

--ADAPTADO AO LATEX DO NOVO PARSER, 1.5.0 DE CZT

\begin{axdef}
  v: \nat
\where
  v = 1
\end{axdef}  

\begin{circus}
\circprocess\ NameReuseP \circdef v: \nat \circspot \circbegin
\end{circus}

    :: This redeclaration the type checker must catch.
    \begin{axdef}
      lconst: \nat
    \where
      lconst = 1
    \end{axdef}  

%    \begin{circus}
%    \circstate\ 
%    \end{circus}

        :: This redeclaration the type checker must catch.
%        \begin{schema}{S}
%        st: \nat
%        \end{schema}
	\begin{circusaction}
    \circstate S ~~==~~ [~ st: \nat ~]
    \end{circusaction}

    :: Redeclaration of local variables and action parameters must
    :: not be permitted by the translation strategy because the Java
    :: code will not allow.
    \begin{circusaction}
    A \circdef v: \nat \circspot (
           v := 0 \circseq
           \circvar v1: \nat \circspot (
                \circvar v2: \nat \circspot v := 1
           )
    )       
    \end{circusaction}

\begin{circusaction}
    \circspot A(0)
\end{circusaction}

\begin{circus}
\circend
\end{circus}