Prim.hs

module Prim


import Data.Vect
import Data.Fin
-- import Data.Nat
-- import Data.List
-- %hide Prelude.cong


-- data Bool : Type where
--   True : Bool
--   False : Bool

-- (!!) : {a : Type} -> Nat -> List a -> Maybe a
-- _ !! []            = Nothing
-- (S n) !! (x :: xs) = n !! xs
-- Z     !! (x :: xs) = Just x

infixl 9 !!
(!!) : {a : Type} -> List a -> Nat -> Maybe a
[] !! _            = Nothing
(x :: xs) !! Z     = Just x
(x :: xs) !! (S n) = xs !! n


-- zip : {a : Type} -> {b : Type} -> List a -> List b -> List (a,b)
-- zip [] _ = []
-- zip _ [] = []
-- zip (a :: as) (b :: bs) = (a,b) :: zip as bs

zipWith : {a : Type} -> {b : Type} -> {c : Type} -> (a -> b -> c) -> List a -> List b -> List c
zipWith f [] _ = []
zipWith f _ [] = []
zipWith f (a :: as) (b :: bs) = (f a b) :: zipWith f as bs

zip : {a : Type} -> {b : Type} -> List a -> List b -> List (a,b)
zip as bs = zipWith (,) as bs



data Cap : Type where
  Single : Cap
  Group  : Cap

Collect : Cap -> Type
Collect Single = Nat
Collect Group  = List Nat

create : (c : Cap) -> Nat -> Collect c
create Single n = n
create Group  n = [n]

v : Collect Single
v = create Single 5

vG : Collect Group
vG = create Group 5


-- csum : (c : Cap) -> Collect c -> Nat
-- csum Single n = n
-- csum Group [] = 0
-- csum Group (n :: ns) = n + csum Group ns

-- csum : (c : Cap) -> Collect c -> Nat
-- csum Single = id
-- csum Group  = sum

csum : {c : Cap} -> Collect c -> Nat
csum {c = Single} n = n
csum {c = Group} [] = 0
csum {c = Group} (n :: ns) = n + csum {c = Group} ns

inc : (c : Cap) -> Collect c -> Collect c
inc Single n  = n + 1
inc Group []  = []
inc Group (n :: ns) = (n + 1) :: inc Group ns

eqNat : Nat -> Nat -> Bool
eqNat Z Z         = True
eqNat (S n) (S m) = eqNat n m
eqNat _ _         = False

eqList : {a : Type} -> List a -> List a -> Bool
eqList [] []               = True
eqList (_ :: xs) (_ :: ys) = eqList xs ys
eqList _ _                 = False


-- foldr' : {a : Type} -> {b : Type} -> (a -> b -> b) -> b -> List a -> b
-- foldr' f b [] = b
-- foldr' f b (a :: as) = a `f` (foldr' f b as)


index' : Fin n -> Vect n a -> a
index' FZ (a :: _)       = a
index' (FS fn) (_ :: as) = index' fn as


fiveIsFive : 5 = 5
fiveIsFive = Refl

cong' : 
  {A, B : Type} -> 
  {x, y : A} -> 
  (f : A -> B) -> x = y -> f x = f y
cong' f Refl = Refl

congcong :
  {A : Type} -> 
  {x, y : A} -> 
  (f : A -> A) -> x = y -> f (f x) = f (f y)
congcong f Refl = cong' f Refl

cong'' : (f : a -> b) -> x = y -> f x = f y
cong'' f Refl = Refl

plus_n_0 : (n : Nat) -> n = n + 0
plus_n_0 Z     = Refl
plus_n_0 (S n) = cong' S (plus_n_0 n)

plus_0_l : (n : Nat) -> 0 + n = n
plus_0_l n = Refl

plus_0_r : (n : Nat) -> n + 0 = n
plus_0_r n = sym (plus_n_0 n)

plus_n_Sm : (n, m : Nat) -> S (n + m) = n + (S m)
-- plus_n_Sm Z Z = Refl
-- plus_n_Sm Z (S m) = cong' S Refl
-- plus_n_Sm (S n) Z = cong' S (plus_n_Sm n 0)
plus_n_Sm Z m     = Refl
plus_n_Sm (S n) m = cong' S (plus_n_Sm n m)

pred_Sn : (n : Nat) -> n = pred (S n)
pred_Sn n = Refl

-- eq_add_S : (n, m : Nat) -> S n = S m -> n = m
-- eq_add_S n m sn_eq_sm = eq_add_S n m sn_eq_sm


plus_Sn_m : (n, m : Nat) -> (S n) + m = S (n + m)
plus_Sn_m n m = Refl

plus_comm : (n, m : Nat) -> n + m = m + n
plus_comm Z m = sym $ plus_0_r m -- sym (plus_0_r m)
plus_comm (S n) m = trans (cong' S (plus_comm n m)) (plus_n_Sm m n)
{-
plus_comm (S n) m = 
  let p1 = plus_n_Sm m n 
    in let p2 = plus_comm m (S n) 
      in let p3 = trans p1 p2 
        in let p4 = trans (sym p3) p1 
          in let p5 = plus_n_Sm n m in ?help
-}

plus_Snm_nSm : (n, m : Nat) -> (S n) + m = n + (S m)
plus_Snm_nSm n m = plus_n_Sm n m

plus_assoc : (n, m, k : Nat) -> n + (m + k) = (n + m) + k
plus_assoc Z m k     = Refl
plus_assoc (S n) m k = cong' S (plus_assoc n m k)

plus_permute : (n, m, k : Nat) -> n + (m + k) = m + (n + k)
plus_permute Z m k = Refl
plus_permute (S n) m k = trans (sym $ cong' S (plus_permute m n k)) (plus_Snm_nSm m (n + k))



append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil ms = ms
append (n :: ns) ms = n :: append ns ms

-- append_nil_id : (n : Nat) -> (v : Vect n a) -> v = (append v [])
-- append_nil_id n v = ?h1
-- append_nil_id (a :: as) = ?h1

vsnoc : a -> Vect n a -> Vect (S n) a
vsnoc a Nil = a :: Nil
vsnoc a (x :: xs) = x :: vsnoc a xs


rev : Vect n a -> Vect n a
rev Nil = Nil
rev (a :: as) = vsnoc a (rev as)

cons_vsnoc_rev : (x : a) -> (xs : Vect n a) -> rev (x :: xs) = vsnoc x (rev xs)
cons_vsnoc_rev x xs = Refl

-- vsnoc_rev_id : (x : a) -> (xs : Vect n a) -> vsnoc x (rev xs) = x :: xs
-- vsnoc_rev_id

cons_vsnoc : (x : a) -> (xs : Vect n a) -> rev (vsnoc x xs) = x :: rev xs
cons_vsnoc {n=Z} x' Nil = Refl
cons_vsnoc {n=(S n')} x' (x :: xs) = rewrite cons_vsnoc x' xs in cong'' ((::) x') Refl
-- cons_vsnoc {n=(S n')} x' (x :: xs) = rewrite cons_vsnoc x' xs in ?h1 -- (Prelude.cong ((::) x') Refl)


-- rev_rev_id : {a : Type} -> {n : Nat} -> (v : Vect n a) -> rev (rev v) = v
-- rev_rev_id {a} {n = Z} Nil = Refl
-- rev_rev_id {a} {n = S n'} (x :: xs) = ?h2

rev_rev_id : (n : Nat) -> (v : Vect n a) -> rev (rev v) = v
rev_rev_id Z Nil = Refl
rev_rev_id (S n) (v :: vs) = let p = cons_vsnoc_rev v vs in ?h2
  -- case rev vs of
  --   (x :: xs) => ?h1 -- rev_rev_id (S n') vs

-- rev_rev_id Nil = Refl
-- rev_rev_id {n = S n'} (x :: xs) = let p = cons_vsnoc_rev x xs in ?h2
  -- = case xs of
  --   Nil => Refl
  --   (x' :: xs') => ?h2