🍬 Script_tc_errors.v

Translated OCaml

See simulations, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require TezosOfOCaml.Proto_alpha.Alpha_context.

Inductive kind : Set :=
| Int_kind : kind
| String_kind : kind
| Bytes_kind : kind
| Prim_kind : kind
| Seq_kind : kind.

Definition unparsed_stack_ty : Set := list Alpha_context.Script.expr.

Definition type_map : Set :=
  list (Alpha_context.Script.location × (unparsed_stack_ty × unparsed_stack_ty)).

Module Ill_typed_view.
  Record record : Set := Build {
    loc : Alpha_context.Script.location;
    actual : unparsed_stack_ty;
    expected : unparsed_stack_ty;
  }.
  Definition with_loc loc (r : record) :=
    Build loc r.(actual) r.(expected).
  Definition with_actual actual (r : record) :=
    Build r.(loc) actual r.(expected).
  Definition with_expected expected (r : record) :=
    Build r.(loc) r.(actual) expected.
End Ill_typed_view.
Definition Ill_typed_view := Ill_typed_view.record.

Inductive context_desc : Set :=
| Lambda : context_desc
| View : context_desc.

Inductive inconsistent_types_fast_error : Set :=
| Inconsistent_types_fast : inconsistent_types_fast_error.

Inductive error_details (error_context : Set) : Set :=
| Informative : error_context → error_details error_context
| Fast : error_details error_context.

Arguments Informative {_}.
Arguments Fast {_}.