Skip to main content

🍃 List.v

Environment

Gitlab

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 :: mSome 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 yf x
    | Nonefind_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 :: leq_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) :: tlif 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) :: tleq 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 kff 0%nat :: nat_init er k (fun vff (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
  | Z0Pervasives.Ok []
  | Zpos x
    Pervasives.Ok (nat_init er (Z.to_nat n) (fun xff (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 :: tl2combine_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 xPervasives.Ok x
  | NonePervasives.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 xPervasives.Ok (rev x)
  | NonePervasives.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 l3Pervasives.Ok (f x y :: l3)
    | Pervasives.Error ePervasives.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 l3Pervasives.Ok (List.rev l3)
  | Pervasives.Error _ as ee
  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 ee
    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 l2fold_left2 er
    (fun acc x yacc && 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 l2fold_left2 er
    (fun acc x yacc || 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%natPervasives.Ok []
  | S k
    match ff 0%nat with
    | Pervasives.Error ePervasives.Error e
    | Pervasives.Ok x
      match nat_init_e er k (fun vff (S v)) with
      | Pervasives.Error _ as ee
      | Pervasives.Ok lPervasives.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
  | Z0Pervasives.Ok []
  | Zpos _nat_init_e er (Z.to_nat n) (fun xff (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 ePervasives.Error e
    | Pervasives.Ok truePervasives.Ok (Some x)
    | Pervasives.Ok falsefind_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 ee
    | Pervasives.Ok (Some _) as resres
    | Pervasives.Ok Nonefind_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 lList.rev (filter p l).

Definition rev_filteri : {a : Set},
  (int a bool) list a list a :=
  fun a p lList.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 lList.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 lList.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 lList.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 lList.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 lList.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 lpartition 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 lpartition_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 lpartition_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 lpartition_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 yreturn? (y :: l1, l2)
    | Either.Right yreturn? (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 lpartition_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 ltt.

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 ltt.

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 lList.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
    | Nonefilter_map f l'
    | Some yy :: filter_map f l'
    end
  end.

Definition rev_filter_map : {a b : Set},
  (a option b) list a list b :=
  fun a b f lList.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
    | Nonefilter_map_e f l'
    | Some zlet? 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 lfilter_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 yy :: l'
    | Nonel'
    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 yreturn? (y :: l')
    | Nonereturn? 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 lList.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 itemlet? 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 itemlet? 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
    | Z0compare 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 :: l2eqb 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 fx :: of_seq_node (f tt)
  end.

Definition of_seq : {a : Set}, Seq.t a list a :=
  fun a sof_seq_node (s tt).

Fixpoint nat_init_ep {a : Set} (n : nat) (ff : nat M? a) : M? (list a) :=
  match n with
  | 0%natreturn? []
  | S k
    match ff 0%nat with
    | Pervasives.Ok x
        let? res := nat_init_ep k (fun xff (S x)) in return? (x :: res)
    | Pervasives.Error es
      match nat_init_ep k (fun xff (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
  | Z0return? []
  | Zpos _nat_init_ep (Z.to_nat n) (fun xff (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 bmatch b with
                         | Nonefilter_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.