Module ErgoSpec.ErgoC.Lang.ErgoCTypeContext
Require
Import
String
.
Require
Import
List
.
Require
Import
ErgoSpec.Backend.ErgoBackend
.
Require
Import
ErgoSpec.Common.Utils.Names
.
Require
Import
ErgoSpec.ErgoC.Lang.ErgoC
.
Section
ErgoCTypeContext
.
Context
{
br
:
brand_relation
}.
Import
ErgoCTypes
.
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
((
current_time
,
tdateTime
)
::(
this_contract
,
tunit
)
::(
this_state
,
tunit
)
::(
this_emit
,
tcoll
tbottom
)
::
nil
)
(
nil
).
End
ErgoCTypeContext
.