🍬 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 {_}.
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 {_}.