🍬 Script_tc_errors.v

Simulations

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.

A type family used to represent the GADT [error_details].

Module Error_trace_family.
  Inductive t : Set :=
  | Error_trace : t
  | Inconsistent_types_fast_error : t.

  Definition to_Set (x : t) : Set :=
    match x with
    | Error_trace ⇒ Error_monad.trace Error_monad._error
    | Inconsistent_types_fast_error ⇒
      Script_tc_errors.inconsistent_types_fast_error
    end.
End Error_trace_family.

A dependent version of the type [error_details].

Inductive dep_error_details (error_context : Set) :
  Error_trace_family.t → Set :=
| Dep_informative :
  error_context →
  dep_error_details error_context Error_trace_family.Error_trace
| Dep_fast :
  dep_error_details error_context
    Error_trace_family.Inconsistent_types_fast_error.
Arguments Dep_informative {_}.
Arguments Dep_fast {_}.

Conversion from [dep_error_details] back to its original type.

Definition to_error_details {error_context error_trace}
  (x : dep_error_details error_context error_trace) :
  Script_tc_errors.error_details error_context :=
  match x with
  | Dep_informative details ⇒ Script_tc_errors.Informative details
  | Dep_fast ⇒ Script_tc_errors.Fast
  end.