import Std.Data.List.Basic

section catamorphism
  def cata {α β : Type} (b : β) (f : α → β → β) (x : List α) :=
    match x with
    | [] => b
    | a :: as => f a (cata b f as)

  notation:max "⦅" l:10 "," r:11 "⦆" => cata l r

  -- theorem cata_fusion (h : β → β) (b : β) (f : α → β → β) : h ∘ ⦅b, f⦆ = ⦅b, h ∘ f⦆ := by
    -- sorry

  section length
    def length := ⦅0, Function.const Nat Nat.succ⦆
    theorem length_empty : length [] = Nat.zero := by
      unfold length
      unfold cata
      rfl

    theorem length_cons : length (a :: as) = Nat.succ (length as) := by
      match as with
      | [] =>
        rw [length_empty]
        unfold length
        simp [cata]
      | b :: bs =>
        unfold length
        simp [cata]

    #eval length [1,2,3,4,5,6,7,8,9]
    end length

  section filter
    def filter {α : Type} (p : α → Bool) := ⦅[],
    λ (a as) => if (p a) then (a :: as) else (as)⦆

    theorem filter_nil {α : Type} (p : α → Bool) : filter p [] = [] := by
      unfold filter
      simp [cata]

    theorem filter_cons_pos {α : Type} (p : α → Bool) {a : α} (l : List α) : p a → filter p (a :: l) = a :: (filter p l) := by
      intro hp
      unfold filter
      simp [cata]
      simp [hp]

    theorem filter_cons_neg {α : Type} (p : α → Bool) {a : α} (l : List α) : ¬p a → filter p (a :: l) = filter p l := by
      intro hp
      unfold filter
      simp [cata]
      simp [hp]

    #eval filter (·>5) [1,2,3,4,5,6,7,8,9]
    end filter
end catamorphism

section anamorphism
  partial def ana {α β : Type} (p : β → Bool) (b : β) (g : ∀ (b : β) (_ : ¬p b), α × β) := by
    cases h : (p b)
    have hp := ne_true_of_eq_false h
    let t := g b hp
    exact t.fst :: ana p t.snd g
    exact []

  notation:max "〖" l:10 "," r:11 "〗" => λ b => ana r b l

  section zip
    def p (l : List α × List β) : Bool := (List.length l.1) = 0 || (List.length l.2 = 0)

    -- this si fucking ugly!!!!!!
    def g (l : List α × List β) (hp : ¬p l) := by
      unfold p at hp
      simp at hp
      rw [not_or] at hp

      have left := And.left hp
      rw [List.length_eq_zero] at left
      have right := And.right hp
      rw [List.length_eq_zero] at right

      have lh := List.head l.fst left
      have rh := List.head l.snd right

      exact ((lh, rh), (List.tail l.fst, List.tail l.snd))

    def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
    def zip : List α → List β → List (α × β) := curry 〖g, p〗

    #eval zip [1] [2]
  end zip
end anamorphism

section hylomorphism
  -- partial def hylo (c : φ) (f : β → φ → φ) (p : α → Bool) (a : α) := match p a with
    -- | true => c
    -- | false => let t := g a
              -- f t.fst (hylo c f g p t.snd)

  def hylo (c : φ) (f : β → φ → φ) (p : α → Bool) (g : (b : α) → ¬p b = true → β × α) := ⦅c,f⦆ ∘ 〖g, p〗

  notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f p g

  section factorial
      def g_1 (b : Nat) (_ : ¬decide (b = 0)) : Nat × Nat := (b, b-1)

    def fac : Nat → Nat := ⟦(1, Nat.mul), (g_1, (·=0))⟧

    #eval fac 8

  end factorial

end hylomorphism