🍃 List.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Either.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.Seq.
Import Error_monad.Notations.
Import Pervasives.Notations.
Definition t (a : Set) : Set := list a.
Definition nil : ∀ {a : Set}, list a :=
fun _ ⇒
[].
Definition nil_e : ∀ {a trace : Set}, Pervasives.result (list a) trace :=
fun _ _ ⇒
return? [].
Definition nil_s : ∀ {a : Set}, list a :=
fun _ ⇒
[].
Definition nil_es : ∀ {a trace : Set},
Pervasives.result (list a) trace :=
fun _ _ ⇒
return? [].
Definition cons_value : ∀ {a : Set}, a → list a → list a :=
@cons.
Definition is_empty {a : Set} (l : list a) : bool :=
match l with
| [] ⇒ true
| _ :: _ ⇒ false
end.
Definition hd : ∀ {a : Set}, list a → option a :=
fun _ l ⇒
match l with
| [] ⇒ None
| x :: _ ⇒ Some x
end.
Definition tl : ∀ {a : Set}, list a → option (list a) :=
fun _ l ⇒
match l with
| [] ⇒ None
| _x :: m ⇒ Some m
end.
Fixpoint nth_z {a : Set} (l : list a) (i : Z.t) {struct l} : option a :=
match l, i with
| [], _ ⇒ None
| x :: _, 0 ⇒ Some x
| _ :: l, _ ⇒ nth_z l (i - 1)
end.
Definition nth : ∀ {a : Set}, list a → int → option a :=
@nth_z.
Definition nth_opt : ∀ {a : Set}, list a → int → option a :=
@nth_z.
Definition last : ∀ {a : Set}, a → list a → a :=
fun _ x l ⇒
List.last l x.
Fixpoint last_opt {a : Set} (l: list a) : option a :=
match l with
| [] ⇒ None
| [z] ⇒ Some z
| x :: tl ⇒ (last_opt tl)
end.
Definition find : ∀ {a : Set}, (a → bool) → list a → option a :=
fun a ⇒
List.find (A := a).
Definition find_opt : ∀ {a : Set}, (a → bool) → list a → option a :=
fun _ ⇒
find.
Fixpoint find_map {a b : Set} (f : a → option b) (l : list a) : option b :=
match l with
| [] ⇒ None
| x :: l' ⇒
match f x with
| Some y ⇒ f x
| None ⇒ find_map f l'
end
end.
Fixpoint mem {a : Set} (eq_dec : a → a → bool) (v : a) (l : list a) : bool :=
match l with
| [] ⇒ false
| x :: l ⇒ eq_dec v x || mem eq_dec v l
end.
Fixpoint assoc {a b : Set}
(eq : a → a → bool)
(k : a)
(l : list (a × b))
: option b :=
match l with
| [] ⇒ None
| (h, x) :: tl ⇒ if eq k h then Some x else assoc eq k tl
end.
Definition assoc_opt : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → option b :=
fun _ _ ⇒ assoc.
(* not definable without decidable equality *)
Parameter assq : ∀ {a b : Set}, a → list (a × b) → option b.
(* not definable without decidable equality *)
Parameter assq_opt : ∀ {a b : Set}, a → list (a × b) → option b.
Fixpoint mem_assoc {a b : Set}
(eq : a → a → bool)
(k : a)
(l : list (a × b))
: bool :=
match l with
| [] ⇒ false
| (h, x) :: tl ⇒ eq k h || mem_assoc eq k tl
end.
(* not definable without decidable equality *)
Parameter mem_assq : ∀ {a b : Set}, a → list (a × b) → bool.
Fixpoint remove_assoc {a b : Set}
(eq : a → a → bool)
(k : a)
(l : list (a × b))
: list (a × b) :=
match l with
| [] ⇒ []
| (h, x) :: tl ⇒
if eq k h then
tl
else
(h, x) :: remove_assoc eq k tl
end.
(* not definable without decidable equality *)
Parameter remove_assq : ∀ {a b : Set}, a → list (a × b) → list (a × b).
Fixpoint nat_init {a trace : Set} (er : trace) (n : nat) (ff : nat → a)
: list a :=
match n with
| 0%nat ⇒ []
| S k ⇒ ff 0%nat :: nat_init er k (fun v ⇒ ff (S v))
end.
Definition init_value {a trace : Set}
(er : trace) (n : int) (ff : int → a)
: Pervasives.result (list a) trace :=
match n with
| Zneg _ ⇒ Pervasives.Error er
| Z0 ⇒ Pervasives.Ok []
| Zpos x ⇒
Pervasives.Ok (nat_init er (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x)))
end.
Fixpoint length {a : Set} (l : list a) : int :=
match l with
| [] ⇒ 0
| _ :: l ⇒ (length l) +i 1
end.
Definition rev {a : Set} (l : list a) : list a :=
Lists.List.rev' l.
Definition concat : ∀ {a : Set}, list (list a) → list a :=
fun _ ⇒
List.concat.
Definition append : ∀ {a : Set}, list a → list a → list a :=
fun _ ⇒
List.append.
Definition rev_append : ∀ {a : Set}, list a → list a → list a :=
fun _ ⇒
List.rev_append.
Definition flatten : ∀ {a : Set}, list (list a) → list a :=
fun _ ⇒
List.concat.
Fixpoint combine_aux {a b : Set}
(list1 : list a)
(list2 :list b)
(partial : list (a × b))
: option (list (a × b)) :=
match list1, list2 with
| [], _ :: _ | _ :: _, [] ⇒ None
| [], [] ⇒ Some partial
| h1 :: tl1 , h2 :: tl2 ⇒ combine_aux tl1 tl2 ((h1, h2) :: partial)
end.
Definition combine {a b trace : Set} (er : trace)
(l1 : list a) (l2 : list b)
: Pervasives.result (list (a × b)) trace :=
match combine_aux l1 l2 [] with
| Some x ⇒ Pervasives.Ok x
| None ⇒ Pervasives.Error er
end.
Definition rev_combine {a b trace : Set} (er : trace)
(l1 : list a) (l2 : list b)
: Pervasives.result (list (a × b)) trace :=
match combine_aux l1 l2 [] with
| Some x ⇒ Pervasives.Ok (rev x)
| None ⇒ Pervasives.Error er
end.
Definition split : ∀ {a b : Set}, list (a × b) → list a × list b :=
fun _ _ ⇒
List.split.
Fixpoint iter2 {a b trace : Set} (er : trace)
(f : a → b → unit) (l1 : list a) (l2 : list b)
: Pervasives.result unit trace :=
match l1,l2 with
| [], [] ⇒ Pervasives.Ok tt
| _ :: l1', _ :: l2' ⇒ iter2 er f l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Fixpoint map2 {a b c trace : Set} (er : trace)
(f : a → b → c) (l1 : list a) (l2 : list b)
: Pervasives.result (list c) trace :=
match l1, l2 with
| [], [] ⇒ Pervasives.Ok []
| x :: l1', y :: l2' ⇒
match map2 er f l1' l2' with
| Pervasives.Ok l3 ⇒ Pervasives.Ok (f x y :: l3)
| Pervasives.Error e ⇒ Pervasives.Error e
end
| _, _ ⇒ Pervasives.Error er
end.
Definition rev_map2 : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace :=
fun a b c trace er f l1 l2 ⇒
match map2 er f l1 l2 with
| Pervasives.Ok l3 ⇒ Pervasives.Ok (List.rev l3)
| Pervasives.Error _ as e ⇒ e
end.
Fixpoint fold_left2 {a b c trace : Set} (er : trace)
(f : a → b → c → a) (acc : a) (l1 : list b) (l2 : list c)
: Pervasives.result a trace :=
match l1, l2 with
| [], [] ⇒ Pervasives.Ok acc
| x :: l1', y :: l2' ⇒ fold_left2 er f (f acc x y) l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Fixpoint fold_right2 {a b c trace : Set} (er : trace)
(f : a → b → c → c) (l1 : list a) (l2 : list b) (acc : c)
: Pervasives.result c trace :=
match l1, l2 with
| [], [] ⇒ Pervasives.Ok acc
| x :: l1', y :: l2' ⇒
match fold_right2 er f l1' l2' acc with
| Pervasives.Ok acc' ⇒ Pervasives.Ok (f x y acc')
| Pervasives.Error _ as e ⇒ e
end
| _, _ ⇒ Pervasives.Error er
end.
Definition for_all2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
fun a b trace er p l1 l2 ⇒ fold_left2 er
(fun acc x y ⇒ acc && p x y) true l1 l2.
Definition _exists2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
fun a b trace er p l1 l2 ⇒ fold_left2 er
(fun acc x y ⇒ acc || p x y) false l1 l2.
Fixpoint nat_init_e {a trace : Set} (er : trace) (n : nat)
(ff : nat → Pervasives.result a trace)
: Pervasives.result (list a) trace :=
match n with
| 0%nat ⇒ Pervasives.Ok []
| S k ⇒
match ff 0%nat with
| Pervasives.Error e ⇒ Pervasives.Error e
| Pervasives.Ok x ⇒
match nat_init_e er k (fun v ⇒ ff (S v)) with
| Pervasives.Error _ as e ⇒ e
| Pervasives.Ok l ⇒ Pervasives.Ok (x :: l)
end
end
end.
Definition init_e : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace :=
fun a trace er n ff ⇒
match n with
| Zneg _ ⇒ Pervasives.Error er
| Z0 ⇒ Pervasives.Ok []
| Zpos _ ⇒ nat_init_e er (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x))
end.
Definition init_s : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace :=
@init_value.
Definition init_es : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace :=
@init_e.
Definition init_p : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace :=
@init_value.
Fixpoint find_e {a trace : Set}
(ep : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (option a) trace :=
match l with
| [] ⇒ Pervasives.Ok None
| x :: l' ⇒
match ep x with
| Pervasives.Error e ⇒ Pervasives.Error e
| Pervasives.Ok true ⇒ Pervasives.Ok (Some x)
| Pervasives.Ok false ⇒ find_e ep l'
end
end.
Definition find_s : ∀ {a : Set},
(a → bool) → list a → option a :=
@find.
Definition find_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (option a) trace :=
@find_e.
Fixpoint find_map_e {a b trace : Set}
(f : a → Pervasives.result (option b) trace) (l : list a)
: Pervasives.result (option b) trace :=
match l with
| [] ⇒ Pervasives.Ok None
| x :: l' ⇒
match f x with
| Pervasives.Error _ as e ⇒ e
| Pervasives.Ok (Some _) as res ⇒ res
| Pervasives.Ok None ⇒ find_map_e f l'
end
end.
Definition find_map_s : ∀ {a b : Set},
(a → option b) → list a → option b :=
@find_map.
Definition find_map_es : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (option b) trace :=
@find_map_e.
Definition filter : ∀ {a : Set}, (a → bool) → list a → list a :=
fun _ ⇒
List.filter.
Fixpoint filteri_aux {a : Set} (i : int) (p : int → a → bool) (l : list a)
: list a :=
match l with
| [] ⇒ []
| x :: l' ⇒ if p i x
then x :: filteri_aux (i+1)%Z p l'
else filteri_aux (i+1)%Z p l'
end.
Definition filteri : ∀ {a : Set}, (int → a → bool) → list a → list a :=
fun a ⇒ @filteri_aux a 0.
Definition find_all : ∀ {a : Set}, (a → bool) → list a → list a :=
@filter.
Definition rev_filter : ∀ {a : Set}, (a → bool) → list a → list a :=
fun a p l ⇒ List.rev (filter p l).
Definition rev_filteri : ∀ {a : Set},
(int → a → bool) → list a → list a :=
fun a p l ⇒ List.rev (filteri p l).
Fixpoint filter_some {a : Set} (l : list (option a)) : list a :=
match l with
| [] ⇒ []
| None :: l' ⇒ filter_some l'
| Some x :: l' ⇒ x :: filter_some l'
end.
Definition rev_filter_some : ∀ {a : Set}, list (option a) → list a :=
fun a l ⇒ List.rev (filter_some l).
Fixpoint filter_ok {a b : Set} (l : list (Pervasives.result a b)) : list a :=
match l with
| [] ⇒ []
| Pervasives.Error _ :: l' ⇒ filter_ok l'
| Pervasives.Ok x :: l' ⇒ x :: filter_ok l'
end.
Definition rev_filter_ok : ∀ {a b : Set},
list (Pervasives.result a b) → list a :=
fun a b l ⇒ List.rev (filter_ok l).
Fixpoint filter_error {a b : Set} (l : list (Pervasives.result a b)) : list b :=
match l with
| [] ⇒ []
| Pervasives.Ok _ :: l' ⇒ filter_error l'
| Pervasives.Error e :: l' ⇒ e :: filter_error l'
end.
Definition rev_filter_error : ∀ {a b : Set},
list (Pervasives.result a b) → list b :=
fun a b l ⇒ List.rev (filter_error l).
Fixpoint filter_left {a b : Set} (l : list (Either.t a b)) : list a :=
match l with
| [] ⇒ []
| Either.Left x :: l' ⇒ x :: filter_left l'
| Either.Right _ :: l' ⇒ filter_left l'
end.
Definition rev_filter_left : ∀ {a b : Set}, list (Either.t a b) → list a :=
fun a b l ⇒ List.rev (filter_left l).
Fixpoint filter_right {a b : Set} (l : list (Either.t a b)) : list b :=
match l with
| [] ⇒ []
| Either.Right x :: l' ⇒ x :: filter_right l'
| Either.Left _ :: l' ⇒ filter_right l'
end.
Definition rev_filter_right : ∀ {a b : Set},
list (Either.t a b) → list b :=
fun a b l ⇒ List.rev (filter_right l).
Fixpoint filter_e {a trace : Set}
(f : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? b := f x in
let? l := filter_e f l in
if b then
return? (x :: l)
else
return? l
end.
Definition rev_filter_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
fun a trace f l ⇒
let? l' := filter_e f l in
return? List.rev l'.
Fixpoint filter_s {a : Set}
(f : a → bool) (l : list a) : list a :=
match l with
| [] ⇒ []
| x :: l ⇒
let b := f x in
let l := filter_s f l in
if b then
x :: l
else
l
end.
Definition rev_filter_s : ∀ {a : Set},
(a → bool) → list a → list a :=
fun a p l ⇒
List.rev (filter_s p l).
Definition rev_filter_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
@rev_filter_e.
Fixpoint filter_es {a trace : Set}
(f : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? b := f x in
let? l := filter_es f l in
if b then
return? (x :: l)
else
return? l
end.
Fixpoint filteri_e_aux {a trace : Set} (i : int)
(p : int → a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a) trace :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
let? b := p i x in
let? res := filteri_e_aux (i + 1)%Z p l' in
return? (if b then x :: res else res)
end.
Definition filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
fun a trace ⇒ @filteri_e_aux a trace 0.
Definition rev_filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
fun a trace p l ⇒
let? res := filteri_e p l in
return? List.rev res.
Definition rev_filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a :=
@rev_filteri.
Definition filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a :=
@filteri.
Definition rev_filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
@rev_filteri_e.
Definition filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
@filteri_e.
Definition filter_p : ∀ {a : Set},
(a → bool) → list a → list a :=
@filter.
Definition partition : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
fun _ ⇒
List.partition.
Definition rev_partition : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
fun a p l ⇒ partition p (List.rev l).
Fixpoint partition_map {a b c : Set}
(f : a → Either.t b c) (l : list a)
: list b × list c :=
match l with
| [] ⇒ ([], [])
| x :: l' ⇒
let '(l1, l2) := partition_map f l' in
match f x with
| Either.Left y ⇒ (y :: l1, l2)
| Either.Right y ⇒ (l1, y :: l2)
end
end.
Definition rev_partition_map : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c :=
fun a b c f l ⇒
partition_map f (List.rev l).
Fixpoint partition_result {a b : Set}
(l : list (Pervasives.result a b)) : list a × list b :=
match l with
| [] ⇒ ([], [])
| x :: l' ⇒
let '(l1, l2) := partition_result l' in
match x with
| Pervasives.Ok x ⇒ (x :: l1, l2)
| Pervasives.Error e ⇒ (l1, e :: l2)
end
end.
Definition rev_partition_result : ∀ {a b : Set},
list (Pervasives.result a b) → list a × list b :=
fun a b l ⇒ partition_result (List.rev l).
Fixpoint partition_either {a b : Set}
(l : list (Either.t a b)) : list a × list b :=
match l with
| [] ⇒ ([], [])
| x :: l' ⇒
let '(l1, l2) := partition_either l' in
match x with
| Either.Left y ⇒ (y :: l1, l2)
| Either.Right y ⇒ (l1, y :: l2)
end
end.
Definition rev_partition_either : ∀ {a b : Set},
list (Either.t a b) → list a × list b :=
fun a b l ⇒ partition_either (List.rev l).
Fixpoint partition_e {a trace : Set}
(p : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a × list a) trace :=
match l with
| [] ⇒ return? ([], [])
| x :: l' ⇒
let? b := p x in
let? '(l1, l2) := partition_e p l' in
return? (if b then (x :: l1, l2) else (l1, x :: l2))
end.
Definition rev_partition_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace :=
fun a trace p l ⇒ partition_e p (List.rev l).
Definition rev_partition_s : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
@rev_partition.
Fixpoint partition_s {a : Set}
(f : a → bool) (l : list a) : list a × list a :=
match l with
| [] ⇒ ([], [])
| x :: l ⇒
let b := f x in
let '(yes, no) := partition_s f l in
if b then
(x :: yes, no)
else
(yes, x :: no)
end.
Definition rev_partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace :=
@rev_partition_e.
Definition partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace :=
@partition_e.
Definition partition_p : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
@partition.
Fixpoint partition_map_e {a b c trace : Set}
(f : a → Pervasives.result (Either.t b c) trace) (l : list a) :
Pervasives.result (list b × list c) trace :=
match l with
| [] ⇒ return? ([], [])
| x :: l' ⇒
let? e := f x in
let? '(l1, l2) := partition_map_e f l' in
match e with
| Either.Left y ⇒ return? (y :: l1, l2)
| Either.Right y ⇒ return? (l1, y :: l2)
end
end.
Definition rev_partition_map_e : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace :=
fun a b c trace f l ⇒ partition_map_e f (List.rev l).
Definition rev_partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c :=
@rev_partition_map.
Definition partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c :=
@partition_map.
Definition rev_partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace :=
@rev_partition_map_e.
Definition partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace :=
@partition_map_e.
Definition iter : ∀ {a : Set},
(a → unit) → list a → unit :=
fun a f l ⇒ tt.
Fixpoint iter_e {a trace : Set}
(f : a → Pervasives.result unit trace) (l : list a)
: Pervasives.result unit trace :=
match l with
| [] ⇒ return? tt
| x :: l ⇒
let? _ := f x in
iter_e f l
end.
Fixpoint iter_s {a : Set}
(f : a → unit) (l : list a) : unit :=
match l with
| [] ⇒ tt
| x :: l ⇒
let _ := f x in
iter_s f l
end.
Fixpoint iter_es {a trace : Set}
(f : a → Pervasives.result unit trace) (l : list a)
: Pervasives.result unit trace :=
match l with
| [] ⇒ return? tt
| x :: l ⇒
let? _ := f x in
iter_es f l
end.
Definition iter_p : ∀ {a : Set}, (a → unit) → list a → unit :=
@iter.
Definition iteri : ∀ {a : Set}, (int → a → unit) → list a → unit :=
fun a f l ⇒ tt.
Fixpoint iteri_e_aux {a trace : Set} (i : int)
(f : int → a → Pervasives.result unit trace) (l : list a)
: Pervasives.result unit trace :=
match l with
| [] ⇒ return? tt
| x :: l' ⇒
let? _ := f i x in
iteri_e_aux (i + 1)%Z f l'
end.
Definition iteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace :=
fun a trace ⇒ @iteri_e_aux a trace 0.
Definition iteri_s : ∀ {a : Set},
(int → a → unit) → list a → unit :=
@iteri.
Definition iteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace :=
@iteri_e.
Definition iteri_p : ∀ {a : Set},
(int → a → unit) → list a → unit :=
@iteri.
Definition map : ∀ {a b : Set}, (a → b) → list a → list b :=
@Lists.List.map.
Fixpoint map_e {a b trace : Set}
(f : a → Pervasives.result b trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? y := f x in
let? l' := map_e f l in
return? (y :: l')
end.
Fixpoint map_s {a b : Set}
(f : a → b) (l : list a) : list b :=
match l with
| [] ⇒ []
| x :: l ⇒
let x := f x in
let l := map_s f l in
x :: l
end.
Fixpoint map_es {a b trace : Set}
(f : a → Pervasives.result b trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? y := f x in
let? l' := map_es f l in
return? (y :: l')
end.
Definition map_p : ∀ {a b : Set},
(a → b) → list a → list b :=
@map.
Definition mapi : ∀ {a b : Set}, (int → a → b) → list a → list b :=
fun _ _ ⇒
List.mapi.
Fixpoint mapi_e_aux {a b trace : Set} (i : int)
(f : int → a → Pervasives.result b trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
let? y := f i x in
let? res := mapi_e_aux (i+1)%Z f l' in
return? (y :: res)
end.
Definition mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace ⇒ @mapi_e_aux a b trace 0.
Definition mapi_s : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@mapi.
Definition mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
@mapi_e.
Definition mapi_p : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@mapi.
Definition rev_map : ∀ {a b : Set}, (a → b) → list a → list b :=
fun _ _ ⇒
List.rev_map.
Definition rev_mapi : ∀ {a b : Set}, (int → a → b) → list a → list b :=
fun a b f l ⇒ List.rev (mapi f l).
Definition rev_map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace f l ⇒
let? res := map_e f l in
return? (List.rev res).
Definition rev_map_s : ∀ {a b : Set},
(a → b) → list a → list b :=
@rev_map.
Definition rev_map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
@rev_map_e.
Definition rev_map_p : ∀ {a b : Set},
(a → b) → list a → list b :=
@rev_map.
Definition rev_mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace f l ⇒
let? res := mapi_e f l in
return? List.rev res.
Definition rev_mapi_s : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@rev_mapi.
Definition rev_mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
@rev_mapi_e.
Definition rev_mapi_p : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@rev_mapi.
Fixpoint filter_map {a b : Set} (f : a → option b) (l : list a) : list b :=
match l with
| [] ⇒ []
| x :: l' ⇒
match f x with
| None ⇒ filter_map f l'
| Some y ⇒ y :: filter_map f l'
end
end.
Definition rev_filter_map : ∀ {a b : Set},
(a → option b) → list a → list b :=
fun a b f l ⇒ List.rev (filter_map f l).
Fixpoint filter_map_e {a b trace : Set}
(f : a → Pervasives.result (option b) trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
let? y := f x in
match y with
| None ⇒ filter_map_e f l'
| Some z ⇒ let? res := filter_map_e f l' in return? (z :: res)
end
end.
Definition rev_filter_map_e : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace f l ⇒ filter_map_e f (List.rev l).
Definition rev_filter_map_s : ∀ {a b : Set},
(a → option b) → list a → list b :=
@rev_filter_map.
Fixpoint filter_map_s {a b : Set}
(f : a → option b) (l : list a) : list b :=
match l with
| [] ⇒ []
| x :: l ⇒
let y := f x in
let l' := filter_map_s f l in
match y with
| Some y ⇒ y :: l'
| None ⇒ l'
end
end.
Definition rev_filter_map_es : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (list b) trace :=
@rev_filter_map_e.
Fixpoint filter_map_es {a b trace : Set}
(f : a → Pervasives.result (option b) trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? y := f x in
let? l' := filter_map_es f l in
match y with
| Some y ⇒ return? (y :: l')
| None ⇒ return? l'
end
end.
Definition filter_map_p : ∀ {a b : Set},
(a → option b) → list a → list b :=
@filter_map.
Definition concat_map : ∀ {a b : Set}, (a → list b) → list a → list b :=
fun a b f l ⇒ List.concat (List.map f l).
Definition concat_map_s : ∀ {a b : Set},
(a → list b) → list a → list b :=
@concat_map.
Definition concat_map_e : ∀ {_error a b : Set},
(a → Pervasives.result (list b) _error) → list a →
Pervasives.result (list b) _error :=
fun _error a b f l ⇒
let? ls := map_e f l in
return? concat ls.
Definition concat_map_es : ∀ {_error a b : Set},
(a → Pervasives.result (list b) _error) → list a →
Pervasives.result (list b) _error :=
@concat_map_e.
Definition concat_map_p : ∀ {a b : Set},
(a → list b) → list a → list b :=
@concat_map.
Definition fold_left {a b : Set} (f : a → b → a) (acc : a) (l : list b) : a :=
Lists.List.fold_left f l acc.
Definition fold_left_e {a b trace : Set}
(f : a → b → Pervasives.result a trace) (acc : a) (l : list b) :
Pervasives.result a trace :=
fold_left (fun acc item ⇒ let? acc := acc in f acc item) (return? acc) l.
Definition fold_left_s : ∀ {a b : Set},
(a → b → a) → a → list b → a :=
fun _ _ ⇒
fold_left.
Definition fold_left_es : ∀ {a b trace : Set},
(a → b → Pervasives.result a trace) → a → list b →
Pervasives.result a trace :=
fun _ _ _ ⇒
fold_left_e.
Fixpoint fold_left_map {a b c : Set} (f : a → b → a × c)
(acc : a) (l : list b) : a × list c :=
match l with
| [] ⇒ (acc, [])
| x :: l' ⇒
let '(acc1, y) := f acc x in
let '(acc2, res) := fold_left_map f acc1 l' in (acc2, y :: res)
end.
Fixpoint fold_left_map_e {a b c trace : Set}
(f : a → b → Pervasives.result (a × c) trace) (acc : a) (l : list b) :
Pervasives.result (a × list c) trace :=
match l with
| [] ⇒ return? (acc, [])
| x :: l' ⇒
let? '(acc1, y) := f acc x in
let? '(acc2, res) := fold_left_map_e f acc1 l' in
return? (acc2, y :: res)
end.
Definition fold_left_map_s : ∀ {a b c : Set},
(a → b → a × c) → a → list b → a × list c :=
@fold_left_map.
Definition fold_left_map_es : ∀ {a b c trace : Set},
(a → b → Pervasives.result (a × c) trace) → a → list b →
Pervasives.result (a × list c) trace :=
@fold_left_map_e.
Definition fold_left_i {a b : Set}
(f : int → a → b → a) (acc : a) (l : list b) : a :=
snd (
fold_left
(fun '(index, acc) item ⇒
let acc := f index acc item in
(index +i 1, acc)
)
(0, acc)
l
).
Definition fold_left_i_e {a b trace : Set}
(f : int → a → b → Pervasives.result a trace) (acc : a) (l : list b) :
Pervasives.result a trace :=
fold_left_i
(fun index acc item ⇒ let? acc := acc in f index acc item)
(return? acc)
l.
Definition fold_left_i_s := @fold_left_i.
Arguments fold_left_i_s {a b}.
Definition fold_left_i_es := @fold_left_i_e.
Arguments fold_left_i_es {a b trace}.
Definition fold_right : ∀ {a b : Set}, (a → b → b) → list a → b → b :=
fun _ _ ⇒
List.fold_right.
Fixpoint fold_right_e {a b trace : Set}
(f : a → b → Pervasives.result b trace) (l : list a) (acc : b) :
Pervasives.result b trace :=
match l with
| [] ⇒ return? acc
| x :: l' ⇒
let? acc' := fold_right_e f l' acc in
f x acc'
end.
Fixpoint fold_right_s {a b : Set}
(f : a → b → b) (l : list a) (accumulator : b) : b :=
match l with
| [] ⇒ accumulator
| x :: l ⇒
let accumulator := fold_right_s f l accumulator in
f x accumulator
end.
Fixpoint fold_right_es {a b trace : Set}
(f : a → b → Pervasives.result b trace) (l : list a)
(accumulator : b) : Pervasives.result b trace :=
match l with
| [] ⇒ return? accumulator
| x :: l ⇒
let? accumulator := fold_right_es f l accumulator in
f x accumulator
end.
Fixpoint iter2_e {a b trace : Set} (er : trace)
(f : a → b → Pervasives.result unit trace) (l1 : list a) (l2 : list b)
: Pervasives.result unit trace :=
match l1, l2 with
| [], [] ⇒ return? tt
| x :: l1', y :: l2' ⇒
let? _ := f x y in iter2_e er f l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Definition iter2_s : ∀ {a b trace : Set},
trace → (a → b → unit) → list a → list b →
Pervasives.result unit trace :=
@iter2.
Definition iter2_es : ∀ {a b trace : Set},
trace → (a → b → Pervasives.result unit trace) → list a →
list b → Pervasives.result unit trace :=
@iter2_e.
Fixpoint map2_e {a b c trace : Set} (er : trace)
(f : a → b → Pervasives.result c trace) (l1 : list a) (l2 : list b) :
Pervasives.result (list c) trace :=
match l1, l2 with
| [], [] ⇒ return? []
| x :: l1', y :: l2' ⇒
let? z := f x y in
let? res := map2_e er f l1' l2' in return? (z :: res)
| _, _ ⇒ Pervasives.Error er
end.
Definition map2_s : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace :=
@map2.
Definition map2_es : ∀ {a b c trace : Set},
trace → (a → b → Pervasives.result c trace) → list a →
list b → Pervasives.result (list c) trace :=
@map2_e.
Definition rev_map2_e : ∀ {a b c trace : Set},
trace → (a → b → Pervasives.result c trace) → list a → list b →
Pervasives.result (list c) trace :=
fun a b c trace er f l1 l2 ⇒
let? res := map2_e er f l1 l2 in return? List.rev res.
Definition rev_map2_s : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace :=
@rev_map2.
Definition rev_map2_es : ∀ {a b c trace : Set},
trace → (a → b → Pervasives.result c trace) → list a →
list b → Pervasives.result (list c) trace :=
@rev_map2_e.
Fixpoint fold_left2_e {a b c trace : Set} (er : trace)
(f : a → b → c → Pervasives.result a trace) (acc : a) (l1 : list b) (l2 : list c)
: Pervasives.result a trace :=
match l1, l2 with
| [], [] ⇒ return? acc
| x :: l1', y :: l2' ⇒
let? acc' := f acc x y in
fold_left2_e er f acc' l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Definition fold_left2_s : ∀ {a b c trace : Set},
trace → (a → b → c → a) → a → list b → list c →
Pervasives.result a trace :=
@fold_left2.
Definition fold_left2_es : ∀ {a b c trace : Set},
trace → (a → b → c → Pervasives.result a trace) → a →
list b → list c → Pervasives.result a trace :=
@fold_left2_e.
Fixpoint fold_right2_e {a b c trace : Set} (er : trace)
(f : a → b → c → Pervasives.result c trace) (l1 : list a) (l2 : list b) (acc : c)
: Pervasives.result c trace :=
match l1, l2 with
| [], [] ⇒ return? acc
| x :: l1', y :: l2' ⇒
let? acc' := fold_right2_e er f l1' l2' acc in
f x y acc'
| _, _ ⇒ Pervasives.Error er
end.
Definition fold_right2_s : ∀ {a b c trace : Set},
trace → (a → b → c → c) → list a → list b → c →
Pervasives.result c trace :=
@fold_right2.
Definition fold_right2_es : ∀ {a b c trace : Set},
trace → (a → b → c → Pervasives.result c trace) → list a →
list b → c → Pervasives.result c trace :=
@fold_right2_e.
Definition for_all : ∀ {a : Set}, (a → bool) → list a → bool :=
fun a ⇒
List.forallb (A := a).
(* intended semantics? *)
Fixpoint for_all_e {a trace : Set}
(p : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result bool trace :=
match l with
| [] ⇒ return? true
| x :: l' ⇒
let? b := p x in
let? res := for_all_e p l' in
return? (b && res)
end.
Fixpoint for_all_s {a : Set}
(f : a → bool) (l : list a) : bool :=
match l with
| [] ⇒ true
| x :: l ⇒
let b := f x in
if b then
for_all_s f l
else
false
end.
Definition for_all_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result bool trace :=
@for_all_e.
Definition for_all_p : ∀ {a : Set},
(a → bool) → list a → bool :=
@for_all.
Definition _exists : ∀ {a : Set}, (a → bool) → list a → bool :=
fun a ⇒
List.existsb (A := a).
Fixpoint exists_e {a trace : Set}
(p : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result bool trace :=
match l with
| [] ⇒ return? false
| x :: l' ⇒
let? b := p x in
let? res := exists_e p l' in
return? (b || res)
end.
Fixpoint exists_s {a : Set}
(f : a → bool) (l : list a) : bool :=
match l with
| [] ⇒ false
| x :: l ⇒
let b := f x in
if b then
true
else
exists_s f l
end.
Definition exists_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result bool trace :=
@exists_e.
Definition exists_p : ∀ {a : Set},
(a → bool) → list a → bool :=
@_exists.
Fixpoint for_all2_e {a b trace : Set} (er : trace)
(f : a → b → Pervasives.result bool trace) (l1 : list a) (l2 : list b)
: Pervasives.result bool trace :=
match l1, l2 with
| [], [] ⇒ return? true
| x :: l1', y :: l2' ⇒
let? b := f x y in
let? res := for_all2_e er f l1' l2' in
return? (b && res)
| _, _ ⇒ Pervasives.Error er
end.
Definition for_all2_s : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
@for_all2.
Definition for_all2_es : ∀ {a b trace : Set},
trace → (a → b → Pervasives.result bool trace) → list a →
list b → Pervasives.result bool trace :=
@for_all2_e.
Fixpoint exists2_e {a b trace : Set} (er : trace)
(f : a → b → Pervasives.result bool trace) (l1 : list a) (l2 : list b)
: Pervasives.result bool trace :=
match l1, l2 with
| [], [] ⇒ return? false
| x :: l1', y :: l2' ⇒
let? b := f x y in
let? res := exists2_e er f l1' l2' in
return? (b || res)
| _, _ ⇒ Pervasives.Error er
end.
Definition exists2_s : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
@_exists2.
Definition exists2_es : ∀ {a b trace : Set},
trace → (a → b → Pervasives.result bool trace) → list a →
list b → Pervasives.result bool trace :=
@exists2_e.
Fixpoint combine_drop {a b : Set} (l1 : list a) (l2 : list b) : list (a × b) :=
match l1, l2 with
| [], _ ⇒ []
| _, [] ⇒ []
| x :: l1', y :: l2' ⇒ (x, y) :: combine_drop l1' l2'
end.
Fixpoint combine_with_leftovers {a b : Set} (l1 : list a) (l2 : list b)
: list (a × b) × option (Either.t (list a) (list b)) :=
match l1, l2 with
| [], [] ⇒ ([], None)
| [], _ ⇒ ([], Some (Either.Right l2))
| _, [] ⇒ ([], Some (Either.Left l1))
| x :: l1', y :: l2' ⇒
let '(combine, leftovers) := combine_with_leftovers l1' l2' in
((x, y) :: combine, leftovers)
end.
Parameter product : ∀ {a b : Set}, list a → list b → list (a × b).
Fixpoint compare {a : Set} (cmp : a → a → int) (l1 l2 : list a)
: int :=
match l1, l2 with
| [], [] ⇒ 0
| [], _ ⇒ -1
| _, [] ⇒ 1
| x :: l1', y :: l2' ⇒
match cmp x y with
| Z0 ⇒ compare cmp l1' l2'
| Zpos _ ⇒ 1
| Zneg _ ⇒ -1
end
end.
Definition compare_lengths : ∀ {a b : Set}, list a → list b → int :=
fun _ _ l1 l2 ⇒
(length l1) -i (length l2).
Definition compare_length_with : ∀ {a : Set}, list a → int → int :=
fun _ l n ⇒
length l -i n.
Fixpoint equal {a : Set} (eqb : a → a → bool) (l1 l2 : list a) : bool :=
match l1, l2 with
| [], [] ⇒ true
| x1 :: l1, x2 :: l2 ⇒ eqb x1 x2 && equal eqb l1 l2
| _, _ ⇒ false
end.
(* inserts new val just before first value greater than it *)
Fixpoint insert {a : Set} (cmp : a → a → int) (x : a) (l : list a) : list a :=
match l with
| [] ⇒ [x]
| y :: l' ⇒
match cmp x y with
| Zpos _ ⇒ y :: insert cmp x l'
| _ ⇒ x :: l
end
end.
Fixpoint sort {a : Set} (cmp : a → a → int) (l : list a) : list a :=
match l with
| [] ⇒ []
| x :: l' ⇒ insert cmp x (sort cmp l')
end.
Definition stable_sort : ∀ {a : Set}, (a → a → int) → list a → list a :=
@sort.
Definition fast_sort : ∀ {a : Set}, (a → a → int) → list a → list a :=
@sort.
Definition sort_uniq : ∀ {a : Set}, (a → a → int) → list a → list a :=
@sort.
Fixpoint to_seq_node {a : Set} (l : list a) : Seq.node a :=
match l with
| [] ⇒ Seq.Nil
| x :: l' ⇒ Seq.Cons x (fun _ ⇒ to_seq_node l')
end.
Definition to_seq : ∀ {a : Set}, list a → Seq.t a :=
fun a l _ ⇒ to_seq_node l.
Fixpoint of_seq_node {a : Set} (s : Seq.node a) : list a :=
match s with
| Seq.Nil ⇒ []
| Seq.Cons x f ⇒ x :: of_seq_node (f tt)
end.
Definition of_seq : ∀ {a : Set}, Seq.t a → list a :=
fun a s ⇒ of_seq_node (s tt).
Fixpoint nat_init_ep {a : Set} (n : nat) (ff : nat → M? a) : M? (list a) :=
match n with
| 0%nat ⇒ return? []
| S k ⇒
match ff 0%nat with
| Pervasives.Ok x ⇒
let? res := nat_init_ep k (fun x ⇒ ff (S x)) in return? (x :: res)
| Pervasives.Error es ⇒
match nat_init_ep k (fun x ⇒ ff (S x)) with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition init_ep : ∀ {_error a : Set},
_error → int → (int → M? a) → M? (list a) :=
fun _error a er n ff ⇒
match n with
| Z0 ⇒ return? []
| Zpos _ ⇒ nat_init_ep (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x))
| Zneg _ ⇒ let error := Build_extensible "negative value" _ er in
Pervasives.Error [error]
end.
Fixpoint filter_ep {a : Set} (p : a → M? bool) (l : list a)
: M? (list a) :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
match p x with
| Pervasives.Ok b ⇒
let? res := filter_ep p l' in
return? (if b then (x :: res) else res)
| Pervasives.Error es ⇒
match filter_ep p l' with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint partition_ep {a : Set}
(p : a → M? bool) (l : list a) : M? (list a × list a) :=
match l with
| [] ⇒ return? ([], [])
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? '(res_left, res_right) := partition_ep p tl in
return? (
if b
then (hd :: res_left, res_right)
else (res_left, hd :: res_right)
)
| Pervasives.Error es ⇒
match partition_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint partition_map_ep {a b c : Set}
(p : a → M? (Either.t b c)) (l : list a) : M? (list b × list c) :=
match l with
| [] ⇒ return? ([], [])
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
match b with
| Either.Left b ⇒
let? '(res_left, res_right) := partition_map_ep p tl in
return? (b :: res_left, res_right)
| Either.Right c ⇒
let? '(res_left, res_right) := partition_map_ep p tl in
return? (res_left, c :: res_right)
end
| Pervasives.Error es ⇒
match partition_map_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint iter_ep {a : Set} (p : a → M? unit) (l : list a) : M? unit :=
match l with
| [] ⇒ return? tt
| hd :: tl ⇒
match p hd with
| Pervasives.Ok _ ⇒ iter_ep p tl
| Pervasives.Error es ⇒
match iter_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition iteri_ep {a : Set}
(p : int → a → M? unit) (l : list a) : M? unit :=
let fix iteri_ep_aux (index : int) (l : list a) : M? unit :=
match l with
| [] ⇒ return? tt
| hd :: tl ⇒
match p index hd with
| Pervasives.Ok _ ⇒ iteri_ep_aux (index +i 1) tl
| Pervasives.Error es ⇒
match iteri_ep_aux (index +i 1) tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end
in
iteri_ep_aux 0 l.
Fixpoint map_ep {a b : Set}
(p : a → M? b) (l : list a) : M? (list b) :=
match l with
| [] ⇒ return? []
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? res := map_ep p tl in
return? (b :: res)
| Pervasives.Error es ⇒
match map_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition mapi_ep {a b : Set}
(p : int → a → M? b) (l : list a) : M? (list b) :=
let fix mapi_ep_aux index l :=
match l with
| [] ⇒ return? []
| hd :: tl ⇒
match p index hd with
| Pervasives.Ok b ⇒
let? res := mapi_ep_aux (index +i 1) tl in
return? (b :: res)
| Pervasives.Error es ⇒
match mapi_ep_aux (index +i 1) tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end in
mapi_ep_aux 0 l.
Definition rev_map_ep {a b : Set}
(p : a → M? b) (l : list a) : M? (list b) :=
let? res := map_ep p l in
return? (List.rev res).
Definition rev_mapi_ep {a b : Set}
(p : int → a → M? b) (l : list a) : M? (list b) :=
let? res := mapi_ep p l in
return? (List.rev res).
Fixpoint filter_map_ep {a b : Set}
(p : a → M? (option b)) (l : list a) : M? (list b) :=
match l with
| [] ⇒ return? []
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒ match b with
| None ⇒ filter_map_ep p tl
| Some v ⇒
let? res := filter_map_ep p tl in
return? (v :: res)
end
| Pervasives.Error es ⇒
match filter_map_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition concat_map_ep {a b : Set}
(p : a → M? (list b)) (l : list a) : M? (list b) :=
let? res := map_ep p l in
return? (List.concat res).
Fixpoint for_all_ep {a : Set}
(p : a → M? bool) (l : list a) : M? bool :=
match l with
| [] ⇒ return? true
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? res := for_all_ep p tl in
return? (b && res)
| Pervasives.Error es ⇒
match for_all_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint exists_ep {a : Set}
(p : a → M? bool) (l : list a) : M? bool :=
match l with
| [] ⇒ return? false
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? res := exists_ep p tl in
return? (b || res)
| Pervasives.Error es ⇒
match exists_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Either.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.Seq.
Import Error_monad.Notations.
Import Pervasives.Notations.
Definition t (a : Set) : Set := list a.
Definition nil : ∀ {a : Set}, list a :=
fun _ ⇒
[].
Definition nil_e : ∀ {a trace : Set}, Pervasives.result (list a) trace :=
fun _ _ ⇒
return? [].
Definition nil_s : ∀ {a : Set}, list a :=
fun _ ⇒
[].
Definition nil_es : ∀ {a trace : Set},
Pervasives.result (list a) trace :=
fun _ _ ⇒
return? [].
Definition cons_value : ∀ {a : Set}, a → list a → list a :=
@cons.
Definition is_empty {a : Set} (l : list a) : bool :=
match l with
| [] ⇒ true
| _ :: _ ⇒ false
end.
Definition hd : ∀ {a : Set}, list a → option a :=
fun _ l ⇒
match l with
| [] ⇒ None
| x :: _ ⇒ Some x
end.
Definition tl : ∀ {a : Set}, list a → option (list a) :=
fun _ l ⇒
match l with
| [] ⇒ None
| _x :: m ⇒ Some m
end.
Fixpoint nth_z {a : Set} (l : list a) (i : Z.t) {struct l} : option a :=
match l, i with
| [], _ ⇒ None
| x :: _, 0 ⇒ Some x
| _ :: l, _ ⇒ nth_z l (i - 1)
end.
Definition nth : ∀ {a : Set}, list a → int → option a :=
@nth_z.
Definition nth_opt : ∀ {a : Set}, list a → int → option a :=
@nth_z.
Definition last : ∀ {a : Set}, a → list a → a :=
fun _ x l ⇒
List.last l x.
Fixpoint last_opt {a : Set} (l: list a) : option a :=
match l with
| [] ⇒ None
| [z] ⇒ Some z
| x :: tl ⇒ (last_opt tl)
end.
Definition find : ∀ {a : Set}, (a → bool) → list a → option a :=
fun a ⇒
List.find (A := a).
Definition find_opt : ∀ {a : Set}, (a → bool) → list a → option a :=
fun _ ⇒
find.
Fixpoint find_map {a b : Set} (f : a → option b) (l : list a) : option b :=
match l with
| [] ⇒ None
| x :: l' ⇒
match f x with
| Some y ⇒ f x
| None ⇒ find_map f l'
end
end.
Fixpoint mem {a : Set} (eq_dec : a → a → bool) (v : a) (l : list a) : bool :=
match l with
| [] ⇒ false
| x :: l ⇒ eq_dec v x || mem eq_dec v l
end.
Fixpoint assoc {a b : Set}
(eq : a → a → bool)
(k : a)
(l : list (a × b))
: option b :=
match l with
| [] ⇒ None
| (h, x) :: tl ⇒ if eq k h then Some x else assoc eq k tl
end.
Definition assoc_opt : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → option b :=
fun _ _ ⇒ assoc.
(* not definable without decidable equality *)
Parameter assq : ∀ {a b : Set}, a → list (a × b) → option b.
(* not definable without decidable equality *)
Parameter assq_opt : ∀ {a b : Set}, a → list (a × b) → option b.
Fixpoint mem_assoc {a b : Set}
(eq : a → a → bool)
(k : a)
(l : list (a × b))
: bool :=
match l with
| [] ⇒ false
| (h, x) :: tl ⇒ eq k h || mem_assoc eq k tl
end.
(* not definable without decidable equality *)
Parameter mem_assq : ∀ {a b : Set}, a → list (a × b) → bool.
Fixpoint remove_assoc {a b : Set}
(eq : a → a → bool)
(k : a)
(l : list (a × b))
: list (a × b) :=
match l with
| [] ⇒ []
| (h, x) :: tl ⇒
if eq k h then
tl
else
(h, x) :: remove_assoc eq k tl
end.
(* not definable without decidable equality *)
Parameter remove_assq : ∀ {a b : Set}, a → list (a × b) → list (a × b).
Fixpoint nat_init {a trace : Set} (er : trace) (n : nat) (ff : nat → a)
: list a :=
match n with
| 0%nat ⇒ []
| S k ⇒ ff 0%nat :: nat_init er k (fun v ⇒ ff (S v))
end.
Definition init_value {a trace : Set}
(er : trace) (n : int) (ff : int → a)
: Pervasives.result (list a) trace :=
match n with
| Zneg _ ⇒ Pervasives.Error er
| Z0 ⇒ Pervasives.Ok []
| Zpos x ⇒
Pervasives.Ok (nat_init er (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x)))
end.
Fixpoint length {a : Set} (l : list a) : int :=
match l with
| [] ⇒ 0
| _ :: l ⇒ (length l) +i 1
end.
Definition rev {a : Set} (l : list a) : list a :=
Lists.List.rev' l.
Definition concat : ∀ {a : Set}, list (list a) → list a :=
fun _ ⇒
List.concat.
Definition append : ∀ {a : Set}, list a → list a → list a :=
fun _ ⇒
List.append.
Definition rev_append : ∀ {a : Set}, list a → list a → list a :=
fun _ ⇒
List.rev_append.
Definition flatten : ∀ {a : Set}, list (list a) → list a :=
fun _ ⇒
List.concat.
Fixpoint combine_aux {a b : Set}
(list1 : list a)
(list2 :list b)
(partial : list (a × b))
: option (list (a × b)) :=
match list1, list2 with
| [], _ :: _ | _ :: _, [] ⇒ None
| [], [] ⇒ Some partial
| h1 :: tl1 , h2 :: tl2 ⇒ combine_aux tl1 tl2 ((h1, h2) :: partial)
end.
Definition combine {a b trace : Set} (er : trace)
(l1 : list a) (l2 : list b)
: Pervasives.result (list (a × b)) trace :=
match combine_aux l1 l2 [] with
| Some x ⇒ Pervasives.Ok x
| None ⇒ Pervasives.Error er
end.
Definition rev_combine {a b trace : Set} (er : trace)
(l1 : list a) (l2 : list b)
: Pervasives.result (list (a × b)) trace :=
match combine_aux l1 l2 [] with
| Some x ⇒ Pervasives.Ok (rev x)
| None ⇒ Pervasives.Error er
end.
Definition split : ∀ {a b : Set}, list (a × b) → list a × list b :=
fun _ _ ⇒
List.split.
Fixpoint iter2 {a b trace : Set} (er : trace)
(f : a → b → unit) (l1 : list a) (l2 : list b)
: Pervasives.result unit trace :=
match l1,l2 with
| [], [] ⇒ Pervasives.Ok tt
| _ :: l1', _ :: l2' ⇒ iter2 er f l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Fixpoint map2 {a b c trace : Set} (er : trace)
(f : a → b → c) (l1 : list a) (l2 : list b)
: Pervasives.result (list c) trace :=
match l1, l2 with
| [], [] ⇒ Pervasives.Ok []
| x :: l1', y :: l2' ⇒
match map2 er f l1' l2' with
| Pervasives.Ok l3 ⇒ Pervasives.Ok (f x y :: l3)
| Pervasives.Error e ⇒ Pervasives.Error e
end
| _, _ ⇒ Pervasives.Error er
end.
Definition rev_map2 : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace :=
fun a b c trace er f l1 l2 ⇒
match map2 er f l1 l2 with
| Pervasives.Ok l3 ⇒ Pervasives.Ok (List.rev l3)
| Pervasives.Error _ as e ⇒ e
end.
Fixpoint fold_left2 {a b c trace : Set} (er : trace)
(f : a → b → c → a) (acc : a) (l1 : list b) (l2 : list c)
: Pervasives.result a trace :=
match l1, l2 with
| [], [] ⇒ Pervasives.Ok acc
| x :: l1', y :: l2' ⇒ fold_left2 er f (f acc x y) l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Fixpoint fold_right2 {a b c trace : Set} (er : trace)
(f : a → b → c → c) (l1 : list a) (l2 : list b) (acc : c)
: Pervasives.result c trace :=
match l1, l2 with
| [], [] ⇒ Pervasives.Ok acc
| x :: l1', y :: l2' ⇒
match fold_right2 er f l1' l2' acc with
| Pervasives.Ok acc' ⇒ Pervasives.Ok (f x y acc')
| Pervasives.Error _ as e ⇒ e
end
| _, _ ⇒ Pervasives.Error er
end.
Definition for_all2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
fun a b trace er p l1 l2 ⇒ fold_left2 er
(fun acc x y ⇒ acc && p x y) true l1 l2.
Definition _exists2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
fun a b trace er p l1 l2 ⇒ fold_left2 er
(fun acc x y ⇒ acc || p x y) false l1 l2.
Fixpoint nat_init_e {a trace : Set} (er : trace) (n : nat)
(ff : nat → Pervasives.result a trace)
: Pervasives.result (list a) trace :=
match n with
| 0%nat ⇒ Pervasives.Ok []
| S k ⇒
match ff 0%nat with
| Pervasives.Error e ⇒ Pervasives.Error e
| Pervasives.Ok x ⇒
match nat_init_e er k (fun v ⇒ ff (S v)) with
| Pervasives.Error _ as e ⇒ e
| Pervasives.Ok l ⇒ Pervasives.Ok (x :: l)
end
end
end.
Definition init_e : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace :=
fun a trace er n ff ⇒
match n with
| Zneg _ ⇒ Pervasives.Error er
| Z0 ⇒ Pervasives.Ok []
| Zpos _ ⇒ nat_init_e er (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x))
end.
Definition init_s : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace :=
@init_value.
Definition init_es : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace :=
@init_e.
Definition init_p : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace :=
@init_value.
Fixpoint find_e {a trace : Set}
(ep : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (option a) trace :=
match l with
| [] ⇒ Pervasives.Ok None
| x :: l' ⇒
match ep x with
| Pervasives.Error e ⇒ Pervasives.Error e
| Pervasives.Ok true ⇒ Pervasives.Ok (Some x)
| Pervasives.Ok false ⇒ find_e ep l'
end
end.
Definition find_s : ∀ {a : Set},
(a → bool) → list a → option a :=
@find.
Definition find_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (option a) trace :=
@find_e.
Fixpoint find_map_e {a b trace : Set}
(f : a → Pervasives.result (option b) trace) (l : list a)
: Pervasives.result (option b) trace :=
match l with
| [] ⇒ Pervasives.Ok None
| x :: l' ⇒
match f x with
| Pervasives.Error _ as e ⇒ e
| Pervasives.Ok (Some _) as res ⇒ res
| Pervasives.Ok None ⇒ find_map_e f l'
end
end.
Definition find_map_s : ∀ {a b : Set},
(a → option b) → list a → option b :=
@find_map.
Definition find_map_es : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (option b) trace :=
@find_map_e.
Definition filter : ∀ {a : Set}, (a → bool) → list a → list a :=
fun _ ⇒
List.filter.
Fixpoint filteri_aux {a : Set} (i : int) (p : int → a → bool) (l : list a)
: list a :=
match l with
| [] ⇒ []
| x :: l' ⇒ if p i x
then x :: filteri_aux (i+1)%Z p l'
else filteri_aux (i+1)%Z p l'
end.
Definition filteri : ∀ {a : Set}, (int → a → bool) → list a → list a :=
fun a ⇒ @filteri_aux a 0.
Definition find_all : ∀ {a : Set}, (a → bool) → list a → list a :=
@filter.
Definition rev_filter : ∀ {a : Set}, (a → bool) → list a → list a :=
fun a p l ⇒ List.rev (filter p l).
Definition rev_filteri : ∀ {a : Set},
(int → a → bool) → list a → list a :=
fun a p l ⇒ List.rev (filteri p l).
Fixpoint filter_some {a : Set} (l : list (option a)) : list a :=
match l with
| [] ⇒ []
| None :: l' ⇒ filter_some l'
| Some x :: l' ⇒ x :: filter_some l'
end.
Definition rev_filter_some : ∀ {a : Set}, list (option a) → list a :=
fun a l ⇒ List.rev (filter_some l).
Fixpoint filter_ok {a b : Set} (l : list (Pervasives.result a b)) : list a :=
match l with
| [] ⇒ []
| Pervasives.Error _ :: l' ⇒ filter_ok l'
| Pervasives.Ok x :: l' ⇒ x :: filter_ok l'
end.
Definition rev_filter_ok : ∀ {a b : Set},
list (Pervasives.result a b) → list a :=
fun a b l ⇒ List.rev (filter_ok l).
Fixpoint filter_error {a b : Set} (l : list (Pervasives.result a b)) : list b :=
match l with
| [] ⇒ []
| Pervasives.Ok _ :: l' ⇒ filter_error l'
| Pervasives.Error e :: l' ⇒ e :: filter_error l'
end.
Definition rev_filter_error : ∀ {a b : Set},
list (Pervasives.result a b) → list b :=
fun a b l ⇒ List.rev (filter_error l).
Fixpoint filter_left {a b : Set} (l : list (Either.t a b)) : list a :=
match l with
| [] ⇒ []
| Either.Left x :: l' ⇒ x :: filter_left l'
| Either.Right _ :: l' ⇒ filter_left l'
end.
Definition rev_filter_left : ∀ {a b : Set}, list (Either.t a b) → list a :=
fun a b l ⇒ List.rev (filter_left l).
Fixpoint filter_right {a b : Set} (l : list (Either.t a b)) : list b :=
match l with
| [] ⇒ []
| Either.Right x :: l' ⇒ x :: filter_right l'
| Either.Left _ :: l' ⇒ filter_right l'
end.
Definition rev_filter_right : ∀ {a b : Set},
list (Either.t a b) → list b :=
fun a b l ⇒ List.rev (filter_right l).
Fixpoint filter_e {a trace : Set}
(f : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? b := f x in
let? l := filter_e f l in
if b then
return? (x :: l)
else
return? l
end.
Definition rev_filter_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
fun a trace f l ⇒
let? l' := filter_e f l in
return? List.rev l'.
Fixpoint filter_s {a : Set}
(f : a → bool) (l : list a) : list a :=
match l with
| [] ⇒ []
| x :: l ⇒
let b := f x in
let l := filter_s f l in
if b then
x :: l
else
l
end.
Definition rev_filter_s : ∀ {a : Set},
(a → bool) → list a → list a :=
fun a p l ⇒
List.rev (filter_s p l).
Definition rev_filter_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
@rev_filter_e.
Fixpoint filter_es {a trace : Set}
(f : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? b := f x in
let? l := filter_es f l in
if b then
return? (x :: l)
else
return? l
end.
Fixpoint filteri_e_aux {a trace : Set} (i : int)
(p : int → a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a) trace :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
let? b := p i x in
let? res := filteri_e_aux (i + 1)%Z p l' in
return? (if b then x :: res else res)
end.
Definition filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
fun a trace ⇒ @filteri_e_aux a trace 0.
Definition rev_filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
fun a trace p l ⇒
let? res := filteri_e p l in
return? List.rev res.
Definition rev_filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a :=
@rev_filteri.
Definition filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a :=
@filteri.
Definition rev_filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
@rev_filteri_e.
Definition filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace :=
@filteri_e.
Definition filter_p : ∀ {a : Set},
(a → bool) → list a → list a :=
@filter.
Definition partition : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
fun _ ⇒
List.partition.
Definition rev_partition : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
fun a p l ⇒ partition p (List.rev l).
Fixpoint partition_map {a b c : Set}
(f : a → Either.t b c) (l : list a)
: list b × list c :=
match l with
| [] ⇒ ([], [])
| x :: l' ⇒
let '(l1, l2) := partition_map f l' in
match f x with
| Either.Left y ⇒ (y :: l1, l2)
| Either.Right y ⇒ (l1, y :: l2)
end
end.
Definition rev_partition_map : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c :=
fun a b c f l ⇒
partition_map f (List.rev l).
Fixpoint partition_result {a b : Set}
(l : list (Pervasives.result a b)) : list a × list b :=
match l with
| [] ⇒ ([], [])
| x :: l' ⇒
let '(l1, l2) := partition_result l' in
match x with
| Pervasives.Ok x ⇒ (x :: l1, l2)
| Pervasives.Error e ⇒ (l1, e :: l2)
end
end.
Definition rev_partition_result : ∀ {a b : Set},
list (Pervasives.result a b) → list a × list b :=
fun a b l ⇒ partition_result (List.rev l).
Fixpoint partition_either {a b : Set}
(l : list (Either.t a b)) : list a × list b :=
match l with
| [] ⇒ ([], [])
| x :: l' ⇒
let '(l1, l2) := partition_either l' in
match x with
| Either.Left y ⇒ (y :: l1, l2)
| Either.Right y ⇒ (l1, y :: l2)
end
end.
Definition rev_partition_either : ∀ {a b : Set},
list (Either.t a b) → list a × list b :=
fun a b l ⇒ partition_either (List.rev l).
Fixpoint partition_e {a trace : Set}
(p : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result (list a × list a) trace :=
match l with
| [] ⇒ return? ([], [])
| x :: l' ⇒
let? b := p x in
let? '(l1, l2) := partition_e p l' in
return? (if b then (x :: l1, l2) else (l1, x :: l2))
end.
Definition rev_partition_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace :=
fun a trace p l ⇒ partition_e p (List.rev l).
Definition rev_partition_s : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
@rev_partition.
Fixpoint partition_s {a : Set}
(f : a → bool) (l : list a) : list a × list a :=
match l with
| [] ⇒ ([], [])
| x :: l ⇒
let b := f x in
let '(yes, no) := partition_s f l in
if b then
(x :: yes, no)
else
(yes, x :: no)
end.
Definition rev_partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace :=
@rev_partition_e.
Definition partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace :=
@partition_e.
Definition partition_p : ∀ {a : Set},
(a → bool) → list a → list a × list a :=
@partition.
Fixpoint partition_map_e {a b c trace : Set}
(f : a → Pervasives.result (Either.t b c) trace) (l : list a) :
Pervasives.result (list b × list c) trace :=
match l with
| [] ⇒ return? ([], [])
| x :: l' ⇒
let? e := f x in
let? '(l1, l2) := partition_map_e f l' in
match e with
| Either.Left y ⇒ return? (y :: l1, l2)
| Either.Right y ⇒ return? (l1, y :: l2)
end
end.
Definition rev_partition_map_e : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace :=
fun a b c trace f l ⇒ partition_map_e f (List.rev l).
Definition rev_partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c :=
@rev_partition_map.
Definition partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c :=
@partition_map.
Definition rev_partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace :=
@rev_partition_map_e.
Definition partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace :=
@partition_map_e.
Definition iter : ∀ {a : Set},
(a → unit) → list a → unit :=
fun a f l ⇒ tt.
Fixpoint iter_e {a trace : Set}
(f : a → Pervasives.result unit trace) (l : list a)
: Pervasives.result unit trace :=
match l with
| [] ⇒ return? tt
| x :: l ⇒
let? _ := f x in
iter_e f l
end.
Fixpoint iter_s {a : Set}
(f : a → unit) (l : list a) : unit :=
match l with
| [] ⇒ tt
| x :: l ⇒
let _ := f x in
iter_s f l
end.
Fixpoint iter_es {a trace : Set}
(f : a → Pervasives.result unit trace) (l : list a)
: Pervasives.result unit trace :=
match l with
| [] ⇒ return? tt
| x :: l ⇒
let? _ := f x in
iter_es f l
end.
Definition iter_p : ∀ {a : Set}, (a → unit) → list a → unit :=
@iter.
Definition iteri : ∀ {a : Set}, (int → a → unit) → list a → unit :=
fun a f l ⇒ tt.
Fixpoint iteri_e_aux {a trace : Set} (i : int)
(f : int → a → Pervasives.result unit trace) (l : list a)
: Pervasives.result unit trace :=
match l with
| [] ⇒ return? tt
| x :: l' ⇒
let? _ := f i x in
iteri_e_aux (i + 1)%Z f l'
end.
Definition iteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace :=
fun a trace ⇒ @iteri_e_aux a trace 0.
Definition iteri_s : ∀ {a : Set},
(int → a → unit) → list a → unit :=
@iteri.
Definition iteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace :=
@iteri_e.
Definition iteri_p : ∀ {a : Set},
(int → a → unit) → list a → unit :=
@iteri.
Definition map : ∀ {a b : Set}, (a → b) → list a → list b :=
@Lists.List.map.
Fixpoint map_e {a b trace : Set}
(f : a → Pervasives.result b trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? y := f x in
let? l' := map_e f l in
return? (y :: l')
end.
Fixpoint map_s {a b : Set}
(f : a → b) (l : list a) : list b :=
match l with
| [] ⇒ []
| x :: l ⇒
let x := f x in
let l := map_s f l in
x :: l
end.
Fixpoint map_es {a b trace : Set}
(f : a → Pervasives.result b trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? y := f x in
let? l' := map_es f l in
return? (y :: l')
end.
Definition map_p : ∀ {a b : Set},
(a → b) → list a → list b :=
@map.
Definition mapi : ∀ {a b : Set}, (int → a → b) → list a → list b :=
fun _ _ ⇒
List.mapi.
Fixpoint mapi_e_aux {a b trace : Set} (i : int)
(f : int → a → Pervasives.result b trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
let? y := f i x in
let? res := mapi_e_aux (i+1)%Z f l' in
return? (y :: res)
end.
Definition mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace ⇒ @mapi_e_aux a b trace 0.
Definition mapi_s : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@mapi.
Definition mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
@mapi_e.
Definition mapi_p : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@mapi.
Definition rev_map : ∀ {a b : Set}, (a → b) → list a → list b :=
fun _ _ ⇒
List.rev_map.
Definition rev_mapi : ∀ {a b : Set}, (int → a → b) → list a → list b :=
fun a b f l ⇒ List.rev (mapi f l).
Definition rev_map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace f l ⇒
let? res := map_e f l in
return? (List.rev res).
Definition rev_map_s : ∀ {a b : Set},
(a → b) → list a → list b :=
@rev_map.
Definition rev_map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
@rev_map_e.
Definition rev_map_p : ∀ {a b : Set},
(a → b) → list a → list b :=
@rev_map.
Definition rev_mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace f l ⇒
let? res := mapi_e f l in
return? List.rev res.
Definition rev_mapi_s : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@rev_mapi.
Definition rev_mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace :=
@rev_mapi_e.
Definition rev_mapi_p : ∀ {a b : Set},
(int → a → b) → list a → list b :=
@rev_mapi.
Fixpoint filter_map {a b : Set} (f : a → option b) (l : list a) : list b :=
match l with
| [] ⇒ []
| x :: l' ⇒
match f x with
| None ⇒ filter_map f l'
| Some y ⇒ y :: filter_map f l'
end
end.
Definition rev_filter_map : ∀ {a b : Set},
(a → option b) → list a → list b :=
fun a b f l ⇒ List.rev (filter_map f l).
Fixpoint filter_map_e {a b trace : Set}
(f : a → Pervasives.result (option b) trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
let? y := f x in
match y with
| None ⇒ filter_map_e f l'
| Some z ⇒ let? res := filter_map_e f l' in return? (z :: res)
end
end.
Definition rev_filter_map_e : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (list b) trace :=
fun a b trace f l ⇒ filter_map_e f (List.rev l).
Definition rev_filter_map_s : ∀ {a b : Set},
(a → option b) → list a → list b :=
@rev_filter_map.
Fixpoint filter_map_s {a b : Set}
(f : a → option b) (l : list a) : list b :=
match l with
| [] ⇒ []
| x :: l ⇒
let y := f x in
let l' := filter_map_s f l in
match y with
| Some y ⇒ y :: l'
| None ⇒ l'
end
end.
Definition rev_filter_map_es : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (list b) trace :=
@rev_filter_map_e.
Fixpoint filter_map_es {a b trace : Set}
(f : a → Pervasives.result (option b) trace) (l : list a)
: Pervasives.result (list b) trace :=
match l with
| [] ⇒ return? []
| x :: l ⇒
let? y := f x in
let? l' := filter_map_es f l in
match y with
| Some y ⇒ return? (y :: l')
| None ⇒ return? l'
end
end.
Definition filter_map_p : ∀ {a b : Set},
(a → option b) → list a → list b :=
@filter_map.
Definition concat_map : ∀ {a b : Set}, (a → list b) → list a → list b :=
fun a b f l ⇒ List.concat (List.map f l).
Definition concat_map_s : ∀ {a b : Set},
(a → list b) → list a → list b :=
@concat_map.
Definition concat_map_e : ∀ {_error a b : Set},
(a → Pervasives.result (list b) _error) → list a →
Pervasives.result (list b) _error :=
fun _error a b f l ⇒
let? ls := map_e f l in
return? concat ls.
Definition concat_map_es : ∀ {_error a b : Set},
(a → Pervasives.result (list b) _error) → list a →
Pervasives.result (list b) _error :=
@concat_map_e.
Definition concat_map_p : ∀ {a b : Set},
(a → list b) → list a → list b :=
@concat_map.
Definition fold_left {a b : Set} (f : a → b → a) (acc : a) (l : list b) : a :=
Lists.List.fold_left f l acc.
Definition fold_left_e {a b trace : Set}
(f : a → b → Pervasives.result a trace) (acc : a) (l : list b) :
Pervasives.result a trace :=
fold_left (fun acc item ⇒ let? acc := acc in f acc item) (return? acc) l.
Definition fold_left_s : ∀ {a b : Set},
(a → b → a) → a → list b → a :=
fun _ _ ⇒
fold_left.
Definition fold_left_es : ∀ {a b trace : Set},
(a → b → Pervasives.result a trace) → a → list b →
Pervasives.result a trace :=
fun _ _ _ ⇒
fold_left_e.
Fixpoint fold_left_map {a b c : Set} (f : a → b → a × c)
(acc : a) (l : list b) : a × list c :=
match l with
| [] ⇒ (acc, [])
| x :: l' ⇒
let '(acc1, y) := f acc x in
let '(acc2, res) := fold_left_map f acc1 l' in (acc2, y :: res)
end.
Fixpoint fold_left_map_e {a b c trace : Set}
(f : a → b → Pervasives.result (a × c) trace) (acc : a) (l : list b) :
Pervasives.result (a × list c) trace :=
match l with
| [] ⇒ return? (acc, [])
| x :: l' ⇒
let? '(acc1, y) := f acc x in
let? '(acc2, res) := fold_left_map_e f acc1 l' in
return? (acc2, y :: res)
end.
Definition fold_left_map_s : ∀ {a b c : Set},
(a → b → a × c) → a → list b → a × list c :=
@fold_left_map.
Definition fold_left_map_es : ∀ {a b c trace : Set},
(a → b → Pervasives.result (a × c) trace) → a → list b →
Pervasives.result (a × list c) trace :=
@fold_left_map_e.
Definition fold_left_i {a b : Set}
(f : int → a → b → a) (acc : a) (l : list b) : a :=
snd (
fold_left
(fun '(index, acc) item ⇒
let acc := f index acc item in
(index +i 1, acc)
)
(0, acc)
l
).
Definition fold_left_i_e {a b trace : Set}
(f : int → a → b → Pervasives.result a trace) (acc : a) (l : list b) :
Pervasives.result a trace :=
fold_left_i
(fun index acc item ⇒ let? acc := acc in f index acc item)
(return? acc)
l.
Definition fold_left_i_s := @fold_left_i.
Arguments fold_left_i_s {a b}.
Definition fold_left_i_es := @fold_left_i_e.
Arguments fold_left_i_es {a b trace}.
Definition fold_right : ∀ {a b : Set}, (a → b → b) → list a → b → b :=
fun _ _ ⇒
List.fold_right.
Fixpoint fold_right_e {a b trace : Set}
(f : a → b → Pervasives.result b trace) (l : list a) (acc : b) :
Pervasives.result b trace :=
match l with
| [] ⇒ return? acc
| x :: l' ⇒
let? acc' := fold_right_e f l' acc in
f x acc'
end.
Fixpoint fold_right_s {a b : Set}
(f : a → b → b) (l : list a) (accumulator : b) : b :=
match l with
| [] ⇒ accumulator
| x :: l ⇒
let accumulator := fold_right_s f l accumulator in
f x accumulator
end.
Fixpoint fold_right_es {a b trace : Set}
(f : a → b → Pervasives.result b trace) (l : list a)
(accumulator : b) : Pervasives.result b trace :=
match l with
| [] ⇒ return? accumulator
| x :: l ⇒
let? accumulator := fold_right_es f l accumulator in
f x accumulator
end.
Fixpoint iter2_e {a b trace : Set} (er : trace)
(f : a → b → Pervasives.result unit trace) (l1 : list a) (l2 : list b)
: Pervasives.result unit trace :=
match l1, l2 with
| [], [] ⇒ return? tt
| x :: l1', y :: l2' ⇒
let? _ := f x y in iter2_e er f l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Definition iter2_s : ∀ {a b trace : Set},
trace → (a → b → unit) → list a → list b →
Pervasives.result unit trace :=
@iter2.
Definition iter2_es : ∀ {a b trace : Set},
trace → (a → b → Pervasives.result unit trace) → list a →
list b → Pervasives.result unit trace :=
@iter2_e.
Fixpoint map2_e {a b c trace : Set} (er : trace)
(f : a → b → Pervasives.result c trace) (l1 : list a) (l2 : list b) :
Pervasives.result (list c) trace :=
match l1, l2 with
| [], [] ⇒ return? []
| x :: l1', y :: l2' ⇒
let? z := f x y in
let? res := map2_e er f l1' l2' in return? (z :: res)
| _, _ ⇒ Pervasives.Error er
end.
Definition map2_s : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace :=
@map2.
Definition map2_es : ∀ {a b c trace : Set},
trace → (a → b → Pervasives.result c trace) → list a →
list b → Pervasives.result (list c) trace :=
@map2_e.
Definition rev_map2_e : ∀ {a b c trace : Set},
trace → (a → b → Pervasives.result c trace) → list a → list b →
Pervasives.result (list c) trace :=
fun a b c trace er f l1 l2 ⇒
let? res := map2_e er f l1 l2 in return? List.rev res.
Definition rev_map2_s : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace :=
@rev_map2.
Definition rev_map2_es : ∀ {a b c trace : Set},
trace → (a → b → Pervasives.result c trace) → list a →
list b → Pervasives.result (list c) trace :=
@rev_map2_e.
Fixpoint fold_left2_e {a b c trace : Set} (er : trace)
(f : a → b → c → Pervasives.result a trace) (acc : a) (l1 : list b) (l2 : list c)
: Pervasives.result a trace :=
match l1, l2 with
| [], [] ⇒ return? acc
| x :: l1', y :: l2' ⇒
let? acc' := f acc x y in
fold_left2_e er f acc' l1' l2'
| _, _ ⇒ Pervasives.Error er
end.
Definition fold_left2_s : ∀ {a b c trace : Set},
trace → (a → b → c → a) → a → list b → list c →
Pervasives.result a trace :=
@fold_left2.
Definition fold_left2_es : ∀ {a b c trace : Set},
trace → (a → b → c → Pervasives.result a trace) → a →
list b → list c → Pervasives.result a trace :=
@fold_left2_e.
Fixpoint fold_right2_e {a b c trace : Set} (er : trace)
(f : a → b → c → Pervasives.result c trace) (l1 : list a) (l2 : list b) (acc : c)
: Pervasives.result c trace :=
match l1, l2 with
| [], [] ⇒ return? acc
| x :: l1', y :: l2' ⇒
let? acc' := fold_right2_e er f l1' l2' acc in
f x y acc'
| _, _ ⇒ Pervasives.Error er
end.
Definition fold_right2_s : ∀ {a b c trace : Set},
trace → (a → b → c → c) → list a → list b → c →
Pervasives.result c trace :=
@fold_right2.
Definition fold_right2_es : ∀ {a b c trace : Set},
trace → (a → b → c → Pervasives.result c trace) → list a →
list b → c → Pervasives.result c trace :=
@fold_right2_e.
Definition for_all : ∀ {a : Set}, (a → bool) → list a → bool :=
fun a ⇒
List.forallb (A := a).
(* intended semantics? *)
Fixpoint for_all_e {a trace : Set}
(p : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result bool trace :=
match l with
| [] ⇒ return? true
| x :: l' ⇒
let? b := p x in
let? res := for_all_e p l' in
return? (b && res)
end.
Fixpoint for_all_s {a : Set}
(f : a → bool) (l : list a) : bool :=
match l with
| [] ⇒ true
| x :: l ⇒
let b := f x in
if b then
for_all_s f l
else
false
end.
Definition for_all_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result bool trace :=
@for_all_e.
Definition for_all_p : ∀ {a : Set},
(a → bool) → list a → bool :=
@for_all.
Definition _exists : ∀ {a : Set}, (a → bool) → list a → bool :=
fun a ⇒
List.existsb (A := a).
Fixpoint exists_e {a trace : Set}
(p : a → Pervasives.result bool trace) (l : list a)
: Pervasives.result bool trace :=
match l with
| [] ⇒ return? false
| x :: l' ⇒
let? b := p x in
let? res := exists_e p l' in
return? (b || res)
end.
Fixpoint exists_s {a : Set}
(f : a → bool) (l : list a) : bool :=
match l with
| [] ⇒ false
| x :: l ⇒
let b := f x in
if b then
true
else
exists_s f l
end.
Definition exists_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result bool trace :=
@exists_e.
Definition exists_p : ∀ {a : Set},
(a → bool) → list a → bool :=
@_exists.
Fixpoint for_all2_e {a b trace : Set} (er : trace)
(f : a → b → Pervasives.result bool trace) (l1 : list a) (l2 : list b)
: Pervasives.result bool trace :=
match l1, l2 with
| [], [] ⇒ return? true
| x :: l1', y :: l2' ⇒
let? b := f x y in
let? res := for_all2_e er f l1' l2' in
return? (b && res)
| _, _ ⇒ Pervasives.Error er
end.
Definition for_all2_s : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
@for_all2.
Definition for_all2_es : ∀ {a b trace : Set},
trace → (a → b → Pervasives.result bool trace) → list a →
list b → Pervasives.result bool trace :=
@for_all2_e.
Fixpoint exists2_e {a b trace : Set} (er : trace)
(f : a → b → Pervasives.result bool trace) (l1 : list a) (l2 : list b)
: Pervasives.result bool trace :=
match l1, l2 with
| [], [] ⇒ return? false
| x :: l1', y :: l2' ⇒
let? b := f x y in
let? res := exists2_e er f l1' l2' in
return? (b || res)
| _, _ ⇒ Pervasives.Error er
end.
Definition exists2_s : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace :=
@_exists2.
Definition exists2_es : ∀ {a b trace : Set},
trace → (a → b → Pervasives.result bool trace) → list a →
list b → Pervasives.result bool trace :=
@exists2_e.
Fixpoint combine_drop {a b : Set} (l1 : list a) (l2 : list b) : list (a × b) :=
match l1, l2 with
| [], _ ⇒ []
| _, [] ⇒ []
| x :: l1', y :: l2' ⇒ (x, y) :: combine_drop l1' l2'
end.
Fixpoint combine_with_leftovers {a b : Set} (l1 : list a) (l2 : list b)
: list (a × b) × option (Either.t (list a) (list b)) :=
match l1, l2 with
| [], [] ⇒ ([], None)
| [], _ ⇒ ([], Some (Either.Right l2))
| _, [] ⇒ ([], Some (Either.Left l1))
| x :: l1', y :: l2' ⇒
let '(combine, leftovers) := combine_with_leftovers l1' l2' in
((x, y) :: combine, leftovers)
end.
Parameter product : ∀ {a b : Set}, list a → list b → list (a × b).
Fixpoint compare {a : Set} (cmp : a → a → int) (l1 l2 : list a)
: int :=
match l1, l2 with
| [], [] ⇒ 0
| [], _ ⇒ -1
| _, [] ⇒ 1
| x :: l1', y :: l2' ⇒
match cmp x y with
| Z0 ⇒ compare cmp l1' l2'
| Zpos _ ⇒ 1
| Zneg _ ⇒ -1
end
end.
Definition compare_lengths : ∀ {a b : Set}, list a → list b → int :=
fun _ _ l1 l2 ⇒
(length l1) -i (length l2).
Definition compare_length_with : ∀ {a : Set}, list a → int → int :=
fun _ l n ⇒
length l -i n.
Fixpoint equal {a : Set} (eqb : a → a → bool) (l1 l2 : list a) : bool :=
match l1, l2 with
| [], [] ⇒ true
| x1 :: l1, x2 :: l2 ⇒ eqb x1 x2 && equal eqb l1 l2
| _, _ ⇒ false
end.
(* inserts new val just before first value greater than it *)
Fixpoint insert {a : Set} (cmp : a → a → int) (x : a) (l : list a) : list a :=
match l with
| [] ⇒ [x]
| y :: l' ⇒
match cmp x y with
| Zpos _ ⇒ y :: insert cmp x l'
| _ ⇒ x :: l
end
end.
Fixpoint sort {a : Set} (cmp : a → a → int) (l : list a) : list a :=
match l with
| [] ⇒ []
| x :: l' ⇒ insert cmp x (sort cmp l')
end.
Definition stable_sort : ∀ {a : Set}, (a → a → int) → list a → list a :=
@sort.
Definition fast_sort : ∀ {a : Set}, (a → a → int) → list a → list a :=
@sort.
Definition sort_uniq : ∀ {a : Set}, (a → a → int) → list a → list a :=
@sort.
Fixpoint to_seq_node {a : Set} (l : list a) : Seq.node a :=
match l with
| [] ⇒ Seq.Nil
| x :: l' ⇒ Seq.Cons x (fun _ ⇒ to_seq_node l')
end.
Definition to_seq : ∀ {a : Set}, list a → Seq.t a :=
fun a l _ ⇒ to_seq_node l.
Fixpoint of_seq_node {a : Set} (s : Seq.node a) : list a :=
match s with
| Seq.Nil ⇒ []
| Seq.Cons x f ⇒ x :: of_seq_node (f tt)
end.
Definition of_seq : ∀ {a : Set}, Seq.t a → list a :=
fun a s ⇒ of_seq_node (s tt).
Fixpoint nat_init_ep {a : Set} (n : nat) (ff : nat → M? a) : M? (list a) :=
match n with
| 0%nat ⇒ return? []
| S k ⇒
match ff 0%nat with
| Pervasives.Ok x ⇒
let? res := nat_init_ep k (fun x ⇒ ff (S x)) in return? (x :: res)
| Pervasives.Error es ⇒
match nat_init_ep k (fun x ⇒ ff (S x)) with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition init_ep : ∀ {_error a : Set},
_error → int → (int → M? a) → M? (list a) :=
fun _error a er n ff ⇒
match n with
| Z0 ⇒ return? []
| Zpos _ ⇒ nat_init_ep (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x))
| Zneg _ ⇒ let error := Build_extensible "negative value" _ er in
Pervasives.Error [error]
end.
Fixpoint filter_ep {a : Set} (p : a → M? bool) (l : list a)
: M? (list a) :=
match l with
| [] ⇒ return? []
| x :: l' ⇒
match p x with
| Pervasives.Ok b ⇒
let? res := filter_ep p l' in
return? (if b then (x :: res) else res)
| Pervasives.Error es ⇒
match filter_ep p l' with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint partition_ep {a : Set}
(p : a → M? bool) (l : list a) : M? (list a × list a) :=
match l with
| [] ⇒ return? ([], [])
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? '(res_left, res_right) := partition_ep p tl in
return? (
if b
then (hd :: res_left, res_right)
else (res_left, hd :: res_right)
)
| Pervasives.Error es ⇒
match partition_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint partition_map_ep {a b c : Set}
(p : a → M? (Either.t b c)) (l : list a) : M? (list b × list c) :=
match l with
| [] ⇒ return? ([], [])
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
match b with
| Either.Left b ⇒
let? '(res_left, res_right) := partition_map_ep p tl in
return? (b :: res_left, res_right)
| Either.Right c ⇒
let? '(res_left, res_right) := partition_map_ep p tl in
return? (res_left, c :: res_right)
end
| Pervasives.Error es ⇒
match partition_map_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint iter_ep {a : Set} (p : a → M? unit) (l : list a) : M? unit :=
match l with
| [] ⇒ return? tt
| hd :: tl ⇒
match p hd with
| Pervasives.Ok _ ⇒ iter_ep p tl
| Pervasives.Error es ⇒
match iter_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition iteri_ep {a : Set}
(p : int → a → M? unit) (l : list a) : M? unit :=
let fix iteri_ep_aux (index : int) (l : list a) : M? unit :=
match l with
| [] ⇒ return? tt
| hd :: tl ⇒
match p index hd with
| Pervasives.Ok _ ⇒ iteri_ep_aux (index +i 1) tl
| Pervasives.Error es ⇒
match iteri_ep_aux (index +i 1) tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end
in
iteri_ep_aux 0 l.
Fixpoint map_ep {a b : Set}
(p : a → M? b) (l : list a) : M? (list b) :=
match l with
| [] ⇒ return? []
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? res := map_ep p tl in
return? (b :: res)
| Pervasives.Error es ⇒
match map_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition mapi_ep {a b : Set}
(p : int → a → M? b) (l : list a) : M? (list b) :=
let fix mapi_ep_aux index l :=
match l with
| [] ⇒ return? []
| hd :: tl ⇒
match p index hd with
| Pervasives.Ok b ⇒
let? res := mapi_ep_aux (index +i 1) tl in
return? (b :: res)
| Pervasives.Error es ⇒
match mapi_ep_aux (index +i 1) tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end in
mapi_ep_aux 0 l.
Definition rev_map_ep {a b : Set}
(p : a → M? b) (l : list a) : M? (list b) :=
let? res := map_ep p l in
return? (List.rev res).
Definition rev_mapi_ep {a b : Set}
(p : int → a → M? b) (l : list a) : M? (list b) :=
let? res := mapi_ep p l in
return? (List.rev res).
Fixpoint filter_map_ep {a b : Set}
(p : a → M? (option b)) (l : list a) : M? (list b) :=
match l with
| [] ⇒ return? []
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒ match b with
| None ⇒ filter_map_ep p tl
| Some v ⇒
let? res := filter_map_ep p tl in
return? (v :: res)
end
| Pervasives.Error es ⇒
match filter_map_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Definition concat_map_ep {a b : Set}
(p : a → M? (list b)) (l : list a) : M? (list b) :=
let? res := map_ep p l in
return? (List.concat res).
Fixpoint for_all_ep {a : Set}
(p : a → M? bool) (l : list a) : M? bool :=
match l with
| [] ⇒ return? true
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? res := for_all_ep p tl in
return? (b && res)
| Pervasives.Error es ⇒
match for_all_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.
Fixpoint exists_ep {a : Set}
(p : a → M? bool) (l : list a) : M? bool :=
match l with
| [] ⇒ return? false
| hd :: tl ⇒
match p hd with
| Pervasives.Ok b ⇒
let? res := exists_ep p tl in
return? (b || res)
| Pervasives.Error es ⇒
match exists_ep p tl with
| Pervasives.Error es' ⇒ Pervasives.Error (List.app es es')
| Pervasives.Ok _ ⇒ Pervasives.Error es
end
end
end.