# 🍃 Seq.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Pervasives.

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
| Nils2 tt
| Cons x1 s1Cons 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
| NilNil
| Cons x nCons (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
| NilNil
| 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
| NilNil
| Cons x s
match f x with
| Nonefilter_map_node f (s tt)
| Some yCons 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
| Nilempty
| Cons x nappend (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
| Nilacc
| Cons x sfold_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
| Niltt
| 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
| Noneempty
| Some (v, next)cons_value v (unfold f next)
end.

Definition first {a : Set} (s : t a) : option a :=
match s tt with
| NilNone
| 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 xlet? 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
| Nilreturn? 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 {_}.