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
210ce906
Commit
210ce906
authored
Mar 22, 2010
by
Francois Bobot
Browse files
alt-ergo.ml : Ajout d'un flush entre chaque declarations
parent
86d4f8ff
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/printer/alt_ergo.ml
View file @
210ce906
...
...
@@ -53,10 +53,12 @@ let rec print_type drv fmt ty = match ty.ty_node with
|
Tyapp
(
ts
,
[]
)
->
print_ident
fmt
ts
.
ts_name
|
Tyapp
(
ts
,
[
ty
])
->
fprintf
fmt
"%a %a"
(
print_type
drv
)
ty
print_ident
ts
.
ts_name
fprintf
fmt
"%a %a"
(
print_type
drv
)
ty
print_ident
ts
.
ts_name
|
Tyapp
(
ts
,
tyl
)
->
fprintf
fmt
"(%a) %a"
(
print_list
comma
(
print_type
drv
))
tyl
print_ident
ts
.
ts_name
(
print_list
comma
(
print_type
drv
))
tyl
print_ident
ts
.
ts_name
end
let
rec
print_term
drv
fmt
t
=
match
t
.
t_node
with
|
Tbvar
_
->
...
...
@@ -126,7 +128,8 @@ let rec print_fmla drv fmt f = match f.f_node with
fprintf
fmt
"false"
|
Fif
(
f1
,
f2
,
f3
)
->
fprintf
fmt
"((%a and %a) or (not %a and %a))"
(
print_fmla
drv
)
f1
(
print_fmla
drv
)
f2
(
print_fmla
drv
)
f1
(
print_fmla
drv
)
f3
(
print_fmla
drv
)
f1
(
print_fmla
drv
)
f2
(
print_fmla
drv
)
f1
(
print_fmla
drv
)
f3
|
Flet
_
->
assert
false
|
Fcase
_
->
...
...
@@ -207,7 +210,7 @@ let print_decl drv task fmt d = match d.d_node with
let
print_context
drv
fmt
task
=
let
decls
=
Task
.
task_decls
task
in
ignore
(
print_list_opt
newline2
(
print_decl
drv
task
)
fmt
decls
)
ignore
(
print_list_opt
(
add_flush
newline2
)
(
print_decl
drv
task
)
fmt
decls
)
let
()
=
Driver
.
register_printer
"alt-ergo"
(
fun
drv
fmt
task
->
...
...
src/util/pp.ml
View file @
210ce906
...
...
@@ -90,6 +90,7 @@ let rchevron fmt () = fprintf fmt ">"
let
nothing
fmt
_
=
()
let
string
fmt
s
=
fprintf
fmt
"%s"
s
let
constant_string
s
fmt
()
=
string
fmt
s
let
add_flush
sep
fmt
x
=
sep
fmt
x
;
pp_print_flush
fmt
()
let
print_pair
pr1
=
print_pair_delim
lparen
comma
rparen
pr1
...
...
src/util/pp.mli
View file @
210ce906
...
...
@@ -86,12 +86,15 @@ val nothing : formatter -> 'a -> unit
val
string
:
formatter
->
string
->
unit
val
constant_string
:
string
->
formatter
->
unit
->
unit
val
hov
:
int
->
formatter
->
(
'
a
->
unit
)
->
'
a
->
unit
val
add_flush
:
(
formatter
->
'
a
->
unit
)
->
formatter
->
'
a
->
unit
val
open_formatter
:
?
margin
:
int
->
out_channel
->
formatter
val
close_formatter
:
formatter
->
unit
val
open_file_and_formatter
:
?
margin
:
int
->
string
->
out_channel
*
formatter
val
close_file_and_formatter
:
out_channel
*
formatter
->
unit
val
print_in_file_no_close
:
?
margin
:
int
->
(
Format
.
formatter
->
unit
)
->
string
->
out_channel
val
print_in_file_no_close
:
?
margin
:
int
->
(
Format
.
formatter
->
unit
)
->
string
->
out_channel
val
print_in_file
:
?
margin
:
int
->
(
Format
.
formatter
->
unit
)
->
string
->
unit
...
...
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