Module Qcert.Data.ModelTyping.ForeignDataTyping
Require
Import
Utils
.
Require
Import
ForeignData
.
Require
Import
DataModel
.
Require
Import
Types
.
Section
ForeignDataTyping
.
Class
foreign_data_typing
{
fdata
:
foreign_data
}
{
ftype
:
foreign_type
}
:
Type
:=
mk_foreign_data_typing
{
foreign_data_typing_has_type
(
d
:
foreign_data_model
)
(τ:
foreign_type_type
) :
Prop
;
foreign_data_typing_normalized
{
d
:
foreign_data_model
}
{τ:
foreign_type_type
} :
foreign_data_typing_has_type
d
τ ->
foreign_data_normalized
d
;
foreign_data_typing_subtype
{
d
:
foreign_data_model
}
{τ₁ τ₂:
foreign_type_type
} :
foreign_data_typing_has_type
d
τ₁ ->
τ₁ ≤ τ₂ ->
foreign_data_typing_has_type
d
τ₂
;
foreign_data_typing_meet
{
d
:
foreign_data_model
}
{τ₁ τ₂:
foreign_type_type
} :
foreign_data_typing_has_type
d
τ₁ ->
foreign_data_typing_has_type
d
τ₂ ->
foreign_data_typing_has_type
d
(τ₁ ⊓ τ₂)
;
foreign_data_typing_infer
(
d
:
foreign_data_model
)
:
option
foreign_type_type
;
foreign_data_typing_infer_normalized
{
d
} :
foreign_data_normalized
d
->
{τ |
foreign_data_typing_infer
d
=
Some
τ}
;
foreign_data_typing_infer_correct
{
d
τ} :
foreign_data_typing_infer
d
=
Some
τ ->
foreign_data_typing_has_type
d
τ
;
foreign_data_typing_infer_least
{
d
τ₁ τ₂} :
foreign_data_typing_infer
d
=
Some
τ₁ ->
foreign_data_typing_has_type
d
τ₂ ->
τ₁ ≤ τ₂
}.
Theorem
foreign_data_typing_infer_complete
{
fdata
:
foreign_data
}
{
ftype
:
foreign_type
}
{
ftyping
:
foreign_data_typing
}
{
d
τ} :
foreign_data_typing_has_type
d
τ -> {τ' |
foreign_data_typing_infer
d
=
Some
τ'}.
Proof.
intros
.
apply
foreign_data_typing_infer_normalized
.
apply
foreign_data_typing_normalized
in
H
.
trivial
.
Qed.
End
ForeignDataTyping
.