Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
1f836cd2
Commit
1f836cd2
authored
Nov 09, 2010
by
François Bobot
Browse files
add open stdlib where needed
parent
231fc690
Changes
11
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
1f836cd2
...
...
@@ -112,7 +112,7 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml
\
src/driver/driver_lexer.ml
LIB_UTIL
=
exn_printer debug pp loc print_tree
\
LIB_UTIL
=
stdlib
exn_printer debug pp loc print_tree
\
hashweak hashcons util sysutil rc
LIB_CORE
=
ident ty term pattern decl theory task pretty
env
printer trans
...
...
src/core/decl.mli
View file @
1f836cd2
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open
Stdlib
(** Logic Declarations *)
open
Ident
...
...
src/core/ident.ml
View file @
1f836cd2
...
...
@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open
Stdlib
open
Util
(** Labels *)
...
...
src/core/ident.mli
View file @
1f836cd2
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open
Stdlib
(** Identifiers *)
(** {2 Labels} *)
...
...
src/core/term.mli
View file @
1f836cd2
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open
Stdlib
(** Terms and Formulas *)
open
Ident
...
...
src/core/theory.mli
View file @
1f836cd2
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open
Stdlib
(** Theories and Namespaces *)
open
Ident
...
...
src/core/ty.mli
View file @
1f836cd2
...
...
@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open
Stdlib
open
Ident
(** Types *)
...
...
src/util/
map
.ml
→
src/util/
stdlib
.ml
View file @
1f836cd2
...
...
@@ -13,6 +13,8 @@
(* $Id: map.ml 10468 2010-05-25 13:29:43Z frisch $ *)
module
Map
=
struct
module
type
OrderedType
=
sig
type
t
...
...
@@ -29,7 +31,8 @@ module type S =
val
add
:
key
->
'
a
->
'
a
t
->
'
a
t
val
singleton
:
key
->
'
a
->
'
a
t
val
remove
:
key
->
'
a
t
->
'
a
t
val
merge
:
(
key
->
'
a
option
->
'
b
option
->
'
c
option
)
->
'
a
t
->
'
b
t
->
'
c
t
val
merge
:
(
key
->
'
a
option
->
'
b
option
->
'
c
option
)
->
'
a
t
->
'
b
t
->
'
c
t
val
compare
:
(
'
a
->
'
a
->
int
)
->
'
a
t
->
'
a
t
->
int
val
equal
:
(
'
a
->
'
a
->
bool
)
->
'
a
t
->
'
a
t
->
bool
val
iter
:
(
key
->
'
a
->
unit
)
->
'
a
t
->
unit
...
...
@@ -124,23 +127,23 @@ module Make(Ord: OrderedType) = struct
let
rec
mem
x
=
function
Empty
->
false
|
Node
(
l
,
v
,
d
,
r
,
_
)
->
|
Node
(
l
,
v
,
_
d
,
r
,
_
)
->
let
c
=
Ord
.
compare
x
v
in
c
=
0
||
mem
x
(
if
c
<
0
then
l
else
r
)
let
rec
min_binding
=
function
Empty
->
raise
Not_found
|
Node
(
Empty
,
x
,
d
,
r
,
_
)
->
(
x
,
d
)
|
Node
(
l
,
x
,
d
,
r
,
_
)
->
min_binding
l
|
Node
(
Empty
,
x
,
d
,
_
r
,
_
)
->
(
x
,
d
)
|
Node
(
l
,
_
x
,
_
d
,
_
r
,
_
)
->
min_binding
l
let
rec
max_binding
=
function
Empty
->
raise
Not_found
|
Node
(
l
,
x
,
d
,
Empty
,
_
)
->
(
x
,
d
)
|
Node
(
l
,
x
,
d
,
r
,
_
)
->
max_binding
r
|
Node
(
_
l
,
x
,
d
,
Empty
,
_
)
->
(
x
,
d
)
|
Node
(
_
l
,
_
x
,
_
d
,
r
,
_
)
->
max_binding
r
let
rec
remove_min_binding
=
function
Empty
->
invalid_arg
"Map.remove_min_elt"
|
Node
(
Empty
,
x
,
d
,
r
,
_
)
->
r
|
Node
(
Empty
,
_
x
,
_
d
,
r
,
_
)
->
r
|
Node
(
l
,
x
,
d
,
r
,
_
)
->
bal
(
remove_min_binding
l
)
x
d
r
let
merge
t1
t2
=
...
...
@@ -154,7 +157,7 @@ module Make(Ord: OrderedType) = struct
let
rec
remove
x
=
function
Empty
->
Empty
|
Node
(
l
,
v
,
d
,
r
,
h
)
->
|
Node
(
l
,
v
,
d
,
r
,
_
h
)
->
let
c
=
Ord
.
compare
x
v
in
if
c
=
0
then
merge
l
r
...
...
@@ -211,7 +214,8 @@ module Make(Ord: OrderedType) = struct
let
rec
part
(
t
,
f
as
accu
)
=
function
|
Empty
->
accu
|
Node
(
l
,
v
,
d
,
r
,
_
)
->
part
(
part
(
if
p
v
d
then
(
add
v
d
t
,
f
)
else
(
t
,
add
v
d
f
))
l
)
r
in
part
(
part
(
if
p
v
d
then
(
add
v
d
t
,
f
)
else
(
t
,
add
v
d
f
))
l
)
r
in
part
(
Empty
,
Empty
)
s
(* Same as create and bal, but no assumptions are made on the
...
...
@@ -260,7 +264,7 @@ module Make(Ord: OrderedType) = struct
|
(
Node
(
l1
,
v1
,
d1
,
r1
,
h1
)
,
_
)
when
h1
>=
height
s2
->
let
(
l2
,
d2
,
r2
)
=
split
v1
s2
in
concat_or_join
(
merge
f
l1
l2
)
v1
(
f
v1
(
Some
d1
)
d2
)
(
merge
f
r1
r2
)
|
(
_
,
Node
(
l2
,
v2
,
d2
,
r2
,
h2
))
->
|
(
_
,
Node
(
l2
,
v2
,
d2
,
r2
,
_
h2
))
->
let
(
l1
,
d1
,
r1
)
=
split
v2
s1
in
concat_or_join
(
merge
f
l1
l2
)
v2
(
f
v2
d1
(
Some
d2
))
(
merge
f
r1
r2
)
|
_
->
...
...
@@ -312,3 +316,5 @@ module Make(Ord: OrderedType) = struct
let
choose
=
min_binding
end
end
src/util/
map
.mli
→
src/util/
stdlib
.mli
View file @
1f836cd2
...
...
@@ -13,6 +13,8 @@
(* $Id: map.mli 10483 2010-05-31 12:48:13Z doligez $ *)
module
Map
:
sig
(** Association tables over ordered types.
This module implements applicative association tables, also known as
...
...
@@ -192,3 +194,5 @@ module type S =
module
Make
(
Ord
:
OrderedType
)
:
S
with
type
key
=
Ord
.
t
(** Functor building an implementation of the map structure
given a totally ordered type. *)
end
src/util/util.ml
View file @
1f836cd2
...
...
@@ -16,7 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open
Stdlib
(* useful combinators *)
let
(
$
)
f
x
=
f
x
...
...
src/util/util.mli
View file @
1f836cd2
...
...
@@ -16,7 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open
Stdlib
(** Useful functions *)
val
(
$
)
:
(
'
a
->
'
b
)
->
'
a
->
'
b
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment