Skip to content
GitLab
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
187aa4a6
Commit
187aa4a6
authored
Apr 14, 2016
by
Andrei Paskevich
Browse files
avoid using Str when Strings suffices
parent
a4f0cad6
Changes
7
Hide whitespace changes
Inline
Side-by-side
src/core/pretty.ml
View file @
187aa4a6
...
...
@@ -77,19 +77,16 @@ let forget_var vs = forget_id iprinter vs.vs_name
let
extract_op
ls
=
let
s
=
ls
.
ls_name
.
id_string
in
let
len
=
String
.
length
s
in
if
len
<
7
then
None
else
let
inf
=
String
.
sub
s
0
6
in
if
inf
=
"infix "
then
Some
(
String
.
sub
s
6
(
len
-
6
))
else
let
prf
=
String
.
sub
s
0
7
in
if
prf
=
"prefix "
then
Some
(
String
.
sub
s
7
(
len
-
7
))
else
try
Some
(
Strings
.
remove_prefix
"infix "
s
)
with
Not_found
->
try
Some
(
Strings
.
remove_prefix
"prefix "
s
)
with
Not_found
->
None
let
tight_op
s
=
let
c
=
String
.
sub
s
0
1
in
c
=
"!"
||
c
=
"?"
let
tight_op
s
=
s
<>
""
&&
(
let
c
=
String
.
get
s
0
in
c
=
'
!
'
||
c
=
'
?
'
)
let
escape_op
s
=
let
s
=
Str
.
replace_first
(
Str
.
regexp
"^
\\
*."
)
"
\\
0"
s
in
let
s
=
Str
.
replace_first
(
Str
.
regexp
".
\\
*$"
)
"
\\
0 "
s
in
let
s
=
if
Strings
.
has_prefix
"*"
s
then
" "
^
s
else
s
in
let
s
=
if
Strings
.
ends_with
s
"*"
then
s
^
" "
else
s
in
s
(* theory names always start with an upper case letter *)
...
...
src/mlw/expr.ml
View file @
187aa4a6
...
...
@@ -1106,17 +1106,13 @@ let forget_let_defn = function
|
LDsym
(
s
,_
)
->
forget_rs
s
|
LDrec
rdl
->
List
.
iter
(
fun
fd
->
forget_rs
fd
.
rec_sym
)
rdl
let
extract_op
s
=
let
s
=
s
.
id_string
in
let
len
=
String
.
length
s
in
if
len
<
7
then
None
else
let
inf
=
String
.
sub
s
0
6
in
if
inf
=
"infix "
then
Some
(
String
.
sub
s
6
(
len
-
6
))
else
let
prf
=
String
.
sub
s
0
7
in
if
prf
=
"prefix "
then
Some
(
String
.
sub
s
7
(
len
-
7
))
else
let
extract_op
{
id_string
=
s
}
=
try
Some
(
Strings
.
remove_prefix
"infix "
s
)
with
Not_found
->
try
Some
(
Strings
.
remove_prefix
"prefix "
s
)
with
Not_found
->
None
let
tight_op
s
=
let
c
=
String
.
sub
s
0
1
in
c
=
"!"
||
c
=
"?"
let
tight_op
s
=
s
<>
""
&&
(
let
c
=
String
.
get
s
0
in
c
=
'
!
'
||
c
=
'
?
'
)
let
print_rs
fmt
({
rs_name
=
{
id_string
=
nm
}}
as
s
)
=
if
nm
=
"mixfix []"
then
pp_print_string
fmt
"([])"
else
...
...
@@ -1127,8 +1123,8 @@ let print_rs fmt ({rs_name = {id_string = nm}} as s) =
if
nm
=
"mixfix [_.._]"
then
pp_print_string
fmt
"([_.._])"
else
match
extract_op
s
.
rs_name
,
s
.
rs_logic
with
|
Some
s
,
_
->
let
s
=
Str
.
replace_first
(
Str
.
regexp
"^
\\
*."
)
"
\\
0"
s
in
let
s
=
Str
.
replace_first
(
Str
.
regexp
".
\\
*$"
)
"
\\
0 "
s
in
let
s
=
if
Strings
.
has_prefix
"*"
s
then
" "
^
s
else
s
in
let
s
=
if
Strings
.
ends_with
s
"*"
then
s
^
" "
else
s
in
fprintf
fmt
"(%s)"
s
|
_
,
RLnone
|
_
,
RLlemma
->
pp_print_string
fmt
(
id_unique
sprinter
s
.
rs_name
)
...
...
src/mlw/vc.ml
View file @
187aa4a6
...
...
@@ -109,8 +109,8 @@ let expl_loop_vari = Ident.create_label "expl:loop variant decrease"
let
expl_variant
=
Ident
.
create_label
"expl:variant decrease"
let
_expl_type_inv
=
Ident
.
create_label
"expl:type invariant"
let
lab_has_expl
=
let
expl_regexp
=
Str
.
regexp
"expl:"
in
Slab
.
exists
(
fun
l
->
Str
.
string_match
expl_regexp
l
.
lab_string
0
)
let
lab_has_expl
lab
=
Slab
.
exists
(
fun
l
->
Str
ings
.
has_prefix
"expl:"
l
.
lab_string
)
lab
let
vc_expl
loc
l
({
t_label
=
lab
}
as
f
)
=
let
lab
=
if
lab_has_expl
lab
then
lab
else
Slab
.
add
l
lab
in
...
...
src/parser/parser.mly
View file @
187aa4a6
...
...
@@ -25,47 +25,26 @@
let
model_label
=
Ident
.
create_label
"model"
let
model_projected
=
Ident
.
create_label
"model_projected"
let
is_model_label
l
=
match
l
with
let
is_model_label
l
=
match
l
with
|
Lstr
lab
->
Ident
.
lab_equal
lab
model_label
||
Ident
.
lab_equal
lab
model_projected
|
Lpos
_
->
false
|
Lstr
lab
->
(
lab
=
model_label
)
||
(
lab
=
model_projected
)
let
model_lab_present
labels
=
List
.
exists
is_model_label
labels
let
model_lab_present
labels
=
try
ignore
(
List
.
find
is_model_label
labels
);
true
with
Not_found
->
false
let
model_trace_regexp
=
Str
.
regexp
"model_trace:"
let
is_model_trace_label
l
=
match
l
with
let
is_model_trace_label
l
=
match
l
with
|
Lstr
lab
->
Strings
.
has_prefix
"model_trace:"
lab
.
Ident
.
lab_string
|
Lpos
_
->
false
|
Lstr
lab
->
try
ignore
(
Str
.
search_forward
model_trace_regexp
lab
.
Ident
.
lab_string
0
);
true
with
Not_found
->
false
let
model_trace_lab_present
labels
=
try
ignore
(
List
.
find
is_model_trace_label
labels
);
true
with
Not_found
->
false
let
model_trace_lab_present
labels
=
List
.
exists
is_model_trace_label
labels
let
add_model_trace
name
labels
=
if
(
model_lab_present
labels
)
&&
(
not
(
model_trace_lab_present
labels
)
)
then
if
model_lab_present
labels
&&
not
(
model_trace_lab_present
labels
)
then
(
Lstr
(
Ident
.
create_label
(
"model_trace:"
^
name
)))
::
labels
else
labels
let
add_lab
id
l
=
let
l
=
add_model_trace
id
.
id_str
l
in
{
id
with
id_lab
=
l
}
let
add_lab
id
l
=
{
id
with
id_lab
=
add_model_trace
id
.
id_str
l
}
let
id_anonymous
loc
=
{
id_str
=
"_"
;
id_lab
=
[]
;
id_loc
=
loc
}
...
...
src/printer/smtv2.ml
View file @
187aa4a6
...
...
@@ -205,18 +205,14 @@ let collect_model_ls info ls =
add_model_element
(
t_label
?
loc
:
ls
.
ls_name
.
id_loc
ls
.
ls_name
.
id_label
t
)
info
.
info_model
let
model_trace_re
gexp
=
Str
.
regexp
"model_trace:"
let
model_trace_
p
re
fix
=
"model_trace:"
(* The term labeled with "model_trace:name" will be in counter-example with name "name" *)
let
label_starts_with
regexp
l
=
try
ignore
(
Str
.
search_forward
regexp
l
.
lab_string
0
);
true
with
Not_found
->
false
let
get_label
labels
regexp
=
Slab
.
choose
(
Slab
.
filter
(
label_starts_with
regexp
)
labels
)
let
get_label
labels
prefix
=
let
check
l
=
Strings
.
has_prefix
prefix
l
.
lab_string
in
Slab
.
choose
(
Slab
.
filter
check
labels
)
(* TODO: add "remove_suffix" to Strings and use it here instead of regexps *)
let
add_old
lab_str
=
try
let
pos
=
Str
.
search_forward
(
Str
.
regexp
"@"
)
lab_str
0
in
...
...
@@ -234,7 +230,7 @@ let model_trace_for_postcondition ~labels info =
model_trace label in a form function_name@result
*)
try
let
trace_label
=
get_label
labels
model_trace_re
gexp
in
let
trace_label
=
get_label
labels
model_trace_
p
re
fix
in
let
lab_str
=
add_old
trace_label
.
lab_string
in
if
lab_str
=
trace_label
.
lab_string
then
labels
...
...
@@ -271,7 +267,7 @@ let check_enter_vc_term t info =
try
(* Label "model_func" => the VC is postcondition or precondition *)
(* Extract the function name from "model_func" label *)
let
fun_label
=
get_label
t
.
t_label
(
Str
.
regexp
"model_func"
)
in
let
fun_label
=
get_label
t
.
t_label
"model_func
:
"
in
vc_term_info
.
vc_func_name
<-
Some
(
get_fun_name
fun_label
.
lab_string
);
with
Not_found
->
(* No label "model_func" => the VC is not postcondition or precondition *)
...
...
src/transform/intro_vc_vars_counterexmp.ml
View file @
187aa4a6
...
...
@@ -28,7 +28,7 @@ let model_vc_label = Ident.create_label "model_vc"
(* Identifies the term that triggers the VC. *)
let
model_vc_post_label
=
Ident
.
create_label
"model_vc_post"
(* Identifies the postcondition that triggers the VC. *)
let
model_trace_re
gexp
=
Str
.
regexp
"model_trace:"
let
model_trace_
p
re
fix
=
"model_trace:"
(* The term labeled with "model_trace:name" will be in counterexample with name "name" *)
(* Information about the term that triggers VC. *)
...
...
@@ -41,17 +41,12 @@ type vc_term_info = {
(* true if VC was generated for precondition or postcondition *)
}
let
label_starts_with
regexp
l
=
try
ignore
(
Str
.
search_forward
regexp
l
.
lab_string
0
);
true
with
Not_found
->
false
let
get_label
labels
regexp
=
Slab
.
choose
(
Slab
.
filter
(
label_starts_with
regexp
)
labels
)
let
get_label
labels
prefix
=
let
check
l
=
Strings
.
has_prefix
prefix
l
.
lab_string
in
Slab
.
choose
(
Slab
.
filter
check
labels
)
let
is_model_vc_label
l
=
if
l
=
model_vc_label
||
l
=
model_vc_post_label
then
true
else
false
let
is_model_vc_label
l
=
lab_equal
l
model_vc_label
||
lab_equal
l
model_vc_post_label
let
check_enter_vc_term
t
info
=
(* Check whether the term that triggers VC is entered.
...
...
@@ -71,6 +66,7 @@ let check_exit_vc_term t info =
info
.
vc_inside
<-
false
;
end
(* TODO: add "remove_suffix" to Strings and use it here instead of regexps *)
let
add_old
lab_str
=
try
let
pos
=
Str
.
search_forward
(
Str
.
regexp
"@"
)
lab_str
0
in
...
...
@@ -89,7 +85,7 @@ let model_trace_for_postcondition ~labels =
exist model_trace label in labels, labels otherwise.
*)
try
let
trace_label
=
get_label
labels
model_trace_re
gexp
in
let
trace_label
=
get_label
labels
model_trace_
p
re
fix
in
let
lab_str
=
add_old
trace_label
.
lab_string
in
if
lab_str
=
trace_label
.
lab_string
then
labels
...
...
src/util/strings.ml
View file @
187aa4a6
...
...
@@ -73,7 +73,8 @@ let has_prefix pref s =
with
Exit
->
false
let
remove_prefix
pref
s
=
let
sl
=
String
.
length
s
in
let
l
=
String
.
length
pref
in
if
String
.
length
s
<
l
then
raise
Not_found
else
if
s
l
<
l
then
raise
Not_found
else
for
i
=
0
to
l
-
1
do
if
s
.
[
i
]
<>
pref
.
[
i
]
then
raise
Not_found
done
;
String
.
sub
s
l
(
String
.
length
s
-
l
)
String
.
sub
s
l
(
s
l
-
l
)
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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