Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
58fbf6cb
Commit
58fbf6cb
authored
Oct 21, 2012
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
move option utilities from Util to Opt
+ rename Debug.Opt to Debug.Args to avoid conflicts
parent
4468018f
Changes
63
Hide whitespace changes
Inline
Side-by-side
Showing
63 changed files
with
348 additions
and
329 deletions
+348
-329
Makefile.in
Makefile.in
+1
-1
examples/runstrat/runstrat.ml
examples/runstrat/runstrat.ml
+5
-5
plugins/tptp/tptp_typing.ml
plugins/tptp/tptp_typing.ml
+16
-16
src/coq-tactic/why3tac.ml
src/coq-tactic/why3tac.ml
+3
-3
src/core/decl.ml
src/core/decl.ml
+10
-10
src/core/pattern.ml
src/core/pattern.ml
+1
-1
src/core/pretty.ml
src/core/pretty.ml
+2
-2
src/core/task.ml
src/core/task.ml
+5
-5
src/core/term.ml
src/core/term.ml
+3
-3
src/core/theory.ml
src/core/theory.ml
+5
-5
src/core/ty.ml
src/core/ty.ml
+6
-6
src/driver/autodetection.ml
src/driver/autodetection.ml
+2
-2
src/driver/call_provers.ml
src/driver/call_provers.ml
+1
-1
src/driver/driver.ml
src/driver/driver.ml
+2
-2
src/driver/whyconf.ml
src/driver/whyconf.ml
+5
-5
src/ide/gmain.ml
src/ide/gmain.ml
+7
-7
src/ide/replay.ml
src/ide/replay.ml
+7
-7
src/main.ml
src/main.ml
+16
-16
src/parser/denv.ml
src/parser/denv.ml
+2
-2
src/parser/lexer.mll
src/parser/lexer.mll
+1
-1
src/parser/typing.ml
src/parser/typing.ml
+11
-11
src/printer/alt_ergo.ml
src/printer/alt_ergo.ml
+2
-2
src/printer/coq.ml
src/printer/coq.ml
+2
-2
src/printer/cvc3.ml
src/printer/cvc3.ml
+2
-2
src/printer/pvs.ml
src/printer/pvs.ml
+2
-2
src/printer/why3printer.ml
src/printer/why3printer.ml
+1
-1
src/printer/yices.ml
src/printer/yices.ml
+1
-1
src/programs/pgm_typing.ml
src/programs/pgm_typing.ml
+26
-26
src/programs/pgm_wp.ml
src/programs/pgm_wp.ml
+2
-2
src/session/session.ml
src/session/session.ml
+10
-10
src/session/session_scheduler.ml
src/session/session_scheduler.ml
+1
-1
src/transform/eliminate_algebraic.ml
src/transform/eliminate_algebraic.ml
+8
-8
src/transform/encoding_decoexp.ml
src/transform/encoding_decoexp.ml
+2
-2
src/transform/encoding_decorate.ml
src/transform/encoding_decorate.ml
+2
-2
src/transform/encoding_explicit.ml
src/transform/encoding_explicit.ml
+2
-2
src/transform/encoding_guard.ml
src/transform/encoding_guard.ml
+4
-4
src/transform/encoding_instantiate.ml
src/transform/encoding_instantiate.ml
+4
-4
src/transform/encoding_sort.ml
src/transform/encoding_sort.ml
+3
-3
src/transform/encoding_twin.ml
src/transform/encoding_twin.ml
+1
-1
src/transform/eval_match.ml
src/transform/eval_match.ml
+1
-1
src/transform/libencoding.ml
src/transform/libencoding.ml
+1
-1
src/transform/simplify_recursive_definition.ml
src/transform/simplify_recursive_definition.ml
+1
-1
src/util/debug.ml
src/util/debug.ml
+2
-2
src/util/debug.mli
src/util/debug.mli
+1
-1
src/util/opt.ml
src/util/opt.ml
+44
-0
src/util/opt.mli
src/util/opt.mli
+39
-0
src/util/util.ml
src/util/util.ml
+0
-34
src/util/util.mli
src/util/util.mli
+0
-29
src/util/warning.ml
src/util/warning.ml
+1
-2
src/why3bench/benchrc.ml
src/why3bench/benchrc.ml
+2
-2
src/why3bench/why3bench.ml
src/why3bench/why3bench.ml
+8
-8
src/why3config/why3config.ml
src/why3config/why3config.ml
+7
-7
src/why3session/why3session_info.ml
src/why3session/why3session_info.ml
+1
-1
src/why3session/why3session_lib.ml
src/why3session/why3session_lib.ml
+5
-5
src/whyml/mlw_decl.ml
src/whyml/mlw_decl.ml
+4
-4
src/whyml/mlw_dty.ml
src/whyml/mlw_dty.ml
+1
-1
src/whyml/mlw_expr.ml
src/whyml/mlw_expr.ml
+10
-10
src/whyml/mlw_module.ml
src/whyml/mlw_module.ml
+4
-4
src/whyml/mlw_ocaml.ml
src/whyml/mlw_ocaml.ml
+7
-7
src/whyml/mlw_pretty.ml
src/whyml/mlw_pretty.ml
+1
-1
src/whyml/mlw_ty.ml
src/whyml/mlw_ty.ml
+5
-5
src/whyml/mlw_typing.ml
src/whyml/mlw_typing.ml
+10
-10
src/whyml/mlw_wp.ml
src/whyml/mlw_wp.ml
+7
-7
No files found.
Makefile.in
View file @
58fbf6cb
...
...
@@ -108,7 +108,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml
\
src/driver/driver_lexer.ml src/session/xml.ml
LIB_UTIL
=
config stdlib exn_printer pp debug loc print_tree
\
LIB_UTIL
=
config
opt
stdlib exn_printer pp debug loc print_tree
\
cmdline hashweak hashcons util warning sysutil rc plugin
LIB_CORE
=
ident ty term pattern decl theory task pretty
env
trans printer
...
...
examples/runstrat/runstrat.ml
View file @
58fbf6cb
...
...
@@ -90,9 +90,9 @@ let option_list = Arg.align [
" same as -m"
;
"-j"
,
Arg
.
Int
(
fun
i
->
opt_j
:=
Some
i
)
,
"<int> Set the number of worker to use (default:1)"
;
Debug
.
Opt
.
desc_debug_list
;
Debug
.
Opt
.
desc_debug_all
;
Debug
.
Opt
.
desc_debug
;
Debug
.
Args
.
desc_debug_list
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug
;
]
type
runnable_prover
=
...
...
@@ -109,12 +109,12 @@ let env,provers = try
let
main
=
get_main
config
in
Whyconf
.
load_plugins
main
;
Debug
.
Opt
.
set_flags_selected
()
;
Debug
.
Args
.
set_flags_selected
()
;
(** listings*)
let
opt_list
=
ref
false
in
opt_list
:=
Debug
.
Opt
.
option_list
()
||
!
opt_list
;
opt_list
:=
Debug
.
Args
.
option_list
()
||
!
opt_list
;
if
!
opt_list
then
exit
0
;
if
Queue
.
is_empty
opt_queue
then
begin
...
...
plugins/tptp/tptp_typing.ml
View file @
58fbf6cb
...
...
@@ -270,7 +270,7 @@ let find_dobj ~loc denv env impl s =
|
_
->
assert
false
(* impossible *)
let
ty_check
loc
s
ty1
t
=
Loc
.
try3
loc
ty_match
s
ty1
(
of_option
t
.
t_ty
)
Loc
.
try3
loc
ty_match
s
ty1
(
Opt
.
get
t
.
t_ty
)
let
rec
ty
denv
env
impl
{
e_loc
=
loc
;
e_node
=
n
}
=
match
n
with
|
Eapp
(
aw
,
al
)
->
...
...
@@ -303,7 +303,7 @@ let rec term denv env impl { e_loc = loc; e_node = n } = match n with
|
Enum
(
Nint
s
)
->
t_int_const
s
|
Enum
(
Nreal
(
i
,
f
,
e
))
->
t_real_const
(
RConstDecimal
(
i
,
Util
.
def_option
"0"
f
,
e
))
t_real_const
(
RConstDecimal
(
i
,
Opt
.
get_def
"0"
f
,
e
))
|
Enum
(
Nrat
(
n
,
d
))
->
let
n
=
t_int_const
n
and
d
=
t_int_const
d
in
let
frac
=
ns_find_ls
denv
.
th_rat
.
th_export
[
"frac"
]
in
...
...
@@ -314,7 +314,7 @@ let rec term denv env impl { e_loc = loc; e_node = n } = match n with
begin
match
Mstr
.
find
s
env
with
|
SletF
([]
,_,
[]
,
t
)
->
let
id
=
id_user
s
def
.
e_loc
in
let
vs
=
create_vsymbol
id
(
of_option
t
.
t_ty
)
in
let
vs
=
create_vsymbol
id
(
Opt
.
get
t
.
t_ty
)
in
let
env
=
Mstr
.
add
s
(
SVar
vs
)
env
in
let
t1
=
term
denv
env
impl
e
in
t_let_close
vs
t
t1
...
...
@@ -345,7 +345,7 @@ and fmla denv env impl pol tvl { e_loc = loc; e_node = n } = match n with
begin
match
Mstr
.
find
s
env
with
|
SletF
([]
,_,
[]
,
t
)
->
let
id
=
id_user
s
def
.
e_loc
in
let
vs
=
create_vsymbol
id
(
of_option
t
.
t_ty
)
in
let
vs
=
create_vsymbol
id
(
Opt
.
get
t
.
t_ty
)
in
let
env
=
Mstr
.
add
s
(
SVar
vs
)
env
in
let
f
,
b
=
fmla
denv
env
impl
pol
tvl
e
in
t_let_close
vs
t
f
,
b
...
...
@@ -394,8 +394,8 @@ and fmla denv env impl pol tvl { e_loc = loc; e_node = n } = match n with
let
f1
,
b1
=
fmla
denv
env
impl
pol
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
pol
tvl
e2
in
if
b1
||
b2
then
let
g1
,_
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e1
in
let
g2
,_
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e2
in
let
g1
,_
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e1
in
let
g2
,_
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e2
in
t_and
(
t_implies
g1
f2
)
(
t_implies
g2
f1
)
,
true
else
t_iff
f1
f2
,
false
...
...
@@ -403,18 +403,18 @@ and fmla denv env impl pol tvl { e_loc = loc; e_node = n } = match n with
let
f1
,
b1
=
fmla
denv
env
impl
pol
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
pol
tvl
e2
in
if
b1
||
b2
then
let
g1
,_
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e1
in
let
g2
,_
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e2
in
let
g1
,_
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e1
in
let
g2
,_
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e2
in
t_not
(
t_and
(
t_implies
f1
g2
)
(
t_implies
f2
g1
))
,
true
else
t_not
(
t_iff
f1
f2
)
,
false
|
Ebin
(
BOimp
,
e1
,
e2
)
->
let
f1
,
b1
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e1
in
let
f1
,
b1
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
pol
tvl
e2
in
t_implies
f1
f2
,
b1
||
b2
|
Ebin
(
BOpmi
,
e1
,
e2
)
->
let
f1
,
b1
=
fmla
denv
env
impl
pol
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e2
in
let
f2
,
b2
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e2
in
t_implies
f2
f1
,
b1
||
b2
|
Ebin
(
BOand
,
e1
,
e2
)
->
let
f1
,
b1
=
fmla
denv
env
impl
pol
tvl
e1
in
...
...
@@ -425,15 +425,15 @@ and fmla denv env impl pol tvl { e_loc = loc; e_node = n } = match n with
let
f2
,
b2
=
fmla
denv
env
impl
pol
tvl
e2
in
t_or
f1
f2
,
b1
||
b2
|
Ebin
(
BOnand
,
e1
,
e2
)
->
let
f1
,
b1
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e2
in
let
f1
,
b1
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e2
in
t_not
(
t_and
f1
f2
)
,
b1
||
b2
|
Ebin
(
BOnor
,
e1
,
e2
)
->
let
f1
,
b1
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e2
in
let
f1
,
b1
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e1
in
let
f2
,
b2
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e2
in
t_not
(
t_or
f1
f2
)
,
b1
||
b2
|
Enot
e1
->
let
f1
,
b1
=
fmla
denv
env
impl
(
option_
map
not
pol
)
tvl
e1
in
let
f1
,
b1
=
fmla
denv
env
impl
(
Opt
.
map
not
pol
)
tvl
e1
in
t_not
f1
,
b1
|
Eequ
(
e1
,
e2
)
->
let
t1
=
term
denv
env
impl
e1
in
...
...
@@ -499,7 +499,7 @@ and ls_args denv env impl loc fs tvl gl mvs al =
fs_app
denv
.
fs_ghost
[]
(
ty_app
denv
.
ts_ghost
[
Mtv
.
find
v
tvm
])
in
let
tl
=
List
.
map
ghost
gl
@
List
.
map
(
term
denv
env
impl
)
al
in
let
tvm
=
List
.
fold_left2
(
ty_check
loc
)
tvm
fs
.
ls_args
tl
in
let
ty
=
option_
map
(
ty_inst
tvm
)
fs
.
ls_value
in
let
ty
=
Opt
.
map
(
ty_inst
tvm
)
fs
.
ls_value
in
t_app
fs
tl
ty
|
_
->
error
~
loc
BadArity
in
...
...
src/coq-tactic/why3tac.ml
View file @
58fbf6cb
...
...
@@ -560,7 +560,7 @@ and tr_global_ts dep env r =
(* Format.printf "decl = %a@." Pretty.print_decl decl; *)
List
.
iter
(
add_new_decl
dep
!
dep'
)
tl
;
List
.
iter
(
add_dep
dep'
)
tl
;
Util
.
option_
iter
(
add_new_decl
dep
!
dep'
)
decl
;
Opt
.
iter
(
add_new_decl
dep
!
dep'
)
decl
;
lookup_table
global_ts
r
(* the function/predicate symbol for r *)
...
...
@@ -599,14 +599,14 @@ and tr_global_ls dep env r =
let
pl
,
d
=
decompose_definition
dep'
env
c
in
List
.
iter
(
add_new_decl
dep
!
dep'
)
pl
;
List
.
iter
(
add_dep
dep'
)
pl
;
Util
.
option_
iter
(
add_new_decl
dep
!
dep'
)
d
;
Opt
.
iter
(
add_new_decl
dep
!
dep'
)
d
;
lookup_table
global_ls
r
|
IndRef
i
->
assert
(
is_Prop
t
);
let
pl
,
d
=
decompose_inductive
dep'
env
i
in
List
.
iter
(
add_new_decl
dep
!
dep'
)
pl
;
List
.
iter
(
add_dep
dep'
)
pl
;
Util
.
option_
iter
(
add_new_decl
dep
!
dep'
)
d
;
Opt
.
iter
(
add_new_decl
dep
!
dep'
)
d
;
lookup_table
global_ls
r
|
VarRef
_
->
make_one_ls
dep'
env
r
;
...
...
src/core/decl.ml
View file @
58fbf6cb
...
...
@@ -316,7 +316,7 @@ module Hsdecl = Hashcons.Make (struct
type
t
=
decl
let
cs_equal
(
cs1
,
pl1
)
(
cs2
,
pl2
)
=
ls_equal
cs1
cs2
&&
list_all2
(
option_eq
ls_equal
)
pl1
pl2
ls_equal
cs1
cs2
&&
list_all2
(
Opt
.
equal
ls_equal
)
pl1
pl2
let
eq_td
(
ts1
,
td1
)
(
ts2
,
td2
)
=
ts_equal
ts1
ts2
&&
list_all2
cs_equal
td1
td2
...
...
@@ -413,7 +413,7 @@ let syms_ty s ty = ty_s_fold syms_ts s ty
let
syms_term
s
t
=
t_s_fold
syms_ty
syms_ls
s
t
let
create_ty_decl
ts
=
let
syms
=
Util
.
option_
fold
syms_ty
Sid
.
empty
ts
.
ts_def
in
let
syms
=
Opt
.
fold
syms_ty
Sid
.
empty
ts
.
ts_def
in
let
news
=
Sid
.
singleton
ts
.
ts_name
in
mk_decl
(
Dtype
ts
)
syms
news
...
...
@@ -430,7 +430,7 @@ let create_data_decl tdl =
|
Some
ls
->
raise
(
BadRecordField
ls
)
in
let
check_constr
tys
ty
pjs
(
syms
,
news
)
(
fs
,
pl
)
=
ty_equal_check
ty
(
exn_optio
n
(
BadConstructor
fs
)
fs
.
ls_value
);
ty_equal_check
ty
(
Opt
.
get_ex
n
(
BadConstructor
fs
)
fs
.
ls_value
);
let
fs_pjs
=
try
List
.
fold_left2
(
check_proj
fs
ty
)
Sls
.
empty
fs
.
ls_args
pl
with
Invalid_argument
_
->
raise
(
BadConstructor
fs
)
in
...
...
@@ -455,7 +455,7 @@ let create_data_decl tdl =
if
ts
.
ts_def
<>
None
then
raise
(
IllegalTypeAlias
ts
);
let
news
=
news_id
news
ts
.
ts_name
in
let
pjs
=
List
.
fold_left
(
fun
s
(
_
,
pl
)
->
List
.
fold_left
(
option_
fold
(
fun
s
ls
->
Sls
.
add
ls
s
))
s
pl
)
Sls
.
empty
cl
in
(
Opt
.
fold
(
fun
s
ls
->
Sls
.
add
ls
s
))
s
pl
)
Sls
.
empty
cl
in
let
news
=
Sls
.
fold
(
fun
pj
s
->
news_id
s
pj
.
ls_name
)
pjs
news
in
let
ty
=
ty_app
ts
(
List
.
map
ty_var
ts
.
ts_args
)
in
List
.
fold_left
(
check_constr
ts
ty
pjs
)
(
syms
,
news
)
cl
...
...
@@ -464,7 +464,7 @@ let create_data_decl tdl =
mk_decl
(
Ddata
tdl
)
syms
news
let
create_param_decl
ls
=
let
syms
=
Util
.
option_
fold
syms_ty
Sid
.
empty
ls
.
ls_value
in
let
syms
=
Opt
.
fold
syms_ty
Sid
.
empty
ls
.
ls_value
in
let
syms
=
List
.
fold_left
syms_ty
syms
ls
.
ls_args
in
let
news
=
Sid
.
singleton
ls
.
ls_name
in
mk_decl
(
Dparam
ls
)
syms
news
...
...
@@ -494,9 +494,9 @@ let rec f_pos_ps sps pol f = match f.t_node, pol with
|
Tbinop
(
Tiff
,
f
,
g
)
,
_
->
f_pos_ps
sps
None
f
&&
f_pos_ps
sps
None
g
|
Tbinop
(
Timplies
,
f
,
g
)
,
_
->
f_pos_ps
sps
(
option_
map
not
pol
)
f
&&
f_pos_ps
sps
pol
g
f_pos_ps
sps
(
Opt
.
map
not
pol
)
f
&&
f_pos_ps
sps
pol
g
|
Tnot
f
,
_
->
f_pos_ps
sps
(
option_
map
not
pol
)
f
f_pos_ps
sps
(
Opt
.
map
not
pol
)
f
|
Tif
(
f
,
g
,
h
)
,
_
->
f_pos_ps
sps
None
f
&&
f_pos_ps
sps
pol
g
&&
f_pos_ps
sps
pol
h
|
_
->
TermTF
.
t_all
(
t_pos_ps
sps
)
(
f_pos_ps
sps
pol
)
f
...
...
@@ -775,7 +775,7 @@ let parse_record kn fll =
|
[{
ty_node
=
Tyapp
(
ts
,_
)
}]
->
ts
|
_
->
raise
(
BadRecordField
fs
)
in
let
cs
,
pjl
=
match
find_constructors
kn
ts
with
|
[
cs
,
pjl
]
->
cs
,
List
.
map
(
exn_optio
n
(
BadRecordField
fs
))
pjl
|
[
cs
,
pjl
]
->
cs
,
List
.
map
(
Opt
.
get_ex
n
(
BadRecordField
fs
))
pjl
|
_
->
raise
(
BadRecordField
fs
)
in
let
pjs
=
List
.
fold_left
(
fun
s
pj
->
Sls
.
add
pj
s
)
Sls
.
empty
pjl
in
let
flm
=
List
.
fold_left
(
fun
m
(
pj
,
v
)
->
...
...
@@ -797,10 +797,10 @@ let make_record_update kn t fll ty =
let
make_record_pattern
kn
fll
ty
=
let
cs
,
pjl
,
flm
=
parse_record
kn
fll
in
let
s
=
ty_match
Mtv
.
empty
(
of_option
cs
.
ls_value
)
ty
in
let
s
=
ty_match
Mtv
.
empty
(
Opt
.
get
cs
.
ls_value
)
ty
in
let
get_arg
pj
=
match
Mls
.
find_opt
pj
flm
with
|
Some
v
->
v
|
None
->
pat_wild
(
ty_inst
s
(
of_option
pj
.
ls_value
))
|
None
->
pat_wild
(
ty_inst
s
(
Opt
.
get
pj
.
ls_value
))
in
pat_app
cs
(
List
.
map
get_arg
pjl
)
ty
src/core/pattern.ml
View file @
58fbf6cb
...
...
@@ -104,7 +104,7 @@ module Compile (X : Action) = struct
with
NonExhaustive
pl
->
let
find_cs
cs
=
if
Mls
.
mem
cs
types
then
()
else
let
tm
=
ty_match
Mtv
.
empty
(
of_option
cs
.
ls_value
)
ty
in
let
tm
=
ty_match
Mtv
.
empty
(
Opt
.
get
cs
.
ls_value
)
ty
in
let
wild
ty
=
pat_wild
(
ty_inst
tm
ty
)
in
let
pw
=
pat_app
cs
(
List
.
map
wild
cs
.
ls_args
)
ty
in
raise
(
NonExhaustive
(
pw
::
pl
))
...
...
src/core/pretty.ml
View file @
58fbf6cb
...
...
@@ -58,7 +58,7 @@ let print_ident_labels fmt id =
not
(
Slab
.
is_empty
id
.
id_label
)
then
fprintf
fmt
"@ %a"
print_labels
id
.
id_label
;
if
Debug
.
test_flag
debug_print_locs
then
Util
.
option_
iter
(
fprintf
fmt
"@ %a"
print_loc
)
id
.
id_loc
Opt
.
iter
(
fprintf
fmt
"@ %a"
print_loc
)
id
.
id_loc
(* type variables always start with a quote *)
let
print_tv
fmt
tv
=
...
...
@@ -148,7 +148,7 @@ let unambig_fs fs =
|
Tyvar
u
when
not
(
lookup
u
)
->
false
|
_
->
ty_all
inspect
ty
in
option_apply
true
inspect
fs
.
ls_value
Opt
.
fold
(
fun
_
->
inspect
)
true
fs
.
ls_value
(** Patterns, terms, and formulas *)
...
...
src/core/task.ml
View file @
58fbf6cb
...
...
@@ -85,7 +85,7 @@ let task_equal t1 t2 = match t1, t2 with
|
None
,
None
->
true
|
_
->
false
let
task_hash
t
=
option_apply
0
(
fun
t
->
task_hd_hash
t
+
1
)
t
let
task_hash
t
=
Opt
.
fold
(
fun
_
t
->
task_hd_hash
t
+
1
)
0
t
module
Hstask
=
Hashcons
.
Make
(
struct
type
t
=
task_hd
...
...
@@ -107,9 +107,9 @@ let mk_task decl prev known clone meta = Some (Hstask.hashcons {
task_tag
=
Hashweak
.
dummy_tag
;
})
let
task_known
=
option_apply
Mid
.
empty
(
fun
t
->
t
.
task_known
)
let
task_clone
=
option_apply
Mid
.
empty
(
fun
t
->
t
.
task_clone
)
let
task_meta
=
option_apply
Mmeta
.
empty
(
fun
t
->
t
.
task_meta
)
let
task_known
=
Opt
.
fold
(
fun
_
t
->
t
.
task_known
)
Mid
.
empty
let
task_clone
=
Opt
.
fold
(
fun
_
t
->
t
.
task_clone
)
Mid
.
empty
let
task_meta
=
Opt
.
fold
(
fun
_
t
->
t
.
task_meta
)
Mmeta
.
empty
let
find_clone_tds
task
(
th
:
theory
)
=
cm_find
(
task_clone
task
)
th
let
find_meta_tds
task
(
t
:
meta
)
=
mm_find
(
task_meta
task
)
t
...
...
@@ -202,7 +202,7 @@ let add_meta task t al = new_meta task t (create_meta t al)
let
split_tdecl
names
(
res
,
task
)
td
=
match
td
.
td_node
with
|
Decl
{
d_node
=
Dprop
((
Pgoal
|
Plemma
)
,
pr
,
f
)
}
when
option_apply
true
(
Spr
.
mem
pr
)
names
->
when
Opt
.
fold
(
fun
_
->
Spr
.
mem
pr
)
true
names
->
let
res
=
add_prop_decl
task
Pgoal
pr
f
::
res
in
res
,
flat_tdecl
task
td
|
_
->
...
...
src/core/term.ml
View file @
58fbf6cb
...
...
@@ -392,7 +392,7 @@ module Hsterm = Hashcons.Make (struct
oty_equal
t1
.
t_ty
t2
.
t_ty
&&
t_equal_node
t1
.
t_node
t2
.
t_node
&&
Slab
.
equal
t1
.
t_label
t2
.
t_label
&&
option_eq
Loc
.
equal
t1
.
t_loc
t2
.
t_loc
Opt
.
equal
Loc
.
equal
t1
.
t_loc
t2
.
t_loc
let
t_hash_bound
(
v
,
b
,
t
)
=
Hashcons
.
combine
(
vs_hash
v
)
(
bnd_hash
b
(
t_hash
t
))
...
...
@@ -881,7 +881,7 @@ let rec t_gen_map fnT fnL m t =
|
Tconst
_
->
t
|
Tapp
(
fs
,
tl
)
->
t_app
(
fnL
fs
)
(
List
.
map
fn
tl
)
(
option_
map
fnT
t
.
t_ty
)
t_app
(
fnL
fs
)
(
List
.
map
fn
tl
)
(
Opt
.
map
fnT
t
.
t_ty
)
|
Tif
(
f
,
t1
,
t2
)
->
t_if
(
fn
f
)
(
fn
t1
)
(
fn
t2
)
|
Tlet
(
t1
,
(
u
,
b
,
t2
))
->
...
...
@@ -933,7 +933,7 @@ let t_ty_subst mapT mapV t =
let
rec
t_gen_fold
fnT
fnL
acc
t
=
let
fn
=
t_gen_fold
fnT
fnL
in
let
acc
=
option_
fold
fnT
acc
t
.
t_ty
in
let
acc
=
Opt
.
fold
fnT
acc
t
.
t_ty
in
match
t
.
t_node
with
|
Tconst
_
|
Tvar
_
->
acc
|
Tapp
(
f
,
tl
)
->
List
.
fold_left
fn
(
fnL
acc
f
)
tl
...
...
src/core/theory.ml
View file @
58fbf6cb
...
...
@@ -460,7 +460,7 @@ let rec cl_find_ts cl ts =
if
not
(
Sid
.
mem
ts
.
ts_name
cl
.
cl_local
)
then
ts
else
try
Mts
.
find
ts
cl
.
ts_table
with
Not_found
->
let
td'
=
option_
map
(
cl_trans_ty
cl
)
ts
.
ts_def
in
let
td'
=
Opt
.
map
(
cl_trans_ty
cl
)
ts
.
ts_def
in
let
ts'
=
create_tysymbol
(
id_clone
ts
.
ts_name
)
ts
.
ts_args
td'
in
cl
.
ts_table
<-
Mts
.
add
ts
ts'
cl
.
ts_table
;
ts'
...
...
@@ -472,7 +472,7 @@ let cl_find_ls cl ls =
else
try
Mls
.
find
ls
cl
.
ls_table
with
Not_found
->
let
ta'
=
List
.
map
(
cl_trans_ty
cl
)
ls
.
ls_args
in
let
vt'
=
option_
map
(
cl_trans_ty
cl
)
ls
.
ls_value
in
let
vt'
=
Opt
.
map
(
cl_trans_ty
cl
)
ls
.
ls_value
in
let
ls'
=
create_lsymbol
(
id_clone
ls
.
ls_name
)
ta'
vt'
in
cl
.
ls_table
<-
Mls
.
add
ls
ls'
cl
.
ls_table
;
ls'
...
...
@@ -542,7 +542,7 @@ let cl_data cl inst tdl =
cl_find_ls
cl
ls
in
let
add_constr
(
ls
,
pl
)
=
add_ls
ls
,
List
.
map
(
option_
map
add_ls
)
pl
add_ls
ls
,
List
.
map
(
Opt
.
map
add_ls
)
pl
in
let
add_type
(
ts
,
csl
)
=
if
Mts
.
mem
ts
inst
.
inst_ts
then
...
...
@@ -632,7 +632,7 @@ let clone_theory cl add_td acc th inst =
try
Some
(
mk_tdecl
(
cl_tdecl
cl
inst
td
))
with
EmptyDecl
->
None
in
option_apply
acc
(
add_td
acc
)
td
Opt
.
fold
add_td
acc
td
in
let
acc
=
List
.
fold_left
add
acc
th
.
th_decls
in
let
sm
=
{
...
...
@@ -738,7 +738,7 @@ let clone_meta tdt sm = match tdt.td_node with
(** access to meta *)
(*
let theory_meta
= option_apply Mmeta.empty (fun t -> t.task_meta)
let theory_meta
= Opt.fold (fun _ t -> t.task_meta) Mmeta.empty
let find_meta_tds th (t : meta) = mm_find (theory_meta th) t
...
...
src/core/ty.ml
View file @
58fbf6cb
...
...
@@ -152,7 +152,7 @@ let create_tysymbol name args def =
let
add
s
v
=
Stv
.
add_new
(
DuplicateTypeVar
v
)
v
s
in
let
s
=
List
.
fold_left
add
Stv
.
empty
args
in
let
check
v
=
Stv
.
mem
v
s
||
raise
(
UnboundTypeVar
v
)
in
ignore
(
option_
map
(
ty_v_all
check
)
def
);
ignore
(
Opt
.
map
(
ty_v_all
check
)
def
);
mk_ts
name
args
def
let
ty_app
s
tl
=
...
...
@@ -251,17 +251,17 @@ exception UnexpectedProp
let
oty_type
=
function
Some
ty
->
ty
|
None
->
raise
UnexpectedProp
let
oty_equal
=
Util
.
option_eq
ty_equal
let
oty_hash
=
Util
.
option_apply
1
ty_hash
let
oty_equal
=
Opt
.
equal
ty_equal
let
oty_hash
=
Opt
.
fold
(
fun
_
->
ty_hash
)
1
let
oty_match
m
o1
o2
=
match
o1
,
o2
with
|
Some
ty1
,
Some
ty2
->
ty_match
m
ty1
ty2
|
None
,
None
->
m
|
_
->
raise
UnexpectedProp
let
oty_inst
m
=
Util
.
option_
map
(
ty_inst
m
)
let
oty_freevars
=
Util
.
option_
fold
ty_freevars
let
oty_cons
=
Util
.
option_
fold
(
fun
tl
t
->
t
::
tl
)
let
oty_inst
m
=
Opt
.
map
(
ty_inst
m
)
let
oty_freevars
=
Opt
.
fold
ty_freevars
let
oty_cons
=
Opt
.
fold
(
fun
tl
t
->
t
::
tl
)
let
ty_equal_check
ty1
ty2
=
if
not
(
ty_equal
ty1
ty2
)
then
raise
(
TypeMismatch
(
ty1
,
ty2
))
...
...
src/driver/autodetection.ml
View file @
58fbf6cb
...
...
@@ -335,7 +335,7 @@ let detect_exec env main data acc exec_name =
known_version
env
exec_name
;
eprintf
"Found prover %s version %s%s@."
data
.
prover_name
ver
(
def_option
(
Opt
.
get_def
". This version of the prover is known to have problems."
data
.
message
);
acc
...
...
@@ -362,7 +362,7 @@ let detect_exec env main data acc exec_name =
if
good
||
old
then
begin
eprintf
"Found prover %s version %s%s@."
data
.
prover_name
ver
(
def_option
(
if
old
then
(
Opt
.
get_def
(
if
old
then
" (it is an old version that is less tested than \
the current one)."
else
", Ok."
)
data
.
message
);
...
...
src/driver/call_provers.ml
View file @
58fbf6cb
...
...
@@ -198,7 +198,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
(
try
List
.
assoc
n
exitcodes
with
Not_found
->
grep
out
regexps
)
in
Debug
.
dprintf
debug
"Call_provers: prover output:@
\n
%s@."
out
;
let
time
=
Util
.
def_option
time
(
grep_time
out
timeregexps
)
in
let
time
=
Opt
.
get_def
time
(
grep_time
out
timeregexps
)
in
let
ans
=
match
ans
with
|
HighFailure
when
!
on_timelimit
&&
timelimit
>
0
&&
time
>=
(
0
.
9
*.
float
timelimit
)
->
Timeout
...
...
src/driver/driver.ml
View file @
58fbf6cb
...
...
@@ -304,9 +304,9 @@ let prove_task_prepared
~
command
?
timelimit
?
memlimit
?
old
?
inplace
drv
task
=
let
buf
=
Buffer
.
create
1024
in
let
fmt
=
formatter_of_buffer
buf
in
let
old_channel
=
option_
map
open_in
old
in
let
old_channel
=
Opt
.
map
open_in
old
in
print_task_prepared
?
old
:
old_channel
drv
fmt
task
;
pp_print_flush
fmt
()
;
option_
iter
close_in
old_channel
;
Opt
.
iter
close_in
old_channel
;
let
filename
=
match
old
,
inplace
with
|
Some
fn
,
Some
true
->
fn
|
_
->
...
...
src/driver/whyconf.ml
View file @
58fbf6cb
...
...
@@ -512,8 +512,8 @@ let mk_filter_prover ?version ?altern name =
|
Some
""
->
invalid_arg
"mk_filter_prover: version can't be an empty string"
|
_
->
()
end
;
{
filter_name
=
mk_regexp
name
;
filter_version
=
option_
map
mk_regexp
version
;
filter_altern
=
option_
map
mk_regexp
altern
;
filter_version
=
Opt
.
map
mk_regexp
version
;
filter_altern
=
Opt
.
map
mk_regexp
altern
;
}
let
print_filter_prover
fmt
fp
=
...
...
@@ -540,8 +540,8 @@ let parse_filter_prover s =
let
filter_prover
fp
p
=
let
check
s
schema
=
Str
.
string_match
schema
.
reg
s
0
in
check
p
.
prover_name
fp
.
filter_name
&&
option_apply
true
(
check
p
.
prover_version
)
fp
.
filter_version
&&
option_apply
true
(
check
p
.
prover_altern
)
fp
.
filter_altern
&&
Opt
.
fold
(
fun
_
->
check
p
.
prover_version
)
true
fp
.
filter_version
&&
Opt
.
fold
(
fun
_
->
check
p
.
prover_altern
)
true
fp
.
filter_altern
let
filter_provers
whyconf
fp
=
try
...
...
@@ -647,7 +647,7 @@ let set_main config main =
}
let
set_provers
config
?
shortcuts
provers
=
let
shortcuts
=
def_option
config
.
prover_shortcuts
shortcuts
in
let
shortcuts
=
Opt
.
get_def
config
.
prover_shortcuts
shortcuts
in
{
config
with
config
=
set_provers_shortcuts
config
.
config
shortcuts
provers
;
provers
=
provers
;
...
...
src/ide/gmain.ml
View file @
58fbf6cb
...
...
@@ -60,9 +60,9 @@ let spec = Arg.align [
Arg.String (fun s -> input_files := s :: !input_files),
"<f> add file f to the project (ignored if it is already there)") ;
*)
Debug
.
Opt
.
desc_debug_list
;
Debug
.
Opt
.
desc_debug_all
;
Debug
.
Opt
.
desc_debug
;
Debug
.
Args
.
desc_debug_list
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug
;
(
"-v"
,
Arg
.
Set
opt_version
,
" print version information"
)
;
...
...
@@ -94,8 +94,8 @@ let () = Gconfig.read_config !opt_config !opt_extra
let
()
=
C
.
load_plugins
(
get_main
()
)
let
()
=
Debug
.
Opt
.
set_flags_selected
()
;
if
Debug
.
Opt
.
option_list
()
then
exit
0
Debug
.
Args
.
set_flags_selected
()
;
if
Debug
.
Args
.
option_list
()
then
exit
0
let
()
=
if
!
opt_list_formats
then
begin
...
...
@@ -1668,7 +1668,7 @@ let color_loc ~color loc =
let
rec
color_locs
~
color
f
=
let
b
=
ref
false
in
Util
.
option_
iter
(
fun
loc
->
color_loc
~
color
loc
;
b
:=
true
)
f
.
Term
.
t_loc
;
Opt
.
iter
(
fun
loc
->
color_loc
~
color
loc
;
b
:=
true
)
f
.
Term
.
t_loc
;
Term
.
t_fold
(
fun
b
loc
->
color_locs
~
color
loc
||
b
)
!
b
f
(* FIXME: we shouldn't open binders _every_time_ we redraw screen!!!
...
...
@@ -1698,7 +1698,7 @@ let scroll_to_source_goal g =
{
Theory
.
td_node
=
Theory
.
Decl
{
Decl
.
d_node
=
Decl
.
Dprop
(
Decl
.
Pgoal
,
_
,
f
)}}}
->
if
not
(
color_t_locs
f
)
then
Util
.
option_
iter
(
color_loc
~
color
:
goal_tag
)
id
.
Ident
.
id_loc
Opt
.
iter
(
color_loc
~
color
:
goal_tag
)
id
.
Ident
.
id_loc
|
_
->
assert
false
...
...
src/ide/replay.ml
View file @
58fbf6cb
...
...
@@ -85,12 +85,12 @@ let spec = Arg.align [
"--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
" try to find compatible provers for all unknown provers";
*)
Debug
.
Opt
.
desc_debug_list
;
Debug
.
Opt
.
desc_shortcut
"parse_only"
"--parse-only"
" Stop after parsing"
;
Debug
.
Opt
.
desc_shortcut
Debug
.
Args
.
desc_debug_list
;
Debug
.
Args
.
desc_shortcut
"parse_only"
"--parse-only"
" Stop after parsing"
;
Debug
.
Args
.
desc_shortcut
"type_only"
"--type-only"
" Stop after type checking"
;
Debug
.
Opt
.
desc_debug_all
;
Debug
.
Opt
.
desc_debug
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug
;
]
...
...
@@ -140,8 +140,8 @@ let env = Env.create_env loadpath
let
()
=
Whyconf
.
load_plugins
(
Whyconf
.
get_main
config
)
let
()
=
Debug
.
Opt
.
set_flags_selected
()
;
if
Debug
.
Opt
.
option_list
()
then
exit
0
Debug
.
Args
.
set_flags_selected
()
;
if
Debug
.
Args
.
option_list
()
then
exit
0
module
O
=
struct
...
...
src/main.ml
View file @
58fbf6cb
...
...
@@ -190,14 +190,14 @@ let option_list = Arg.align [
" List known input formats"
;
"--list-metas"
,
Arg
.
Set
opt_list_metas
,
" List known metas"
;
Debug
.
Opt
.
desc_debug_list
;
Debug
.
Args
.
desc_debug_list
;
"--token-count"
,
Arg
.
Set
opt_token_count
,
" Only lexing, and give numbers of tokens in spec vs in program"
;
Debug
.
Opt
.
desc_shortcut
"parse_only"
"--parse-only"
" Stop after parsing"
;
Debug
.
Opt
.
desc_shortcut
Debug
.
Args
.
desc_shortcut
"parse_only"
"--parse-only"
" Stop after parsing"
;
Debug
.
Args
.
desc_shortcut
"type_only"
"--type-only"
" Stop after type checking"
;
Debug
.
Opt
.
desc_debug_all
;
Debug
.
Opt
.
desc_debug
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug
;
"--print-libdir"
,
Arg
.
Set
opt_print_libdir
,
" Print location of binary components (plugins, etc)"
;
"--print-datadir"
,
Arg
.
Set
opt_print_datadir
,
...
...
@@ -227,7 +227,7 @@ let () = try
let
main
=
get_main
config
in
Whyconf
.
load_plugins
main
;
Debug
.
Opt
.
set_flags_selected
()
;
Debug
.
Args
.
set_flags_selected
()
;