Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
55d1902f
Commit
55d1902f
authored
Sep 07, 2015
by
David Hauzar
Browse files
Minor refactoring of Model_parser.
parent
13921d03
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/core/model_parser.ml
View file @
55d1902f
...
...
@@ -93,14 +93,19 @@ print_model_value fmt value =
** Model elements
***************************************************************
*)
type
model_element_type
=
type
model_element_kind
=
|
Result
|
Old
|
Other
type
model_element_name
=
{
men_name
:
string
;
men_kind
:
model_element_kind
;
}
type
model_element
=
{
me_name
:
string
;
me_type
:
model_element_type
;
me_name
:
model_element_name
;
me_value
:
model_value
;
me_location
:
Loc
.
position
option
;
me_term
:
Term
.
term
option
;
...
...
@@ -111,20 +116,23 @@ let split_me_name name =
let
splitted
=
Str
.
bounded_split
(
Str
.
regexp_string
"@"
)
name
2
in
match
splitted
with
|
[
first
]
->
(
first
,
""
)
|
first
::
[
second
]
->
(
first
,
second
)
|
[
first
;
second
]
->
(
first
,
second
)
|
_
->
(* here, "_" can only stand for [] *)
(
""
,
""
)
let
create_model_element
~
name
~
value
?
location
?
term
()
=
let
(
name
,
type_s
)
=
split_me_name
name
in
let
t
=
match
type_s
with
let
me_kind
=
match
type_s
with
|
"result"
->
Result
|
"old"
->
Old
|
_
->
Other
in
let
me_name
=
{
men_name
=
name
;
men_kind
=
me_kind
;
}
in
{
me_name
=
name
;
me_type
=
t
;
me_name
=
me_name
;
me_value
=
value
;
me_location
=
location
;
me_term
=
term
;
...
...
@@ -173,9 +181,9 @@ type raw_model_parser = string -> model_element list
*)
let
print_model_element
me_name_trans
fmt
m_element
=
if
m_element
.
me_text_info
then
fprintf
fmt
"%s"
m_element
.
me_name
fprintf
fmt
"%s"
m_element
.
me_name
.
men_name
else
let
me_name
=
me_name_trans
(
m_element
.
me_name
,
m_element
.
me_type
)
in
let
me_name
=
me_name_trans
m_element
.
me_name
in
fprintf
fmt
"%s = %a"
me_name
print_model_value
m_element
.
me_value
...
...
@@ -190,11 +198,11 @@ let print_model_file fmt me_name_trans filename model_file =
print_model_elements
me_name_trans
fmt
m_elements
)
model_file
let
why_name_trans
(
me_name
,
me_type
)
=
match
me_
type
with
let
why_name_trans
me_name
=
match
me_
name
.
men_kind
with
|
Result
->
"result"
|
Old
->
"old"
^
" "
^
me_name
|
Other
->
me_name
|
Old
->
"old"
^
" "
^
me_name
.
men_name
|
Other
->
me_name
.
men_name
let
print_model
?
(
me_name_trans
=
why_name_trans
)
...
...
@@ -322,7 +330,7 @@ let print_model_json
fmt
model
=
let
me_name_to_str
=
fun
me
->
me_name_trans
(
me
.
me_name
,
me
.
me_type
)
in
me_name_trans
me
.
me_name
in
Json
.
map_bindings
(
fun
s
->
s
)
(
print_model_elements_on_lines_json
me_name_to_str
)
...
...
@@ -379,9 +387,9 @@ match raw_model with
|
model_element
::
raw_strings_tail
->
let
(
element_name
,
element_location
,
element_term
,
terms_tail
)
=
match
terms
with
|
[]
->
(
model_element
.
me_name
,
None
,
None
,
[]
)
|
[]
->
(
model_element
.
me_name
.
men_name
,
None
,
None
,
[]
)
|
term
::
t_tail
->
((
get_element_name
term
model_element
.
me_name
)
,
((
get_element_name
term
model_element
.
me_name
.
men_name
)
,
term
.
t_loc
,
Some
term
,
t_tail
)
in
let
new_model_element
=
create_model_element
...
...
@@ -415,9 +423,12 @@ let handle_contradictory_vc model_files vc_term_loc =
let
model_elements
=
get_elements
model_file
line_number
in
if
model_elements
=
[]
then
(* The vc is contradictory, add special model element *)
let
me_name
=
{
men_name
=
"the check fails with all inputs"
;
men_kind
=
Other
;
}
in
let
me
=
{
me_name
=
"the check fails with all inputs"
;
me_type
=
Other
;
me_name
=
me_name
;
me_value
=
Unparsed
""
;
me_location
=
Some
pos
;
me_term
=
None
;
...
...
src/core/model_parser.mli
View file @
55d1902f
...
...
@@ -56,21 +56,26 @@ val print_model_value : Format.formatter -> model_value -> unit
***************************************************************
*)
type
model_element_
type
=
type
model_element_
kind
=
|
Result
(* Result of a function call (if the counter-example is for postcondition) *)
|
Old
(* Old value of function argument (if the counter-example is for postcondition) *)
|
Other
(** Information about the name of the model element *)
type
model_element_name
=
{
men_name
:
string
;
(** The name of the source-code element. *)
men_kind
:
model_element_kind
;
(** The kind of model element. *)
}
(** Counter-example model elements. Each element represents
a counter-example for a single source-code element.*)
type
model_element
=
{
me_name
:
string
;
(** The name of the source-code element. *)
me_type
:
model_element_type
;
(** The type of model element. *)
me_name
:
model_element_name
;
(** Information about the name of the model element *)
me_value
:
model_value
;
(** Counter-example value for the element. *)
me_location
:
Loc
.
position
option
;
...
...
@@ -116,27 +121,26 @@ val default_model : model
*)
val
print_model
:
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
Format
.
formatter
->
model
->
unit
(** Prints the counter-example model
@param me_name_trans the transformation of the model elements
names. The input is a pair consisting of the name of model
element and type of the model element. The output is the
name of the model element that should be displayed.
names. The input is information about model element name. The
output is the name of the model element that should be displayed.
@param model the counter-example model to print
*)
val
model_to_string
:
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
model
->
string
(** See print_model *)
val
print_model_vc_term
:
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
?
sep
:
string
->
Format
.
formatter
->
model
->
...
...
@@ -150,7 +154,7 @@ val print_model_vc_term :
*)
val
model_vc_term_to_string
:
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
?
sep
:
string
->
model
->
string
...
...
@@ -160,7 +164,7 @@ val model_vc_term_to_string :
*)
val
print_model_json
:
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
Format
.
formatter
->
model
->
unit
...
...
@@ -171,7 +175,7 @@ val print_model_json :
*)
val
model_to_string_json
:
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
model
->
string
(** See print_model_json *)
...
...
@@ -179,7 +183,7 @@ val model_to_string_json :
val
interleave_with_source
:
?
start_comment
:
string
->
?
end_comment
:
string
->
?
me_name_trans
:
(
(
string
*
model_element_
type
)
->
string
)
->
?
me_name_trans
:
(
model_element_
name
->
string
)
->
model
->
filename
:
string
->
source_code
:
string
->
...
...
Write
Preview
Markdown
is supported
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