🍬 Script_set.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.V8.
Require TezosOfOCaml.Proto_alpha.Gas_comparable_input_size.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Definition make {A : Set}
  (x_value :
    {OPS_t : Set @
      Script_typed_ir.Boxed_set (elt := A)
        (OPS_t := OPS_t)}) : Script_typed_ir.set A :=
  Script_typed_ir.Set_tag x_value.

Definition get {A : Set} (function_parameter : Script_typed_ir.set A)
  : {OPS_t : Set @
    Script_typed_ir.Boxed_set (elt := A)
      (OPS_t := OPS_t)} :=
  let 'Script_typed_ir.Set_tag x_value := function_parameter in
  x_value.

Definition empty {a : Set} (ty_value : Script_typed_ir.comparable_ty)
  : Script_typed_ir.set a :=
  let OPS :=
    let elt_size := Gas_comparable_input_size.size_of_comparable_value ty_value
      in
    let _Set :=
      _Set.Make
        (let t : Set := a in
        let compare := Script_comparable.compare_comparable ty_value in
        {|
          Compare.COMPARABLE.compare := compare
        |}) in
    let t : Set := _Set.(_Set.S.t) in
    let elt : Set := a in
    let empty := _Set.(_Set.S.empty) in
    let add := _Set.(_Set.S.add) in
    let mem := _Set.(_Set.S.mem) in
    let remove := _Set.(_Set.S.remove) in
    let fold {B : Set} : (a → B → B) → _Set.(_Set.S.t) → B → B :=
      _Set.(_Set.S.fold) in
    {|
      Script_typed_ir.Boxed_set_OPS.elt_size := elt_size;
      Script_typed_ir.Boxed_set_OPS.empty := empty;
      Script_typed_ir.Boxed_set_OPS.add := add;
      Script_typed_ir.Boxed_set_OPS.mem := mem;
      Script_typed_ir.Boxed_set_OPS.remove := remove;
      Script_typed_ir.Boxed_set_OPS.fold _ := fold
    |} in
  Script_typed_ir.Set_tag
    (existS (A := Set) _ _
      (let elt : Set := a in
      let OPS := OPS in
      let boxed := OPS.(Script_typed_ir.Boxed_set_OPS.empty) in
      let size_value := 0 in
      {|
        Script_typed_ir.Boxed_set.OPS := OPS;
        Script_typed_ir.Boxed_set.boxed := boxed;
        Script_typed_ir.Boxed_set.size_value := size_value
      |})).

Definition update {a : Set}
  (v_value : a) (b_value : bool) (function_parameter : Script_typed_ir.set a)
  : Script_typed_ir.set a :=
  let 'Script_typed_ir.Set_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Script_typed_ir.Set_tag
    (existS (A := Set) _ _
      (let elt : Set := a in
      let OPS := Box.(Script_typed_ir.Boxed_set.OPS) in
      let boxed :=
        if b_value then
          Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.add)
            v_value Box.(Script_typed_ir.Boxed_set.boxed)
        else
          Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.remove)
            v_value Box.(Script_typed_ir.Boxed_set.boxed) in
      let size_value :=
        let mem :=
          Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.mem)
            v_value Box.(Script_typed_ir.Boxed_set.boxed) in
        if mem then
          if b_value then
            Box.(Script_typed_ir.Boxed_set.size_value)
          else
            Box.(Script_typed_ir.Boxed_set.size_value) -i 1
        else
          if b_value then
            Box.(Script_typed_ir.Boxed_set.size_value) +i 1
          else
            Box.(Script_typed_ir.Boxed_set.size_value) in
      {|
        Script_typed_ir.Boxed_set.OPS := OPS;
        Script_typed_ir.Boxed_set.boxed := boxed;
        Script_typed_ir.Boxed_set.size_value := size_value
      |})).

Definition mem {elt : Set}
  (v_value : elt) (function_parameter : Script_typed_ir.set elt) : bool :=
  let 'Script_typed_ir.Set_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.mem)
    v_value Box.(Script_typed_ir.Boxed_set.boxed).

Definition fold {elt acc : Set}
  (f_value : elt → acc → acc) (function_parameter : Script_typed_ir.set elt)
  : acc → acc :=
  let 'Script_typed_ir.Set_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.fold)
    f_value Box.(Script_typed_ir.Boxed_set.boxed).

Definition size_value {elt : Set} (function_parameter : Script_typed_ir.set elt)
  : Script_int.num :=
  let 'Script_typed_ir.Set_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Script_int.abs (Script_int.of_int Box.(Script_typed_ir.Boxed_set.size_value)).