Module Backend
Require
Import
String
.
Require
Import
NumC
.
Require
Import
ProgVar
.
Require
Import
LinTerm
.
Require
Import
CstrC
.
Require
Import
CertC
.
Require
Import
ConsSet
.
Require
Export
ImpureConfig
.
Axiom
t
:
Set
.
Inductive
bndT
:
Set
:=
|
Infty
:
bndT
|
Open
:
QNum.t
->
Cert.frag_t
->
bndT
|
Closed
:
QNum.t
->
Cert.frag_t
->
bndT
.
Record
itvT
:
Set
:=
mk
{
low
:
bndT
;
up
:
bndT
}.
Inductive
addPrecT
:
Set
:=
Added
:
t
->
Cert.t
*
Cert.t
->
addPrecT
|
Contrad
:
Cert.t
->
addPrecT
.
Axiom
freshId
:
t
->
imp
Cert.id_t
.
Axiom
top
:
t
.
Axiom
isEmpty
:
t
->
imp
(
option
Cert.t
).
Axiom
isIncl
:
t
*
t
->
imp
(
option
Cert.t
).
Axiom
add
:
t
*
Cstr.t
->
imp
(
option
t
*
Cert.t
).
Axiom
addp
:
t
*
Cstr.t
->
imp
addPrecT
.
Axiom
meet
:
t
*
t
->
imp
(
option
t
*
Cert.meetT
).
Axiom
join
:
t
*
t
->
imp
(
t
*
Cert.joinT
).
Axiom
widen
:
t
*
t
->
imp
(
t
*
Cs.t
).
Axiom
getItv
:
t
*
LinQ.t
->
imp
itvT
.
Axiom
getUpperBound
:
t
*
LinQ.t
->
imp
bndT
.
Axiom
getLowerBound
:
t
*
LinQ.t
->
imp
bndT
.
Axiom
project
:
t
*
PVar.t
->
imp
(
t
*
Cert.t
).
Axiom
rename
:
PVar.t
*
PVar.t
*
t
->
imp
t
.
Axiom
pr
:
t
->
string
.