💾 Storage_description.v

Simulations

See code, See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Storage_description.

A dependent version of the GADT [args].

Inductive dep_args (key : Set) : Set → Set → Set :=
| Dep_One : ∀ {a : Set},
  Storage_description.args.One a →
  dep_args key a (key × a)
| Dep_Pair : ∀ {a b inter_key sub_key: Set},
  dep_args key a inter_key →
  dep_args inter_key b sub_key →
  dep_args key (a × b) sub_key.

Arguments Dep_One {_ _}.
Arguments Dep_Pair {_ _ _ _ _}.

Injection from [dep_args] to [args].

Fixpoint to_args {a b c : Set} (v : dep_args a b c)
  : Storage_description.args :=
  match v with
  | Dep_One x ⇒ Storage_description.One x
  | Dep_Pair l r ⇒ Storage_description.Pair (to_args l) (to_args r)
  end.

A dependent version of [unpack].

Fixpoint dep_unpack {a b c : Set} (v : dep_args a b c) (x : c) {struct v}
  : a × b :=
  match v, x with
  | Dep_One _, _ ⇒ x
  | Dep_Pair l r, _ ⇒
    let '(c, d) := dep_unpack r x in
    let '(b, a) := dep_unpack l c in
    (b, (a, d))
  end.

A dependent version of [_pack].

Fixpoint dep_pack {a b c : Set} (v : dep_args a b c) (x : a) (y : b)
  {struct v} : c :=
  match v, x, y with
  | Dep_One _, _, _ ⇒ (x, y)
  | Dep_Pair l r, _, _ ⇒
    let '(a, d) := y in
    let c := dep_pack l x a in
    dep_pack r c d
  end.

Module INDEX.

Conversion to [Path_encoding.S].

  Definition to_Path_encoding_S {t : Set}
    (x : Storage_description.INDEX.signature (t := t)) :
    Path_encoding.S (t := t) := {|
    Path_encoding.S.to_path := x.(Storage_description.INDEX.to_path);
    Path_encoding.S.of_path := x.(Storage_description.INDEX.of_path);
    Path_encoding.S.path_length := x.(Storage_description.INDEX.path_length);
  |}.
End INDEX.