Skip to main content

🎲 Sampler.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.

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).