packages feed

Agda-2.3.2.2: src/core/Cont.lhs

\section{Cont: The context and operations on it}
%if False %% only to be seen by the Haskell compiler
\begin{code}
module Cont where

import Val
import Exp
import Conv
\end{code}
%endif
All type-checking is done in a context, which consists of an
environment for the values and types of all constants. The
context contains only type correct declarations.
\begin{code}
type Cont = ([Val],[Val])
\end{code}
The scope analysis guarantees that all constants will have a value and
a type in the context.

This modules contains operations to manipulate the context:
\begin{description}
\item[getVal, getType] looks up the value and type of an identifier.
\begin{code}
getVal   n  (env,tenv)  =  getRef n env
getType  n  (env,tenv)  =  getRef n tenv
\end{code}
\item[upCon] updates the context with a new identifier with its value
  and type.
\begin{code}
upCon                   :: Val -> Val -> Cont -> Cont
-- upCon u a con adds the declaration i:a=u to the context con
upCon u a (env,tenv)    = (u:env,a:tenv)
\end{code}
\item[genCon] generates a new constant in the current context. The expression
|genCon con n v| generates a new constant with name |n| and type |v|. It
uses the length of the context to quarantee that the constant is new.
\begin{code}
genCon                  :: Cont -> Name -> Val -> G Val
genCon (env,_)          = gensym (length env) 
\end{code}
\item[evalCon] evaluates an expression in a context. It just strips away the typing
declarations.
\begin{code}
evalCon                 :: Cont -> Exp -> Val
evalCon (env,_)         = eval env 
\end{code}
\item[lastCon] looks up the last declaration in the context.
\begin{code}
lastCon                 :: Cont -> G (Val,Val,Cont)
lastCon ([],_)          = fail "lastCon"
lastCon (_,[])          = fail "lastCon"
lastCon (u:env,a:tenv)  = return (u,a,(env,tenv))
\end{code}
\item[lengthCon] the length of the context.
\begin{code}
lengthCon (env,_)       = length env
\end{code}
\end{description}
\begin{code}
evalBodyCon             :: Cont -> Val -> Exp -> Val
-- evalBodyCon con v e 
evalBodyCon (env,_)     = evalBody env 
-- lastCon con computes the last declaration in con
\end{code}