Module ErgoSpec.ErgoC.Lang.ErgoCTypecheckContext

Require Import String.
Require Import List.

Require Import ErgoSpec.Backend.QLib.
Require Import ErgoSpec.Common.Names.

Section ErgoCTypecheckContext.
  Context {br : brand_relation}.
  Import QcertType.

  Record type_context :=
    mkEvalContext
      { type_context_global_env : list (string * ergoc_type);
        type_context_local_env : list (string * ergoc_type);
      }.

  Definition type_context_update_global_env
             (ctxt : type_context)
             (name : string)
             (value : ergoc_type) : type_context :=
    mkEvalContext ((name, value)::ctxt.(type_context_global_env))
                  ctxt.(type_context_local_env).

  Definition type_context_update_local_env
             (ctxt : type_context)
             (name : string)
             (value : ergoc_type) : type_context :=
    mkEvalContext ctxt.(type_context_global_env)
                  ((name, value)::ctxt.(type_context_local_env)).

  Definition type_context_set_local_env
             (ctxt : type_context)
             (new_local_env : list (string * ergoc_type)) : type_context :=
    mkEvalContext ctxt.(type_context_global_env)
                  new_local_env.

  Definition empty_type_context :=
    mkEvalContext ((options,tbrand (default_options::nil))
                      ::(current_time,tdateTime)
                      ::(this_contract,tunit)
                      ::(this_state,tunit)
                      ::(this_emit,tcoll tbottom)
                      ::nil)
                   (nil).
  
End ErgoCTypecheckContext.