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
1cedcd8c
Commit
1cedcd8c
authored
Jul 06, 2010
by
Francois Bobot
Browse files
simplify_array en tant que transformation builtin au lieu de plugin
parent
df2a638a
Changes
2
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
1cedcd8c
...
...
@@ -106,7 +106,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction encoding_decorate
\
eliminate_definition eliminate_algebraic
\
eliminate_inductive eliminate_let eliminate_if
\
explicit_polymorphism simple_types encoding_instantiate
explicit_polymorphism simple_types encoding_instantiate
\
simplify_array
LIB_PRINTER
=
print_real alt_ergo why3 smt coq tptp simplify gappa
...
...
@@ -538,7 +539,7 @@ bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
"bin/why.@OCAMLBEST@"
\
"bin/whyml.@OCAMLBEST@"
BENCH_PLUGINS_CMO
:=
helloworld.cmo
simplify_array.cmo
BENCH_PLUGINS_CMO
:=
helloworld.cmo
BENCH_PLUGINS_CMO
:=
$(
addprefix
bench/plugins/,
$(BENCH_PLUGINS_CMO)
)
BENCH_PLUGINS_CMXS
:=
$(BENCH_PLUGINS_CMO:.cmo=.cmxs)
...
...
@@ -547,8 +548,6 @@ bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
tests/test-jcf.why
-T
Test
-G
G
bin/why.
$(OCAMLBEST)
-D
bench/plugins/helloworld.drv
\
tests/test-jcf.why
-T
Test
-G
G
bin/why.
$(OCAMLBEST)
-D
bench/plugins/simplify_array.drv
\
tests/test-jcf.why
-T
Test_simplify_array
-G
G
###############
# test targets
...
...
bench/plugins
/simplify_array.ml
→
src/transform
/simplify_array.ml
View file @
1cedcd8c
...
...
@@ -17,7 +17,6 @@
(* *)
(**************************************************************************)
open
Why
open
Term
open
Theory
open
Env
...
...
@@ -31,7 +30,7 @@ let make_rt_rf env =
let
array
=
try
find_theory
env
prelude
array
with
TheoryNotFound
(
l
,
s
)
->
with
TheoryNotFound
(
_
,
s
)
->
Format
.
eprintf
"The theory %s is unknown"
s
;
exit
1
in
let
store
=
(
ns_find_ls
array
.
th_export
store
)
.
ls_name
in
...
...
@@ -49,8 +48,8 @@ let make_rt_rf env =
let
t
=
Register
.
store_env
(
fun
()
env
->
(
fun
env
->
let
rt
,
rf
=
make_rt_rf
env
in
Trans
.
rewrite
rt
rf
None
)
let
()
=
Driv
er
.
register_transform
"simplify_array"
t
let
()
=
Regist
er
.
register_transform
"simplify_array"
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