🍃 Seq.v
Environment
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 {_}.
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 {_}.