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
124
Issues
124
List
Boards
Labels
Service Desk
Milestones
Merge Requests
18
Merge Requests
18
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
14dedf27
Commit
14dedf27
authored
Sep 03, 2015
by
David Hauzar
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'counter-examples'
parents
d3a9cc19
101ed70b
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
30 additions
and
8 deletions
+30
-8
src/core/ident.ml
src/core/ident.ml
+6
-3
src/core/ident.mli
src/core/ident.mli
+7
-0
src/core/model_parser.ml
src/core/model_parser.ml
+2
-2
src/transform/eval_match.ml
src/transform/eval_match.ml
+15
-3
No files found.
src/core/ident.ml
View file @
14dedf27
...
...
@@ -52,12 +52,12 @@ let is_model_trace_label label =
true
with
Not_found
->
false
let
get_model_trace_label
labels
=
let
get_model_trace_label
~
labels
=
Slab
.
choose
(
Slab
.
filter
is_model_trace_label
labels
)
let
transform_model_trace_label
labels
trans_fun
=
try
let
trace_label
=
get_model_trace_label
labels
in
let
trace_label
=
get_model_trace_label
~
labels
in
let
labels_without_trace
=
Slab
.
remove
trace_label
labels
in
let
new_trace_label
=
create_label
(
trans_fun
trace_label
.
lab_string
)
in
Slab
.
add
new_trace_label
labels_without_trace
...
...
@@ -76,7 +76,7 @@ let append_to_model_trace_label ~labels ~to_append =
transform_model_trace_label
labels
trans
let
get_model_element_name
~
labels
=
let
trace_label
=
get_model_trace_label
labels
in
let
trace_label
=
get_model_trace_label
~
labels
in
let
splitted1
=
Str
.
bounded_split
(
Str
.
regexp_string
":"
)
trace_label
.
lab_string
2
in
match
splitted1
with
|
[
_
;
content
]
->
...
...
@@ -140,6 +140,9 @@ let id_fresh ?(label = Slab.empty) ?loc nm =
let
id_user
?
(
label
=
Slab
.
empty
)
nm
loc
=
create_ident
nm
label
(
Some
loc
)
let
id_lab
label
id
=
create_ident
id
.
id_string
label
id
.
id_loc
let
id_clone
?
(
label
=
Slab
.
empty
)
id
=
let
ll
=
Slab
.
union
label
id
.
id_label
in
create_ident
id
.
id_string
ll
id
.
id_loc
...
...
src/core/ident.mli
View file @
14dedf27
...
...
@@ -49,6 +49,10 @@ val get_model_element_name : labels : Slab.t -> string
Throws Not_found if there is no element name (there is no
label of the form "model_trace:+". *)
val
get_model_trace_label
:
labels
:
Slab
.
t
->
Slab
.
elt
(** Return label of the for "model_trace:*".
Throws Not_found if there is no such label.*)
(** {2 Identifiers} *)
type
ident
=
private
{
...
...
@@ -83,6 +87,9 @@ val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
(* create a localized pre-ident *)
val
id_user
:
?
label
:
Slab
.
t
->
string
->
Loc
.
position
->
preid
(* create a duplicate pre-ident with given labels *)
val
id_lab
:
Slab
.
t
->
ident
->
preid
(* create a duplicate pre-ident *)
val
id_clone
:
?
label
:
Slab
.
t
->
ident
->
preid
...
...
src/core/model_parser.ml
View file @
14dedf27
...
...
@@ -69,10 +69,10 @@ let rec print_indices fmt indices =
print_indices
fmt
tail
and
print_array
fmt
arr
=
fprintf
fmt
"
[others -
> "
;
fprintf
fmt
"
(others =
> "
;
print_model_value
fmt
arr
.
arr_others
;
print_indices
fmt
arr
.
arr_indices
;
fprintf
fmt
"
]
"
fprintf
fmt
"
)
"
and
print_model_value_sanit
sanit_print
fmt
value
=
(* Prints model value. *)
...
...
src/transform/eval_match.ml
View file @
14dedf27
...
...
@@ -62,6 +62,7 @@ let rec add_quant kn (vl,tl,f) v =
in
match
cl
with
|
[
ls
,
pjl
]
->
(* there is only one constructor *)
let
s
=
ty_match
Mtv
.
empty
(
Opt
.
get
ls
.
ls_value
)
ty
in
let
mk_v
ty
pj
=
(* The name of the field corresponding to the variable that is created *)
...
...
@@ -76,7 +77,7 @@ let rec add_quant kn (vl,tl,f) v =
end
in
let
label
=
Ident
.
append_to_model_element_name
~
labels
:
v
.
vs_name
.
id_label
~
to_append
:
(
"."
^
field_name
)
in
create_vsymbol
(
id_
clone
~
label
v
.
vs_name
)
(
ty_inst
s
ty
)
in
create_vsymbol
(
id_
lab
label
v
.
vs_name
)
(
ty_inst
s
ty
)
in
let
nvl
=
List
.
map2
mk_v
ls
.
ls_args
pjl
in
let
t
=
fs_app
ls
(
List
.
map
t_var
nvl
)
ty
in
...
...
@@ -128,7 +129,7 @@ let eval_match ~inline kn t =
let
rec
eval
stop
env
t
=
let
stop
=
stop
||
Slab
.
mem
Split_goal
.
stop_split
t
.
t_label
in
let
eval
=
eval
stop
in
match
t
.
t_node
with
let
t_eval_matched
=
(
match
t
.
t_node
with
|
Tapp
(
ls
,
[
t1
;
t2
])
when
ls_equal
ls
ps_equ
->
cs_equ
kn
env
(
eval
env
t1
)
(
eval
env
t2
)
|
Tapp
(
ls
,
[
t1
])
when
is_projection
kn
ls
->
...
...
@@ -156,7 +157,18 @@ let eval_match ~inline kn t =
else
List
.
fold_left
(
add_quant
kn
)
([]
,
tl
,
f
)
vl
in
t_quant_simp
q
(
close
(
List
.
rev
vl
)
tl
(
eval
env
f
))
|
_
->
t_map_simp
(
eval
env
)
t
t_map_simp
(
eval
env
)
t
)
in
(* Copy all labels of t to t_eval_matched except for "model_trace:*" label.
This label is not copied if both t and t_eval_matched contain it. *)
let
t
=
(
try
let
_
=
Ident
.
get_model_trace_label
~
labels
:
t_eval_matched
.
t_label
in
let
original_mt_label
=
Ident
.
get_model_trace_label
~
labels
:
t
.
t_label
in
(* If both t_eval_matched and t contain model_trace label, remove it *)
t_label_remove
original_mt_label
t
with
Not_found
->
t
)
in
t_label_copy
t
t_eval_matched
in
eval
false
Mvs
.
empty
t
...
...
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