Module TNRAEnv
Section
TNRAEnv
.
Require
Import
String
.
Require
Import
List
.
Require
Import
Compare_dec
.
Require
Import
Program
.
Require
Import
Utils
BasicSystem
.
Require
Import
cNRAEnv
TcNRAEnv
.
Require
Import
NRAEnv
NRAEnvEq
.
Local
Open
Scope
nraenv_scope
.
Typing for NRA
Section
typ
.
Context
{
m
:
basic_model
}.
Context
(τ
constants
:
list
(
string
*
rtype
)).
Definition
nraenv_type
(
q
:
nraenv
) :
rtype
->
rtype
->
rtype
->
Prop
:=
@
nraenv_core_type
m
τ
constants
(
nraenv_core_of_nraenv
q
).
End
typ
.
Notation
"
Op
▷ₓ
A
>=>
B
⊣
C
;
E
" := (
nraenv_type
C
Op
E
A
B
) (
at
level
70).
Type lemmas for individual algebraic expressions
Section
prop
.
Context
{
m
:
basic_model
}.
Main typing soundness theorem for the NRA
Lemma
typed_nraenv_yields_typed_nraenv_core
{τ
c
τ
env
τ
in
τ
out
} (
op
:
nraenv
):
(
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
) ->
nraenv_core_type
τ
c
(
nraenv_core_of_nraenv
op
) τ
env
τ
in
τ
out
.
Proof.
unfold
nraenv_type
;
intro
;
assumption
.
Qed.
Lemma
typed_nraenv_core_yields_typed_nraenv
{τ
c
τ
env
τ
in
τ
out
} (
op
:
nraenv
):
nraenv_core_type
τ
c
(
nraenv_core_of_nraenv
op
) τ
env
τ
in
τ
out
-> (
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
).
Proof.
revert
τ
in
τ
out
τ
env
.
induction
op
;
intros
;
Takes care of all core operators *)
unfold
nraenv_type
;
assumption
;
try
(
solve
[
inversion
H
;
clear
H
;
subst
;
repeat
econstructor
;
eauto
]).
Qed.
Theorem
typed_nraenv_core_iff_typed_nraenv
{τ
c
τ
env
τ
in
τ
out
} (
op
:
nraenv
):
(
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
) <->
nraenv_core_type
τ
c
(
nraenv_core_of_nraenv
op
) τ
env
τ
in
τ
out
.
Proof.
split
.
apply
typed_nraenv_yields_typed_nraenv_core
.
apply
typed_nraenv_core_yields_typed_nraenv
.
Qed.
Theorem
typed_nraenv_yields_typed_data
{τ
c
τ
env
τ
in
τ
out
}
c
(
env
:
data
) (
d
:
data
) (
op
:
nraenv
):
bindings_type
c
τ
c
->
(
env
▹ τ
env
) -> (
d
▹ τ
in
) -> (
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
) ->
(
exists
x
, (
nraenv_eval
brand_relation_brands
c
op
env
d
=
Some
x
/\ (
x
▹ τ
out
))).
Proof.
intros
.
unfold
nraenv_eval
.
apply
(@
typed_nraenv_core_yields_typed_data
m
τ
c
τ
env
τ
in
τ
out
);
try
assumption
.
Qed.
Corrolaries of the main type soudness theorem
Definition
typed_nraenv_total
{τ
c
τ
env
τ
in
τ
out
} (
op
:
nraenv
) (
HOpT
:
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
)
c
(
env
:
data
) (
d
:
data
):
bindings_type
c
τ
c
->
(
env
▹ τ
env
) ->
(
d
▹ τ
in
) ->
{
x
:
data
|
x
▹ τ
out
}.
Proof.
intros
Hc
Henv
.
intros
HdT
.
generalize
(
typed_nraenv_yields_typed_data
c
env
d
op
Hc
Henv
HdT
HOpT
).
intros
.
destruct
(
nraenv_eval
brand_relation_brands
c
op
env
d
).
assert
(
data_type
d0
τ
out
).
-
inversion
H
.
inversion
H0
.
inversion
H1
.
trivial
.
-
exists
d0
.
trivial
.
-
cut
False
.
intuition
.
inversion
H
.
destruct
H0
.
inversion
H0
.
Defined.
Definition
tnraenv_eval
{τ
c
τ
env
τ
in
τ
out
} (
op
:
nraenv
) (
HOpT
:
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
)
c
(
env
:
data
) (
d
:
data
):
bindings_type
c
τ
c
->
(
env
▹ τ
env
) -> (
d
▹ τ
in
) ->
data
.
Proof.
intros
Hc
Henv
.
intros
HdT
.
destruct
(
typed_nraenv_total
op
HOpT
c
env
d
Hc
Henv
HdT
).
exact
x
.
Defined.
End
prop
.
End
TNRAEnv
.
Notation
"
Op
▷ₓ
A
>=>
B
⊣
C
;
E
" := (
nraenv_type
C
Op
E
A
B
) (
at
level
70).
Notation
"
Op
@▷ₓ
d
⊣
C
;
e
" := (
tnraenv_eval
C
Op
e
d
) (
at
level
70).
Hint
Unfold
nraenv_type
.
Hint
Constructors
unaryOp_type
.
Hint
Constructors
binOp_type
.
Ltac
nraenv_inferer
:=
unfold
nraenv_type
in
*;
unfold
nraenv_eval
;
simpl
in
*;
try
nraenv_core_inverter
;
subst
;
try
eauto
.
Ltac
nraenv_input_well_typed
:=
repeat
progress
match
goal
with
| [
HO
:?
op
▷ₓ ?τ
in
>=> ?τ
out
⊣ ?τ
c
; ?τ
env
,
HI
:?
x
▹ ?τ
in
,
HE
:?
env
▹ ?τ
env
,
HC
:
bindings_type
?
c
?τ
c
|-
context
[(
nraenv_eval
?
h
?
c
?
op
?
env
?
x
)]] =>
let
xout
:=
fresh
"
dout
"
in
let
xtype
:=
fresh
"τ
out
"
in
let
xeval
:=
fresh
"
eout
"
in
destruct
(
typed_nraenv_yields_typed_data
_
_
_
op
HC
HE
HI
HO
)
as
[
xout
[
xeval
xtype
]];
rewrite
xeval
in
*;
simpl
end
;
input_well_typed
.