Commit 37da1e08 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Better formatting of why3doc

{h ... }: html escape
[ ... ] : Why3 code escape
parent 7d05b166
......@@ -1185,6 +1185,7 @@ STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS)))
stdlibdoc: $(STDLIBFILES) bin/why3doc
mkdir -p doc/stdlibdoc
rm -f doc/stdlibdoc/style.css
bin/why3doc -o doc/stdlibdoc $(STDLIBFILES)
clean::
......
......@@ -48,22 +48,19 @@ a:active {color : Red; text-decoration : underline; }
.warning { color : Red ; font-weight : bold }
.info { margin-left : 3em; margin-right : 3em }
.code { color : #465F91 ; }
h1 { font-size : 20pt ; text-align: center; }
h2 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ;padding: 2px; }
h3 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ;padding: 2px; }
h4 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90EDFF ;padding: 2px; }
h5 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90FDFF ;padding: 2px; }
h6 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ; padding: 2px; }
div.h7 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ; padding: 2px; }
div.h8 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #F0FFFF ; padding: 2px; }
div.h9 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #FFFFFF ; padding: 2px; }
h1 { font-size : 20pt ; border: 1px solid #000000; margin-top: 10px; margin-bottom: 10px;text-align: center; background-color: #90BDFF ;padding: 10px; }
h2 { font-size : 18pt ; border: 1px solid #000000; margin-top: 8px; margin-bottom: 8px;text-align: left; background-color: #90DDFF ;padding: 8px; }
h3 { font-size : 16pt ; border: 1px solid #000000; margin-top: 6px; margin-bottom: 6px;text-align: left; background-color: #90EDFF ;padding: 6px; }
h4 { font-size : 14pt ; border: 1px solid #000000; margin-top: 4px; margin-bottom: 4px;text-align: left; background-color: #90FDFF ;padding: 4px; }
h5 { font-size : 12pt ; border: 1px solid #000000; margin-top: 2px; margin-bottom: 2px;text-align: left; background-color: #90BDFF ; padding: 2px; }
h6 { font-size : 10pt ; border: 1px solid #000000; margin-top: 0px; margin-bottom: 0px;text-align: left; background-color: #90BDFF ; padding: 0px; }
.typetable { border-style : hidden }
.indextable { border-style : hidden }
.paramstable { border-style : hidden ; padding: 5pt 5pt}
body { background-color : White }
tr { background-color : White }
td.typefieldcomment { background-color : #FFFFFF }
pre { margin-bottom: 4px }
pre { margin-top: 1px ; margin-bottom: 2px; }
div.sig_block {margin-left: 2em}";
close_out c
......@@ -28,11 +28,10 @@
let output_comments = ref true
let newline lexbuf fmt =
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum };
fprintf fmt "\n"
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let make_table l =
let ht = Hashtbl.create 97 in
......@@ -65,19 +64,37 @@
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
rule scan fmt = parse
| "(*)" { fprintf fmt "(*)"; scan fmt lexbuf }
| "(**" { fprintf fmt "</pre>@\n";
doc fmt [] lexbuf;
fprintf fmt "<pre>@\n";
scan fmt lexbuf }
| "(*i" { comment fmt false lexbuf;
scan fmt lexbuf }
| "(*" { fprintf fmt "<font class=\"comment\">(*";
comment fmt true lexbuf;
fprintf fmt "</font>";
scan fmt lexbuf }
| eof { () }
rule scan fmt embedded = parse
| "(*)" as s
{ pp_print_string fmt s; scan fmt embedded lexbuf }
| "(***" as s
{ if embedded then pp_print_string fmt s else
comment fmt false lexbuf;
scan fmt embedded lexbuf }
| "(**" as s
{ if embedded then pp_print_string fmt s else
begin
fprintf fmt "</pre>@\n";
doc fmt [] lexbuf;
fprintf fmt "<pre>@\n";
end;
scan fmt embedded lexbuf }
| "(*" as s
{ if embedded then pp_print_string fmt s else
begin
fprintf fmt "<font class=\"comment\">(*";
comment fmt true lexbuf;
fprintf fmt "</font>";
end;
scan fmt embedded lexbuf }
| ']' as c
{ if embedded then () else
begin
pp_print_char fmt c;
scan fmt embedded lexbuf
end
}
| eof { () }
| ident as s
{ if is_keyword1 s then
fprintf fmt "<font class=\"keyword1\">%s</font>" s
......@@ -98,17 +115,17 @@ rule scan fmt = parse
fprintf fmt "<a href=\"%s#%s\">%s</a>" fn t s
with Not_found ->
(* otherwise, just print it *)
fprintf fmt "%s" s
pp_print_string fmt s
end;
scan fmt lexbuf }
| "<" { fprintf fmt "&lt;"; scan fmt lexbuf }
| ">" { fprintf fmt "&gt;"; scan fmt lexbuf }
| "&" { fprintf fmt "&amp;"; scan fmt lexbuf }
| "\n" { newline lexbuf fmt; scan fmt lexbuf }
scan fmt embedded lexbuf }
| "<" { fprintf fmt "&lt;"; scan fmt embedded lexbuf }
| ">" { fprintf fmt "&gt;"; scan fmt embedded lexbuf }
| "&" { fprintf fmt "&amp;"; scan fmt embedded lexbuf }
| "\n" { newline lexbuf; fprintf fmt "\n"; scan fmt embedded lexbuf }
| '"' { fprintf fmt "&quot;"; string fmt true lexbuf;
scan fmt lexbuf }
scan fmt embedded lexbuf }
| "'\"'"
| _ as s { fprintf fmt "%s" s; scan fmt lexbuf }
| _ as s { pp_print_string fmt s; scan fmt embedded lexbuf }
and comment fmt do_output = parse
| "(*" { if do_output then fprintf fmt "(*";
......@@ -116,7 +133,8 @@ and comment fmt do_output = parse
comment fmt do_output lexbuf }
| "*)" { if do_output then fprintf fmt "*)" }
| eof { () }
| "\n" { if do_output then newline lexbuf fmt;
| "\n" { newline lexbuf;
if do_output then fprintf fmt "\n";
comment fmt do_output lexbuf }
| '"' { if do_output then fprintf fmt "&quot;";
string fmt do_output lexbuf;
......@@ -126,11 +144,12 @@ and comment fmt do_output = parse
| "&" { if do_output then fprintf fmt "&amp;";
comment fmt do_output lexbuf }
| "'\"'"
| _ as s { if do_output then fprintf fmt "%s" s;
| _ as s { if do_output then pp_print_string fmt s;
comment fmt do_output lexbuf }
and string fmt do_output = parse
| "\n" { if do_output then newline lexbuf fmt;
| "\n" { newline lexbuf;
if do_output then fprintf fmt "\n";
string fmt do_output lexbuf }
| '"' { if do_output then fprintf fmt "&quot;" }
| "<" { if do_output then fprintf fmt "&lt;";
......@@ -140,29 +159,56 @@ and string fmt do_output = parse
| "&" { if do_output then fprintf fmt "&amp;";
string fmt do_output lexbuf }
| "\\" _
| _ as s { if do_output then fprintf fmt "%s" s;
| _ as s { if do_output then pp_print_string fmt s;
string fmt do_output lexbuf }
and doc fmt headings = parse
| "*)" { () }
| eof { () }
| '{' (['1''2''3'] as c)
{ let n = Char.code c - Char.code '0' + 1 in
| "\n" { newline lexbuf;
fprintf fmt "\n";
doc fmt headings lexbuf }
| '{' (['1'-'6'] as c)
{ let n = Char.code c - Char.code '0' in
fprintf fmt "<h%d>" n;
doc fmt (n::headings) lexbuf }
| '{' { fprintf fmt "{"; doc fmt (0::headings) lexbuf }
| '{''h' { raw_html fmt 0 lexbuf; doc fmt headings lexbuf }
| '{' { fprintf fmt "{"; doc fmt (0::headings) lexbuf }
| '}' { match headings with
| [] -> fprintf fmt "}"; doc fmt headings lexbuf
| n :: r ->
if n >= 2 then fprintf fmt "</h%d>" n else fprintf fmt "}";
doc fmt r lexbuf
}
| [] -> fprintf fmt "}"; doc fmt headings lexbuf
| n :: r ->
if n >= 1 then fprintf fmt "</h%d>" n else
fprintf fmt "}";
doc fmt r lexbuf
}
| '[' { pp_print_string fmt "<code>";
scan fmt true lexbuf;
pp_print_string fmt "</code>";
doc fmt headings lexbuf }
| '"' { fprintf fmt "&quot;"; doc fmt headings lexbuf }
| '\'' { fprintf fmt "&apos;"; doc fmt headings lexbuf }
| '&' { fprintf fmt "&amp;"; doc fmt headings lexbuf }
| "<" { fprintf fmt "&lt;"; doc fmt headings lexbuf }
| ">" { fprintf fmt "&gt;"; doc fmt headings lexbuf }
| _ as c { fprintf fmt "%c" c; doc fmt headings lexbuf }
| _ as c { pp_print_char fmt c; doc fmt headings lexbuf }
and raw_html fmt depth = parse
| eof { () }
| "\n" { newline lexbuf;
fprintf fmt "\n";
raw_html fmt depth lexbuf }
| '{' { fprintf fmt "{"; raw_html fmt (succ depth) lexbuf }
| '}' { if depth = 0 then () else
begin
fprintf fmt "{";
raw_html fmt (pred depth) lexbuf
end }
| _ as c { pp_print_char fmt c; raw_html fmt depth lexbuf }
{
let do_file fmt fname =
......@@ -172,9 +218,8 @@ and doc fmt headings = parse
lb.Lexing.lex_curr_p <-
{ lb.Lexing.lex_curr_p with Lexing.pos_fname = fname };
(* output *)
fprintf fmt "<h1>File %s</h1>" fname;
fprintf fmt "<pre>@\n";
scan fmt lb;
scan fmt false lb;
fprintf fmt "</pre>@\n";
close_in cin
......
......@@ -107,7 +107,7 @@ theory Bag
end
(*i
(***
Local Variables:
compile-command: "why3ide bag.why"
End:
......
(** {1 Formalization of Floating-Point Arithmetic, norm IEEE-754} *)
(** {1 Formalization of Floating-Point Arithmetic}
This formalization follows the {h <a href="http://ieeexplore.ieee.org/servlet/opac?punumber=4610933">IEEE-754 norm</a>}
*)
(** {2 definition of IEEE-754 rounding modes} *)
theory Rounding
......
......@@ -67,7 +67,7 @@ theory IntPathWeight
end
(*i
(***
theory SimplePath
use import list.List
......@@ -96,7 +96,7 @@ theory SimplePath
end
*)
(*i
(***
Local Variables:
compile-command: "make -C .. theories/graph.gui"
End:
......
(** {1 Theory of integers}
This file provides the basic theory of integers, and several additional theories for classical functions
*)
(** {2 Integers and the basic operators} *)
theory Int
constant zero : int = 0
......@@ -13,6 +22,8 @@ theory Int
end
(** {2 Absolute Value} *)
theory Abs
use import Int
......@@ -23,12 +34,14 @@ theory Abs
lemma Abs_pos: forall x:int. abs x >= 0
(*
(***
lemma Abs_zero: forall x:int. abs x = 0 -> x = 0
*)
end
(** {2 Minimum and Maximum} *)
theory MinMax
use import Int
......@@ -36,6 +49,8 @@ theory MinMax
end
(** {2 The Basic Well-Founded Order on Integers} *)
theory Lex2
use import Int
......@@ -47,10 +62,15 @@ theory Lex2
end
(** {2 Euclidean Division}
division and modulo operators with the convention that division
rounds down, and thus modulo is always non-negative
*)
theory EuclideanDivision
(** division and modulo operators with the convention that division
rounds down, and thus modulo is always non-negative *)
use import Int
use import Abs
......@@ -77,7 +97,11 @@ theory EuclideanDivision
end
(** the particular case of Euclidean division by 2 *)
(** {2 Division by 2}
The particular case of Euclidean division by 2
*)
theory Div2
use import Int
......@@ -87,12 +111,17 @@ theory Div2
end
theory ComputerDivision
(** {2 Computer Division}
(** division and modulo operators with the same conventions as
Division and modulo operators with the same conventions as
mainstream programming language such C, Java, OCaml, that is
division rounds towards zero, and thus (x mod y) has the same sign
as x *)
division rounds towards zero, and thus [mod x y] has the same sign
as x
*)
theory ComputerDivision
use import Int
use import Abs
......@@ -142,6 +171,7 @@ theory ComputerDivision
end
(** {2 Generic Exponentation of something to an integer exponent} *)
theory Exponentiation
use import Int
......@@ -165,6 +195,7 @@ theory Exponentiation
end
(** {2 Power of an integer to an integer } *)
theory Power
use import Int
......@@ -174,6 +205,12 @@ theory Power
end
(** {2 Number of elements satisfying a given predicate}
This theory is parametrized by a predicate [pr]. It is supposed to be cloned
with needed instances for [pr]. It is also parametrized by a type [param] to be used as an additional parameter to [pr].
*)
theory NumOfParam
type param
......@@ -247,6 +284,13 @@ theory NumOfParam
end
(** {2 Specific version of number of elements satisfying a predicate}
This is an instance of the above, where the type parameter is unused
*)
theory NumOf
predicate pr int
......@@ -259,7 +303,9 @@ theory NumOf
end
theory Fact "Factorial"
(** {2 Factorial function} *)
theory Fact
use export Int
......@@ -270,6 +316,8 @@ theory Fact "Factorial"
end
(** {2 Generic iteration of a function} *)
theory Iter
use import Int
......@@ -288,7 +336,7 @@ theory Iter
end
(** integers extended with infinity *)
(** {2 Integers extended with an infinite value} *)
theory IntInf
use import Int
......@@ -322,6 +370,12 @@ theory IntInf
end
(** {2 Induction principle on integers}
This theory can be cloned with the wanted predicate, to perform an induction, either
on non-negative integers, or more generally on integers greater or equal a given bound.
*)
theory Induction
......@@ -342,7 +396,7 @@ theory Induction
end
(*i
(***
Local Variables:
compile-command: "make -C .. theories/int.gui"
End:
......
(** {1 Theory of reals}
This file provides the basic theory of real numbers, and several additional theories for classical real functions
*)
(** {2 Real numbers and the basic unary and binary operators} *)
theory Real
constant zero : real = 0.0
......@@ -11,12 +19,18 @@ theory Real
clone export algebra.OrderedField with type t = real,
constant zero = zero, constant one = one, predicate (<=) = (<=)
(*
(***
lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
*)
end
(** {2 Alternative Infix Operators}
This theory should be used instead of Real when one wants to use both integer and real binary operators.
*)
theory RealInfix
use import Real
......@@ -35,6 +49,8 @@ theory RealInfix
end
(** {2 Absolute Value} *)
theory Abs
use import Real
......@@ -45,7 +61,7 @@ theory Abs
lemma Abs_pos: forall x:real. abs x >= 0.0
(*
(***
lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
*)
......@@ -58,6 +74,8 @@ theory Abs
end
(** {2 Minimum and Maximum} *)
theory MinMax
use import Real
......@@ -72,6 +90,8 @@ theory MinMax
end
(** {2 Injection of integers into reals} *)
theory FromInt
use int.Int
......@@ -93,6 +113,8 @@ theory FromInt
end
(** {2 Various truncation functions} *)
theory Truncate
use import Real
......@@ -150,6 +172,7 @@ theory Truncate
end
(** {2 Square and Square Root} *)
theory Square
......@@ -170,6 +193,8 @@ theory Square
end
(** {2 Exponential and Logarithm} *)
theory ExpLog
use import Real
......@@ -194,6 +219,7 @@ theory ExpLog
end
(** {2 Power of a real to an integer} *)
theory PowerInt
use int.Int
......@@ -205,6 +231,7 @@ theory PowerInt
end
(** {2 Power of a real to a real exponent} *)
theory PowerReal
use import Real
......@@ -237,9 +264,9 @@ theory PowerReal
end
(** {2 Trigonometric functions}
(** {2 Trigonometric Functions}
See [http://en.wikipedia.org/wiki/Trigonometric_function]
See {h <a href="http://en.wikipedia.org/wiki/Trigonometric_function">wikipedia page</a>}
*)
theory Trigonometry
......@@ -295,8 +322,8 @@ theory Trigonometry
end
(** {2 hyperbolic functions}
See [http://en.wikipedia.org/wiki/Hyperbolic_function]
(** {2 Hyperbolic Functions}
See {h <a href="http://en.wikipedia.org/wiki/Hyperbolic_function">wikipedia page</a>}
*)
theory Hyperbolic
......@@ -318,8 +345,8 @@ theory Hyperbolic
end
(** {2 polar coordinates}
atan2, hypot, see [http://en.wikipedia.org/wiki/Atan2]
(** {2 Polar Coordinates}
atan2, hypot, see {h <a href="http://en.wikipedia.org/wiki/Atan2">wikipedia page</a>}
*)
theory Polar
......
......@@ -241,7 +241,7 @@ theory SetMap
end
(*i
(***
Local Variables:
compile-command: "make -C .. theories/set"
End:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment