Skip to main content

💾 Storage_description.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.

Definition StringMap :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := String.compare
    |}.

Records for the constructor parameters
Module ConstructorRecords_description.
  Module description.
    Module Value.
      Record record {get encoding : Set} : Set := Build {
        get : get;
        encoding : encoding;
      }.
      Arguments record : clear implicits.
      Definition with_get {t_get t_encoding} get
        (r : record t_get t_encoding) :=
        Build t_get t_encoding get r.(encoding).
      Definition with_encoding {t_get t_encoding} encoding
        (r : record t_get t_encoding) :=
        Build t_get t_encoding r.(get) encoding.
    End Value.
    Definition Value_skeleton := Value.record.

    Module IndexedDir.
      Record record {arg arg_encoding list subdir : Set} : Set := Build {
        arg : arg;
        arg_encoding : arg_encoding;
        list : list;
        subdir : subdir;
      }.
      Arguments record : clear implicits.
      Definition with_arg {t_arg t_arg_encoding t_list t_subdir} arg
        (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir arg r.(arg_encoding) r.(list)
          r.(subdir).
      Definition with_arg_encoding {t_arg t_arg_encoding t_list t_subdir}
        arg_encoding (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir r.(arg) arg_encoding r.(list)
          r.(subdir).
      Definition with_list {t_arg t_arg_encoding t_list t_subdir} list
        (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir r.(arg) r.(arg_encoding) list
          r.(subdir).
      Definition with_subdir {t_arg t_arg_encoding t_list t_subdir} subdir
        (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir r.(arg) r.(arg_encoding)
          r.(list) subdir.
    End IndexedDir.
    Definition IndexedDir_skeleton := IndexedDir.record.
  End description.
End ConstructorRecords_description.
Import ConstructorRecords_description.

Module desc_with_path.
  Record record {rev_path dir : Set} : Set := Build {
    rev_path : rev_path;
    dir : dir;
  }.
  Arguments record : clear implicits.
  Definition with_rev_path {t_rev_path t_dir} rev_path
    (r : record t_rev_path t_dir) :=
    Build t_rev_path t_dir rev_path r.(dir).
  Definition with_dir {t_rev_path t_dir} dir (r : record t_rev_path t_dir) :=
    Build t_rev_path t_dir r.(rev_path) dir.
End desc_with_path.
Definition desc_with_path_skeleton := desc_with_path.record.

Reserved Notation "'description.Value".
Reserved Notation "'description.IndexedDir".
Reserved Notation "'t".
Reserved Notation "'desc_with_path".

Inductive description (key : Set) : Set :=
| Empty : description key
| Value : {a : Set}, 'description.Value a key description key
| NamedDir : StringMap.(Map.S.t) ('t key) description key
| IndexedDir : {a : Set},
  'description.IndexedDir a key description key

where "'desc_with_path" :=
  (fun (t_key : Set) ⇒ desc_with_path_skeleton (list string)
    (description t_key))
and "'t" := (fun (t_key : Set) ⇒ 'desc_with_path t_key)
and "'description.Value" :=
  (fun (t_a t_key : Set) ⇒ description.Value_skeleton
    (t_key M? (option t_a)) (Data_encoding.t t_a))
and "'description.IndexedDir" :=
  (fun (t_a t_key : Set) ⇒ description.IndexedDir_skeleton (RPC_arg.t t_a)
    (Data_encoding.t t_a) (t_key M? (list t_a)) ('t (t_key × t_a))).

Module description.
  Include ConstructorRecords_description.description.
  Definition Value := 'description.Value.
  Definition IndexedDir := 'description.IndexedDir.
End description.

Definition t := 't.
Definition desc_with_path := 'desc_with_path.

Arguments Empty {_}.
Arguments Value {_ _}.
Arguments NamedDir {_}.
Arguments IndexedDir {_ _}.

Reserved Notation "'pp_item".

#[bypass_check(guard)]
Fixpoint pp {a : Set} (ppf : Format.formatter) (function_parameter : t a)
  {struct function_parameter} : unit :=
  let pp_item {a} := 'pp_item a in
  let '{| desc_with_path.dir := dir |} := function_parameter in
  match dir with
  | Empty
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Empty"
          CamlinternalFormatBasics.End_of_format) "Empty")
  | Value _e
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Value"
          CamlinternalFormatBasics.End_of_format) "Value")
  | NamedDir map
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v>"
                CamlinternalFormatBasics.End_of_format) "<v>"))
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Formatting_lit
              CamlinternalFormatBasics.Close_box
              CamlinternalFormatBasics.End_of_format))) "@[<v>%a@]")
      (Format.pp_print_list None pp_item) (StringMap.(Map.S.bindings) map)
  |
    IndexedDir {|
      description.IndexedDir.arg := arg;
        description.IndexedDir.subdir := subdir
        |} ⇒
    let name :=
      Format.asprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Char_literal "<" % char
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              (CamlinternalFormatBasics.Char_literal ">" % char
                CamlinternalFormatBasics.End_of_format))) "<%s>")
        (RPC_arg.descr_value arg).(RPC_arg.descr.name) in
    pp_item ppf (name, subdir)
  end

where "'pp_item" :=
  (fun (a : Set) ⇒ fun
    (ppf : Format.formatter) (function_parameter : string × t a) ⇒
    let '(name, desc) := function_parameter in
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<hv 2>"
                CamlinternalFormatBasics.End_of_format) "<hv 2>"))
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Formatting_lit
                  CamlinternalFormatBasics.Close_box
                  CamlinternalFormatBasics.End_of_format))))) "@[<hv 2>%s@ %a@]")
      name pp desc).

Definition pp_item {a : Set} := 'pp_item a.

Definition pp_rev_path (ppf : Format.formatter) (path : list string) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Char_literal "[" % char
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Char_literal "]" % char
            CamlinternalFormatBasics.End_of_format))) "[%a]")
    (Format.pp_print_list
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf " / ")) Format.pp_print_string)
    (List.rev path).

Fixpoint register_named_subcontext {r : Set} (desc : t r) (names : list string)
  : t r :=
  match (desc.(desc_with_path.dir), names) with
  | (_, [])desc
  | ((Value _, _) | (IndexedDir _, _)) ⇒
    Format.kasprintf Pervasives.invalid_arg
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Could not register a named subcontext at "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal " because of an existing "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal "." % char
                  CamlinternalFormatBasics.End_of_format)))))
        "Could not register a named subcontext at %a because of an existing %a.")
      pp_rev_path desc.(desc_with_path.rev_path) pp desc
  | (Empty, cons name names)
    let subdir :=
      {| desc_with_path.rev_path := cons name desc.(desc_with_path.rev_path);
        desc_with_path.dir := Empty; |} in
    let '_ :=
      (* ❌ Set record field not handled. *)
      set_record_field desc "dir"
        (NamedDir (StringMap.(Map.S.singleton) name subdir)) in
    register_named_subcontext subdir names
  | (NamedDir map, cons name names)
    let subdir :=
      match StringMap.(Map.S.find) name map with
      | Some subdirsubdir
      | None
        let subdir :=
          {|
            desc_with_path.rev_path := cons name desc.(desc_with_path.rev_path);
            desc_with_path.dir := Empty; |} in
        let '_ :=
          (* ❌ Set record field not handled. *)
          set_record_field desc "dir"
            (NamedDir (StringMap.(Map.S.add) name subdir map)) in
        subdir
      end in
    register_named_subcontext subdir names
  end.

Records for the constructor parameters
Module ConstructorRecords_args.
  Module args.
    Module One.
      Record record {rpc_arg encoding compare : Set} : Set := Build {
        rpc_arg : rpc_arg;
        encoding : encoding;
        compare : compare;
      }.
      Arguments record : clear implicits.
      Definition with_rpc_arg {t_rpc_arg t_encoding t_compare} rpc_arg
        (r : record t_rpc_arg t_encoding t_compare) :=
        Build t_rpc_arg t_encoding t_compare rpc_arg r.(encoding) r.(compare).
      Definition with_encoding {t_rpc_arg t_encoding t_compare} encoding
        (r : record t_rpc_arg t_encoding t_compare) :=
        Build t_rpc_arg t_encoding t_compare r.(rpc_arg) encoding r.(compare).
      Definition with_compare {t_rpc_arg t_encoding t_compare} compare
        (r : record t_rpc_arg t_encoding t_compare) :=
        Build t_rpc_arg t_encoding t_compare r.(rpc_arg) r.(encoding) compare.
    End One.
    Definition One_skeleton := One.record.
  End args.
End ConstructorRecords_args.
Import ConstructorRecords_args.

Reserved Notation "'args.One".

Inductive args : Set :=
| One : {a : Set}, 'args.One a args
| Pair : args args args

where "'args.One" :=
  (fun (t_a : Set) ⇒ args.One_skeleton (RPC_arg.t t_a) (Data_encoding.t t_a)
    (t_a t_a int)).

Module args.
  Include ConstructorRecords_args.args.
  Definition One := 'args.One.
End args.

#[bypass_check(guard)]
Fixpoint unpack {c a b : Set} (function_parameter : args)
  {struct function_parameter} : c a × b :=
  match function_parameter with
  | One _cast (c a × b) (fun (x_value : c) ⇒ x_value)
  | Pair l_value r_value
    let 'existT _ [__Pair_'inter_key, __1, __0] [r_value, l_value] :=
      cast_exists (Es := [Set ** Set ** Set])
        (fun '[__Pair_'inter_key, __1, __0][args ** args])
        [r_value, l_value] in
    cast (c a × b)
    (let unpack_l := (unpack : args __Pair_'inter_key a × __0) l_value in
    let unpack_r := (unpack : args c __Pair_'inter_key × __1) r_value in
    fun (x_value : c) ⇒
      let '(c_value, d_value) := unpack_r x_value in
      let '(b_value, a_value) := unpack_l c_value in
      (b_value, (a_value, d_value)))
  end.

#[bypass_check(guard)]
Fixpoint _pack {a b c : Set} (function_parameter : args)
  {struct function_parameter} : a b c :=
  match function_parameter with
  | One _
    cast (a b c)
    (fun (b_value : a) ⇒ fun (a_value : b) ⇒ (b_value, a_value))
  | Pair l_value r_value
    let 'existT _ [__Pair_'inter_key, __1, __0] [r_value, l_value] :=
      cast_exists (Es := [Set ** Set ** Set])
        (fun '[__Pair_'inter_key, __1, __0][args ** args])
        [r_value, l_value] in
    cast (a b c)
    (let pack_l := (_pack : args a __0 __Pair_'inter_key) l_value in
    let pack_r := (_pack : args __Pair_'inter_key __1 c) r_value in
    fun (b_value : a) ⇒
      fun (function_parameter : __0 × __1) ⇒
        let '(a_value, d_value) := function_parameter in
        let c_value := pack_l b_value a_value in
        pack_r c_value d_value)
  end.

Axiom compare : {b : Set}, args b b int.

Definition destutter {A B : Set}
  (equal : A A bool) (l_value : list (A × B)) : list A :=
  match l_value with
  | []nil
  | cons (i_value, _) l_value
    let fix loop {C : Set}
      (acc_value : list A) (i_value : A) (function_parameter : list (A × C))
      : list A :=
      match function_parameter with
      | []acc_value
      | cons (j_value, _) l_value
        if equal i_value j_value then
          loop acc_value i_value l_value
        else
          loop (cons j_value acc_value) j_value l_value
      end in
    loop [ i_value ] i_value l_value
  end.

Axiom register_indexed_subcontext : {r a b : Set},
  t r (r M? (list a)) args t b.

Definition register_value {a b : Set}
  (desc : t a) (get : a M? (option b)) (encoding : Data_encoding.t b)
  : unit :=
  match desc.(desc_with_path.dir) with
  | Empty
    (* ❌ Set record field not handled. *)
    set_record_field desc "dir"
      (Value
        {| description.Value.get := get; description.Value.encoding := encoding;
          |})
  | _
    Format.kasprintf Pervasives.invalid_arg
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Could not register a value at "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal " because of an existing "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal "." % char
                  CamlinternalFormatBasics.End_of_format)))))
        "Could not register a value at %a because of an existing %a.")
      pp_rev_path desc.(desc_with_path.rev_path) pp desc
  end.

Definition create {A : Set} (function_parameter : unit) : desc_with_path A :=
  let '_ := function_parameter in
  {| desc_with_path.rev_path := nil; desc_with_path.dir := Empty; |}.

Module INDEX.
  Record signature {t : Set} : Set := {
    t := t;
    to_path : t list string list string;
    of_path : list string option t;
    path_length : int;
    rpc_arg : RPC_arg.t t;
    encoding : Data_encoding.t t;
    compare : t t int;
  }.
End INDEX.
Definition INDEX := @INDEX.signature.
Arguments INDEX {_}.

Records for the constructor parameters
Module ConstructorRecords_handler.
  Module handler.
    Module Handler.
      Record record {encoding get : Set} : Set := Build {
        encoding : encoding;
        get : get;
      }.
      Arguments record : clear implicits.
      Definition with_encoding {t_encoding t_get} encoding
        (r : record t_encoding t_get) :=
        Build t_encoding t_get encoding r.(get).
      Definition with_get {t_encoding t_get} get
        (r : record t_encoding t_get) :=
        Build t_encoding t_get r.(encoding) get.
    End Handler.
    Definition Handler_skeleton := Handler.record.
  End handler.
End ConstructorRecords_handler.
Import ConstructorRecords_handler.

Reserved Notation "'handler.Handler".

Inductive handler : Set :=
| Handler : {a key : Set}, 'handler.Handler a key handler

where "'handler.Handler" :=
  (fun (t_a t_key : Set) ⇒ handler.Handler_skeleton (Data_encoding.t t_a)
    (t_key int M? t_a)).

Module handler.
  Include ConstructorRecords_handler.handler.
  Definition Handler := 'handler.Handler.
End handler.

Records for the constructor parameters
Module ConstructorRecords_opt_handler.
  Module opt_handler.
    Module Opt_handler.
      Record record {encoding get : Set} : Set := Build {
        encoding : encoding;
        get : get;
      }.
      Arguments record : clear implicits.
      Definition with_encoding {t_encoding t_get} encoding
        (r : record t_encoding t_get) :=
        Build t_encoding t_get encoding r.(get).
      Definition with_get {t_encoding t_get} get
        (r : record t_encoding t_get) :=
        Build t_encoding t_get r.(encoding) get.
    End Opt_handler.
    Definition Opt_handler_skeleton := Opt_handler.record.
  End opt_handler.
End ConstructorRecords_opt_handler.
Import ConstructorRecords_opt_handler.

Reserved Notation "'opt_handler.Opt_handler".

Inductive opt_handler : Set :=
| Opt_handler : {a key : Set},
  'opt_handler.Opt_handler a key opt_handler

where "'opt_handler.Opt_handler" :=
  (fun (t_a t_key : Set) ⇒ opt_handler.Opt_handler_skeleton
    (Data_encoding.t t_a) (t_key int M? (option t_a))).

Module opt_handler.
  Include ConstructorRecords_opt_handler.opt_handler.
  Definition Opt_handler := 'opt_handler.Opt_handler.
End opt_handler.

Axiom combine_object : list (string × opt_handler) handler.

Module query.
  Record record : Set := Build {
    depth : int;
  }.
  Definition with_depth depth (r : record) :=
    Build depth.
End query.
Definition query := query.record.

Definition depth_query : RPC_query.t query :=
  RPC_query.seal
    (RPC_query.op_pipeplus
      (RPC_query.query_value (fun (depth : int) ⇒ {| query.depth := depth; |}))
      (RPC_query.field_value None "depth" RPC_arg.uint 0
        (fun (t_value : query) ⇒ t_value.(query.depth)))).

Axiom build_directory : {key : Set}, t key RPC_directory.t key.