Commit fc16f6f6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve the documentation of the standard library by uniformizing its layout and fix some typos.

parent 02f803a7
......@@ -4,32 +4,39 @@
(** {2 Associativity} *)
theory Assoc
type t
function op t t : t
axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)
end
(** {2 Commutativity} *)
theory Comm
type t
function op t t : t
axiom Comm : forall x y : t. op x y = op y x
end
(** {2 Associativity and Commutativity} *)
theory AC
type t
function op t t : t
clone Assoc with type t = t, function op = op
clone Comm with type t = t, function op = op
meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
end
(** {2 Group theory} *)
theory Group
type t
constant unit : t
......@@ -51,16 +58,18 @@ end
(** {2 Commutative groups} *)
theory CommutativeGroup
clone export Group
clone Comm with type t = t, function op = op
meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
end
(** {2 Rings} *)
theory Ring
type t
constant zero : t
function (+) t t : t
......@@ -77,28 +86,34 @@ theory Ring
axiom Mul_distr: forall x y z : t. x * (y + z) = x * y + x * z
function (-) (x y : t) : t = x + -y
end
(** {2 Commutative Rings} *)
theory CommutativeRing
clone export Ring
clone Comm with type t = t, function op = (*)
meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*)
end
(** {2 Commutative Rings with Unit} *)
theory UnitaryCommutativeRing
clone export CommutativeRing
constant one : t
axiom Unitary : forall x:t. one * x = x
axiom NonTrivialRing : zero <> one
end
(** {2 Ordered Commutative Rings} *)
theory OrderedUnitaryCommutativeRing
clone export UnitaryCommutativeRing
predicate (<=) t t
predicate (>=) (x y : t) = y <= x
......@@ -110,11 +125,13 @@ theory OrderedUnitaryCommutativeRing
forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult :
forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
(** {2 Field theory} *)
theory Field
clone export UnitaryCommutativeRing
function inv t : t
axiom Inverse : forall x:t. x <> zero -> x * inv x = one
......@@ -137,6 +154,7 @@ end
(** {2 Ordered Fields} *)
theory OrderedField
clone export Field
predicate (<=) t t
......@@ -148,6 +166,7 @@ theory OrderedField
axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult :
forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
(***
......
......@@ -19,10 +19,10 @@ theory Abs
function abs(x : t) : t
axiom Abs_def : if ge x zero then abs x = x else abs x = neg x
*)
end
end
(** {2 minimum and maximum} *)
(** {2 Minimum and maximum} *)
theory MinMax
......@@ -57,5 +57,4 @@ theory MinMax
function max (x y : t) : t = if ge x y then x else y
*)
end
(** {1 Formalization of Floating-Point Arithmetic}
(** {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>}
This formalization follows the {h <a href="http://ieeexplore.ieee.org/servlet/opac?punumber=4610933">IEEE-754 standard</a>}.
*)
(** {2 definition of IEEE-754 rounding modes} *)
(** {2 Definition of IEEE-754 rounding modes} *)
theory Rounding
type mode = NearestTiesToEven | ToZero | Up | Down | NearestTiesToAway
......@@ -13,15 +14,15 @@ theory Rounding
end
(** {2 Handling of IEEE-754 special values}
(** {2 handling of IEEE-754 special values}
Special values are +infinity, -infinity; NaN, +0, -0. These are
Special values are +infinity, -infinity, NaN, +0, -0. These are
handled as described in {h <a
href="http://www.lri.fr/~marche/ayad10ijcar.pdf">[Ayad, March&eacute;,
IJCAR, 2010]</a>}
href="http://www.lri.fr/~marche/ayad10ijcar.pdf">[Ayad, Marché,
IJCAR, 2010]</a>}.
*)
theory SpecialValues
type class = Finite | Infinite | NaN
......@@ -43,7 +44,7 @@ the maximal representable number, and the integer constant
[max_representable_integer] which is the maximal integer [n] such that
every integer between [0] and [n] are representable.
*)
*)
theory GenFloat
......@@ -104,10 +105,11 @@ theory GenFloat
end
(** {2 single precision floats}
(** {2 Single precision floats}
a.k.a 32-bits floats
*)
A.k.a. binary32 numbers.
*)
theory Single
......@@ -123,12 +125,12 @@ theory Single
end
(** {2 Double precision floats}
A.k.a. binary64 numbers.
(** {2 Double precision floats}
*)
a.k.a 64-bits floats
*)
theory Double
type double
......@@ -143,12 +145,11 @@ theory Double
end
(** {2 Generic Full theory of floats}
this theory extends the generic theory above by adding the special values
This theory extends the generic theory above by adding the special values.
*)
*)
theory GenFloatFull
......@@ -216,7 +217,6 @@ theory GenFloatFull
end
(** {2 Full theory of single precision floats} *)
theory SingleFull
......@@ -233,7 +233,6 @@ theory SingleFull
end
(** {2 Full theory of double precision floats} *)
theory DoubleFull
......@@ -241,7 +240,7 @@ theory DoubleFull
type double
constant max_double : real = 0x1.FFFFFFFFFFFFFp1023
constant max_int : int = 9007199254740992 (* 2^23 *)
constant max_int : int = 9007199254740992 (* 2^53 *)
clone export GenFloatFull with
type t = double,
......
theory Injective
type a
type v
function to_ a : v
......@@ -12,6 +13,7 @@ theory Injective
end
theory Surjective
type a
type v
function to_ a : v
......@@ -27,4 +29,4 @@ theory Bijective
use import Injective
clone Surjective with namespace . = .
end
\ No newline at end of file
end
......@@ -10,8 +10,8 @@ theory Path
predicate edge vertex vertex
(** path v0 [v0; v1; ...; vn-1] vn
means a path from v0 to vn composed of n edges (vi,vi+1) *)
(** [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:
forall x: vertex. path x Nil x
......
......@@ -2,11 +2,10 @@
(** {1 Theory of integers}
This file provides the basic theory of integers, and several additional
theories for classical functions
theories for classical functions.
*)
(** {2 Integers and the basic operators} *)
theory Int
......@@ -65,7 +64,7 @@ end
(** {2 Euclidean Division}
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
*)
......@@ -103,6 +102,7 @@ end
The particular case of Euclidean division by 2
*)
theory Div2
use import Int
......@@ -115,14 +115,13 @@ end
(** {2 Computer Division}
Division and modulo operators with the same conventions as mainstream
programming language such C, Java, OCaml, that is division rounds
programming language such as C, Java, OCaml, that is, division rounds
towards zero, and thus [mod x y] has the same sign as x
*)
theory ComputerDivision
use import Int
use import Abs
......@@ -171,9 +170,10 @@ theory ComputerDivision
end
(** {2 Generic Exponentation of something to an integer exponent} *)
(** {2 Generic Exponentiation of something to an integer exponent} *)
theory Exponentiation
use import Int
type t
......@@ -197,6 +197,7 @@ theory Exponentiation
end
(** {2 Power of an integer to an integer } *)
theory Power
use import Int
......@@ -213,6 +214,7 @@ 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
......@@ -288,11 +290,10 @@ end
(** {2 Specific version of number of elements satisfying a predicate}
This is an instance of the above, where the type parameter is unused
This is an instance of the above, where the type parameter is unused.
*)
theory NumOf
predicate pr int
......@@ -376,10 +377,10 @@ 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
induction, either on nonnegative integers, or more generally on
integers greater or equal a given bound.
*)
*)
theory Induction
......
......@@ -12,6 +12,7 @@ end
(** {2 Length of a list} *)
theory Length
use import int.Int
use import List
......@@ -42,6 +43,7 @@ end
(** {2 Nth element of a list} *)
theory Nth
use export List
use export option.Option
use import int.Int
......@@ -55,7 +57,7 @@ end
(** {2 Head and tail} *)
theory HdTl
theory HdTl
use export List
use export option.Option
......@@ -72,7 +74,7 @@ theory HdTl
end
(** {2 Relation between head, tail and nth} *)
(** {2 Relation between head, tail, and nth} *)
theory NthHdTl
......@@ -124,7 +126,7 @@ theory Append
end
(** {2 Rerversing a list} *)
(** {2 Reversing a list} *)
theory Reverse
......@@ -192,7 +194,7 @@ theory NumOcc
use import int.Int
use import List
(* number of occurence of x in l *)
(* number of occurrence of x in l *)
function num_occ (x: 'a) (l: list 'a) : int =
match l with
| Nil -> 0
......@@ -292,6 +294,7 @@ end
(** {2 Induction on lists} *)
theory Induction
use import List
type elt
......@@ -308,6 +311,7 @@ end
(** {2 Maps as lists of pairs} *)
theory Map
use import List
type a
......@@ -324,6 +328,7 @@ end
(** {2 Generic recursors on lists} *)
theory FoldLeft
use import List
type a
......@@ -335,9 +340,11 @@ theory FoldLeft
| Nil -> acc
| Cons x r -> fold_left (f acc x) r
end
end
theory FoldRight
use import List
type a
......@@ -349,11 +356,13 @@ theory FoldRight
| Nil -> acc
| Cons x r -> f x (fold_right r acc)
end
end
(** {2 Importation of all list theories in one} *)
theory ListRich
use export List
use export Length
use export Mem
......@@ -365,6 +374,7 @@ theory ListRich
use export Sorted
use export NumOcc
use export Permut
end
(***
......
......@@ -185,7 +185,6 @@ theory BitVector
end
theory BV32
constant size : int = 32
......@@ -194,7 +193,6 @@ theory BV32
end
theory TestBv32
use import BV32
......
(** {1 Theory of reals}
This file provides the basic theory of real numbers, and several additional theories for classical real functions
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
......@@ -25,9 +26,10 @@ theory Real
end
(** {2 Alternative Infix Operators}
(** {2 Alternative Infix Operators}
This theory should be used instead of Real when one wants to use both integer and real binary operators.
This theory should be used instead of Real when one wants to use both
integer and real binary operators.
*)
......@@ -220,6 +222,7 @@ theory ExpLog
end
(** {2 Power of a real to an integer} *)
theory PowerInt
use int.Int
......@@ -228,10 +231,10 @@ theory PowerInt
clone export int.Exponentiation with
type t = real, constant one = Real.one, function (*) = Real.(*)
end
(** {2 Power of a real to a real exponent} *)
theory PowerReal
use import Real
......@@ -263,11 +266,12 @@ theory PowerReal
end
(** {2 Trigonometric Functions}
See {h <a href="http://en.wikipedia.org/wiki/Trigonometric_function">wikipedia page</a>}
See the {h <a href="http://en.wikipedia.org/wiki/Trigonometric_function">wikipedia page</a>}.
*)
theory Trigonometry
use import Real
......@@ -323,8 +327,11 @@ theory Trigonometry
end
(** {2 Hyperbolic Functions}
See {h <a href="http://en.wikipedia.org/wiki/Hyperbolic_function">wikipedia page</a>}
See the {h <a href="http://en.wikipedia.org/wiki/Hyperbolic_function">wikipedia page</a>}.
*)
theory Hyperbolic
use import Real
......@@ -346,8 +353,11 @@ theory Hyperbolic
end
(** {2 Polar Coordinates}
atan2, hypot, see {h <a href="http://en.wikipedia.org/wiki/Atan2">wikipedia page</a>}
See the {h <a href="http://en.wikipedia.org/wiki/Atan2">wikipedia page</a>}.
*)
theory Polar
use import Real
......@@ -362,5 +372,6 @@ theory Polar
axiom Y_from_polar:
forall x y:real. y = hypot x y * sin (atan2 y x)
end
......@@ -109,9 +109,10 @@ theory SetComprehension
end
(** {2 finite sets} *)
(** {2 Finite sets} *)
theory Fset
use import int.Int
clone export Set
......@@ -149,7 +150,8 @@ theory Fset
end
(** {2 finite sets of integers} *)
(** {2 Finite sets of integers} *)
theory Fsetint
use export int.Int
......@@ -191,6 +193,7 @@ theory FsetExt
end
theory SetMap
use import map.Map
use import bool.Bool
......
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