module InterimReport where

import Level

module Core where
  data Exists (A : Set) (B : A -> Set) : Set where
    _,_ : (x : A) -> B x -> Exists A B

  fst : forall {A B} -> Exists A B -> A
  fst (x , _) = x

  snd : forall {A B} -> (s : Exists A B) -> B (fst s)
  snd (_ , x) = x
  
  data Bot : Set where
  
  absurd : {A : Set} -> Bot -> A
  absurd ()
  
  data Top : Set where
    <> : Top
  
  data Bool : Set where
    true  : Bool
    false : Bool
  
  if_/_then_else_ : forall {a} (x : Bool) ->
                    (P : Bool -> Set a) -> P true -> P false -> P x
  if true  / _ then x else _ = x
  if false / _ then _ else x = x
  
  if_then_else_ : forall {a} {P : Bool -> Set a}
                  (x : Bool) -> P true -> P false -> P x
  if true  then x else _ = x
  if false then _ else y = y
  
  data W (A : Set) (B : A -> Set) : Set where
    _<!_ : (a : A) -> (B a -> W A B) -> W A B
  
  -- Ugh!  Comments and definiton stolen from
  -- <http://www.e-pig.org/epilogue/?p=324>
  rec : forall {S P}
        (C : W S P -> Set) ->      -- some conclusion we hope holds
        ((s : S) ->                -- given a shape...
         (f : P s -> W S P) ->     -- ...and a bunch of kids…
         ((p : P s) -> C (f p)) -> -- ...and C for each kid in the bunch…
         C (s <! f)) ->            -- ...does C hold for the node?
        (x : W S P) ->             -- If so, ...
        C x                        -- ...C always holds.
  rec C c (s <! f) = c s f (\ p -> rec C c (f p))
  
  _\/_ : (A B : Set) -> Set
  A \/ B = Exists Bool (\ b -> if b then A else B)
  
  inl : forall {A B} -> A -> A \/ B
  inl x = true , x
  
  inr : forall {A B} -> B -> A \/ B
  inr x = false , x
  
  case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
  case {A} {B} {C} x f g =
    (if (fst x) / (\ b -> (if b then A else B) -> C) then f else g)
    (snd x)
  
  Tr : Bool -> Set
  Tr b = if b then Top else Bot
  
  Nat : Set
  Nat = W Bool Tr
  
  zero : Nat
  zero = false <! absurd
  
  suc : Nat -> Nat
  suc n = true <! \ _ -> n
  
  plus : Nat -> Nat -> Nat
  plus x y =
    rec (\ _ -> Nat)
        (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
                then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
  
  data _==_ {A : Set} : A -> A -> Set where
    refl : {x : A} -> x == x
  
  subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
  subst refl T t = t

  _/==_ : forall {A} -> A -> A -> Set
  x /== y = x == y -> Bot

module Ext where
  data List (A : Set) : Set where
    nil  : List A
    _::_ : A -> List A -> List A

  data Nat : Set where
    zero : Nat
    suc  : Nat -> Nat

  data Vec (A : Set) : Nat -> Set where
    nil  : Vec A zero
    _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)

  head : forall {A n} -> Vec A (suc n) -> A
  head (x :: _) = x

  data Fin : Nat -> Set where
    fzero : forall {n} -> Fin (suc n)
    fsuc  : forall {n} -> Fin n -> Fin (suc n)

  _!!_ : forall {A n} -> Vec A n -> Fin n -> A
  (x :: _)  !! fzero  = x
  (x :: xs) !! fsuc i = xs !! i

  open Core using (_==_; refl; subst)

  id : {A : Set} -> A -> A
  id x = x

  map : forall {A B} -> (A -> B) -> List A -> List B
  map _ nil       = nil
  map f (x :: xs) = f x :: map f xs

  cong : forall {A B} {x y : A} (f : A -> B) -> x == y -> f x == f y
  cong f refl = refl

  map-id==id : {A : Set} (xs : List A) -> map id xs == id xs
  map-id==id nil       = refl
  map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs)

  _#_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
  f # g = \ x -> f (g x)

  map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) ->
                 map (f # g) xs == (map f # map g) xs
  map-#==#-map f g nil       = refl
  map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs)

  -- If we could have this...
  postulate ext : forall {A B} {f g : A -> B} ->
                  ((x : A) -> f x == g x) -> f == g

  map-id==id' : forall {A} -> map {A} id == id
  map-id==id' = ext map-id==id

  map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
                  map (f # g) == (map f # map g)
  map-#==#-map' f g = ext (map-#==#-map f g)