Skip to content

why3
why3
Commit 48131b9f authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Nicer output for why3doc

parent a30f305f
Hide whitespace changes
Inline Side-by-side
Showing with 121 additions and 68 deletions
.gitignore
View file @ 48131b9f
......@@ -113,6 +113,7 @@ why3.conf
/doc/*_bnf.tex
/doc/apidoc.tex
/doc/apidoc/
/doc/stdlibdoc/
# /share/
/share/provers-detection-data.conf
......
src/why3doc/doc_html.ml
View file @ 48131b9f
......@@ -28,10 +28,10 @@ let print_header fmt ?(title="") ?css () =
"<link rel=\"stylesheet\" href=\"%s\" type=\"text/css\">@\n" f
end;
fprintf fmt "<title>%s</title>@\n" title;
fprintf fmt "</head>@\n<body>@\n<pre>@\n"
fprintf fmt "</head>@\n<body>@\n"
let print_footer fmt () =
fprintf fmt "</pre></body>@."
fprintf fmt "<hr>@\nGenerated by why3doc@\n</body>@."
let style_css fname =
let c = open_out fname in
......
src/why3doc/doc_lexer.mll
View file @ 48131b9f
......@@ -26,6 +26,8 @@
open Lexing
open Why3
let output_comments = ref true
let newline lexbuf fmt =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
......@@ -65,8 +67,14 @@ 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 lexbuf;
comment fmt true lexbuf;
fprintf fmt "</font>";
scan fmt lexbuf }
| eof { () }
......@@ -94,31 +102,67 @@ rule scan fmt = parse
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 }
| '"' { fprintf fmt "\""; string fmt lexbuf; scan fmt lexbuf }
| '"' { fprintf fmt "&quot;"; string fmt true lexbuf;
scan fmt lexbuf }
| "'\"'"
| _ as s { fprintf fmt "%s" s; scan fmt lexbuf }
and comment fmt = parse
| "(*" { fprintf fmt "(*"; comment fmt lexbuf; comment fmt lexbuf }
| "*)" { fprintf fmt "*)" }
and comment fmt do_output = parse
| "(*" { if do_output then fprintf fmt "(*";
comment fmt do_output lexbuf;
comment fmt do_output lexbuf }
| "*)" { if do_output then fprintf fmt "*)" }
| eof { () }
| "\n" { newline lexbuf fmt; comment fmt lexbuf }
| '"' { fprintf fmt "\""; string fmt lexbuf; comment fmt lexbuf }
| "<" { fprintf fmt "&lt;"; comment fmt lexbuf }
| "&" { fprintf fmt "&amp;"; comment fmt lexbuf }
| "\n" { if do_output then newline lexbuf fmt;
comment fmt do_output lexbuf }
| '"' { if do_output then fprintf fmt "&quot;";
string fmt do_output lexbuf;
comment fmt do_output lexbuf }
| "<" { if do_output then fprintf fmt "&lt;";
comment fmt do_output lexbuf }
| "&" { if do_output then fprintf fmt "&amp;";
comment fmt do_output lexbuf }
| "'\"'"
| _ as s { fprintf fmt "%s" s; comment fmt lexbuf }
and string fmt = parse
| "\n" { newline lexbuf fmt; string fmt lexbuf }
| '"' { fprintf fmt "\"" }
| "<" { fprintf fmt "&lt;"; string fmt lexbuf }
| "&" { fprintf fmt "&amp;"; string fmt lexbuf }
| _ as s { if do_output then fprintf fmt "%s" s;
comment fmt do_output lexbuf }
and string fmt do_output = parse
| "\n" { if do_output then newline lexbuf fmt;
string fmt do_output lexbuf }
| '"' { if do_output then fprintf fmt "&quot;" }
| "<" { if do_output then fprintf fmt "&lt;";
string fmt do_output lexbuf }
| ">" { if do_output then fprintf fmt "&gt;";
string fmt do_output lexbuf }
| "&" { if do_output then fprintf fmt "&amp;";
string fmt do_output lexbuf }
| "\\" _
| _ as s { fprintf fmt "%s" s; string fmt lexbuf }
| _ as s { if do_output then fprintf fmt "%s" 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
fprintf fmt "<h%d>" n;
doc fmt (n::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 "&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 }
{
let do_file fmt fname =
......@@ -128,6 +172,7 @@ and string fmt = 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;
fprintf fmt "</pre>@\n";
......
theories/algebra.why
View file @ 48131b9f
(** Basic Algebra Theories *)
theory Assoc
type t
function op t t : t
......
theories/bag.why
View file @ 48131b9f
(* Multisets (aka bags) *)
(** {1 Multisets (aka bags)} *)
theory Bag
......@@ -7,7 +7,7 @@ theory Bag
type bag 'a
(* the most basic operation is the number of occurrences *)
(** the most basic operation is the number of occurrences *)
function nb_occ (x: 'a) (b: bag 'a): int
......@@ -15,14 +15,14 @@ theory Bag
predicate mem (x: 'a) (b: bag 'a) = nb_occ x b > 0
(* equality of bags *)
(** equality of bags *)
predicate eq_bag (a b: bag 'a) =
forall x:'a. nb_occ x a = nb_occ x b
axiom bag_extensionality: forall a b: bag 'a. eq_bag a b -> a = b
(* basic constructors of bags *)
(** basic constructors of bags *)
function empty_bag: bag 'a
......@@ -48,7 +48,7 @@ theory Bag
forall x: 'a, a b: bag 'a.
nb_occ x (union a b) = nb_occ x a + nb_occ x b
(* union commutative, associative with identity empty_bag *)
(** union commutative, associative with identity empty_bag *)
lemma Union_comm: forall a b: bag 'a. union a b = union b a
......@@ -63,7 +63,7 @@ theory Bag
lemma bag_simpl_left:
forall a b c: bag 'a. union a b = union a c -> b = c
(* add operation *)
(** add operation *)
function add (x: 'a) (b: bag 'a) : bag 'a = union (singleton x) b
......@@ -74,7 +74,7 @@ theory Bag
lemma occ_add_neq: forall b: bag 'a, x y: 'a.
x <> y -> nb_occ y (add x b) = nb_occ y b
(* cardinality of bags *)
(** cardinality of bags *)
function card (bag 'a): int
......@@ -85,7 +85,7 @@ theory Bag
axiom Card_union: forall x y: bag 'a. card (union x y) = card x + card y
lemma Card_add: forall x: 'a, b: bag 'a. card (add x b) = 1 + card b
(* bag difference *)
(** bag difference *)
use import int.MinMax
......@@ -107,7 +107,7 @@ theory Bag
end
(*
(*i
Local Variables:
compile-command: "why3ide bag.why"
End:
......
theories/floating_point.why
View file @ 48131b9f
(** {1 Formalization of Floating-Point Arithmetic, norm IEEE-754} *)
(* definition of IEEE-754 rounding modes *)
(** {2 definition of IEEE-754 rounding modes} *)
theory Rounding
type mode = NearestTiesToEven | ToZero | Up | Down | NearestTiesToAway
......@@ -9,7 +10,7 @@ theory Rounding
end
(* handling of IEEE-754 special values +\infty, -\infty, NaN, +0, -0 *)
(** {2 handling of IEEE-754 special values +\infty, -\infty, NaN, +0, -0} *)
theory SpecialValues
type class = Finite | Infinite | NaN
......@@ -71,7 +72,7 @@ theory GenFloat
Int.(<=) i max_representable_integer ->
round m (from_int i) = from_int i
(* rounding up and down *)
(** rounding up and down *)
axiom Round_down_le:
forall x:real. round Down x <= x
axiom Round_up_ge:
......@@ -123,7 +124,7 @@ theory GenFloatFull
clone export GenFloat
(* special values *)
(** special values *)
function class t : class
predicate is_finite (x:t) = class x = Finite
......
theories/graph.why
View file @ 48131b9f
(* Graph theory *)
(** {1 Graph theory} *)
theory Path
......@@ -10,7 +10,7 @@ theory Path
predicate edge vertex vertex
(* path v0 [v0; v1; ...; vn-1] vn
(** path v0 [v0; v1; ...; vn-1] vn
means a path from v0 to vn composed of n edges (vi,vi+1) *)
inductive path vertex (list vertex) vertex =
| Path_empty:
......@@ -49,7 +49,7 @@ theory IntPathWeight
function weight vertex vertex : int
(* the total weight of a path [path _ l dst] *)
(** the total weight of a path [path _ l dst] *)
function path_weight (l: list vertex) (dst: vertex) : int = match l with
| Nil -> 0
| Cons x Nil -> weight x dst
......@@ -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:
......
theories/int.why
View file @ 48131b9f
......@@ -49,7 +49,7 @@ end
theory EuclideanDivision
(* division and modulo operators with the convention that division
(** division and modulo operators with the convention that division
rounds down, and thus modulo is always non-negative *)
use import Int
......@@ -77,7 +77,7 @@ theory EuclideanDivision
end
(* the particular case of Euclidean division by 2 *)
(** the particular case of Euclidean division by 2 *)
theory Div2
use import Int
......@@ -89,7 +89,7 @@ end
theory ComputerDivision
(* 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 *)
......@@ -288,7 +288,7 @@ theory Iter
end
(* integers extended with infinity *)
(** integers extended with infinity *)
theory IntInf
use import Int
......@@ -342,7 +342,7 @@ theory Induction
end
(*
(*i
Local Variables:
compile-command: "make -C .. theories/int.gui"
End:
......
theories/real.why
View file @ 48131b9f
......@@ -98,7 +98,7 @@ theory Truncate
use import Real
use import FromInt
(* truncate: rounds towards zero *)
(** truncate: rounds towards zero *)
function truncate real : int
......@@ -125,7 +125,7 @@ theory Truncate
axiom Truncate_monotonic_int2:
forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x)
(* roundings up and down *)
(** roundings up and down *)
function floor real : int
function ceil real : int
......@@ -237,8 +237,9 @@ theory PowerReal
end
(** Trigonometric functions
[http://en.wikipedia.org/wiki/Trigonometric_function]
(** {2 Trigonometric functions}
See [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
theory Trigonometry
......@@ -294,8 +295,8 @@ theory Trigonometry
end
(** hyperbolic functions
[http://en.wikipedia.org/wiki/Hyperbolic_function]
(** {2 hyperbolic functions}
See [http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
theory Hyperbolic
......@@ -317,8 +318,8 @@ theory Hyperbolic
end
(** polar coordinates: atan2, hypot
[http://en.wikipedia.org/wiki/Atan2]
(** {2 polar coordinates}
atan2, hypot, see [http://en.wikipedia.org/wiki/Atan2]
*)
theory Polar
......
theories/set.why
View file @ 48131b9f
(** {1 Set theories} *)
theory Set
type set 'a
(* membership *)
(** membership *)
predicate mem 'a (set 'a)
(* equality *)
(** equality *)
predicate (==) (s1 s2: set 'a) = forall x : 'a. mem x s1 <-> mem x s2
axiom extensionality:
forall s1 s2: set 'a. s1 == s2 -> s1 = s2
(* inclusion *)
(** inclusion *)
predicate subset (s1 s2: set 'a) = forall x : 'a. mem x s1 -> mem x s2
lemma subset_trans:
forall s1 s2 s3: set 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3
(* empty set *)
(** empty set *)
constant empty : set 'a
predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s)
axiom empty_def1: is_empty (empty : set 'a)
(* addition *)
(** addition *)
function add 'a (set 'a) : set 'a
axiom add_def1:
......@@ -34,7 +36,7 @@ theory Set
function singleton (x: 'a) : set 'a = add x empty
(* removal *)
(** removal *)
function remove 'a (set 'a) : set 'a
axiom remove_def1:
......@@ -44,21 +46,21 @@ theory Set
lemma subset_remove:
forall x: 'a, s: set 'a. subset (remove x s) s
(* union *)
(** union *)
function union (set 'a) (set 'a) : set 'a
axiom union_def1:
forall s1 s2: set 'a, x: 'a.
mem x (union s1 s2) <-> mem x s1 \/ mem x s2
(* intersection *)
(** intersection *)
function inter (set 'a) (set 'a) : set 'a
axiom inter_def1:
forall s1 s2: set 'a, x: 'a.
mem x (inter s1 s2) <-> mem x s1 /\ mem x s2
(* difference *)
(** difference *)
function diff (set 'a) (set 'a) : set 'a
axiom diff_def1:
......@@ -68,13 +70,13 @@ theory Set
lemma subset_diff:
forall s1 s2: set 'a. subset (diff s1 s2) s1
(* arbitrary element *)
(** arbitrary element *)
function choose (s:set 'a) : 'a
axiom choose_def:
forall s: set 'a. not (is_empty s) -> mem (choose s) s
(* the set of all x of type 'a *)
(** the set of all x of type 'a *)
constant all: set 'a
axiom all_def: forall x: 'a. mem x all
......@@ -86,18 +88,18 @@ theory SetComprehension
use export Set
use HighOrd as HO
(* { x | p x } *)
(** { x | p x } *)
function comprehension (p: HO.pred 'a) : set 'a
axiom comprehension_def:
forall p: HO.pred 'a.
forall x: 'a. mem x (comprehension p) <-> p x
(* { x | x in U and p(x) *)
(** { x | x in U and p(x) } *)
function filter (p: HO.pred 'a) (u: set 'a) : set 'a =
comprehension (\ x: 'a. p x /\ mem x u)
(* { f x | x in U } *)
(** { f x | x in U } *)
function map (f: HO.func 'a 'b) (u: set 'a) : set 'b =
comprehension (\ y: 'b. exists x: 'a. mem x u /\ y = f x)
......@@ -107,7 +109,8 @@ theory SetComprehension
end
(* finite sets *)
(** {2 finite sets} *)
theory Fset
use import int.Int
clone export Set
......@@ -146,7 +149,7 @@ theory Fset
end
(* finite sets of integers *)
(** {2 finite sets of integers} *)
theory Fsetint
use export int.Int
......@@ -168,7 +171,7 @@ theory Fsetint
forall s: set int. not (is_empty s) ->
forall x: int. mem x s -> x <= max_elt s
(* the set {0,1,...,n-1} *)
(** the set {0,1,...,n-1} *)
function below int : set int
axiom below_def: forall x n: int. mem x (below n) <-> 0 <= x < n
......@@ -238,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