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

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

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

\begin{circus}
\circprocess\ NameReuse_P \defs v: \nat @ \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}

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

\begin{circus}
    @ A(0)
\circend
\end{circus}