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
001a7db8
Commit
001a7db8
authored
Mar 17, 2010
by
Andrei Paskevich
Browse files
move driver to its proper directory
parent
a9239775
Changes
21
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
001a7db8
...
...
@@ -63,7 +63,7 @@ DYNLINKOFLAGS =
endif
INCLUDES
=
-I
src/core
-I
src/util
-I
src/parser
-I
src/output
\
INCLUDES
=
-I
src/core
-I
src/util
-I
src/driver
-I
src/parser
-I
src/output
\
-I
src/transform
-I
src/programs
-I
src
BFLAGS
=
-w
Aelz
-dtypes
-g
$(INCLUDES)
@INCLUDEGTK2@
-I
+threads @OCAMLGRAPHLIB@ str.cma unix.cma
$(DYNLINKBFLAGS)
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
...
...
@@ -76,10 +76,10 @@ COQLIB = "@COQLIB@"
COQVER
=
@COQVER@
GENERATED
=
src/version.ml src/parser/parser.mli src/parser/parser.ml
\
src/parser/lexer.ml src/
output
/driver_lexer.ml
\
src/
output
/driver_parser.mli src/
output
/driver_parser.ml
\
src/parser/lexer.ml src/
driver
/driver_lexer.ml
\
src/
driver
/driver_parser.mli src/
driver
/driver_parser.ml
\
src/programs/pgm_lexer.ml src/programs/pgm_parser.mli
\
src/programs/pgm_parser.ml src/
util
/dynlink_compat.ml
src/programs/pgm_parser.ml src/
driver
/dynlink_compat.ml
# main targets
##############
...
...
@@ -117,30 +117,28 @@ doc/version.tex src/version.ml: Version version.sh config.status
# why
#####
CORE_CMO
:=
ident.cmo ty.cmo term.cmo decl.cmo theory2.cmo
\
task.cmo
env.cmo theory
.cmo pretty.cmo
CORE_CMO
:=
ident.cmo ty.cmo term.cmo decl.cmo
theory.cmo
theory2.cmo
\
task.cmo
trans.cmo env
.cmo pretty.cmo
CORE_CMO
:=
$(
addprefix
src/core/,
$(CORE_CMO)
)
UTIL_CMO
:=
pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo
\
dynlink_compat.cmo
UTIL_CMO
:=
pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo
UTIL_CMO
:=
$(
addprefix
src/util/,
$(UTIL_CMO)
)
PARSER_CMO
:=
parser.cmo lexer.cmo typing.cmo
PARSER_CMO
:=
$(
addprefix
src/parser/,
$(PARSER_CMO)
)
TRANSFORM_CMO
:=
simplify_recursive_definition.cmo inlining.cmo
\
split_conjunction.cmo split_goals.cmo
split_conjunction.cmo split_goals.cmo
TRANSFORM_CMO
:=
$(
addprefix
src/transform/,
$(TRANSFORM_CMO)
)
DRIVER_CMO
:=
call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo
DRIVER_CMO
:=
$(
addprefix
src/output/,
$(DRIVER_CMO)
)
DRIVER_CMO
:=
call_provers.cmo dynlink_compat.cmo driver_parser.cmo
\
driver_lexer.cmo driver.cmo
DRIVER_CMO
:=
$(
addprefix
src/driver/,
$(DRIVER_CMO)
)
OUTPUT_CMO
:=
call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo
\
print_real.cmo alt_ergo.cmo why3.cmo
OUTPUT_CMO
:=
print_real.cmo alt_ergo.cmo why3.cmo
OUTPUT_CMO
:=
$(
addprefix
src/output/,
$(OUTPUT_CMO)
)
CMO
=
$(UTIL_CMO)
$(CORE_CMO)
$(PARSER_CMO)
\
src/transform/transform.cmo
$(DRIVER_CMO)
\
CMO
=
$(UTIL_CMO)
$(CORE_CMO)
$(PARSER_CMO)
$(DRIVER_CMO)
\
$(TRANSFORM_CMO)
$(OUTPUT_CMO)
src/main.cmo
CMX
=
$(CMO:.cmo=.cmx)
...
...
@@ -177,8 +175,7 @@ testl: bin/whyl.byte
PGM_CMO
:=
pgm_parser.cmo pgm_lexer.cmo pgm_main.cmo
PGM_CMO
:=
$(
addprefix
src/programs/,
$(PGM_CMO)
)
WHYL_CMO
=
$(UTIL_CMO)
$(CORE_CMO)
$(PARSER_CMO)
\
src/transform/transform.cmo
$(DRIVER_CMO)
\
WHYL_CMO
=
$(UTIL_CMO)
$(CORE_CMO)
$(PARSER_CMO)
$(DRIVER_CMO)
\
$(TRANSFORM_CMO)
$(OUTPUT_CMO)
$(PGM_CMO)
WHYL_CMX
=
$(WHYL_CMO:.cmo=.cmx)
...
...
configure.in
View file @
001a7db8
...
...
@@ -494,7 +494,7 @@ AC_SUBST(PSVIEWER)
AC_SUBST(PDFVIEWER)
# Finally create the Makefile from Makefile.in
dnl AC_OUTPUT(Makefile)
AC_CONFIG_FILES(Makefile bench/bench src/
util
/dynlink_compat.ml)
AC_CONFIG_FILES(Makefile bench/bench src/
driver
/dynlink_compat.ml)
AC_OUTPUT
chmod a-w Makefile
chmod a-w bench/bench
...
...
src/
transf
or
m
/trans
form
.ml
→
src/
c
or
e
/trans.ml
View file @
001a7db8
File moved
src/
transf
or
m
/trans
form
.mli
→
src/
c
or
e
/trans.mli
View file @
001a7db8
File moved
src/
output
/call_provers.ml
→
src/
driver
/call_provers.ml
View file @
001a7db8
File moved
src/
output
/call_provers.mli
→
src/
driver
/call_provers.mli
View file @
001a7db8
File moved
src/
output
/driver.ml
→
src/
driver
/driver.ml
View file @
001a7db8
...
...
@@ -126,7 +126,7 @@ and driver = {
drv_prover
:
Call_provers
.
prover
;
drv_prelude
:
string
option
;
drv_filename
:
string
option
;
drv_transforms
:
Trans
form
.
ctxt_list_t
;
drv_transforms
:
Trans
.
ctxt_list_t
;
drv_rules
:
theory_rules
list
;
drv_thprelude
:
string
Hid
.
t
;
(* the first is the translation only for this ident, the second is also for representant *)
...
...
@@ -144,12 +144,12 @@ let print_driver fmt driver =
(** registering transformation *)
let
(
transforms
:
(
string
,
unit
->
Trans
form
.
ctxt_list_t
)
Hashtbl
.
t
)
let
(
transforms
:
(
string
,
unit
->
Trans
.
ctxt_list_t
)
Hashtbl
.
t
)
=
Hashtbl
.
create
17
let
register_transform'
name
transform
=
Hashtbl
.
replace
transforms
name
transform
let
register_transform
name
t
=
register_transform'
name
(
fun
()
->
Trans
form
.
singleton
(
t
()
))
(
fun
()
->
Trans
.
singleton
(
t
()
))
let
list_transforms
()
=
Hashtbl
.
fold
(
fun
k
_
acc
->
k
::
acc
)
transforms
[]
(** registering printers *)
...
...
@@ -317,9 +317,9 @@ let load_driver file env =
let
t
=
try
(
Hashtbl
.
find
transforms
s
)
()
with
Not_found
->
errorm
~
loc
"unknown transformation %s"
s
in
Trans
form
.
compose'
acc
t
Trans
.
compose'
acc
t
)
Trans
form
.
identity'
transformations
in
Trans
.
identity'
transformations
in
let
transforms
=
trans
ltransforms
in
{
drv_printer
=
!
printer
;
drv_context
=
Context
.
init_context
env
;
...
...
@@ -362,7 +362,7 @@ let syntax_arguments s print fmt l =
(** using drivers *)
let
apply_transforms
drv
=
Trans
form
.
apply
drv
.
drv_transforms
let
apply_transforms
drv
=
Trans
.
apply
drv
.
drv_transforms
let
print_context
drv
fmt
ctxt
=
match
drv
.
drv_printer
with
|
None
->
errorm
"no printer"
...
...
@@ -379,7 +379,7 @@ let filename_of_goal drv ident_printer filename theory_name ctxt =
match
drv
.
drv_filename
with
|
None
->
errorm
"no filename syntax given"
|
Some
f
->
let
pr_name
=
pr_name
(
Trans
form
.
goal_of_ctxt
ctxt
)
in
let
pr_name
=
pr_name
(
Trans
.
goal_of_ctxt
ctxt
)
in
let
repl_fun
s
=
let
i
=
matched_group
1
s
in
match
i
with
...
...
src/
output
/driver.mli
→
src/
driver
/driver.mli
View file @
001a7db8
...
...
@@ -44,8 +44,8 @@ type printer = driver -> formatter -> context -> unit
val
register_printer
:
string
->
printer
->
unit
val
register_transform
:
string
->
(
unit
->
Trans
form
.
ctxt_t
)
->
unit
val
register_transform'
:
string
->
(
unit
->
Trans
form
.
ctxt_list_t
)
->
unit
val
register_transform
:
string
->
(
unit
->
Trans
.
ctxt_t
)
->
unit
val
register_transform'
:
string
->
(
unit
->
Trans
.
ctxt_list_t
)
->
unit
val
list_printers
:
unit
->
string
list
val
list_transforms
:
unit
->
string
list
...
...
src/
output
/driver_ast.mli
→
src/
driver
/driver_ast.mli
View file @
001a7db8
File moved
src/
output
/driver_lexer.mll
→
src/
driver
/driver_lexer.mll
View file @
001a7db8
File moved
src/
output
/driver_parser.mly
→
src/
driver
/driver_parser.mly
View file @
001a7db8
File moved
src/
util
/dynlink_compat.ml.in
→
src/
driver
/dynlink_compat.ml.in
View file @
001a7db8
File moved
src/
util
/dynlink_compat.mli
→
src/
driver
/dynlink_compat.mli
View file @
001a7db8
File moved
src/main.ml
View file @
001a7db8
...
...
@@ -20,7 +20,7 @@
open
Format
open
Theory
open
Driver
open
Trans
form
open
Trans
let
files
=
Queue
.
create
()
let
parse_only
=
ref
false
...
...
@@ -106,9 +106,9 @@ let transformation l =
let t2 = Inlining.all in
List.map (fun (t,c) ->
let c = if !simplify_recursive
then Trans
form
.apply t1 c
then Trans.apply t1 c
else c in
let c = if !inlining then Trans
form
.apply t2 c
let c = if !inlining then Trans.apply t2 c
else c in
(t,c)) l
*)
...
...
@@ -162,7 +162,7 @@ let extract_goals ?filter =
let
split_goals
=
Split_goals
.
t
?
filter
()
in
fun
env
drv
acc
th
->
let
ctxt
=
Context
.
use_export
(
Context
.
init_context
env
)
th
in
let
l
=
Trans
form
.
apply
split_goals
ctxt
in
let
l
=
Trans
.
apply
split_goals
ctxt
in
let
l
=
List
.
rev_map
(
fun
ctxt
->
(
th
,
ctxt
))
l
in
List
.
rev_append
l
acc
...
...
src/transform/inlining.ml
View file @
001a7db8
...
...
@@ -109,7 +109,7 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
|
Duse
_
|
Dclone
_
->
env
,
add_decl
ctxt
d
let
t
~
isnotinlinedt
~
isnotinlinedf
=
Trans
form
.
fold_map
(
fold
isnotinlinedt
isnotinlinedf
)
(
fun
_
->
empty_env
)
Trans
.
fold_map
(
fold
isnotinlinedt
isnotinlinedf
)
(
fun
_
->
empty_env
)
let
all
()
=
t
~
isnotinlinedt
:
(
fun
_
->
false
)
~
isnotinlinedf
:
(
fun
_
->
false
)
...
...
src/transform/inlining.mli
View file @
001a7db8
...
...
@@ -23,17 +23,17 @@
val
t
:
isnotinlinedt
:
(
Term
.
term
->
bool
)
->
isnotinlinedf
:
(
Term
.
fmla
->
bool
)
->
Trans
form
.
ctxt_t
Trans
.
ctxt_t
(* Inline them all *)
val
all
:
unit
->
Trans
form
.
ctxt_t
val
all
:
unit
->
Trans
.
ctxt_t
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val
trivial
:
unit
->
Trans
form
.
ctxt_t
val
trivial
:
unit
->
Trans
.
ctxt_t
(* Function to use in other transformations if inlining is needed *)
...
...
src/transform/simplify_recursive_definition.ml
View file @
001a7db8
...
...
@@ -129,6 +129,6 @@ let elt d =
|
Dind
_
->
[
d
]
(* TODO *)
|
Dprop
_
|
Dclone
_
|
Duse
_
->
[
d
]
let
t
()
=
Trans
form
.
elt
elt
let
t
()
=
Trans
.
elt
elt
let
()
=
Driver
.
register_transform
"simplify_recursive_definition"
t
src/transform/simplify_recursive_definition.mli
View file @
001a7db8
...
...
@@ -20,7 +20,7 @@
(* Simplify the recursive type and logic definition *)
val
t
:
unit
->
Trans
form
.
ctxt_t
val
t
:
unit
->
Trans
.
ctxt_t
(* ungroup recursive definition *)
...
...
src/transform/split_conjunction.ml
View file @
001a7db8
...
...
@@ -92,12 +92,12 @@ let elt split_pos d =
let
split_pos1
=
split_pos
(
fun
acc
x
->
x
::
acc
)
let
split_conjunction
()
=
Trans
form
.
elt'
(
elt
split_pos1
)
let
split_conjunction
()
=
Trans
.
elt'
(
elt
split_pos1
)
let
rec
split_pos2
acc
d
=
split_pos
split_neg2
acc
d
and
split_neg2
acc
d
=
split_neg
split_pos2
acc
d
let
split_to_cnf
()
=
Trans
form
.
elt'
(
elt
split_pos2
)
let
split_to_cnf
()
=
Trans
.
elt'
(
elt
split_pos2
)
let
()
=
Driver
.
register_transform'
"split_conjunction"
split_conjunction
let
()
=
Driver
.
register_transform'
"split_to_cnf"
split_to_cnf
src/transform/split_goals.ml
View file @
001a7db8
...
...
@@ -39,5 +39,5 @@ let t ?filter () =
(
add_decl
ctxt
d1
,
l
)
|
_
->
(
add_decl
ctxt
decl
,
l
)
in
let
g
=
Trans
form
.
fold
f
(
fun
env
->
init_context
env
,
[]
)
in
Trans
form
.
conv_res
g
snd
let
g
=
Trans
.
fold
f
(
fun
env
->
init_context
env
,
[]
)
in
Trans
.
conv_res
g
snd
Prev
1
2
Next
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