🍃 Seq.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Import Error_monad.Notations.

Reserved Notation "'t".

Inductive node (a : Set) : Set :=
| Nil : node a
| Cons : a → 't a → node a

where "'t" := (fun (t_a : Set) ⇒ unit → node t_a).

Definition t := 't.

Arguments Nil {_}.
Arguments Cons {_}.

Definition empty {a : Set} : t a :=
  fun _ ⇒ Nil.

Definition _return {a : Set} (x : a) : t a :=
  fun _ ⇒ Cons x empty.

Definition cons_value {a : Set} (x : a) (s : t a) : t a :=
  fun _ ⇒ Cons x s.

Fixpoint append_node {a : Set} (n1 : node a) (s2 : t a) : node a :=
  match n1 with
  | Nil ⇒ s2 tt
  | Cons x1 s1 ⇒ Cons x1 (fun _ ⇒ append_node (s1 tt) s2)
  end.

Definition append {a : Set} (s1 s2 : t a) : t a :=
  fun _ ⇒ append_node (s1 tt) s2.

Fixpoint map_node {a b : Set} (f : a → b) (n : node a) : node b :=
  match n with
  | Nil ⇒ Nil
  | Cons x n ⇒ Cons (f x) (fun _ ⇒ map_node f (n tt))
  end.

Definition map {a b : Set} (f : a → b) (s : t a) : t b :=
  fun _ ⇒ map_node f (s tt).

Fixpoint filter_node {a : Set} (p : a → bool) (n : node a) : node a :=
  match n with
  | Nil ⇒ Nil
  | Cons x s ⇒
    if p x then
      Cons x (fun _ ⇒ filter_node p (s tt))
    else
      filter_node p (s tt)
  end.

Definition filter {a : Set} (p : a → bool) (s : t a) : t a :=
  fun _ ⇒ filter_node p (s tt).

Fixpoint filter_map_node {a b : Set} (f : a → option b) (n : node a) :
  node b :=
  match n with
  | Nil ⇒ Nil
  | Cons x s ⇒
    match f x with
    | None ⇒ filter_map_node f (s tt)
    | Some y ⇒ Cons y (fun _ ⇒ filter_map_node f (s tt))
    end
  end.

Definition filter_map {a b : Set} (f : a → option b) (s : t a) : t b :=
  fun _ ⇒ filter_map_node f (s tt).

Fixpoint flat_map_node {a b : Set} (f : a → t b) (n : node a) : t b :=
  match n with
  | Nil ⇒ empty
  | Cons x n ⇒ append (f x) (flat_map_node f (n tt))
  end.

Definition flat_map {a b : Set} (f : a → t b) (s : t a) : t b :=
  flat_map_node f (s tt).

Fixpoint fold_left_node {a b : Set} (f : a → b → a) (acc : a) (n : node b) :
  a :=
  match n with
  | Nil ⇒ acc
  | Cons x s ⇒ fold_left_node f (f acc x) (s tt)
  end.

Definition fold_left {a b : Set} (f : a → b → a) (acc : a) (s : t b) : a :=
  fold_left_node f acc (s tt).

Fixpoint iter_node {a : Set} (f : a → unit) (n : node a) : unit :=
  match n with
  | Nil ⇒ tt
  | Cons x s ⇒
    let _ := f x in
    iter_node f (s tt)
  end.

Definition iter {a : Set} (f : a → unit) (s : t a) : unit :=
  iter_node f (s tt).

#[bypass_check(guard)]
Fixpoint unfold {a b : Set} (f : b → option (a × b)) (init : b) {struct init} :
  t a :=
  match f init with
  | None ⇒ empty
  | Some (v, next) ⇒ cons_value v (unfold f next)
  end.

Definition first {a : Set} (s : t a) : option a :=
  match s tt with
  | Nil ⇒ None
  | Cons x _ ⇒ Some x
  end.

Definition fold_left_e {a b trace : Set}
  (f : a → b → Pervasives.result a trace) (acc : a) (s : t b) :
  Pervasives.result a trace :=
  fold_left (fun acc x ⇒ let? acc := acc in f acc x) (return? acc) s.

Definition fold_left_s := @fold_left.
Arguments fold_left_s {_ _}.

Definition fold_left_es := @fold_left_e.
Arguments fold_left_es {_ _ _}.

Fixpoint iter_e_node {a trace : Set} (f : a → Pervasives.result unit trace)
  (n : node a) : Pervasives.result unit trace :=
  match n with
  | Nil ⇒ return? tt
  | Cons x s ⇒
    let? _ := f x in
    iter_e_node f (s tt)
  end.

Definition iter_e {a trace : Set}
  (f : a → Pervasives.result unit trace) (s : t a) :
  Pervasives.result unit trace :=
  iter_e_node f (s tt).

Definition iter_s := @iter.
Arguments iter_s {_}.

Definition iter_es := @iter_e.
Arguments iter_es {_ _}.

Definition iter_ep {a : Set} :=
  iter_e (a := a) (trace := list Error_monad._error).

Definition iter_p := @iter.
Arguments iter_p {_}.