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
e459c7fc
Commit
e459c7fc
authored
Dec 26, 2010
by
Andrei Paskevich
Browse files
registered transformations are automatically named
parent
18b84207
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/core/trans.ml
View file @
e459c7fc
...
...
@@ -32,6 +32,8 @@ let debug = Debug.register_flag "transform"
type
'
a
trans
=
task
->
'
a
type
'
a
tlist
=
'
a
list
trans
let
apply
f
x
=
f
x
let
identity
x
=
x
let
identity_l
x
=
[
x
]
...
...
@@ -42,18 +44,6 @@ let singleton f x = [f x]
let
compose
f
g
x
=
g
(
f
x
)
let
compose_l
f
g
x
=
list_apply
g
(
f
x
)
exception
TransFailure
of
(
string
*
exn
)
let
apply
f
x
=
f
x
let
apply_named
s
f
x
=
Debug
.
dprintf
debug
"Apply transformation %s@."
s
;
try
apply
f
x
with
|
e
when
not
(
Debug
.
test_flag
Debug
.
stack_trace
)
->
raise
(
TransFailure
(
s
,
e
))
let
catch_named
=
apply_named
module
Wtask
=
Hashweak
.
Make
(
struct
type
t
=
task_hd
let
tag
t
=
t
.
task_tag
...
...
@@ -224,13 +214,11 @@ let on_tagged_pr t fn =
(** debug *)
let
print_meta
f
m
task
=
if
Debug
.
test_flag
f
then
(
let
fmt
=
Debug
.
get_debug_formatter
()
in
Pp
.
print_iter1
Stdecl
.
iter
Pp
.
newline
Pretty
.
print_tdecl
fmt
(
find_meta_tds
task
m
)
.
tds_set
;
(
Pp
.
add_flush
Pp
.
newline
)
fmt
()
);
let
print_tds
fmt
m
=
Pp
.
print_iter1
Stdecl
.
iter
Pp
.
newline
Pretty
.
print_tdecl
fmt
(
find_meta_tds
task
m
)
.
tds_set
in
Debug
.
dprintf
f
"%a@."
print_tds
m
;
task
(** register transformations *)
...
...
@@ -244,25 +232,31 @@ end)
exception
UnknownTrans
of
string
exception
KnownTrans
of
string
exception
TransFailure
of
(
string
*
exn
)
let
named
s
f
(
x
:
task
)
=
Debug
.
dprintf
debug
"Apply transformation %s@."
s
;
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
else
try
f
x
with
e
->
raise
(
TransFailure
(
s
,
e
))
let
transforms
:
(
string
,
env
->
task
trans
)
Hashtbl
.
t
=
Hashtbl
.
create
17
let
transforms_l
:
(
string
,
env
->
task
tlist
)
Hashtbl
.
t
=
Hashtbl
.
create
17
let
register_transform
s
p
=
if
Hashtbl
.
mem
transforms
s
then
raise
(
KnownTrans
s
);
Hashtbl
.
replace
transforms
s
(
fun
_
->
p
)
Hashtbl
.
replace
transforms
s
(
fun
_
->
named
s
p
)
let
register_transform_l
s
p
=
if
Hashtbl
.
mem
transforms_l
s
then
raise
(
KnownTrans
s
);
Hashtbl
.
replace
transforms_l
s
(
fun
_
->
p
)
Hashtbl
.
replace
transforms_l
s
(
fun
_
->
named
s
p
)
let
register_env_transform
s
p
=
if
Hashtbl
.
mem
transforms
s
then
raise
(
KnownTrans
s
);
Hashtbl
.
replace
transforms
s
(
Wenv
.
memoize
3
p
)
Hashtbl
.
replace
transforms
s
(
Wenv
.
memoize
3
(
fun
e
->
named
s
(
p
e
))
)
let
register_env_transform_l
s
p
=
if
Hashtbl
.
mem
transforms_l
s
then
raise
(
KnownTrans
s
);
Hashtbl
.
replace
transforms_l
s
(
Wenv
.
memoize
3
p
)
Hashtbl
.
replace
transforms_l
s
(
Wenv
.
memoize
3
(
fun
e
->
named
s
(
p
e
))
)
let
lookup_transform
s
=
try
Hashtbl
.
find
transforms
s
with
Not_found
->
raise
(
UnknownTrans
s
)
...
...
src/core/trans.mli
View file @
e459c7fc
...
...
@@ -39,9 +39,6 @@ val singleton : 'a trans -> 'a tlist
val
compose
:
task
trans
->
'
a
trans
->
'
a
trans
val
compose_l
:
task
tlist
->
'
a
tlist
->
'
a
tlist
(* Should be only used with functions working in constant time *)
(* val conv_res : ('a -> 'b) -> 'a trans -> 'b trans *)
val
fold
:
(
task_hd
->
'
a
->
'
a
)
->
'
a
->
'
a
trans
val
fold_l
:
(
task_hd
->
'
a
->
'
a
list
)
->
'
a
->
'
a
tlist
...
...
@@ -81,12 +78,12 @@ val on_tagged_pr : meta -> (Spr.t -> 'a trans) -> 'a trans
(** debug transformation *)
val
print_meta
:
Debug
.
flag
->
meta
->
task
trans
(** [print_meta f m] if [d] is set pretty_print on the debug
formatter. In all the case the transformation is indeed the
identity *)
(** [print_meta f m] is an identity transformation that
prints every meta [m] in the task if flag [d] is set *)
(** {2 Registration} *)
exception
TransFailure
of
(
string
*
exn
)
exception
UnknownTrans
of
string
exception
KnownTrans
of
string
...
...
@@ -102,9 +99,6 @@ val lookup_transform_l : string -> Env.env -> task tlist
val
list_transforms
:
unit
->
string
list
val
list_transforms_l
:
unit
->
string
list
exception
TransFailure
of
(
string
*
exn
)
val
apply_named
:
string
->
'
a
trans
->
(
task
->
'
a
)
val
named
:
string
->
'
a
trans
->
'
a
trans
(** give transformation a name without registering *)
val
catch_named
:
string
->
'
a
trans
->
'
a
trans
(** catch the error, and reraise with TransFailure *)
src/driver/driver.ml
View file @
e459c7fc
...
...
@@ -246,9 +246,9 @@ let print_task ?old drv fmt task =
in
let
lookup_transform
t
=
t
,
lookup_transform
t
drv
.
drv_env
in
let
transl
=
List
.
map
lookup_transform
drv
.
drv_transform
in
let
apply
task
(
t
,
tr
)
=
let
apply
task
(
_
t
,
tr
)
=
(* Format.printf "@\n@\n[%f] %s@." (Sys.time ()) t; *)
Trans
.
apply
_named
t
tr
task
Trans
.
apply
tr
task
in
(*Format.printf "@\n@\nTASK";*)
let
task
=
update_task
drv
task
in
...
...
src/main.ml
View file @
e459c7fc
...
...
@@ -375,13 +375,13 @@ let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let
do_tasks
env
drv
fname
tname
th
task
=
let
lookup
acc
t
=
(
try
t
,
Trans
.
singleton
(
Trans
.
lookup_transform
t
env
)
with
Trans
.
UnknownTrans
_
->
t
,
Trans
.
lookup_transform_l
t
env
)
::
acc
(
try
Trans
.
singleton
(
Trans
.
lookup_transform
t
env
)
with
Trans
.
UnknownTrans
_
->
Trans
.
lookup_transform_l
t
env
)
::
acc
in
let
trans
=
List
.
fold_left
lookup
[]
!
opt_trans
in
let
apply
tasks
(
s
,
tr
)
=
let
apply
tasks
tr
=
List
.
rev
(
List
.
fold_left
(
fun
acc
task
->
List
.
rev_append
(
Trans
.
apply
_named
s
tr
task
)
acc
)
[]
tasks
)
List
.
rev_append
(
Trans
.
apply
tr
task
)
acc
)
[]
tasks
)
in
let
tasks
=
List
.
fold_left
apply
[
task
]
trans
in
List
.
iter
(
do_task
drv
fname
tname
th
)
tasks
...
...
src/transform/encoding.ml
View file @
e459c7fc
...
...
@@ -53,7 +53,7 @@ let enco_gen opt env =
|
Some
[
MAstr
s
]
->
s
|
_
->
assert
false
in
try
Trans
.
catch_
named
s
((
Hashtbl
.
find
opt
.
table
s
)
env
)
Trans
.
named
s
((
Hashtbl
.
find
opt
.
table
s
)
env
)
with
Not_found
->
failwith
(
Format
.
sprintf
"encoding : %s wrong argument %s"
opt
.
meta
.
meta_name
s
))
...
...
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