🎲 Sampler.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Module SMass.
Record signature {t : Set} : Set := {
t := t;
encoding : Data_encoding.t t;
zero : t;
of_int : int → t;
mul : t → t → t;
add : t → t → t;
sub : t → t → t;
op_eq : t → t → bool;
op_lteq : t → t → bool;
op_lt : t → t → bool;
}.
End SMass.
Definition SMass := @SMass.signature.
Arguments SMass {_}.
Module S.
Record signature {mass : Set} {t : Set → Set} : Set := {
mass := mass;
t := t;
create : ∀ {a : Set}, list (a × mass) → t a;
sample : ∀ {a : Set}, t a → (int → mass → int × mass) → M? a;
encoding : ∀ {a : Set}, Data_encoding.t a → Data_encoding.t (t a);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Module Make.
Class FArgs {Mass_t : Set} := {
Mass : SMass (t := Mass_t);
}.
Arguments Build_FArgs {_}.
Definition mass `{FArgs} : Set := Mass.(SMass.t).
Module t.
Record record `{FArgs} {a : Set} : Set := Build {
total : Mass.(SMass.t);
support : FallbackArray.t a;
p : FallbackArray.t Mass.(SMass.t);
alias : FallbackArray.t int;
}.
Arguments record {_ _}.
Definition with_total `{FArgs} {t_a} total (r : record t_a) :=
Build _ _ t_a total r.(support) r.(p) r.(alias).
Definition with_support `{FArgs} {t_a} support (r : record t_a) :=
Build _ _ t_a r.(total) support r.(p) r.(alias).
Definition with_p `{FArgs} {t_a} p (r : record t_a) :=
Build _ _ t_a r.(total) r.(support) p r.(alias).
Definition with_alias `{FArgs} {t_a} alias (r : record t_a) :=
Build _ _ t_a r.(total) r.(support) r.(p) alias.
End t.
Definition t `{FArgs} := t.record.
#[bypass_check(guard)]
Fixpoint init_loop `{FArgs}
(total : Mass.(SMass.t)) (p_value : FallbackArray.t Mass.(SMass.t))
(alias : FallbackArray.t int) (small : list (Mass.(SMass.t) × int))
(large : list (Mass.(SMass.t) × int)) {struct small} : unit :=
match (small, large) with
| ([], _) ⇒
List.iter
(fun (function_parameter : Mass.(SMass.t) × int) ⇒
let '(_, i_value) := function_parameter in
FallbackArray.set p_value i_value total) large
| (_, []) ⇒
List.iter
(fun (function_parameter : Mass.(SMass.t) × int) ⇒
let '(_, i_value) := function_parameter in
FallbackArray.set p_value i_value total) small
| (cons (qi, i_value) small', cons (qj, j_value) large') ⇒
let '_ := FallbackArray.set p_value i_value qi in
let '_ := FallbackArray.set alias i_value j_value in
let qj' := Mass.(SMass.sub) (Mass.(SMass.add) qi qj) total in
if Mass.(SMass.op_lt) qj' total then
init_loop total p_value alias (cons (qj', j_value) small') large'
else
init_loop total p_value alias small' (cons (qj', j_value) large')
end.
Definition support `{FArgs} {a : Set}
(fallback : a) (measure : list (a × Mass.(SMass.t))) : FallbackArray.t a :=
FallbackArray.of_list fallback Pervasives.fst measure.
Definition check_and_cleanup `{FArgs} {A : Set}
(measure : list (A × Mass.(SMass.t)))
: A × Mass.(SMass.t) × list (A × Mass.(SMass.t)) :=
let '(total, measure) :=
List.fold_left
(fun (function_parameter : Mass.(SMass.t) × list (A × Mass.(SMass.t)))
⇒
let '(total, m_value) as acc_value := function_parameter in
fun (function_parameter : A × Mass.(SMass.t)) ⇒
let '(_, p_value) as point := function_parameter in
if Mass.(SMass.op_lt) Mass.(SMass.zero) p_value then
((Mass.(SMass.add) total p_value), (cons point m_value))
else
if Mass.(SMass.op_lt) p_value Mass.(SMass.zero) then
Pervasives.invalid_arg "create"
else
acc_value) (Mass.(SMass.zero), nil) measure in
match measure with
| [] ⇒ Pervasives.invalid_arg "create"
| cons (fallback, _) _ ⇒ (fallback, total, measure)
end.
Definition create `{FArgs} {a : Set} (measure : list (a × Mass.(SMass.t)))
: t a :=
let '(fallback, total, measure) := check_and_cleanup measure in
let length := List.length measure in
let n_value := Mass.(SMass.of_int) length in
let '(_, small, large) :=
List.fold_left
(fun (function_parameter :
int × list (Mass.(SMass.t) × int) × list (Mass.(SMass.t) × int)) ⇒
let '(i_value, small, large) := function_parameter in
fun (function_parameter : a × Mass.(SMass.t)) ⇒
let '(_, p_value) := function_parameter in
let q_value := Mass.(SMass.mul) p_value n_value in
if Mass.(SMass.op_lt) q_value total then
((i_value +i 1), (cons (q_value, i_value) small), large)
else
((i_value +i 1), small, (cons (q_value, i_value) large)))
(0, nil, nil) measure in
let support := support fallback measure in
let p_value := FallbackArray.make length Mass.(SMass.zero) in
let alias := FallbackArray.make length (-1) in
let '_ := init_loop total p_value alias small large in
{| t.total := total; t.support := support; t.p := p_value; t.alias := alias;
|}.
Definition sample `{FArgs} {A : Set} (function_parameter : t A)
: (int → Mass.(SMass.t) → int × Mass.(SMass.t)) → M? A :=
let '{|
t.total := total;
t.support := support;
t.p := p_value;
t.alias := alias
|} := function_parameter in
fun (draw_i_elt : int → Mass.(SMass.t) → int × Mass.(SMass.t)) ⇒
let n_value := FallbackArray.length support in
let '(i_value, elt_value) := draw_i_elt n_value total in
let p_value := FallbackArray.get p_value i_value in
if Mass.(SMass.op_lt) elt_value p_value then
return? (FallbackArray.get support i_value)
else
let j_value := FallbackArray.get alias i_value in
if j_value ≥i 0 then
return? (FallbackArray.get support j_value)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition array_encoding `{FArgs} {a : Set} (venc : Data_encoding.t a)
: Data_encoding.t (FallbackArray.t a) :=
Data_encoding.conv
(fun (array_value : FallbackArray.t a) ⇒
let length := FallbackArray.length array_value in
let fallback := FallbackArray.fallback array_value in
let elements :=
List.rev
(FallbackArray.fold
(fun (acc_value : list a) ⇒
fun (elt_value : a) ⇒ cons elt_value acc_value) array_value nil)
in
(length, fallback, elements))
(fun (function_parameter : int × a × list a) ⇒
let '(length, fallback, elements) := function_parameter in
let array_value := FallbackArray.make length fallback in
let '_ :=
List.iteri
(fun (i_value : int) ⇒
fun (elt_value : a) ⇒
FallbackArray.set array_value i_value elt_value) elements in
array_value) None
(Data_encoding.obj3
(Data_encoding.req None None "length" Data_encoding.int31)
(Data_encoding.req None None "fallback" venc)
(Data_encoding.req None None "elements"
(Data_encoding.list_value None venc))).
Definition mass_array_encoding `{FArgs}
: Data_encoding.t (FallbackArray.t Mass.(SMass.t)) :=
array_encoding Mass.(SMass.encoding).
Definition int_array_encoding `{FArgs}
: Data_encoding.t (FallbackArray.t int) :=
array_encoding Data_encoding.int31.
Definition encoding `{FArgs} {A : Set} (enc : Data_encoding.t A)
: Data_encoding.encoding (t A) :=
Data_encoding.conv
(fun (function_parameter : t A) ⇒
let '{|
t.total := total;
t.support := support;
t.p := p_value;
t.alias := alias
|} := function_parameter in
(total, support, p_value, alias))
(fun (function_parameter :
Mass.(SMass.t) × FallbackArray.t A × FallbackArray.t Mass.(SMass.t) ×
FallbackArray.t int) ⇒
let '(total, support, p_value, alias) := function_parameter in
{| t.total := total; t.support := support; t.p := p_value;
t.alias := alias; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "total" Mass.(SMass.encoding))
(Data_encoding.req None None "support" (array_encoding enc))
(Data_encoding.req None None "p" mass_array_encoding)
(Data_encoding.req None None "alias" int_array_encoding)).
(* Make *)
Definition functor `{FArgs} :=
{|
S.create _ := create;
S.sample _ := sample;
S.encoding _ := encoding
|}.
End Make.
Definition Make {Mass_t : Set} (Mass : SMass (t := Mass_t))
: S (mass := Mass.(SMass.t)) (t := _) :=
let '_ := Make.Build_FArgs Mass in
Make.functor.
Module Mass.
Definition t : Set := int64.
Definition encoding : Data_encoding.encoding int64 :=
Data_encoding.int64_value.
Definition zero : int64 := 0.
Definition of_int : int → int64 := Int64.of_int.
Definition mul : int64 → int64 → int64 := Int64.mul.
Definition add : int64 → int64 → int64 := Int64.add.
Definition sub : int64 → int64 → int64 := Int64.sub.
Definition op_eq : int64 → int64 → bool := Compare.Int64.(Compare.S.op_eq).
Definition op_lteq : int64 → int64 → bool :=
Compare.Int64.(Compare.S.op_lteq).
Definition op_lt : int64 → int64 → bool := Compare.Int64.(Compare.S.op_lt).
(* Mass *)
Definition module :=
{|
SMass.encoding := encoding;
SMass.zero := zero;
SMass.of_int := of_int;
SMass.mul := mul;
SMass.add := add;
SMass.sub := sub;
SMass.op_eq := op_eq;
SMass.op_lteq := op_lteq;
SMass.op_lt := op_lt
|}.
End Mass.
Definition Mass : SMass (t := int64) := Mass.module.
Definition Make_include := Make Mass.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Module SMass.
Record signature {t : Set} : Set := {
t := t;
encoding : Data_encoding.t t;
zero : t;
of_int : int → t;
mul : t → t → t;
add : t → t → t;
sub : t → t → t;
op_eq : t → t → bool;
op_lteq : t → t → bool;
op_lt : t → t → bool;
}.
End SMass.
Definition SMass := @SMass.signature.
Arguments SMass {_}.
Module S.
Record signature {mass : Set} {t : Set → Set} : Set := {
mass := mass;
t := t;
create : ∀ {a : Set}, list (a × mass) → t a;
sample : ∀ {a : Set}, t a → (int → mass → int × mass) → M? a;
encoding : ∀ {a : Set}, Data_encoding.t a → Data_encoding.t (t a);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Module Make.
Class FArgs {Mass_t : Set} := {
Mass : SMass (t := Mass_t);
}.
Arguments Build_FArgs {_}.
Definition mass `{FArgs} : Set := Mass.(SMass.t).
Module t.
Record record `{FArgs} {a : Set} : Set := Build {
total : Mass.(SMass.t);
support : FallbackArray.t a;
p : FallbackArray.t Mass.(SMass.t);
alias : FallbackArray.t int;
}.
Arguments record {_ _}.
Definition with_total `{FArgs} {t_a} total (r : record t_a) :=
Build _ _ t_a total r.(support) r.(p) r.(alias).
Definition with_support `{FArgs} {t_a} support (r : record t_a) :=
Build _ _ t_a r.(total) support r.(p) r.(alias).
Definition with_p `{FArgs} {t_a} p (r : record t_a) :=
Build _ _ t_a r.(total) r.(support) p r.(alias).
Definition with_alias `{FArgs} {t_a} alias (r : record t_a) :=
Build _ _ t_a r.(total) r.(support) r.(p) alias.
End t.
Definition t `{FArgs} := t.record.
#[bypass_check(guard)]
Fixpoint init_loop `{FArgs}
(total : Mass.(SMass.t)) (p_value : FallbackArray.t Mass.(SMass.t))
(alias : FallbackArray.t int) (small : list (Mass.(SMass.t) × int))
(large : list (Mass.(SMass.t) × int)) {struct small} : unit :=
match (small, large) with
| ([], _) ⇒
List.iter
(fun (function_parameter : Mass.(SMass.t) × int) ⇒
let '(_, i_value) := function_parameter in
FallbackArray.set p_value i_value total) large
| (_, []) ⇒
List.iter
(fun (function_parameter : Mass.(SMass.t) × int) ⇒
let '(_, i_value) := function_parameter in
FallbackArray.set p_value i_value total) small
| (cons (qi, i_value) small', cons (qj, j_value) large') ⇒
let '_ := FallbackArray.set p_value i_value qi in
let '_ := FallbackArray.set alias i_value j_value in
let qj' := Mass.(SMass.sub) (Mass.(SMass.add) qi qj) total in
if Mass.(SMass.op_lt) qj' total then
init_loop total p_value alias (cons (qj', j_value) small') large'
else
init_loop total p_value alias small' (cons (qj', j_value) large')
end.
Definition support `{FArgs} {a : Set}
(fallback : a) (measure : list (a × Mass.(SMass.t))) : FallbackArray.t a :=
FallbackArray.of_list fallback Pervasives.fst measure.
Definition check_and_cleanup `{FArgs} {A : Set}
(measure : list (A × Mass.(SMass.t)))
: A × Mass.(SMass.t) × list (A × Mass.(SMass.t)) :=
let '(total, measure) :=
List.fold_left
(fun (function_parameter : Mass.(SMass.t) × list (A × Mass.(SMass.t)))
⇒
let '(total, m_value) as acc_value := function_parameter in
fun (function_parameter : A × Mass.(SMass.t)) ⇒
let '(_, p_value) as point := function_parameter in
if Mass.(SMass.op_lt) Mass.(SMass.zero) p_value then
((Mass.(SMass.add) total p_value), (cons point m_value))
else
if Mass.(SMass.op_lt) p_value Mass.(SMass.zero) then
Pervasives.invalid_arg "create"
else
acc_value) (Mass.(SMass.zero), nil) measure in
match measure with
| [] ⇒ Pervasives.invalid_arg "create"
| cons (fallback, _) _ ⇒ (fallback, total, measure)
end.
Definition create `{FArgs} {a : Set} (measure : list (a × Mass.(SMass.t)))
: t a :=
let '(fallback, total, measure) := check_and_cleanup measure in
let length := List.length measure in
let n_value := Mass.(SMass.of_int) length in
let '(_, small, large) :=
List.fold_left
(fun (function_parameter :
int × list (Mass.(SMass.t) × int) × list (Mass.(SMass.t) × int)) ⇒
let '(i_value, small, large) := function_parameter in
fun (function_parameter : a × Mass.(SMass.t)) ⇒
let '(_, p_value) := function_parameter in
let q_value := Mass.(SMass.mul) p_value n_value in
if Mass.(SMass.op_lt) q_value total then
((i_value +i 1), (cons (q_value, i_value) small), large)
else
((i_value +i 1), small, (cons (q_value, i_value) large)))
(0, nil, nil) measure in
let support := support fallback measure in
let p_value := FallbackArray.make length Mass.(SMass.zero) in
let alias := FallbackArray.make length (-1) in
let '_ := init_loop total p_value alias small large in
{| t.total := total; t.support := support; t.p := p_value; t.alias := alias;
|}.
Definition sample `{FArgs} {A : Set} (function_parameter : t A)
: (int → Mass.(SMass.t) → int × Mass.(SMass.t)) → M? A :=
let '{|
t.total := total;
t.support := support;
t.p := p_value;
t.alias := alias
|} := function_parameter in
fun (draw_i_elt : int → Mass.(SMass.t) → int × Mass.(SMass.t)) ⇒
let n_value := FallbackArray.length support in
let '(i_value, elt_value) := draw_i_elt n_value total in
let p_value := FallbackArray.get p_value i_value in
if Mass.(SMass.op_lt) elt_value p_value then
return? (FallbackArray.get support i_value)
else
let j_value := FallbackArray.get alias i_value in
if j_value ≥i 0 then
return? (FallbackArray.get support j_value)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition array_encoding `{FArgs} {a : Set} (venc : Data_encoding.t a)
: Data_encoding.t (FallbackArray.t a) :=
Data_encoding.conv
(fun (array_value : FallbackArray.t a) ⇒
let length := FallbackArray.length array_value in
let fallback := FallbackArray.fallback array_value in
let elements :=
List.rev
(FallbackArray.fold
(fun (acc_value : list a) ⇒
fun (elt_value : a) ⇒ cons elt_value acc_value) array_value nil)
in
(length, fallback, elements))
(fun (function_parameter : int × a × list a) ⇒
let '(length, fallback, elements) := function_parameter in
let array_value := FallbackArray.make length fallback in
let '_ :=
List.iteri
(fun (i_value : int) ⇒
fun (elt_value : a) ⇒
FallbackArray.set array_value i_value elt_value) elements in
array_value) None
(Data_encoding.obj3
(Data_encoding.req None None "length" Data_encoding.int31)
(Data_encoding.req None None "fallback" venc)
(Data_encoding.req None None "elements"
(Data_encoding.list_value None venc))).
Definition mass_array_encoding `{FArgs}
: Data_encoding.t (FallbackArray.t Mass.(SMass.t)) :=
array_encoding Mass.(SMass.encoding).
Definition int_array_encoding `{FArgs}
: Data_encoding.t (FallbackArray.t int) :=
array_encoding Data_encoding.int31.
Definition encoding `{FArgs} {A : Set} (enc : Data_encoding.t A)
: Data_encoding.encoding (t A) :=
Data_encoding.conv
(fun (function_parameter : t A) ⇒
let '{|
t.total := total;
t.support := support;
t.p := p_value;
t.alias := alias
|} := function_parameter in
(total, support, p_value, alias))
(fun (function_parameter :
Mass.(SMass.t) × FallbackArray.t A × FallbackArray.t Mass.(SMass.t) ×
FallbackArray.t int) ⇒
let '(total, support, p_value, alias) := function_parameter in
{| t.total := total; t.support := support; t.p := p_value;
t.alias := alias; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "total" Mass.(SMass.encoding))
(Data_encoding.req None None "support" (array_encoding enc))
(Data_encoding.req None None "p" mass_array_encoding)
(Data_encoding.req None None "alias" int_array_encoding)).
(* Make *)
Definition functor `{FArgs} :=
{|
S.create _ := create;
S.sample _ := sample;
S.encoding _ := encoding
|}.
End Make.
Definition Make {Mass_t : Set} (Mass : SMass (t := Mass_t))
: S (mass := Mass.(SMass.t)) (t := _) :=
let '_ := Make.Build_FArgs Mass in
Make.functor.
Module Mass.
Definition t : Set := int64.
Definition encoding : Data_encoding.encoding int64 :=
Data_encoding.int64_value.
Definition zero : int64 := 0.
Definition of_int : int → int64 := Int64.of_int.
Definition mul : int64 → int64 → int64 := Int64.mul.
Definition add : int64 → int64 → int64 := Int64.add.
Definition sub : int64 → int64 → int64 := Int64.sub.
Definition op_eq : int64 → int64 → bool := Compare.Int64.(Compare.S.op_eq).
Definition op_lteq : int64 → int64 → bool :=
Compare.Int64.(Compare.S.op_lteq).
Definition op_lt : int64 → int64 → bool := Compare.Int64.(Compare.S.op_lt).
(* Mass *)
Definition module :=
{|
SMass.encoding := encoding;
SMass.zero := zero;
SMass.of_int := of_int;
SMass.mul := mul;
SMass.add := add;
SMass.sub := sub;
SMass.op_eq := op_eq;
SMass.op_lteq := op_lteq;
SMass.op_lt := op_lt
|}.
End Mass.
Definition Mass : SMass (t := int64) := Mass.module.
Definition Make_include := Make Mass.
Inclusion of the module [Make_include]
Definition mass := Make_include.(S.mass).
Definition t := Make_include.(S.t).
Definition create {a : Set} := Make_include.(S.create) (a := a).
Definition sample {a : Set} := Make_include.(S.sample) (a := a).
Definition encoding {a : Set} := Make_include.(S.encoding) (a := a).
Definition t := Make_include.(S.t).
Definition create {a : Set} := Make_include.(S.create) (a := a).
Definition sample {a : Set} := Make_include.(S.sample) (a := a).
Definition encoding {a : Set} := Make_include.(S.encoding) (a := a).