Library zoo_std.list__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.options.

Definition list ٠ singleton : val :=
  𝗳𝘂𝗻 "v" →
    "v" :: [].

Definition list ٠ head : val :=
  𝗳𝘂𝗻 "param" →
    𝗺𝗮𝘁𝗰𝗵 "param" 𝘄𝗶𝘁𝗵
    | [] →
        𝗳𝗮𝗶𝗹
    | "v" :: ⎽ →
        "v"
    𝗲𝗻𝗱.

Definition list ٠ tail : val :=
  𝗳𝘂𝗻 "param" →
    𝗺𝗮𝘁𝗰𝗵 "param" 𝘄𝗶𝘁𝗵
    | [] →
        𝗳𝗮𝗶𝗹
    | ⎽ :: "t" →
        "t"
    𝗲𝗻𝗱.

Definition list ٠ is_empty : val :=
  𝗳𝘂𝗻 "param" →
    𝗺𝗮𝘁𝗰𝗵 "param" 𝘄𝗶𝘁𝗵
    | [] →
        true
    | ⎽ :: ⎽ →
        false
    𝗲𝗻𝗱.

Definition list ٠ get : val :=
  𝗿𝗲𝗰 "get" "t" "i" →
    𝗶𝗳 "i" ≤ 0 𝘁𝗵𝗲𝗻 (
      list ٠ head "t"
    ) 𝗲𝗹𝘀𝗲 (
      "get" (list ٠ tail "t") ("i" - 1)
    ).

Definition list ٠ initi₁ : val :=
  𝗿𝗲𝗰 "initi" "sz" "fn" "i" →
    𝗶𝗳 "sz" ≤ "i" 𝘁𝗵𝗲𝗻 (
      []
    ) 𝗲𝗹𝘀𝗲 (
      𝗹𝗲𝘁 "v" = "fn" "i" 𝗶𝗻
      "v" :: "initi" "sz" "fn" ("i" + 1)
    ).

Definition list ٠ initi : val :=
  𝗳𝘂𝗻 "sz" "fn" →
    list ٠ initi₁ "sz" "fn" 0.

Definition list ٠ init : val :=
  𝗳𝘂𝗻 "sz" "fn" →
    list ٠ initi "sz" (𝗳𝘂𝗻 "_i" → "fn" ()).

Definition list ٠ foldli₁ : val :=
  𝗿𝗲𝗰 "foldli" "fn" "i" "acc" "t" →
    𝗺𝗮𝘁𝗰𝗵 "t" 𝘄𝗶𝘁𝗵
    | [] →
        "acc"
    | "v" :: "t" →
        "foldli" "fn" ("i" + 1) ("fn" "i" "acc" "v") "t"
    𝗲𝗻𝗱.

Definition list ٠ foldli : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ foldli₁ "fn" 0.

Definition list ٠ foldl : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ foldli (𝗳𝘂𝗻 "_i" → "fn").

Definition list ٠ foldri₁ : val :=
  𝗿𝗲𝗰 "foldri" "fn" "i" "t" "acc" →
    𝗺𝗮𝘁𝗰𝗵 "t" 𝘄𝗶𝘁𝗵
    | [] →
        "acc"
    | "v" :: "t" →
        "fn" "i" "v" ("foldri" "fn" ("i" + 1) "t" "acc")
    𝗲𝗻𝗱.

Definition list ٠ foldri : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ foldri₁ "fn" 0.

Definition list ٠ foldr : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ foldri (𝗳𝘂𝗻 "_i" → "fn").

Definition list ٠ size : val :=
  𝗳𝘂𝗻 "t" →
    list ٠ foldl (𝗳𝘂𝗻 "acc" ⎽ → "acc" + 1) 0 "t".

Definition list ٠ rev_app : val :=
  𝗳𝘂𝗻 "t1" "t2" →
    list ٠ foldl (𝗳𝘂𝗻 "acc" "v" → "v" :: "acc") "t2" "t1".

Definition list ٠ rev : val :=
  𝗳𝘂𝗻 "t" →
    list ٠ rev_app "t" [].

Definition list ٠ app : val :=
  𝗳𝘂𝗻 "t1" "t2" →
    list ٠ foldr (𝗳𝘂𝗻 "v" "acc" → "v" :: "acc") "t1" "t2".

Definition list ٠ snoc : val :=
  𝗳𝘂𝗻 "t" "v" →
    list ٠ app "t" (list ٠ singleton "v").

Definition list ٠ iteri : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ foldli (𝗳𝘂𝗻 "i" ⎽ → "fn" "i") ().

Definition list ٠ iter : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ iteri (𝗳𝘂𝗻 "_i" → "fn").

Definition list ٠ mapi₁ : val :=
  𝗿𝗲𝗰 "mapi" "fn" "i" "t" →
    𝗺𝗮𝘁𝗰𝗵 "t" 𝘄𝗶𝘁𝗵
    | [] →
        []
    | "v" :: "t" →
        𝗹𝗲𝘁 "v" = "fn" "i" "v" 𝗶𝗻
        "v" :: "mapi" "fn" ("i" + 1) "t"
    𝗲𝗻𝗱.

Definition list ٠ mapi : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ mapi₁ "fn" 0.

Definition list ٠ map : val :=
  𝗳𝘂𝗻 "fn" →
    list ٠ mapi (𝗳𝘂𝗻 "_i" → "fn").

Definition list ٠ ∀ : val :=
  𝗿𝗲𝗰 "forall" "pred" "param" →
    𝗺𝗮𝘁𝗰𝗵 "param" 𝘄𝗶𝘁𝗵
    | [] →
        true
    | "v" :: "t" →
        "pred" "v" 𝗮𝗻𝗱 "forall" "pred" "t"
    𝗲𝗻𝗱.

Definition list ٠ ∃ : val :=
  𝗿𝗲𝗰 "exists" "pred" "param" →
    𝗺𝗮𝘁𝗰𝗵 "param" 𝘄𝗶𝘁𝗵
    | [] →
        false
    | "v" :: "t" →
        "pred" "v" 𝗼𝗿 "exists" "pred" "t"
    𝗲𝗻𝗱.