Skip to main content

🍃 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 _ _ _ annotannot
  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 _ zMicheline.Int dummy_location z
  | Micheline.String _ sMicheline.String dummy_location s
  | Micheline.Bytes _ bMicheline.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 pfix map_strip_locations (ns : list (node A p)) :=
    match ns with
    | [][]
    | n :: nsstrip_locations n :: map_strip_locations ns
    end).

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