Skip to main content

🍃 Error_monad.v


See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.

The encoding [error_encoding] is valid.
Axiom error_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Error_monad.error_encoding.
#[global] Hint Resolve error_encoding_is_valid : Data_encoding_db.

A notion of equality given an equality on values.
Module Eq.
  Definition t {a b : Set} (eq : a b Prop) (x1 : M? a) (x2 : M? b) :
    Prop :=
    match x1, x2 with
    | Pervasives.Ok x1, Pervasives.Ok x2eq x1 x2
    | Pervasives.Error error1, Pervasives.Error error2error1 = error2
    | _, _False
End Eq.

Definition post_when_success {a : Set} (x : M? a) (P : a Prop) : Prop :=
  match x with
  | Pervasives.Ok vP v
  | Pervasives.Error _True

Lemma post_when_success_bind {a b : Set} (e1 : M? a) (e2 : a M? b)
  (P1 : a Prop) (H1 : post_when_success e1 P1) (P2 : b Prop)
  : ( (v1 : a), P1 v1 post_when_success (e2 v1) P2)
    post_when_success (let? v1 := e1 in e2 v1) P2.
  intro H.
  destruct e1; simpl; trivial.
  now apply H.

Definition terminates {A : Set} (x : M? A) : Prop :=
  match x with
  | Pervasives.Error _False
  | Pervasives.Ok _True

Lemma bind_return_eq {A : Set} (e : M? A) :
  (let? x := e in return? x) =
  now destruct e.

Lemma rewrite_bind {A B : Set} (e1 : M? A) (e2 e2' : A M? B)
  (H : v, e2 v = e2' v) :
  Error_monad.op_gtgtquestion e1 e2 =
  Error_monad.op_gtgtquestion e1 e2'.
  destruct e1; now simpl.

Lemma elim_record_trace_eval {A : Set} (mk_error : unit _error)
  (x : M? A) (v : A)
  : x = return? v
    record_trace_eval mk_error x = return? v.
  intro H; now rewrite H.

When adding an error which is not internal, then it can be altogether ignored when check internal errors do not occur.
Lemma letP_Build_extensible_elim {B} {s} {A} {a} {mb : M? B} {P : B Prop} :
  (List.mem eqb s Error.internal_errors = false)
  (letP? x := mb in P x )
  (letP? x := trace_value (Build_extensible s A a) mb in P x).
  Opaque List.mem Error.internal_errors.
  intros H1 H2.
  destruct mb as [res | err] ; [assumption |].
  unfold bind_prop, Error.not_internal, Error.in_ in ×. simpl. rewrite H1.
  Transparent List.mem Error.internal_errors.