Module ImpPrelude
Require
Export
String
.
Require
Export
List
.
Require
Extraction
.
Require
Import
Ascii
.
Require
Import
BinNums
.
Require
Export
ImpCore
.
Require
Export
PArith
.
Import
Notations
.
Local
Open
Scope
impure
.
Impure lazy andb of booleans
Definition
iandb
(
k1
k2
: ??
bool
): ??
bool
:=
DO
r1
<~
k1
;;
if
r1
then
k2
else
RET
false
.
Extraction
Inline
iandb
.
Strings for pretty-printing
Axiom
caml_string
:
Type
.
Extract
Constant
caml_string
=> "
string
".
Definition
nl
:
string
:=
String
(
ascii_of_pos
10%
positive
)
EmptyString
.
Inductive
pstring
:
Type
:=
|
Str
:
string
->
pstring
|
CamlStr
:
caml_string
->
pstring
|
Concat
:
pstring
->
pstring
->
pstring
.
Coercion
Str
:
string
>->
pstring
.
Bind
Scope
string_scope
with
pstring
.
Notation
"
x
+;
y
" := (
Concat
x
y
)
(
at
level
65,
left
associativity
):
string_scope
.
Coq references
Record
cref
{
A
} := {
set
:
A
-> ??
unit
;
get
:
unit
-> ??
A
}.
Arguments
cref
:
clear
implicits
.
Axiom
make_cref
:
forall
{
A
},
A
-> ??
cref
A
.
Extract
Constant
make_cref
=> "(
fun
x
->
let
r
=
ref
x
in
{
set
= (
fun
y
->
r
:=
y
);
get
= (
fun
() -> !
r
) })".
Data-structure for a logger
Record
logger
{
A
:
Type
} := {
log_insert
:
A
-> ??
unit
;
log_info
:
unit
-> ??
pstring
;
}.
Arguments
logger
:
clear
implicits
.
Axiom
count_logger
:
unit
-> ??
logger
unit
.
Extract
Constant
count_logger
=> "(
fun
() ->
let
count
=
ref
0
in
{
log_insert
= (
fun
() ->
count
:= !
count
+ 1);
log_info
= (
fun
() -> (
CamlStr
(
string_of_int
!
count
))) })".
Axioms of Physical equality
Axiom
phys_eq
:
forall
{
A
},
A
->
A
-> ??
bool
.
Axiom
phys_eq_correct
:
forall
A
(
x
y
:
A
),
WHEN
phys_eq
x
y
~>
b
THEN
b
=
true
->
x
=
y
.
Module
PhysEqModel
.
Definition
phys_eq
{
A
} (
x
y
:
A
) :=
ret
false
.
Lemma
phys_eq_correct
:
forall
A
(
x
y
:
A
),
WHEN
phys_eq
x
y
~>
b
THEN
b
=
true
->
x
=
y
.
Proof.
wlp_simplify
.
discriminate
.
Qed.
End
PhysEqModel
.
Extract
Inlined
Constant
phys_eq
=> "(==)".
Hint
Resolve
phys_eq_correct
:
wlp
.
Axiom
struct_eq
:
forall
{
A
},
A
->
A
-> ??
bool
.
Axiom
struct_eq_correct
:
forall
A
(
x
y
:
A
),
WHEN
struct_eq
x
y
~>
b
THEN
if
b
then
x
=
y
else
x
<>
y
.
Extract
Inlined
Constant
struct_eq
=> "(=)".
Hint
Resolve
struct_eq_correct
:
wlp
.
Data-structure for generic hash-consing
Axiom
hashcode
:
Type
.
Extract
Constant
hashcode
=> "
int
".
Axiom
hash_older
:
hashcode
->
hashcode
-> ??
bool
.
Extract
Inlined
Constant
hash_older
=> "(<)".
Module
Dict
.
Record
hash_params
{
A
:
Type
} := {
test_eq
:
A
->
A
-> ??
bool
;
test_eq_correct
:
forall
x
y
,
WHEN
test_eq
x
y
~>
r
THEN
r
=
true
->
x
=
y
;
hashing
:
A
-> ??
hashcode
;
log
:
A
-> ??
unit
}.
Arguments
hash_params
:
clear
implicits
.
Record
t
{
A
B
:
Type
} := {
set
:
A
*
B
-> ??
unit
;
get
:
A
-> ??
option
B
}.
Arguments
t
:
clear
implicits
.
End
Dict
.
Module
HConsingDefs
.
Record
hashinfo
{
A
:
Type
} := {
hdata
:
A
;
hcodes
:
list
hashcode
;
}.
Arguments
hashinfo
:
clear
implicits
.
Record
hashP
{
A
:
Type
}:= {
hash_eq
:
A
->
A
-> ??
bool
;
get_hid
:
A
->
hashcode
;
set_hid
:
A
->
hashcode
->
A
;
}.
Arguments
hashP
:
clear
implicits
.
Axiom
unknown_hid
:
hashcode
.
Extract
Constant
unknown_hid
=> "-1".
Definition
ignore_hid
{
A
} (
hp
:
hashP
A
) (
hv
:
A
) :=
set_hid
hp
hv
unknown_hid
.
Record
hashExport
{
A
:
Type
}:= {
get_info
:
hashcode
-> ??
hashinfo
A
;
iterall
: ((
list
pstring
) ->
hashcode
->
hashinfo
A
-> ??
unit
) -> ??
unit
;
}.
Arguments
hashExport
:
clear
implicits
.
Record
hashConsing
{
A
:
Type
}:= {
hC
:
hashinfo
A
-> ??
A
;
next_hid
:
unit
-> ??
hashcode
;
remove
:
hashinfo
A
-> ??
unit
;
next_log
:
pstring
-> ??
unit
;
export
:
unit
-> ??
hashExport
A
;
}.
Arguments
hashConsing
:
clear
implicits
.
End
HConsingDefs
.
recMode: this is mainly for Tests !
Inductive
recMode
:=
StdRec
|
MemoRec
|
BareRec
|
BuggyRec
.
Lemma
modusponens
:
forall
(
P
Q
:
Prop
),
P
-> (
P
->
Q
) ->
Q
.
Proof.
auto
. Qed.
Ltac
exploit
x
:=
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
_
)
_
)
||
refine
(
modusponens
_
_
(
x
_
)
_
).