Skip to content
GitLab
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
2de30b06
Commit
2de30b06
authored
May 24, 2017
by
Guillaume Melquiond
Browse files
Preserve realization headers in Coq printer.
parent
0e68a951
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/printer/coq.ml
View file @
2de30b06
...
...
@@ -518,8 +518,9 @@ let read_deprecated_script ch in_context =
let
read_old_script
=
let
axm
=
Str
.
regexp
"
\\
(Axiom
\\
|Parameter
\\
)[ ]+
\\
([^ :(.]+
\\
)"
in
let
prelude
=
Str
.
regexp
"(
\\
* This file is generated by Why3.*
\\
*)"
in
fun
ch
->
let
skip_to_empty
=
ref
tru
e
in
let
skip_to_empty
=
ref
fals
e
in
let
last_empty_line
=
ref
0
in
let
sc
=
ref
[]
in
try
...
...
@@ -538,6 +539,9 @@ let read_old_script =
skip_to_empty
:=
true
)
else
if
s
=
"(* Why3 goal *)"
then
(
sc
:=
read_old_proof
ch
::
!
sc
;
skip_to_empty
:=
true
)
else
if
Str
.
string_match
prelude
s
0
then
(
sc
:=
Info
"Why3 prelude"
::
!
sc
;
skip_to_empty
:=
true
)
else
if
s
=
"(* YOU MAY EDIT THE CONTEXT BELOW *)"
then
(
sc
:=
read_deprecated_script
ch
true
;
raise
End_of_file
)
else
if
s
=
"(* YOU MAY EDIT THE PROOF BELOW *)"
then
...
...
@@ -954,8 +958,6 @@ let print_decls ~old info fmt dl =
let
print_task
printer_args
~
realize
~
ssreflect
?
old
fmt
task
=
(* eprintf "Task:%a@.@." Pretty.print_task task; *)
forget_all
()
;
print_prelude
fmt
printer_args
.
prelude
;
print_th_prelude
task
fmt
printer_args
.
th_prelude
;
(* find theories that are both used and realized from metas *)
let
realized_theories
=
Task
.
on_meta
meta_realized_theory
(
fun
mid
args
->
...
...
@@ -982,8 +984,7 @@ let print_task printer_args ~realize ~ssreflect ?old fmt task =
upd_realized_theories
task
|
_
->
assert
false
in
let
realized_theories
=
upd_realized_theories
task
in
let
realized_theories'
=
Mid
.
map
(
fun
(
th
,
s
)
->
fprintf
fmt
"Require %s.@
\n
"
s
;
th
)
realized_theories
in
let
realized_theories'
=
Mid
.
map
fst
realized_theories
in
let
realized_symbols
=
Task
.
used_symbols
realized_theories'
in
let
local_decls
=
Task
.
local_decls
task
realized_symbols
in
(* eprintf "local_decls:%i@." (List.length local_decls); *)
...
...
@@ -1009,6 +1010,10 @@ let print_task printer_args ~realize ~ssreflect ?old fmt task =
let
old
=
ref
(
match
old
with
|
None
->
[]
|
Some
ch
->
read_old_script
ch
)
in
ignore
(
output_till_statement
fmt
old
"Why3 prelude"
);
print_prelude
fmt
printer_args
.
prelude
;
print_th_prelude
task
fmt
printer_args
.
th_prelude
;
Mid
.
iter
(
fun
_
(
_
,
s
)
->
fprintf
fmt
"Require %s.@
\n
"
s
)
realized_theories
;
print_decls
~
old
info
fmt
local_decls
;
output_remaining
fmt
!
old
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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