🍃 Micheline.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.

Definition annot : Set := list string.

Inductive node (l p : Set) : Set :=
| Int : l → Z.t → node l p
| String : l → string → node l p
| Bytes : l → bytes → node l p
| Prim : l → p → list (node l p) → annot → node l p
| Seq : l → list (node l p) → node l p.

Arguments Int {_ _}.
Arguments String {_ _}.
Arguments Bytes {_ _}.
Arguments Prim {_ _}.
Arguments Seq {_ _}.

Parameter canonical_location : Set.

Parameter dummy_location : canonical_location.

Definition canonical (p : Set) : Set := node canonical_location p.

Definition root_value {p : Set} (n : canonical p) : node canonical_location p :=
  n.

Parameter canonical_location_encoding :
  Data_encoding.encoding canonical_location.

Parameter canonical_encoding : ∀ {l : Set},
  string → Data_encoding.encoding l → Data_encoding.encoding (canonical l).

Definition location {l p : Set} (n : node l p) : l :=
  match n with
  | Int l _ | String l _ | Bytes l _ | Prim l _ _ _ | Seq l _ ⇒ l
  end.

Definition annotations {l p : Set} (n : node l p) : list string :=
  match n with
  | Int _ _ | String _ _ | Bytes _ _ | Seq _ _ ⇒ []
  | Prim _ _ _ annot ⇒ annot
  end.

Reserved Notation "'map_strip_locations".

Fixpoint strip_locations {A p : Set} (n : node A p) {struct n} : canonical p :=
  match n with
  | Micheline.Int _ z ⇒ Micheline.Int dummy_location z
  | Micheline.String _ s ⇒ Micheline.String dummy_location s
  | Micheline.Bytes _ b ⇒ Micheline.Bytes dummy_location b
  | Micheline.Prim _ p ns annot ⇒
    Micheline.Prim dummy_location p ('map_strip_locations _ _ ns) annot
  | Micheline.Seq _ ns ⇒
    Micheline.Seq dummy_location ('map_strip_locations _ _ ns)
  end

where "'map_strip_locations" :=
  (fun A p ⇒ fix map_strip_locations (ns : list (node A p)) :=
    match ns with
    | [] ⇒ []
    | n :: ns ⇒ strip_locations n :: map_strip_locations ns
    end).

Definition map_strip_locations {A p} := 'map_strip_locations A p.