Generation of Environment code

[VonTum]

The environment is very much intertwined with the binding representation, so it may be fruitful to generate code to abstract this away. Since the tool knows exactly how the environment is used and modified, it can generate the necessary functions to do this.

A simple DeBruijn-based environment:

data EnvItem = EnvVarValue Type | EnvVarType Type deriving (Eq, Show)
type Env = [EnvItem]

emptyEnv :: Env
emptyEnv = []

getItemFromEnv :: Variable -> Env -> EnvItem
getItemFromEnv Z (item:_) = item
getItemFromEnv (SVarValue v) (EnvVarValue _:rest) = getItemFromEnv v rest
getItemFromEnv (SVarType v) (EnvVarType _:rest) = getItemFromEnv v rest
getItemFromEnv _ _ = error "wrong or no binding for var, or DeBruijn index structure does not match path in term"

getVarValueFromEnv :: Variable -> Env -> Maybe Type
getVarValueFromEnv v env = case getItemFromEnv v env of
  EnvVarValue v -> Just v
  otherwise -> error "requested EnvVarValue but found something else"

getVarTypeFromEnv :: Variable -> Env -> Maybe Type
getVarTypeFromEnv v env = case getItemFromEnv v env of
  EnvVarType v -> Just v
  otherwise -> error "requested EnvVarType but found something else"

shiftEnvItem :: Variable -> EnvItem -> EnvItem
shiftEnvItem v (EnvVarValue t) = EnvVarValue (typeshiftplus v t)
shiftEnvItem v (EnvVarType superType) = EnvVarType (typeshiftplus v superType)

shiftOverVarType :: Type -> Env -> Env
shiftOverVarType superType = map (shiftEnvItem (SVarType Z)) . (EnvVarType superType:)

shiftOverVarValue :: Type -> Env -> Env
shiftOverVarValue t = map (shiftEnvItem (SVarValue Z)) . (EnvVarValue t:)

The same interface for the String implementation:

type Env = Map.Map String Type

emptyEnv :: Env
emptyEnv = Map.empty

getVarValueFromEnv :: Variable -> Env -> Maybe Type
getVarValueFromEnv (SVarValue svv) = Map.lookup svv
getVarValueFromEnv (SVarType svt) = error "this var is not a VarValue"

getVarTypeFromEnv :: Variable -> Env -> Maybe Type
getVarTypeFromEnv (SVarValue svv) = error "this var is not a VarType"
getVarTypeFromEnv (SVarType svt) = Map.lookup svt

shiftOverVarValue :: Variable -> Type -> Env -> Env
shiftOverVarValue (SVarValue svv) typ = Map.insert svv typ -- replacement ensures that inner variables hide outer variables with the same name
shiftOverVarValue (SVarType svt) typ = error "the given var is not a VarValue"

shiftOverVarType :: Variable -> Type -> Env -> Env
shiftOverVarType (SVarValue svv) typ = error "the given var is not a VarType"
shiftOverVarType (SVarType svt) typ = Map.insert svt typ -- replacement ensures that inner variables hide outer variables with the same name

Specification:

namespace VarValue: Term
namespace VarType: Type

sort Term
  inh ctx VarValue
  inh tctx VarType
  | TmVariable (x@ctx)
  | TmApply (t1: Term) (t2: Term)
  | TmTypeApply (t1: Term) (t2: Type)
  | Abstraction (t: Term) (typ: Type) [z: VarValue]
    t.ctx = lhs.vctx, z
    t.tctx = lhs.vtctx
    typ.tyctx = lhs.vtctx
  | TypeAbstraction (typeTerm: Term) (superType: Type) [z: VarType]
    typeTerm.ctx = lhs.vctx
    typeTerm.tctx = lhs.vtctx, z
    superType.tyctx = lhs.vtctx

sort Type
  inh tyctx VarType
  | TypVariable (t@tyctx)
  | TypFunction (from: Type) (to: Type)
  | TypUniversal (on: Type) (superType: Type) [t: VarType]
    on.tyctx = lhs.tyctx, t
    superType.tyctx = lhs.tyctx

the getXFromEnv and shiftOverX functions are certainly within the realm of possibilities to implement. Though how complex this might get for advanced combinations of (perhaps even synthetic) contexts I do not know. And since the tool knows how these contexts are used (especially which modifications to the environment are allowed) it can generate only the neccesary functions.

Of cource, there is still an API difference between the DeBruijn and String implementations, as in the DeBruijn implementation there is the implicit variable name 'Z', whereas this needs to be explicitly supplied for String, but I defer solving this to #4