Commit 19720359 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Convert the standard library.

parent 1d789093
......@@ -150,12 +150,12 @@ module IntArraySorted
predicate sorted_sub (a : array int) (l u : int) =
M.sorted_sub a.elts l u
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
(** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)`
is sorted w.r.t order relation `le` *)
predicate sorted (a : array int) =
M.sorted_sub a.elts 0 a.length
(** [sorted a] is true whenever the array [a] is sorted w.r.t [le] *)
(** `sorted a` is true whenever the array `a` is sorted w.r.t `le` *)
end
......@@ -170,12 +170,12 @@ module Sorted
predicate sorted_sub (a: array elt) (l u: int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
(** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)`
is sorted w.r.t order relation `le` *)
predicate sorted (a: array elt) =
forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2]
(** [sorted a] is true whenever the array [a] is sorted w.r.t [le] *)
(** `sorted a` is true whenever the array `a` is sorted w.r.t `le` *)
end
......@@ -205,8 +205,8 @@ module ArrayExchange
predicate exchange (a1 a2: array 'a) (i j: int) =
a1.length = a2.length /\
M.exchange a1.elts a2.elts 0 a1.length i j
(** [exchange a1 a2 i j] means that arrays [a1] and [a2] only differ
by the swapping of elements at indices [i] and [j] *)
(** `exchange a1 a2 i j` means that arrays `a1` and `a2` only differ
by the swapping of elements at indices `i` and `j` *)
end
......@@ -224,22 +224,22 @@ module ArrayPermut
predicate permut (a1 a2: array 'a) (l u: int) =
a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
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. *)
(** `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. *)
predicate permut_sub (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts 0 l /\
permut a1 a2 l u /\
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. *)
(** `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. *)
predicate permut_all (a1 a2: array 'a) =
a1.length = a2.length /\ M.permut a1.elts a2.elts 0 a1.length
(** [permut_all a1 a2 l u] is true when array [a1] is a permutation
of array [a2]. *)
(** `permut_all a1 a2 l u` is true when array `a1` is a permutation
of array `a2`. *)
lemma exchange_permut_sub:
forall a1 a2: array 'a, i j l u: int.
......@@ -281,7 +281,7 @@ module ArraySum
use import Array
use import map.MapSum as M
(** [sum a l h] is the sum of [a[i]] for [l <= i < h] *)
(** `sum a l h` is the sum of `a[i]` for `l <= i < h` *)
function sum (a: array int) (l h: int) : int = M.sum a.elts l h
end
......@@ -292,7 +292,7 @@ module NumOf
use import Array
use int.NumOf as N
(** the number of [a[i]] such that [l <= i < u] and [pr i a[i]] *)
(** the number of `a[i]` such that `l <= i < u` and `pr i a[i]` *)
function numof (pr: int -> 'a -> bool) (a: array 'a) (l u: int) : int =
N.numof (fun i -> pr i a[i]) l u
......@@ -302,7 +302,7 @@ module NumOfEq
use import Array
use int.NumOf as N
(** the number of [a[i]] such that [l <= i < u] and [a[i] = v] *)
(** the number of `a[i]` such that `l <= i < u` and `a[i] = v` *)
function numof (a: array 'a) (v: 'a) (l u: int) : int =
N.numof (fun i -> a[i] = v) l u
......
......@@ -7,7 +7,7 @@ module Bag
type bag 'a
(** whatever ['a], the type [bag 'a] is always infinite *)
(** whatever `'a`, the type `bag 'a` is always infinite *)
meta "infinite_type" type bag
(** the most basic operation is the number of occurrences *)
......@@ -52,7 +52,7 @@ module Bag
forall x: 'a, a b: bag 'a.
nb_occ x (union a b) = nb_occ x a + nb_occ x b
(** [union] is 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
......
......@@ -111,7 +111,7 @@ module 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
......@@ -156,8 +156,8 @@ module BV_Gen
(** Warning: shift operators of an amount greater than or equal to
the size are specified here, in concordance with SMTLIB. This is
not necessarily the case in hardware, where the amount of the
shift might be taken modulo the size, eg. [lsr x 64] might be
equal to [x], whereas in this theory it is 0.
shift might be taken modulo the size, eg. `lsr x 64` might be
equal to `x`, whereas in this theory it is 0.
*)
val function lsr t int : t
......
......@@ -73,11 +73,11 @@ end
(** {2 Generic theory of floats}
The theory is parametrized by the real constant [max] which denotes
the maximal representable number, the real constant [min] which denotes
The theory is parametrized by the real constant `max` which denotes
the maximal representable number, the real constant `min` which denotes
the minimal number whose rounding is not null, and the integer constant
[max_representable_integer] which is the maximal integer [n] such that
every integer between [0] and [n] are representable.
`max_representable_integer` which is the maximal integer `n` such that
every integer between `0` and `n` are representable.
*)
......@@ -404,7 +404,7 @@ module 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
......
......@@ -16,8 +16,8 @@ module Path
| Path_cons:
forall x y z: vertex, l: list vertex.
edge x y -> path y l z -> path x (Cons x l) z
(** [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)`. *)
lemma path_right_extension:
forall x y z: vertex, l: list vertex.
......@@ -56,7 +56,7 @@ module IntPathWeight
| Cons x Nil -> weight x dst
| Cons x ((Cons y _) as r) -> weight x y + path_weight r dst
end
(** the total weight of a path [path _ l dst] *)
(** the total weight of a path `path _ l dst` *)
lemma path_weight_right_extension:
forall x y: vertex, l: list vertex.
......@@ -81,7 +81,7 @@ module SimplePath
predicate edge graph vertex vertex
(** [simple_path g src [x1;...;xn] dst] is a path
(** `simple_path g src [x1;...;xn] dst` is a path
src --> x1 --> x2 --> ... --> xn --> dst without repetition. *)
inductive simple_path graph vertex (list vertex) vertex =
| Path_empty :
......
......@@ -418,7 +418,7 @@ module NumOcc
| Nil -> 0
| Cons y r -> (if x = y then 1 else 0) + num_occ x r
end
(** number of occurrences of [x] in [l] *)
(** number of occurrences of `x` in `l` *)
lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0
......
......@@ -206,14 +206,14 @@ end
(** {2 Arrays with 63-bit indices}
Contrary to arrays from module [Array], the contents of the array
Contrary to arrays from module `Array`, the contents of the array
is here modeled as a sequence. It makes it easier to resuse existing
functions over sequences. (We may consider doing this for regular arrays
as well in the future.)
A coercion is declared so that an array [a] can be used
as a sequence. As a consequence, notation [a[i]] in the logic is
directly that of sequences. You have to import module [seq.Seq] to be
A coercion is declared so that an array `a` can be used
as a sequence. As a consequence, notation `a[i]` in the logic is
directly that of sequences. You have to import module `seq.Seq` to be
able to use it.
*)
......@@ -335,8 +335,8 @@ module Array63Exchange
predicate exchange (a1 a2: array 'a) (i j: int) =
SE.exchange a1.elts a2.elts i j
(** [exchange a1 a2 i j] means that arrays [a1] and [a2] only differ
by the swapping of elements at indices [i] and [j] *)
(** `exchange a1 a2 i j` means that arrays `a1` and `a2` only differ
by the swapping of elements at indices `i` and `j` *)
end
......@@ -369,9 +369,9 @@ module Array63Permut
predicate permut (a1 a2: array 'a) (l u: int) =
SP.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. *)
(** `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. *)
predicate array_eq (a1 a2: array 'a) (l u: int) =
seq_eq_sub a1.elts a2.elts l u
......@@ -380,14 +380,14 @@ module Array63Permut
seq_eq_sub a1.elts a2.elts 0 l /\
permut a1 a2 l u /\
seq_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. *)
(** `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. *)
predicate permut_all (a1 a2: array 'a) =
SP.permut a1.elts a2.elts 0 a1.length
(** [permut_all a1 a2 l u] is true when array [a1] is a permutation
of array [a2]. *)
(** `permut_all a1 a2 l u` is true when array `a1` is a permutation
of array `a2`. *)
(** we can always enlarge the interval *)
lemma permut_sub_weakening:
......@@ -408,14 +408,14 @@ end
(** {2 Arrays of 63-bit integers}
Here the model is simply a sequence of integers (of type [int]),
instead of being a sequence of values of type [int63].
Here the model is simply a sequence of integers (of type `int`),
instead of being a sequence of values of type `int63`.
As a consequence, we have to provide the additional information
that each of the element fits within the bounds of 63-bit integers.
Caveat: type [array63] below is not compatible with type
[Array63.array int63].
Caveat: type `array63` below is not compatible with type
`Array63.array int63`.
*)
module ArrayInt63
......
......@@ -51,8 +51,8 @@ module MapSorted
predicate sorted_sub (a : map int elt) (l u : int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
(** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)`
is sorted w.r.t order relation `le` *)
end
......@@ -92,7 +92,7 @@ module MapSum
use import int.Int
use export Map
(** [sum m l h] is the sum of [m[i]] for [l <= i < h] *)
(** `sum m l h` is the sum of `m[i]` for `l <= i < h` *)
type container = map int int
clone export sum.Sum with type container = container, function f = get
......@@ -108,7 +108,7 @@ module 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.
......@@ -196,24 +196,24 @@ module MapInjection
predicate injective (a: map int int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
(** [injective a n] is true when [a] is an injection
on the domain [(0..n-1)] *)
(** `injective a n` is true when `a` is an injection
on the domain `(0..n-1)` *)
predicate surjective (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
(** [surjective a n] is true when [a] is a surjection
from [(0..n-1)] to [(0..n-1)] *)
(** `surjective a n` is true when `a` is a surjection
from `(0..n-1)` to `(0..n-1)` *)
predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
(** [range a n] is true when [a] maps the domain
[(0..n-1)] into [(0..n-1)] *)
(** `range a n` is true when `a` maps the domain
`(0..n-1)` into `(0..n-1)` *)
lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range a n -> surjective a n
(** main lemma: an injection on [(0..n-1)] that
ranges into [(0..n-1)] is also a surjection *)
(** main lemma: an injection on `(0..n-1)` that
ranges into `(0..n-1)` is also a surjection *)
use import Occ
......@@ -233,7 +233,7 @@ module MapParam
type elt
type map
(** if ['b] is an infinite type, then [map 'a 'b] is infinite *)
(** if `'b` is an infinite type, then `map 'a 'b` is infinite *)
meta "material_type_arg" type map, 1
function get (map 'a 'b) 'a : 'b
......
......@@ -10,7 +10,7 @@ module Pqueue
(** the abstract type of elements *)
clone export relations.TotalOrder with type t = elt
(** [elt] is equipped with a total order [rel] *)
(** `elt` is equipped with a total order `rel` *)
use import list.List
use import list.Mem
......@@ -30,11 +30,11 @@ module Pqueue
(** push an element in a queue *)
exception Empty
(** exception raised by [pop] and [peek] to signal an empty queue *)
(** exception raised by `pop` and `peek` to signal an empty queue *)
predicate minimal_elt (x: elt) (s: list elt) =
mem x s /\ forall e: elt. mem e s -> rel x e
(** property of the element returned by [pop] and [peek] *)
(** property of the element returned by `pop` and `peek` *)
val pop (q: t) : elt writes {q}
ensures { permut (Cons result q.elts) (old q.elts) }
......@@ -77,7 +77,7 @@ module PqueueNoDup
(** the abstract type of elements *)
clone export relations.TotalOrder with type t = elt
(** [elt] is equipped with a total order [rel] *)
(** `elt` is equipped with a total order `rel` *)
use import set.Fset
......@@ -94,11 +94,11 @@ module PqueueNoDup
(** push an element in a queue *)
exception Empty
(** exception raised by [pop] and [peek] to signal an empty queue *)
(** exception raised by `pop` and `peek` to signal an empty queue *)
predicate minimal_elt (x: elt) (s: set elt) =
mem x s /\ forall e: elt. mem e s -> rel x e
(** property of the element returned by [pop] and [peek] *)
(** property of the element returned by `pop` and `peek` *)
val pop (q: t) : elt writes {q}
ensures { q.elts = remove result (old q.elts) }
......
......@@ -24,8 +24,8 @@ module Regexp
type word = list char
(** Inductive predicate [mem w r] means
``word [w] belongs to the language of [r]''. *)
(** Inductive predicate `mem w r` means
"word `w` belongs to the language of `r`". *)
inductive mem (w: word) (r: regexp) =
| mem_eps:
......
......@@ -13,7 +13,7 @@ module Seq
(** the polymorphic type of sequences *)
type seq 'a
(** [seq 'a] is an infinite type *)
(** `seq 'a` is an infinite type *)
meta "infinite_type" type seq
val function length (seq 'a) : int
......@@ -22,7 +22,7 @@ module Seq
forall s: seq 'a. 0 <= length s
val function get (seq 'a) int : 'a
(** [get s i] is the ([i]+1)-th element of sequence [s]
(** `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 =
......@@ -52,8 +52,8 @@ module Seq
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 *)
(** `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 }
......@@ -89,8 +89,8 @@ module Seq
= while false do variant { 0 } () done;
create (1 + length s) (fun i -> if i = length s then x else s[i])
(** [s[i..j]] is the sub-sequence of [s] from element [i] included
to element [j] excluded *)
(** `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 }
......@@ -122,7 +122,7 @@ module Seq
end
(** {2 Lemma library about algebraic interactions between
[empty]/[singleton]/[cons]/[snoc]/[++]/[[ .. ]]} *)
`empty`/`singleton`/`cons`/`snoc`/`++`/`[ .. ]`} *)
module FreeMonoid
......@@ -373,12 +373,12 @@ module 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.
......@@ -473,22 +473,22 @@ module 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.
......@@ -537,7 +537,7 @@ module FoldLeft
use import Seq
use import int.Int
(** [fold_left f a [b1; ...; bn]] is [f (... (f (f a b1) b2) ...) bn] *)
(** `fold_left f a [b1; ...; bn]` is `f (... (f (f a b1) b2) ...) bn` *)
let rec function fold_left (f: 'a -> 'b -> 'a) (acc: 'a) (s: seq 'b) : 'a
variant { length s }
= if length s = 0 then acc else fold_left f (f acc s[0]) s[1 ..]
......@@ -560,7 +560,7 @@ module FoldRight
use import Seq
use import int.Int
(** [fold_right f [a1; ...; an] b] is [f a1 (f a2 (... (f an b) ...))] *)
(** `fold_right f [a1; ...; an] b` is `f a1 (f a2 (... (f an b) ...))` *)
let rec function fold_right (f: 'b -> 'a -> 'a) (s: seq 'b) (acc: 'a) : 'a
variant { length s }
= if length s = 0 then acc
......
......@@ -10,7 +10,7 @@ module Set
type set 'a = map 'a bool
(** if ['a] is an infinite type, then [set 'a] is infinite *)
(** if `'a` is an infinite type, then `set 'a` is infinite *)
meta "material_type_arg" type set, 0
(** membership *)
......@@ -98,7 +98,7 @@ module SetMap
use export Set
(** { f x | x in U } *)
(** `{ f x | x in U }` *)
function map (f: 'a -> 'b) (u: set 'a) : set 'b =
fun (y: 'b) -> exists x: 'a. mem x u /\ y = f x
......@@ -118,7 +118,7 @@ module Fset
type set 'a
(** if ['a] is an infinite type, then [set 'a] is infinite *)
(** if `'a` is an infinite type, then `set 'a` is infinite *)
meta "material_type_arg" type set, 0
(** membership *)
......@@ -342,7 +342,7 @@ module FsetSum
use import Fset as S
function sum (set 'a) ('a -> int) : int
(** [sum s f] is the sum Sum_{S.mem x s} f x *)
(** `sum s f` is the sum `\sum_{S.mem x s} f x` *)
axiom Sum_def_empty :
forall f. sum (S.empty: set 'a) f = 0
......
......@@ -118,7 +118,7 @@ module Buffer
val create (size:int) : t
requires { size >= 0 } ensures { result.length = 0 }
(** [size] is only given as a hint for the initial size *)
(** `size` is only given as a hint for the initial size *)
val contents (b:t) : string
ensures { S.length result = length b }
......
......@@ -8,10 +8,10 @@ module Sum
type container
function f container int : int
(** [f c i] is the [i]-th element in the container [c] *)
(** `f c i` is the `i`-th element in the container `c` *)
function sum container int int : int
(** [sum c i j] is the sum Sum_{i <= k < j} f c k *)
(** `sum c i j` is the sum `\sum_{i <= k < j} f c k` *)
axiom Sum_def_empty :
forall c : container, i j : int. j <= i -> sum c i j = 0
......
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