Commit fb032dd1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean documentation of standard library.

parent 1f8f096e
......@@ -226,7 +226,7 @@ module ArrayPermut
M.permut a1.elts a2.elts l u
(** [permut a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)].
Values outside of the interval (l..u-1) are ignored. *)
Values outside of the interval [(l..u-1)] are ignored. *)
predicate permut_sub (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts 0 l /\
......@@ -234,7 +234,7 @@ module ArrayPermut
map_eq_sub a1.elts a2.elts u (length a1)
(** [permut_sub a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)]
and values outside of the interval (l..u-1) are equal. *)
and values outside of the interval [(l..u-1)] are equal. *)
predicate permut_all (a1 a2: array 'a) =
a1.length = a2.length /\ M.permut a1.elts a2.elts 0 a1.length
......@@ -247,14 +247,11 @@ module ArrayPermut
0 <= l -> u <= length a1 -> permut_sub a1 a2 l u
(** we can always enlarge the interval *)
lemma permut_sub_weakening:
forall a1 a2: array 'a, l1 u1 l2 u2: int.
permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
permut_sub a1 a2 l2 u2
(** {3 lemmas about [permut_all]} *)
lemma exchange_permut_all:
forall a1 a2: array 'a, i j: int.
exchange a1 a2 i j -> permut_all a1 a2
......
......@@ -52,7 +52,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] is commutative, associative with identity [empty_bag] *)
lemma Union_comm: forall a b: bag 'a. union a b = union b a
......
(** {1 Bit Vectors} *)
(** {2 Powers of two } *)
(** {2 Powers of two} *)
theory Pow2int
use import int.Int
......@@ -110,7 +111,7 @@ theory BV_Gen
type t
(** [nth b n] is the n-th bit of b. Bit 0 is
(** [nth b n] is the [n]-th bit of [b]. Bit 0 is
the least significant bit *)
val function nth t int : bool
......@@ -210,7 +211,7 @@ theory BV_Gen
nth (rotate_left v n) i = nth v (mod (i - n) size)
(* Conversions from/to integers *)
(** Conversions from/to integers *)
use import Pow2int
......@@ -256,7 +257,7 @@ theory BV_Gen
axiom to_uint_one : to_uint one = 1
axiom to_uint_ones : to_uint ones = max_int
(* comparison operators *)
(** comparison operators *)
let predicate ult (x y : t) =
Int.(<) (to_uint x) (to_uint y)
......@@ -355,6 +356,7 @@ theory BV_Gen
to_uint (lsl_bv v n) = mod (Int.( * ) (to_uint v) (pow2 (to_uint n))) two_power_size
(** rotations *)
val function rotate_right_bv (v n : t) : t
val function rotate_left_bv (v n : t) : t
......@@ -365,7 +367,6 @@ theory BV_Gen
axiom rotate_right_bv_is_rotate_right :
forall v n. rotate_right_bv v n = rotate_right v (to_uint n)
(** nth_bv *)
val function nth_bv t t: bool
axiom nth_bv_def:
......@@ -380,7 +381,7 @@ theory BV_Gen
forall x i. 0 <= i < two_power_size ->
nth_bv x (of_int i) = nth x i
(* equality axioms *)
(** equality axioms *)
predicate eq_sub_bv t t t t
......
......@@ -37,7 +37,7 @@ theory SpecialValues
| Neg_case: forall x:real. x < 0.0 -> same_sign_real Neg x
| Pos_case: forall x:real. x > 0.0 -> same_sign_real Pos x
(* useful ???
(*** useful ???
lemma sign_not_pos_neg : forall x:t.
sign(x) <> Pos -> sign(x) = Neg
......@@ -128,6 +128,7 @@ theory GenFloat
round m (from_int i) = from_int i
(** rounding up and down *)
axiom Round_down_le:
forall x:real. round Down x <= x
axiom Round_up_ge:
......@@ -138,6 +139,7 @@ theory GenFloat
forall x:real. round Up (-x) = - round Down x
(** rounding into a float instead of a real *)
function round_logic mode real : t
axiom Round_logic_def:
forall m:mode, x:real.
......@@ -280,6 +282,7 @@ theory GenFloatFull
clone export GenFloat
(** {3 special values} *)
function class t : class
predicate is_finite (x:t) = class x = Finite
......@@ -401,7 +404,7 @@ theory GenFloatFull
is_finite (round_logic m x) /\ value (round_logic m x) < 0.0 /\
sign (round_logic m x) = Neg
(** lemmas on gen_zero *)
(** lemmas on [gen_zero] *)
lemma is_gen_zero_comp1 : forall x y:t.
is_gen_zero x /\ value x = value y /\ is_finite y -> is_gen_zero y
......@@ -715,9 +718,9 @@ theory GenFloatSpecMultiRounding
end
(* TODO: find constants for type single *)
(*** TODO: find constants for type single *)
(*
(***
theory SingleMultiRounding
constant min_normalized_single : real =
......
......@@ -167,6 +167,7 @@ theory GenericFloat
(** {2 Part II - Private Axiomatisation} *)
(** {3 Constructors and Constants} *)
axiom zeroF_is_positive : is_positive zeroF
axiom zeroF_is_zero : is_zero zeroF
......
......@@ -173,7 +173,7 @@ end
Division and modulo operators with the same conventions as mainstream
programming language such as C, Java, OCaml, that is, division rounds
towards zero, and thus [mod x y] has the same sign as x
towards zero, and thus [mod x y] has the same sign as [x].
*)
......
......@@ -28,6 +28,7 @@ module Array32
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int32)
......@@ -127,6 +128,7 @@ module Array31
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int31)
......@@ -226,6 +228,7 @@ module Array63
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int63)
......@@ -347,7 +350,7 @@ module Array63Permut
MP.permut a1.elts a2.elts l u
(** [permut a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)].
Values outside of the interval (l..u-1) are ignored. *)
Values outside of the interval [(l..u-1)] are ignored. *)
predicate array_eq (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts l u
......@@ -358,7 +361,7 @@ module Array63Permut
map_eq_sub a1.elts a2.elts u (length a1)
(** [permut_sub a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)]
and values outside of the interval (l..u-1) are equal. *)
and values outside of the interval [(l..u-1)] are equal. *)
predicate permut_all (a1 a2: array 'a) =
a1.length = a2.length /\ MP.permut a1.elts a2.elts 0 a1.length
......@@ -366,7 +369,6 @@ module Array63Permut
of array [a2]. *)
(** we can always enlarge the interval *)
lemma permut_sub_weakening:
forall a1 a2: array 'a, l1 u1 l2 u2: int.
permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
......
......@@ -57,6 +57,7 @@ theory MapSorted
end
(** {2 Maps Equality (indexed by integers)} *)
theory MapEq
use import int.Int
......@@ -85,6 +86,7 @@ theory MapExchange
end
(** {2 Sum of elements of a map (indexed by integers)} *)
theory MapSum
use import int.Int
......@@ -106,7 +108,7 @@ theory Occ
use import Map
function occ (v: 'a) (m: map int 'a) (l u: int) : int
(** number of occurrences of v in m between l included and u excluded *)
(** number of occurrences of [v] in [m] between [l] included and [u] excluded *)
axiom occ_empty:
forall v: 'a, m: map int 'a, l u: int.
......@@ -186,6 +188,7 @@ end
(** {2 Injectivity and surjectivity for maps (indexed by integers)} *)
theory MapInjection
use import int.Int
......@@ -220,11 +223,10 @@ theory MapInjection
end
(***
(** {2 Parametric Maps} *)
(*
theory MapParam
type idx
......
......@@ -24,6 +24,7 @@ module Matrix
ensures { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: matrix 'a) (r c: int) : 'a
......
......@@ -11,23 +11,19 @@ theory Seq
use import int.Int
(** the polymorphic type of sequences *)
type seq 'a
(** [seq 'a] is an infinite type *)
meta "infinite_type" type seq
(** length *)
val function length (seq 'a) : int
axiom length_nonnegative:
forall s: seq 'a. 0 <= length s
(** n-th element *)
val function get (seq 'a) int : 'a
(** [get s i] is the ([i]+1)-th element of sequence [s]
(the first element has index 0) *)
(** [get s i] is the ([i]+1)-th element of sequence [s]
(the first element has index 0) *)
let function ([]) (s: seq 'a) (i: int) : 'a =
get s i
......@@ -44,25 +40,25 @@ theory Seq
ensures { length result = len }
ensures { forall i. 0 <= i < len -> result[i] = f i }
(** empty sequence *)
(* FIXME: could be defined, but let constant does
(*** FIXME: could be defined, but let constant does
not accept spec. *)
val constant empty : seq 'a
ensures { length result = 0 }
(* let constant empty : seq 'a
(*** let constant empty : seq 'a
ensures { length result = 0 }
= while false do variant { 0 } () done;
create 0 (fun _ requires { false } -> absurd)
*)
(** update *)
(** empty sequence *)
val constant empty : seq 'a
ensures { length result = 0 }
(** [set s i v] is a new sequence [u] such that
[u[i] = v] and [u[j] = s[j]] otherwise *)
let function set (s:seq 'a) (i:int) (v:'a) : seq 'a
requires { 0 <= i < length s }
ensures { length result = length s }
ensures { result[i] = v }
ensures { forall j. 0 <= j < length s /\ j <> i -> result[j] = s[j] }
(** [set s i v] is a new sequence [u] such that
[u[i] = v] and [u[j] = s[j]] otherwise *)
= while false do variant { 0 } () done;
create s.length (fun j -> if j = i then v else s[j])
......@@ -93,13 +89,12 @@ theory Seq
= while false do variant { 0 } () done;
create (1 + length s) (fun i -> if i = length s then x else s[i])
(** sub-sequence *)
(** [s[i..j]] is the sub-sequence of [s] from element [i] included
to element [j] excluded *)
let function ([_.._]) (s:seq 'a) (i:int) (j:int) : seq 'a
requires { 0 <= i <= j <= length s }
ensures { length result = j - i }
ensures { forall k. 0 <= k < j - i -> result[k] = s[i + k] }
(** [s[i..j]] is the sub-sequence of [s] from element [i] included
to element [j] excluded *)
= while false do variant { 0 } () done;
create (j-i) (fun k -> s[i+k])
......@@ -126,8 +121,9 @@ theory Seq
end
(** {2 lemma library about algebraic interactions between
empty/singleton/cons/snoc/++/[ .. ]} *)
(** {2 Lemma library about algebraic interactions between
[empty]/[singleton]/[cons]/[snoc]/[++]/[[ .. ]]} *)
theory FreeMonoid
use import int.Int
......@@ -377,14 +373,12 @@ theory Sorted
predicate sorted_sub (s: seq t) (l u: int) =
forall i1 i2. l <= i1 <= i2 < u -> le s[i1] s[i2]
(** sorted_sub s l u is true whenever the sub-sequence s[l .. u-1] is
sorted w.r.t. order relation le *)
(** [sorted_sub s l u] is true whenever the sub-sequence [s[l .. u-1]] is
sorted w.r.t. order relation [le] *)
predicate sorted (s: seq t) =
sorted_sub s 0 (length s)
(** sorted s is true whenever the sequence s is sorted w.r.t le *)
(** [sorted s] is true whenever the sequence [s] is sorted w.r.t [le] *)
lemma sorted_cons:
forall x: t, s: seq t.
......@@ -478,25 +472,22 @@ theory Permut
length s1 = length s2 /\
0 <= l <= length s1 /\ 0 <= u <= length s1 /\
forall v: 'a. occ v s1 l u = occ v s2 l u
(** permut s1 s2 l u is true when the segment s1[l..u-1] is a
permutation of the segment s2[l..u-1]. Values outside this range are
(** [permut s1 s2 l u] is true when the segment [s1[l..u-1]] is a
permutation of the segment [s2[l..u-1]]. Values outside this range are
ignored. *)
predicate permut_sub (s1 s2: seq 'a) (l u: int) =
seq_eq_sub s1 s2 0 l /\
permut s1 s2 l u /\
seq_eq_sub s1 s2 u (length s1)
(** permut_sub s1 s2 l u is true when the segment s1[l..u-1] is a
permutation of the segment s2[l..u-1] and values outside this range
(** [permut_sub s1 s2 l u] is true when the segment [s1[l..u-1]] is a
permutation of the segment [s2[l..u-1]] and values outside this range
are equal. *)
predicate permut_all (s1 s2: seq 'a) =
length s1 = length s2 /\ permut s1 s2 0 (length s1)
(** permut_all s1 s2 is true when sequence s1 is a permutation of
sequence s2 *)
(** [permut_all s1 s2] is true when sequence [s1] is a permutation of
sequence [s2] *)
lemma exchange_permut_sub:
forall s1 s2: seq 'a, i j l u: int.
......@@ -504,13 +495,12 @@ theory Permut
0 <= l -> u <= length s1 -> permut_sub s1 s2 l u
(** enlarge the interval *)
lemma Permut_sub_weakening:
forall s1 s2: seq 'a, l1 u1 l2 u2: int.
permut_sub s1 s2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length s1 ->
permut_sub s1 s2 l2 u2
(** {2 Lemmas about permut} *)
(** {3 Lemmas about permut} *)
lemma permut_refl: forall s: seq 'a, l u: int.
0 <= l <= length s -> 0 <= u <= length s ->
......@@ -528,7 +518,7 @@ theory Permut
permut s1 s2 l u -> l <= i < u ->
exists j: int. l <= j < u /\ s1[j] = s2[i]
(** {2 Lemmas about permut_all} *)
(** {3 Lemmas about permut_all} *)
use import Mem
......@@ -583,7 +573,7 @@ theory FoldRight
end
(* TODO / TO DISCUSS
(*** TODO / TO DISCUSS
- what about s[i..j] when i..j is not a valid range?
left undefined? empty sequence?
......
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