Library Coq.micromega.VarMap
Require
Import
ZArith_base
.
Require
Import
Coq.Arith.Max
.
Require
Import
List
.
Set Implicit Arguments
.
Inductive
t
{
A
} :
Type
:=
|
Empty
:
t
|
Elt
:
A
->
t
|
Branch
:
t
->
A
->
t
->
t
.
Section
MakeVarMap
.
Variable
A
:
Type
.
Variable
default
:
A
.
Notation
t
:= (
t
A
).
Fixpoint
find
(
vm
:
t
) (
p
:
positive
) {
struct
vm
} :
A
:=
match
vm
with
|
Empty
=>
default
|
Elt
i
=>
i
|
Branch
l
e
r
=>
match
p
with
|
xH
=>
e
|
xO
p
=>
find
l
p
|
xI
p
=>
find
r
p
end
end
.
Fixpoint
singleton
(
x
:
positive
) (
v
:
A
) :
t
:=
match
x
with
|
xH
=>
Elt
v
|
xO
p
=>
Branch
(
singleton
p
v
)
default
Empty
|
xI
p
=>
Branch
Empty
default
(
singleton
p
v
)
end
.
Fixpoint
vm_add
(
x
:
positive
) (
v
:
A
) (
m
:
t
) {
struct
m
} :
t
:=
match
m
with
|
Empty
=>
singleton
x
v
|
Elt
vl
=>
match
x
with
|
xH
=>
Elt
v
|
xO
p
=>
Branch
(
singleton
p
v
)
vl
Empty
|
xI
p
=>
Branch
Empty
vl
(
singleton
p
v
)
end
|
Branch
l
o
r
=>
match
x
with
|
xH
=>
Branch
l
v
r
|
xI
p
=>
Branch
l
o
(
vm_add
p
v
r
)
|
xO
p
=>
Branch
(
vm_add
p
v
l
)
o
r
end
end
.
End
MakeVarMap
.