Maj terminée. Pour consulter la release notes associée voici le lien :

Commit a07707c1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new module array.NumOfParam

simplified example mjrty.mlw using that module
parent 92165a83
......@@ -12,12 +12,12 @@
Changes from the article above:
Changes w.r.t. the article above:
- arrays are 0-based
- we assume the input array to have at least one element
- we use 2x <= y instead of x <= floor(y/2), which is equivalent
- we do not consider arithmetic overflows (easy, but requires an
the extra hypothesis than length a <= max_int)
- we do not consider arithmetic overflows (easy, but requires the
extra hypothesis length a <= max_int)
module Mjrty
......@@ -30,16 +30,12 @@ module Mjrty
exception Found
type candidate
type votes = array candidate
type param = ( int candidate, candidate)
predicate pr (p: param) (i: int) = let (m, v) = p in M.([]) m i = v
clone import int.NumOfParam with type param = param, predicate pr = pr
predicate pr (c: candidate) (i: int) (ai: candidate) = ai = c
clone import array.NumOfParam
with type elt = candidate, type param = candidate, predicate pr = pr
function numof (a: votes) (c: candidate) (l u: int) : int =
num_of (a.elts, c) l u
let mjrty (a: votes) =
let mjrty (a: array candidate) =
{ 1 <= length a }
let n = length a in
let cand = ref a[0] in
This diff is collapsed.
......@@ -198,6 +198,28 @@ module ArraySum
(** {2 Number of array elements satisfying a given predicate}
This module 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].
module NumOfParam
use import Array
type elt
type param
predicate pr (p: param) (i: int) (e: elt)
type param_ = (array elt, param)
predicate pr_ (p: param_) (i: int) = let (a, p) = p in pr p i a[i]
clone import int.NumOfParam with type param = param_, predicate pr = pr_
function numof (a: array elt) (p: param) (l u: int) : int = num_of (a, p) l u
module TestArray
use import int.Int
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