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
d8122567
Commit
d8122567
authored
Sep 13, 2011
by
Asma Tafat-Bouzid
Browse files
Latex statistics
parent
21acd69e
Changes
2
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/programs/isqrt/why3session.xml
View file @
d8122567
This diff is collapsed.
Click to expand it.
src/ide/replay.ml
View file @
d8122567
...
...
@@ -301,8 +301,19 @@ let print_statistics files =
(
List
.
rev
files
)
(* Statistics in LaTeX*)
let
rec
goal_latex_stat
g
=
printf
"%s & %b"
(
M
.
goal_name
g
)
(
M
.
goal_proved
g
);
let
rec
provers_latex_stats
provers
g
=
let
proofs
=
M
.
external_proofs
g
in
Hashtbl
.
iter
(
fun
p
_
->
Hashtbl
.
replace
provers
p
()
)
proofs
;
let
tr
=
M
.
transformations
g
in
Hashtbl
.
iter
(
fun
_st
tr
->
let
goals
=
tr
.
M
.
subgoals
in
List
.
iter
(
provers_latex_stats
provers
)
goals
)
tr
(*let rec goal_latex_stat prov g =*)
let
rec
goal_latex_stat
g
=
(* printf "%s & %b" (M.goal_name g) (M.goal_proved g);*)
printf
"%s "
(
M
.
goal_name
g
);
let
proofs
=
M
.
external_proofs
g
in
Hashtbl
.
iter
(
fun
p
pr
->
let
s
=
pr
.
M
.
proof_state
in
match
s
with
...
...
@@ -317,7 +328,11 @@ let rec goal_latex_stat g =
List
.
iter
goal_latex_stat
goals
)
tr
let
theory_latex_stat
t
=
printf
"
\\
begin{tabular}@."
;
printf
" Collect provers used to proof this theory
\n
"
;
let
provers
=
Hashtbl
.
create
9
in
List
.
iter
(
provers_latex_stats
provers
)
(
M
.
goals
t
);
Hashtbl
.
iter
(
fun
p
_
->
printf
" %s :"
p
)
provers
;
printf
"
\\
begin{tabular}{l|c|r}@."
;
List
.
iter
goal_latex_stat
(
M
.
goals
t
);
printf
"
\\
end{tabular}@."
...
...
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