🍬 Script_tc_errors_registration.v

Translated OCaml

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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.

Definition stack_ty_enc
  : Data_encoding.encoding (list Alpha_context.Script.expr) :=
  Data_encoding.list_value None Alpha_context.Script.expr_encoding.

Definition type_map_enc
  : Data_encoding.encoding
    (list
      (Alpha_context.Script.location ×
        (list Alpha_context.Script.expr × list Alpha_context.Script.expr))) :=
  Data_encoding.list_value None
    (Data_encoding.conv
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (list Alpha_context.Script.expr × list Alpha_context.Script.expr)) ⇒
        let '(loc_value, (bef, aft)) := function_parameter in
        (loc_value, bef, aft))
      (fun (function_parameter :
        Alpha_context.Script.location × list Alpha_context.Script.expr ×
          list Alpha_context.Script.expr) ⇒
        let '(loc_value, bef, aft) := function_parameter in
        (loc_value, (bef, aft))) None
      (Data_encoding.obj3
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "stack_before" stack_ty_enc)
        (Data_encoding.req None None "stack_after" stack_ty_enc))).

Init function; without side-effects in Coq

Definition init_module : unit :=
  let located {A : Set} (enc : Data_encoding.encoding A)
    : Data_encoding.encoding (Alpha_context.Script.location × A) :=
    Data_encoding.merge_objs
      (Data_encoding.obj1
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)) enc in
  let arity_enc := Data_encoding.int8 in
  let namespace_enc :=
    Data_encoding.def "primitiveNamespace" (Some "Primitive namespace")
      (Some
        "One of the five possible namespaces of primitive (data constructor, type name, instruction, keyword, or constant hash).")
      (Data_encoding.string_enum
        [
          ("type", Michelson_v1_primitives.Type_namespace);
          ("constant", Michelson_v1_primitives.Constant_namespace);
          ("instruction", Michelson_v1_primitives.Instr_namespace);
          ("keyword", Michelson_v1_primitives.Keyword_namespace);
          ("constant_hash", Michelson_v1_primitives.Constant_hash_namespace)
        ]) in
  let kind_enc :=
    Data_encoding.def "expressionKind" (Some "Expression kind")
      (Some
        "One of the four possible kinds of expression (integer, string, primitive application or sequence).")
      (Data_encoding.string_enum
        [
          ("integer", Script_tc_errors.Int_kind);
          ("string", Script_tc_errors.String_kind);
          ("bytes", Script_tc_errors.Bytes_kind);
          ("primitiveApplication", Script_tc_errors.Prim_kind);
          ("sequence", Script_tc_errors.Seq_kind)
        ]) in
  let context_desc_enc :=
    Data_encoding.def "michelson_v1.context_desc" None None
      (Data_encoding.string_enum
        [ ("Lambda", Script_tc_errors.Lambda); ("View", Script_tc_errors.View) ])
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_arity" "Invalid arity"
      "In a script or data expression, a primitive was applied to an unsupported number of arguments."
      None
      (located
        (Data_encoding.obj3
          (Data_encoding.req None None "primitive_name"
            Alpha_context.Script.prim_encoding)
          (Data_encoding.req None None "expected_arity" arity_enc)
          (Data_encoding.req None None "wrong_arity" arity_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_arity" then
            let '(loc_value, name, exp, got) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.prim × int
                  × int) payload in
            Some (loc_value, (name, exp, got))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × (Alpha_context.Script.prim × int × int))
        ⇒
        let '(loc_value, (name, exp, got)) := function_parameter in
        Build_extensible "Invalid_arity"
          (Alpha_context.Script.location × Alpha_context.Script.prim × int × int)
          (loc_value, name, exp, got)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_seq_arity" "Invalid sequence arity"
      "In a script or data expression, a sequence was used with a number of elements too small."
      None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "minimal_expected_arity" arity_enc)
          (Data_encoding.req None None "wrong_arity" arity_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_seq_arity" then
            let '(loc_value, exp, got) :=
              cast (Alpha_context.Script.location × int × int) payload in
            Some (loc_value, (exp, got))
          else None
        end)
      (fun (function_parameter : Alpha_context.Script.location × (int × int)) ⇒
        let '(loc_value, (exp, got)) := function_parameter in
        Build_extensible "Invalid_seq_arity"
          (Alpha_context.Script.location × int × int) (loc_value, exp, got)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.missing_script_field"
      "Script is missing a field (parse error)"
      "When parsing script, a field was expected, but not provided" None
      (Data_encoding.obj1
        (Data_encoding.req None None "prim" Alpha_context.Script.prim_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Missing_field" then
            let prim := cast Alpha_context.Script.prim payload in
            Some prim
          else None
        end)
      (fun (prim : Alpha_context.Script.prim) ⇒
        Build_extensible "Missing_field" Alpha_context.Script.prim prim) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_primitive" "Invalid primitive"
      "In a script or data expression, a primitive was unknown." None
      (located
        (Data_encoding.obj2
          (Data_encoding.dft None None "expected_primitive_names"
            (Data_encoding.list_value None Alpha_context.Script.prim_encoding)
            nil)
          (Data_encoding.req None None "wrong_primitive_name"
            Alpha_context.Script.prim_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_primitive" then
            let '(loc_value, exp, got) :=
              cast
                (Alpha_context.Script.location × list Alpha_context.Script.prim
                  × Alpha_context.Script.prim) payload in
            Some (loc_value, (exp, got))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (list Alpha_context.Script.prim × Alpha_context.Script.prim)) ⇒
        let '(loc_value, (exp, got)) := function_parameter in
        Build_extensible "Invalid_primitive"
          (Alpha_context.Script.location × list Alpha_context.Script.prim ×
            Alpha_context.Script.prim) (loc_value, exp, got)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_expression_kind" "Invalid expression kind"
      "In a script or data expression, an expression was of the wrong kind (for instance a string where only a primitive applications can appear)."
      None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "expected_kinds"
            (Data_encoding.list_value None kind_enc))
          (Data_encoding.req None None "wrong_kind" kind_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_kind" then
            let '(loc_value, exp, got) :=
              cast
                (Alpha_context.Script.location × list Script_tc_errors.kind ×
                  Script_tc_errors.kind) payload in
            Some (loc_value, (exp, got))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (list Script_tc_errors.kind × Script_tc_errors.kind)) ⇒
        let '(loc_value, (exp, got)) := function_parameter in
        Build_extensible "Invalid_kind"
          (Alpha_context.Script.location × list Script_tc_errors.kind ×
            Script_tc_errors.kind) (loc_value, exp, got)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_primitive_namespace" "Invalid primitive namespace"
      "In a script or data expression, a primitive was of the wrong namespace."
      None
      (located
        (Data_encoding.obj3
          (Data_encoding.req None None "primitive_name"
            Alpha_context.Script.prim_encoding)
          (Data_encoding.req None None "expected_namespace" namespace_enc)
          (Data_encoding.req None None "wrong_namespace" namespace_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_namespace" then
            let '(loc_value, name, exp, got) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.prim ×
                  Michelson_v1_primitives.namespace ×
                  Michelson_v1_primitives.namespace) payload in
            Some (loc_value, (name, exp, got))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Alpha_context.Script.prim × Michelson_v1_primitives.namespace ×
            Michelson_v1_primitives.namespace)) ⇒
        let '(loc_value, (name, exp, got)) := function_parameter in
        Build_extensible "Invalid_namespace"
          (Alpha_context.Script.location × Alpha_context.Script.prim ×
            Michelson_v1_primitives.namespace ×
            Michelson_v1_primitives.namespace) (loc_value, name, exp, got)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_never_expr" "Invalid expression for type never"
      "In a script or data expression, an expression was provided but a value of type never was expected. No expression can have type never."
      None (located Data_encoding.unit_value)
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_never_expr" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some (loc_value, tt)
          else None
        end)
      (fun (function_parameter : Alpha_context.Script.location × unit) ⇒
        let '(loc_value, _) := function_parameter in
        Build_extensible "Invalid_never_expr" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.duplicate_script_field"
      "Script has a duplicated field (parse error)"
      "When parsing script, a field was found more than once" None
      (Data_encoding.obj2
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "prim" Alpha_context.Script.prim_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Duplicate_field" then
            let '(loc_value, prim) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.prim)
                payload in
            Some (loc_value, prim)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.prim) ⇒
        let '(loc_value, prim) := function_parameter in
        Build_extensible "Duplicate_field"
          (Alpha_context.Script.location × Alpha_context.Script.prim)
          (loc_value, prim)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unexpected_lazy_storage"
      "Lazy storage in unauthorized position (type error)"
      "When parsing script, a big_map or sapling_state type was found in a position where it could end up stored inside a big_map, which is forbidden for now."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpected_lazy_storage" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Unexpected_lazy_storage" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unexpected_operation"
      "Operation in unauthorized position (type error)"
      "When parsing script, an operation type was found in the storage or parameter field."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpected_operation" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Unexpected_operation" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.no_such_entrypoint" "No such entrypoint (type error)"
      "An entrypoint was not found when calling a contract." None
      (Data_encoding.obj1
        (Data_encoding.req None None "entrypoint"
          Alpha_context.Entrypoint.simple_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "No_such_entrypoint" then
            let entrypoint := cast Alpha_context.Entrypoint.t payload in
            Some entrypoint
          else None
        end)
      (fun (entrypoint : Alpha_context.Entrypoint.t) ⇒
        Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
          entrypoint) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unreachable_entrypoint"
      "Unreachable entrypoint (type error)"
      "An entrypoint in the contract is not reachable." None
      (Data_encoding.obj1
        (Data_encoding.req None None "path"
          (Data_encoding.list_value None Alpha_context.Script.prim_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unreachable_entrypoint" then
            let path := cast (list Alpha_context.Script.prim) payload in
            Some path
          else None
        end)
      (fun (path : list Alpha_context.Script.prim) ⇒
        Build_extensible "Unreachable_entrypoint"
          (list Alpha_context.Script.prim) path) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.tx_rollup_bad_deposit_parameter" "Bad deposit parameter"
      "The parameter to the deposit entrypoint of a transaction rollup should be a pair of a ticket and the address of a recipient transaction rollup."
      None
      (located
        (Data_encoding.obj1
          (Data_encoding.req None None "parameter"
            Alpha_context.Script.expr_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Tx_rollup_bad_deposit_parameter" then
            let '(loc_value, expr) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, expr)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, expr) := function_parameter in
        Build_extensible "Tx_rollup_bad_deposit_parameter"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, expr)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_tx_rollup_ticket_amount" "Invalid ticket amount"
      "Ticket amount to be deposited in a transaction rollup should be strictly positive and fit in a signed 64-bit integer"
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "requested_value" Data_encoding.z_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Tx_rollup_invalid_ticket_amount" then
            let z_value := cast Z.t payload in
            Some z_value
          else None
        end)
      (fun (z_value : Z.t) ⇒
        Build_extensible "Tx_rollup_invalid_ticket_amount" Z.t z_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.forbidden_zero_amount_ticket"
      "Zero ticket amount is not allowed"
      "It is not allowed to use a zero amount ticket in this operation." None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Forbidden_zero_ticket_quantity" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Forbidden_zero_ticket_quantity" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.tx_rollup_addresses_disabled"
      "Tx rollup addresses are disabled"
      "Cannot parse a tx_rollup address as tx rollups are disabled." None
      (Data_encoding.obj1
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Tx_rollup_addresses_disabled" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Tx_rollup_addresses_disabled"
          Alpha_context.Script.location loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.sc_rollup_disabled" "Sc rollup are disabled"
      "Cannot use smart-contract rollup features as they are disabled." None
      (Data_encoding.obj1
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Sc_rollup_disabled" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Sc_rollup_disabled" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.duplicate_entrypoint" "Duplicate entrypoint (type error)"
      "Two entrypoints have the same name." None
      (Data_encoding.obj1
        (Data_encoding.req None None "path"
          Alpha_context.Entrypoint.simple_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Duplicate_entrypoint" then
            let entrypoint := cast Alpha_context.Entrypoint.t payload in
            Some entrypoint
          else None
        end)
      (fun (entrypoint : Alpha_context.Entrypoint.t) ⇒
        Build_extensible "Duplicate_entrypoint" Alpha_context.Entrypoint.t
          entrypoint) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unexpected_contract"
      "Contract in unauthorized position (type error)"
      "When parsing script, a contract type was found in the storage or parameter field."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpected_contract" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Unexpected_contract" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unordered_map_literal" "Invalid map key order"
      "Map keys must be in strictly increasing order" None
      (Data_encoding.obj2
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "item" Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unordered_map_keys" then
            let '(loc_value, expr) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, expr)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, expr) := function_parameter in
        Build_extensible "Unordered_map_keys"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, expr)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.duplicate_map_keys" "Duplicate map keys"
      "Map literals cannot contain duplicated keys" None
      (Data_encoding.obj2
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "item" Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Duplicate_map_keys" then
            let '(loc_value, expr) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, expr)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, expr) := function_parameter in
        Build_extensible "Duplicate_map_keys"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, expr)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unordered_set_literal" "Invalid set value order"
      "Set values must be in strictly increasing order" None
      (Data_encoding.obj2
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "value" Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unordered_set_values" then
            let '(loc_value, expr) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, expr)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, expr) := function_parameter in
        Build_extensible "Unordered_set_values"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, expr)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.duplicate_set_values_in_literal"
      "Sets literals cannot contain duplicate elements"
      "Set literals cannot contain duplicate elements, but a duplicate was found while parsing."
      None
      (Data_encoding.obj2
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "value" Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Duplicate_set_values" then
            let '(loc_value, expr) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, expr)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, expr) := function_parameter in
        Build_extensible "Duplicate_set_values"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, expr)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.fail_not_in_tail_position" "FAIL not in tail position"
      "There is non trivial garbage code after a FAIL instruction." None
      (located Data_encoding.empty)
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Fail_not_in_tail_position" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some (loc_value, tt)
          else None
        end)
      (fun (function_parameter : Alpha_context.Script.location × unit) ⇒
        let '(loc_value, _) := function_parameter in
        Build_extensible "Fail_not_in_tail_position"
          Alpha_context.Script.location loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.undefined_binop" "Undefined binop"
      "A binary operation is called on operands of types over which it is not defined."
      None
      (located
        (Data_encoding.obj3
          (Data_encoding.req None None "operator_name"
            Alpha_context.Script.prim_encoding)
          (Data_encoding.req None None "wrong_left_operand_type"
            Alpha_context.Script.expr_encoding)
          (Data_encoding.req None None "wrong_right_operand_type"
            Alpha_context.Script.expr_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Undefined_binop" then
            let '(loc_value, n_value, tyl, tyr) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.prim ×
                  Alpha_context.Script.expr × Alpha_context.Script.expr) payload
                in
            Some (loc_value, (n_value, tyl, tyr))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Alpha_context.Script.prim × Alpha_context.Script.expr ×
            Alpha_context.Script.expr)) ⇒
        let '(loc_value, (n_value, tyl, tyr)) := function_parameter in
        Build_extensible "Undefined_binop"
          (Alpha_context.Script.location × Alpha_context.Script.prim ×
            Alpha_context.Script.expr × Alpha_context.Script.expr)
          (loc_value, n_value, tyl, tyr)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.undefined_unop" "Undefined unop"
      "A unary operation is called on an operand of type over which it is not defined."
      None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "operator_name"
            Alpha_context.Script.prim_encoding)
          (Data_encoding.req None None "wrong_operand_type"
            Alpha_context.Script.expr_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Undefined_unop" then
            let '(loc_value, n_value, ty_value) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.prim ×
                  Alpha_context.Script.expr) payload in
            Some (loc_value, (n_value, ty_value))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Alpha_context.Script.prim × Alpha_context.Script.expr)) ⇒
        let '(loc_value, (n_value, ty_value)) := function_parameter in
        Build_extensible "Undefined_unop"
          (Alpha_context.Script.location × Alpha_context.Script.prim ×
            Alpha_context.Script.expr) (loc_value, n_value, ty_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_return" "Bad return"
      "Unexpected stack at the end of a lambda or script." None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "expected_return_type"
            Alpha_context.Script.expr_encoding)
          (Data_encoding.req None None "wrong_stack_type" stack_ty_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Bad_return" then
            let '(loc_value, sty, ty_value) :=
              cast
                (Alpha_context.Script.location ×
                  Script_tc_errors.unparsed_stack_ty × Alpha_context.Script.expr)
                payload in
            Some (loc_value, (ty_value, sty))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Alpha_context.Script.expr × Script_tc_errors.unparsed_stack_ty)) ⇒
        let '(loc_value, (ty_value, sty)) := function_parameter in
        Build_extensible "Bad_return"
          (Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty ×
            Alpha_context.Script.expr) (loc_value, sty, ty_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_stack" "Bad stack"
      "The stack has an unexpected length or contents." None
      (located
        (Data_encoding.obj3
          (Data_encoding.req None None "primitive_name"
            Alpha_context.Script.prim_encoding)
          (Data_encoding.req None None "relevant_stack_portion"
            Data_encoding.int16)
          (Data_encoding.req None None "wrong_stack_type" stack_ty_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Bad_stack" then
            let '(loc_value, name, s_value, sty) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.prim × int
                  × Script_tc_errors.unparsed_stack_ty) payload in
            Some (loc_value, (name, s_value, sty))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Alpha_context.Script.prim × int × Script_tc_errors.unparsed_stack_ty))
        ⇒
        let '(loc_value, (name, s_value, sty)) := function_parameter in
        Build_extensible "Bad_stack"
          (Alpha_context.Script.location × Alpha_context.Script.prim × int ×
            Script_tc_errors.unparsed_stack_ty) (loc_value, name, s_value, sty))
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unexpected_annotation"
      "An annotation was encountered where no annotation is expected"
      "A node in the syntax tree was improperly annotated" None
      (located Data_encoding.empty)
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpected_annotation" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some (loc_value, tt)
          else None
        end)
      (fun (function_parameter : Alpha_context.Script.location × unit) ⇒
        let '(loc_value, _) := function_parameter in
        Build_extensible "Unexpected_annotation" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.ungrouped_annotations"
      "Annotations of the same kind were found spread apart"
      "Annotations of the same kind must be grouped" None
      (located Data_encoding.empty)
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Ungrouped_annotations" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some (loc_value, tt)
          else None
        end)
      (fun (function_parameter : Alpha_context.Script.location × unit) ⇒
        let '(loc_value, _) := function_parameter in
        Build_extensible "Ungrouped_annotations" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unmatched_branches" "Unmatched branches"
      "At the join point at the end of two code branches the stacks have inconsistent lengths or contents."
      None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "first_stack_type" stack_ty_enc)
          (Data_encoding.req None None "other_stack_type" stack_ty_enc)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unmatched_branches" then
            let '(loc_value, stya, styb) :=
              cast
                (Alpha_context.Script.location ×
                  Script_tc_errors.unparsed_stack_ty ×
                  Script_tc_errors.unparsed_stack_ty) payload in
            Some (loc_value, (stya, styb))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Script_tc_errors.unparsed_stack_ty ×
            Script_tc_errors.unparsed_stack_ty)) ⇒
        let '(loc_value, (stya, styb)) := function_parameter in
        Build_extensible "Unmatched_branches"
          (Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty ×
            Script_tc_errors.unparsed_stack_ty) (loc_value, stya, styb)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_stack_item" "Bad stack item"
      "The type of a stack item is unexpected (this error is always accompanied by a more precise one)."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "item_level" Data_encoding.int16))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Bad_stack_item" then
            let n_value := cast int payload in
            Some n_value
          else None
        end)
      (fun (n_value : int) ⇒ Build_extensible "Bad_stack_item" int n_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.forbidden_instr_in_context"
      "Forbidden instruction in context"
      "An instruction was encountered in a context where it is forbidden." None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "context" context_desc_enc)
          (Data_encoding.req None None "forbidden_instruction"
            Alpha_context.Script.prim_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Forbidden_instr_in_context" then
            let '(loc_value, ctxt, prim) :=
              cast
                (Alpha_context.Script.location × Script_tc_errors.context_desc ×
                  Alpha_context.Script.prim) payload in
            Some (loc_value, (ctxt, prim))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Script_tc_errors.context_desc × Alpha_context.Script.prim)) ⇒
        let '(loc_value, (ctxt, prim)) := function_parameter in
        Build_extensible "Forbidden_instr_in_context"
          (Alpha_context.Script.location × Script_tc_errors.context_desc ×
            Alpha_context.Script.prim) (loc_value, ctxt, prim)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.inconsistent_stack_lengths" "Inconsistent stack lengths"
      "A stack was of an unexpected length (this error is always in the context of a located error)."
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Bad_stack_length" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Bad_stack_length" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_constant" "Invalid constant"
      "A data expression was invalid for its expected type." None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "expected_type"
            Alpha_context.Script.expr_encoding)
          (Data_encoding.req None None "wrong_expression"
            Alpha_context.Script.expr_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_constant" then
            let '(loc_value, expr, ty_value) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.expr ×
                  Alpha_context.Script.expr) payload in
            Some (loc_value, (ty_value, expr))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location ×
          (Alpha_context.Script.expr × Alpha_context.Script.expr)) ⇒
        let '(loc_value, (ty_value, expr)) := function_parameter in
        Build_extensible "Invalid_constant"
          (Alpha_context.Script.location × Alpha_context.Script.expr ×
            Alpha_context.Script.expr) (loc_value, expr, ty_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.view_name_too_long" "View name too long (type error)"
      "A view name exceeds the maximum length of 31 characters." None
      (Data_encoding.obj1
        (Data_encoding.req None None "name" Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "View_name_too_long" then
            let name := cast string payload in
            Some name
          else None
        end)
      (fun (name : string) ⇒ Build_extensible "View_name_too_long" string name)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.duplicated_view_name" "Duplicated view name"
      "The name of view in toplevel should be unique." None
      (Data_encoding.obj1
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Duplicated_view_name" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Duplicated_view_name" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_syntactic_constant" "Invalid constant (parse error)"
      "A compile-time constant was invalid for its expected form." None
      (located
        (Data_encoding.obj2
          (Data_encoding.req None None "expected_form"
            Data_encoding.string_value)
          (Data_encoding.req None None "wrong_expression"
            Alpha_context.Script.expr_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_syntactic_constant" then
            let '(loc_value, expr, expected) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.expr ×
                  string) payload in
            Some (loc_value, (expected, expr))
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × (string × Alpha_context.Script.expr)) ⇒
        let '(loc_value, (expected, expr)) := function_parameter in
        Build_extensible "Invalid_syntactic_constant"
          (Alpha_context.Script.location × Alpha_context.Script.expr × string)
          (loc_value, expr, expected)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_contract" "Invalid contract"
      "A script or data expression references a contract that does not exist or assumes a wrong type for an existing contract."
      None
      (located
        (Data_encoding.obj1
          (Data_encoding.req None None "contract"
            Alpha_context.Contract.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_contract" then
            let '(loc_value, c_value) :=
              cast (Alpha_context.Script.location × Alpha_context.Contract.t)
                payload in
            Some (loc_value, c_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Contract.t) ⇒
        let '(loc_value, c_value) := function_parameter in
        Build_extensible "Invalid_contract"
          (Alpha_context.Script.location × Alpha_context.Contract.t)
          (loc_value, c_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_big_map" "Invalid big_map"
      "A script or data expression references a big_map that does not exist or assumes a wrong type for an existing big_map."
      None
      (located
        (Data_encoding.obj1
          (Data_encoding.req None None "big_map"
            Alpha_context.Big_map.Id.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_big_map" then
            let '(loc_value, c_value) :=
              cast (Alpha_context.Script.location × Alpha_context.Big_map.Id.t)
                payload in
            Some (loc_value, c_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Big_map.Id.t) ⇒
        let '(loc_value, c_value) := function_parameter in
        Build_extensible "Invalid_big_map"
          (Alpha_context.Script.location × Alpha_context.Big_map.Id.t)
          (loc_value, c_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.comparable_type_expected" "Comparable type expected"
      "A non comparable type was used in a place where only comparable types are accepted."
      None
      (located
        (Data_encoding.obj1
          (Data_encoding.req None None "wrong_type"
            Alpha_context.Script.expr_encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Comparable_type_expected" then
            let '(loc_value, ty_value) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, ty_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, ty_value) := function_parameter in
        Build_extensible "Comparable_type_expected"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, ty_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.inconsistent_type_sizes" "Inconsistent type sizes"
      "Two types were expected to be equal but they have different sizes." None
      (Data_encoding.obj2
        (Data_encoding.req None None "first_type_size" Data_encoding.int31)
        (Data_encoding.req None None "other_type_size" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Inconsistent_type_sizes" then
            let '(tya, tyb) := cast (int × int) payload in
            Some (tya, tyb)
          else None
        end)
      (fun (function_parameter : int × int) ⇒
        let '(tya, tyb) := function_parameter in
        Build_extensible "Inconsistent_type_sizes" (int × int) (tya, tyb)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.inconsistent_types" "Inconsistent types"
      "This is the basic type clash error, that appears in several places where the equality of two types have to be proven, it is always accompanied with another error that provides more context."
      None
      (Data_encoding.obj3
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "first_type"
          Alpha_context.Script.expr_encoding)
        (Data_encoding.req None None "other_type"
          Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Inconsistent_types" then
            let '(loc_value, tya, tyb) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.expr ×
                  Alpha_context.Script.expr) payload in
            Some (loc_value, tya, tyb)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr ×
          Alpha_context.Script.expr) ⇒
        let '(loc_value, tya, tyb) := function_parameter in
        Build_extensible "Inconsistent_types"
          (Alpha_context.Script.location × Alpha_context.Script.expr ×
            Alpha_context.Script.expr) (loc_value, tya, tyb)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.inconsistent_memo_sizes" "Inconsistent memo sizes"
      "Memo sizes of two sapling states or transactions do not match" None
      (Data_encoding.obj2
        (Data_encoding.req None None "first_memo_size"
          Alpha_context.Sapling.Memo_size.encoding)
        (Data_encoding.req None None "other_memo_size"
          Alpha_context.Sapling.Memo_size.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Inconsistent_memo_sizes" then
            let '(msa, msb) :=
              cast
                (Alpha_context.Sapling.Memo_size.t ×
                  Alpha_context.Sapling.Memo_size.t) payload in
            Some (msa, msb)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Sapling.Memo_size.t × Alpha_context.Sapling.Memo_size.t)
        ⇒
        let '(msa, msb) := function_parameter in
        Build_extensible "Inconsistent_memo_sizes"
          (Alpha_context.Sapling.Memo_size.t × Alpha_context.Sapling.Memo_size.t)
          (msa, msb)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_view_name" "Bad view name"
      "In a view declaration, the view name must be a string" None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Bad_view_name" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Bad_view_name" Alpha_context.Script.location loc_value)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.ill_typed_view" "Ill typed view"
      "The return of a view block did not match the expected type" None
      (Data_encoding.obj3
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "resulted_view_stack" stack_ty_enc)
        (Data_encoding.req None None "expected_view_stack" stack_ty_enc))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Ill_typed_view" then
            let '{|
              Script_tc_errors.Ill_typed_view.loc := loc_value;
                Script_tc_errors.Ill_typed_view.actual := actual;
                Script_tc_errors.Ill_typed_view.expected := expected
                |} := cast Script_tc_errors.Ill_typed_view payload in
            Some (loc_value, actual, expected)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty ×
          Script_tc_errors.unparsed_stack_ty) ⇒
        let '(loc_value, actual, expected) := function_parameter in
        Build_extensible "Ill_typed_view" Script_tc_errors.Ill_typed_view
          {| Script_tc_errors.Ill_typed_view.loc := loc_value;
            Script_tc_errors.Ill_typed_view.actual := actual;
            Script_tc_errors.Ill_typed_view.expected := expected; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_map_body" "Invalid map body"
      "The body of a map block did not match the expected type" None
      (Data_encoding.obj2
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "body_type" stack_ty_enc))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_map_body" then
            let '(loc_value, stack_value) :=
              cast
                (Alpha_context.Script.location ×
                  Script_tc_errors.unparsed_stack_ty) payload in
            Some (loc_value, stack_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty) ⇒
        let '(loc_value, stack_value) := function_parameter in
        Build_extensible "Invalid_map_body"
          (Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty)
          (loc_value, stack_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_map_block_fail"
      "FAIL instruction occurred as body of map block"
      "FAIL cannot be the only instruction in the body. The proper type of the return list cannot be inferred."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_map_block_fail" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Invalid_map_block_fail" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_iter_body" "ITER body returned wrong stack type"
      "The body of an ITER instruction must result in the same stack type as before the ITER."
      None
      (Data_encoding.obj3
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "bef_stack" stack_ty_enc)
        (Data_encoding.req None None "aft_stack" stack_ty_enc))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_iter_body" then
            let '(loc_value, bef, aft) :=
              cast
                (Alpha_context.Script.location ×
                  Script_tc_errors.unparsed_stack_ty ×
                  Script_tc_errors.unparsed_stack_ty) payload in
            Some (loc_value, bef, aft)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty ×
          Script_tc_errors.unparsed_stack_ty) ⇒
        let '(loc_value, bef, aft) := function_parameter in
        Build_extensible "Invalid_iter_body"
          (Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty ×
            Script_tc_errors.unparsed_stack_ty) (loc_value, bef, aft)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.type_too_large" "Stack item type too large"
      "An instruction generated a type larger than the limit." None
      (Data_encoding.obj2
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "maximum_type_size" Data_encoding.uint16))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Type_too_large" then
            let '(loc_value, maxts) :=
              cast (Alpha_context.Script.location × int) payload in
            Some (loc_value, maxts)
          else None
        end)
      (fun (function_parameter : Alpha_context.Script.location × int) ⇒
        let '(loc_value, maxts) := function_parameter in
        Build_extensible "Type_too_large" (Alpha_context.Script.location × int)
          (loc_value, maxts)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_pair_argument" "0 or 1 passed to PAIR"
      "PAIR expects an argument of at least 2" None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Pair_bad_argument" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Pair_bad_argument" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_unpair_argument" "0 or 1 passed to UNPAIR"
      "UNPAIR expects an argument of at least 2" None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unpair_bad_argument" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Unpair_bad_argument" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_dupn_argument" "0 passed to DUP n"
      "DUP expects an argument of at least 1 (passed 0)" None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Dup_n_bad_argument" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Dup_n_bad_argument" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_dupn_stack" "Stack too short when typing DUP n"
      "Stack present when typing DUP n was too short" None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Dup_n_bad_stack" then
            let x_value := cast Alpha_context.Script.location payload in
            Some x_value
          else None
        end)
      (fun (x_value : Alpha_context.Script.location) ⇒
        Build_extensible "Dup_n_bad_stack" Alpha_context.Script.location x_value)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.ill_typed_data" "Ill typed data"
      "The toplevel error thrown when trying to typecheck a data expression against a given type (always followed by more precise errors)."
      None
      (Data_encoding.obj3
        (Data_encoding.opt None None "identifier" Data_encoding.string_value)
        (Data_encoding.req None None "expected_type"
          Alpha_context.Script.expr_encoding)
        (Data_encoding.req None None "ill_typed_expression"
          Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Ill_typed_data" then
            let '(name, expr, ty_value) :=
              cast
                (option string × Alpha_context.Script.expr ×
                  Alpha_context.Script.expr) payload in
            Some (name, ty_value, expr)
          else None
        end)
      (fun (function_parameter :
        option string × Alpha_context.Script.expr × Alpha_context.Script.expr)
        ⇒
        let '(name, ty_value, expr) := function_parameter in
        Build_extensible "Ill_typed_data"
          (option string × Alpha_context.Script.expr × Alpha_context.Script.expr)
          (name, expr, ty_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.ill_formed_type" "Ill formed type"
      "The toplevel error thrown when trying to parse a type expression (always followed by more precise errors)."
      None
      (Data_encoding.obj3
        (Data_encoding.opt None None "identifier" Data_encoding.string_value)
        (Data_encoding.req None None "ill_formed_expression"
          Alpha_context.Script.expr_encoding)
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Ill_formed_type" then
            let '(name, expr, loc_value) :=
              cast
                (option string × Alpha_context.Script.expr ×
                  Alpha_context.Script.location) payload in
            Some (name, expr, loc_value)
          else None
        end)
      (fun (function_parameter :
        option string × Alpha_context.Script.expr ×
          Alpha_context.Script.location) ⇒
        let '(name, expr, loc_value) := function_parameter in
        Build_extensible "Ill_formed_type"
          (option string × Alpha_context.Script.expr ×
            Alpha_context.Script.location) (name, expr, loc_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.ill_typed_contract" "Ill typed contract"
      "The toplevel error thrown when trying to typecheck a contract code against given input, output and storage types (always followed by more precise errors)."
      None
      (Data_encoding.obj2
        (Data_encoding.req None None "ill_typed_code"
          Alpha_context.Script.expr_encoding)
        (Data_encoding.req None None "type_map" type_map_enc))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Ill_typed_contract" then
            let '(expr, type_map) :=
              cast (Alpha_context.Script.expr × Script_tc_errors.type_map)
                payload in
            Some (expr, type_map)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.expr × Script_tc_errors.type_map) ⇒
        let '(expr, type_map) := function_parameter in
        Build_extensible "Ill_typed_contract"
          (Alpha_context.Script.expr × Script_tc_errors.type_map)
          (expr, type_map)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.deprecated_instruction"
      "Script is using a deprecated instruction"
      "A deprecated instruction usage is disallowed in newly created contracts"
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "prim" Alpha_context.Script.prim_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Deprecated_instruction" then
            let prim := cast Alpha_context.Script.prim payload in
            Some prim
          else None
        end)
      (fun (prim : Alpha_context.Script.prim) ⇒
        Build_extensible "Deprecated_instruction" Alpha_context.Script.prim prim)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "michelson_v1.typechecking_too_many_recursive_calls"
      "Too many recursive calls during typechecking"
      "Too many recursive calls were needed for typechecking" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Typechecking_too_many_recursive_calls" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Typechecking_too_many_recursive_calls" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "michelson_v1.unparsing_stack_overflow"
      "Too many recursive calls during unparsing"
      "Too many recursive calls were needed for unparsing" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unparsing_too_many_recursive_calls" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unparsing_too_many_recursive_calls" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unexpected_forged_value" "Unexpected forged value"
      "A forged value was encountered but disallowed for that position." None
      (Data_encoding.obj1
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpected_forged_value" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Unexpected_forged_value" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unexpected_ticket"
      "Ticket in unauthorized position (type error)"
      "A ticket type has been found" None
      (Data_encoding.obj1
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpected_ticket" then
            let loc_value := cast Alpha_context.Script.location payload in
            Some loc_value
          else None
        end)
      (fun (loc_value : Alpha_context.Script.location) ⇒
        Build_extensible "Unexpected_ticket" Alpha_context.Script.location
          loc_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.non_dupable_type" "Non-dupable type duplication attempt"
      "DUP was used on a non-dupable type (e.g. tickets)." None
      (Data_encoding.obj2
        (Data_encoding.req None None "loc"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "type" Alpha_context.Script.expr_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Non_dupable_type" then
            let '(loc_value, ty_value) :=
              cast (Alpha_context.Script.location × Alpha_context.Script.expr)
                payload in
            Some (loc_value, ty_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr) ⇒
        let '(loc_value, ty_value) := function_parameter in
        Build_extensible "Non_dupable_type"
          (Alpha_context.Script.location × Alpha_context.Script.expr)
          (loc_value, ty_value)) in
  Error_monad.register_error_kind Error_monad.Permanent
    "michelson_v1.unexpected_ticket_owner" "Unexpected ticket owner"
    "Ticket can only be created by a smart contract" None
    (Data_encoding.obj1
      (Data_encoding.req None None "ticketer" Alpha_context.Destination.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Unexpected_ticket_owner" then
          let t_value := cast Alpha_context.Destination.t payload in
          Some t_value
        else None
      end)
    (fun (t_value : Alpha_context.Destination.t) ⇒
      Build_extensible "Unexpected_ticket_owner" Alpha_context.Destination.t
        t_value).