NeilPrelude1

-- Everything I want, as I want it.

module NeilPrelude1 where


-- Precedence -------------------------------------

-- Higher precedence numbers bind tighter

infix  0  if_then_else_

infixr 2  _&_ _×_ _1×_ _×1_ _1×1_

infix  3  _≡_ _≢_ -- _≤_ _∈_ 

-- infixl 4 _>>=_ _>>_

infixr 5  _∨_ _xor_
infixr 6  _∧_

infix  8  _==_ _!=_ -- _<=_
infixl 10 _+_ _-_
infixl 11 _*_
-- infixr 12 _^_

-- infixr 13 _+m+_
-- infixr 15 _++_ _+v+_
infixr 16 _∷_

infixr 90 _∘_ _∘'_ _∘≡_ _≡∘_
-- infixr 90 _⋙_
infixr 91 _∥_ _∥∥_


-- Dependent Functions (Π types) ---------------------

Π : (A : Set) → (A → Set) → Set
Π A B = (a : A) → B a


-- Combinators --

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘ g = λ a → f (g a)

_∘'_ : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → ({a : A} → Π (B a) (C a)) → (g : Π A B) → (a : A) → C a (g a)
f ∘' g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

apply : {A : Set} → {B : A → Set} → Π A B → Π A B
apply = id

applyTo : {A : Set} → {B : A → Set} → (a : A) → Π A B → B a 
applyTo a f = f a

flip : {A B C : Set} → (A → B → C) → B → A → C
flip f b a = f a b

const : {A B : Set} → A → B → A
const a b = a

compose : {A B C : Set} → (A → B) → (B → C) → (A → C)
compose = flip _∘_ 


-- Propositional Equality --

data Unit : Set where
  unit : Unit

data False : Set where

record True : Set where

absurd : {A : Set} → False → A
absurd ()

Not : Set → Set
Not A = A → False

data _≡_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≡ a 

Id : (A : Set) → A → A → Set
Id _ = _≡_ 

_≢_   : {A : Set} → A → A → Set
a ≢ b = Not (a ≡ b)

trans : {A : Set} → {a b : A} → (x : A) → a ≡ x → x ≡ b → a ≡ b
trans _ refl refl = refl

_∘≡_ : {A : Set} → {x a b : A} → x ≡ b → a ≡ x → a ≡ b
refl ∘≡ refl = refl

_≡∘_ : {A : Set} → {x a b : A} → x ≡ a → b ≡ x → a ≡ b
refl ≡∘ refl = refl 

_∘≡∘_ : {A : Set} → {a b c d : A} → a ≡ c → b ≡ d → (a ≡ b → c ≡ d)
refl ∘≡∘ refl = id 

comm : {A : Set} → {a b : A} → a ≡ b → b ≡ a
comm refl = refl

resp : {A B : Set} → {a a' : A} → (f : A → B) → a ≡ a' → f a ≡ f a' 
resp _ refl = refl

resp2 : {A B C : Set} → {a a' : A} → {b b' : B}
     → (f : A → B → C) → a ≡ a' → b ≡ b' → f a b ≡ f a' b'
resp2 {A} {B} {C} {.a} {a} f refl = resp (f a)

resp3 : {A B C D : Set} → {a a' : A} → {b b' : B} → {c c' : C}
     → (f : A → B → C → D) → a ≡ a' → b ≡ b' → c ≡ c' → f a b c ≡ f a' b' c'
resp3 {A} {B} {C} {D} {.a} {a} f refl = resp2 (f a)

resp4 : {A B C D E : Set} → {a a' : A} → {b b' : B} → {c c' : C} → {d d' : D}
     → (f : A → B → C → D → E) → a ≡ a' → b ≡ b' → c ≡ c' → d ≡ d' → f a b c d ≡ f a' b' c' d'
resp4 {A} {B} {C} {D} {E} {.a} {a} f refl = resp3 (f a)

rewriteLHS : {A : Set} → {a b c : A} → a ≡ c → a ≡ b → c ≡ b
rewriteLHS refl refl = refl

rewriteRHS : {A : Set} → {a b c : A} → b ≡ c → a ≡ b → a ≡ c
rewriteRHS refl refl = refl 

data Inspect {A : Set} (a : A) : Set where
  it : (b : A) → a ≡ b → Inspect a

inspect : {A : Set} → (a : A) → Inspect a
inspect a = it a refl


-- Comparisons ---------------------------------------

data Compare {A : Set} : A → A → Set where
  refl : {a : A}   → Compare a a
  neq  : {a b : A} → a ≢ b → Compare a b

data SimpleCompare {A : Set} : A → A → Set where
  refl : {a : A}   → SimpleCompare a a
  neq  : {a b : A} → SimpleCompare a b

data OrdCompare {A : Set} (_<_ : A → A → Set) : A → A → Set where
  refl : {a : A}           → OrdCompare _<_ a a
  less : {a b : A} → a < b → OrdCompare _<_ a b
  more : {a b : A} → b < a → OrdCompare _<_ a b


-- Dependent Products (Σ types) ----------------------

data Σ (A : Set) (B : A → Set) : Set where
  _&_ : (a : A) → B a → Σ A B

data Σ1 (A : Set) (B : A → Set1) : Set1 where
  _&_ : (a : A) → B a → Σ1 A B

data 1Σ (A : Set1) (B : A → Set) : Set1 where
  _&_ : (a : A) → B a → 1Σ A B

data 1Σ1 (A : Set1) (B : A → Set1) : Set1 where
  _&_ : (a : A) → B a → 1Σ1 A B


_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)

_×1_ : (A : Set) → (B : Set1) → Set1
A ×1 B = Σ1 A (λ _ → B)

_1×_ : (A : Set1) → (B : Set) → Set1
A 1× B = 1Σ A (λ _ → B)

_1×1_ : (A B : Set1) → Set1
A 1×1 B = 1Σ1 A (λ _ → B)


fst : {A : Set} → {B : A → Set} → Σ A B → A
fst (a & b) = a

snd : {A : Set} → {B : A → Set} → (ab : Σ A B) → B (fst ab)
snd (a & b) = b

fstsnd : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → (abc : Σ A (λ a → Σ (B a) (C a))) → B (fst abc)
fstsnd (_ & b & _) = b

thd : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → (abc : Σ A (λ a → Σ (B a) (C a))) → C (fst abc) (fstsnd abc)
thd (_ & _ & c) = c

curry : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → ((ab : Σ A B) → C (fst ab) (snd ab)) → (a : A) → (b : B a) → C a b
curry f a b = f (a & b)

uncurry : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → ((a : A) → (b : B a) → C a b) → (ab : Σ A B) → C (fst ab) (snd ab)
uncurry f (a & b) = f a b

uncurry2 : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → {D : (a : A) → (b : B a) → C a b → Set}
           → ((a : A) → (b : B a) → (c : C a b) → D a b c) → (abc : Σ A (λ a → Σ (B a) (C a))) → D (fst abc) (fst (snd abc)) (snd (snd abc)) 
uncurry2 f (a & b & c) = f a b c

uncurry3 : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → {D : (a : A) → (b : B a) → C a b → Set} → {E : (a : A) → (b : B a) → (c : C a b) → D a b c → Set}
           → ((a : A) → (b : B a) → (c : C a b) → (d : D a b c) → E a b c d) → (abcd : Σ A (λ a → Σ (B a) (λ b → Σ (C a b) (D a b)))) → E (fst abcd) (fstsnd abcd) (fst (thd abcd)) (snd (thd abcd))
uncurry3 f (a & b & c & d) = f a b c d

first : {A B C : Set} → (A → C) → A × B → C × B
first f (a & b) = f a & b

second : {A : Set} → {B C : A → Set} → ({a : A} → B a → C a) → Σ A B → Σ A C
second f (a & b) = a & f b

third : {A : Set} → {B : A → Set} → {C D : (a : A) → B a → Set} → ({a : A} → {b : B a} → C a b → D a b) → Σ A (λ a → Σ (B a) (C a)) → Σ A (λ a → Σ (B a) (D a))
third f (a & b & c) = a & b & f c

_∥_ : {A C : Set} → {B : A → Set} → {D : C → Set} → (f : A → C) → ({a : A} → B a → D (f a)) → Σ A B → Σ C D
_∥_ f g (a & b) = f a & g b 

-- cross : (A → C) × (B → D) → A × B → C × D

cross : {A C : Set} → {B : A → Set} → {D : C → Set} → Σ (A → C) (λ f → {a : A} → B a → D (f a)) → Σ A B → Σ C D
cross = uncurry _∥_

_∥∥_ : {A B C : Set} → {J : A → Set} → {K : B → Set} → {L : C → Set} →
         (f : A → B → C) → (g : {a : A} → {b : B} → J a × K b → L (f a b)) → Σ A J × Σ B K → Σ C L
_∥∥_ f g ((a & j) & (b & k)) = f a b & g (j & k)

-- ×map : (A → B) → A × A → B × B

×map : {A : Set} → {B : A → Set} → Π A B → (aa : A × A) → B (fst aa) × B (snd aa)
×map f (a₁ & a₂) = f a₁ & f a₂

-- ×zipWiths : (f : A → B → C) → (g : J → K → L) → (A × J) → (B × K) → C × L

×zipWiths : {A B C : Set} → {J : A → Set} → {K : B → Set} → {L : C → Set} →
           (f : A → B → C) → (g : {a : A} → {b : B} → J a → K b → L (f a b)) → Σ A J → Σ B K → Σ C L
×zipWiths f g (a & j) (b & k) = f a b & g j k

-- across : (A → B → C) → (J → K → L) → (A × J) × (B × K) → C × L

across : {A B C : Set} → {J : A → Set} → {K : B → Set} → {L : C → Set} →
         (f : A → B → C) → (g : {a : A} → {b : B} → J a → K b → L (f a b)) → Σ A J × Σ B K → Σ C L
across f g = uncurry (×zipWiths f g) 

-- pair : (A → B) → (A → C) → A → B × C

pair : {A : Set} → {B : A → Set} → {C : (a : A) → B a → Set} → (f : Π A B) → ((a : A) → C a (f a)) → (a : A) → Σ (B a) (C a)
pair f g a = f a & g a

fork : {A : Set} → A → A × A
fork a = a & a

dup : {A : Set} → A → A × A
dup = fork

swap : {A B : Set} → A × B → B × A
swap (a & b) = b & a

×assoc : {A B C : Set} → (A × B) × C → A × B × C
×assoc ((a & b) & c) = a & b & c

×assocR : {A B C : Set} → A × B × C → (A × B) × C
×assocR (a & b & c) = (a & b) & c


-- Sum Types (a.k.a. co-products) --

data Either (A B : Set) : Set where
  left : A → Either A B
  right : B → Either A B

case : {A B C : Set} → (A → C) → (B → C) → Either A B → C
case f g (left a) = f a
case f g (right b) = g b


Trichotomy : (A B C : Set) → Set
Trichotomy A B C = Either (A × Not B × Not C)
                  (Either (Not A × B × Not C)
                          (Not A × Not B × C))

trichcases : {A B C D : Set} → (A → Not B → Not C → D) → (Not A → B → Not C → D) → (Not A → Not B → C → D) → Trichotomy A B C → D
trichcases f _ _ (left (a & b & c)) = f a b c
trichcases _ f _ (right (left (a & b & c))) = f a b c
trichcases _ _ f (right (right (a & b & c))) = f a b c


-- Maybe --

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

maybe : {A B : Set} → B → (A → B) → Maybe A → B 
maybe b _ nothing = b
maybe _ f (just a) = f a

maybeMergeWith : {A : Set} → (A → A → A) → Maybe A → Maybe A → Maybe A
maybeMergeWith f (just a) (just b) = just (f a b)
maybeMergeWith f nothing mb = mb
maybeMergeWith f ma nothing = ma

maybeMap : {A B : Set} → (A → B) → Maybe A → Maybe B
maybeMap f nothing = nothing
maybeMap f (just a) = just (f a)


-- Booleans --

data Bool : Set where
  false : Bool
  true  : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

not           : Bool → Bool
not false     = true
not true      = false

¬ : {A : Set} → (A → Bool) → (A → Bool)
¬ p = not ∘ p

isTrue : Bool → Set
isTrue true = True
isTrue false = False

-- "Sat"isfies the predicate

Sat : {A : Set} → (A → Bool) → A → Set
Sat p a = isTrue (p a)

isFalse : Bool → Set
isFalse = Sat not

trueIsTrue : {b : Bool} → b ≡ true → isTrue b
trueIsTrue refl = _

falseIsFalse : {b : Bool} → b ≡ false → isFalse b
falseIsFalse refl = _

if_then_else_ : {A : Set} → Bool → A → A → A
if_then_else_ false t e = e
if_then_else_ true t e = t

ifte : {A : Set} → A → A → Bool → A
ifte t e false = e
ifte t e true  = t

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b


-- Natural Numbers --

data ℕ : Set where
  O : ℕ
  S : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO    O #-}
{-# BUILTIN SUC     S #-}

_+_         : ℕ → ℕ → ℕ
O + n       = n
S m + n     = S (m + n)

{-# BUILTIN NATPLUS _+_ #-}

_-_ : ℕ → ℕ → ℕ
m   - O   = m
O   - n   = O
S m - S n = m - n

{-# BUILTIN NATMINUS _-_ #-}

_*_ : ℕ → ℕ → ℕ
O   * n = O
S m * n = n + m * n

{-# BUILTIN NATTIMES _*_ #-}

natrec : {P : ℕ → Set} → P O → ({m : ℕ} → P m → P (S m)) → Π ℕ P
natrec     base step O = base
natrec {P} base step (S n) = step (natrec {P} base step n)

natcases : {A : ℕ → Set} → A O → ((n : ℕ) → A (S n)) → Π ℕ A
natcases a f = natrec a (λ {n} _ → f n)



------------------- Lists ---------------------

-- Lists --

-- import List.agda for functions

data List (A : Set) : Set where
  []   : List A
  _∷_  : A → List A → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []  #-}
{-# BUILTIN CONS _∷_ #-}

data List' (S : Set1) : Set1 where
  []  : List' S
  _∷_ : S → List' S → List' S 


-- Vectors --

-- import Vector.agda for functions

data Vec (A : Set) : ℕ → Set where
  [] : Vec A O
  _∷_  : {n : ℕ} → A → Vec A n → Vec A (S n)

data Fin : ℕ → Set where
  fO : {n : ℕ} → Fin (S n)
  fS : {n : ℕ} → Fin n → Fin (S n)


-- import HetroVector.agda for functions

data HetVec {A : Set} (eType : A → Set) : (List A) → Set where
  ⟨⟩   : HetVec eType []
  _∷_  : {a : A} → {as : List A} → (eType a) → HetVec eType as → HetVec eType (a ∷ as)

data HetVec2 {A B : Set} (eType : A → B → Set) : List A → List B → Set where
  ⟨⟩   : HetVec2 eType [] []
  _∷_  : {a : A} → {b : B} → {as : List A} → {bs : List B} → eType a b → HetVec2 eType as bs → HetVec2 eType (a ∷ as) (b ∷ bs)


-- Integers -------------------------------------

data ℤ : Set where
  +S : ℕ → ℤ  
  Z  : ℤ
  -S : ℕ → ℤ

pred : ℤ → ℤ
pred (+S O)     = Z
pred (+S (S n)) = +S n
pred Z          = -S O
pred (-S n)     = -S (S n)



-- Equality Universe --

data EqUni : Set where
  bool    : EqUni
  nat     : EqUni
  int     : EqUni
  maybeEq : EqUni → EqUni
  list    : EqUni → EqUni
  vector  : EqUni → ℕ → EqUni
  fin     : ℕ → EqUni

eqSet : EqUni → Set
eqSet bool = Bool
eqSet nat = ℕ
eqSet int = ℤ
eqSet (maybeEq t) = Maybe (eqSet t)
eqSet (list t) = List (eqSet t)
eqSet (vector t n) = Vec (eqSet t) n
eqSet (fin n) = Fin n

_==_ : {t : EqUni} → eqSet t → eqSet t → Bool

_==_ {bool} false b = not b
_==_ {bool} true b = b

_==_ {nat} O O = true
_==_ {nat} (S m) (S n) = m == n
_==_ {nat} _ _ = false

_==_ {int} Z Z = true
_==_ {int} (+S m) (+S n) = m == n
_==_ {int} (-S m) (-S n) = m == n
_==_ {int} _ _ = false

_==_ {maybeEq t} nothing nothing = true
_==_ {maybeEq t} (just a) (just b) = a == b
_==_ {maybeEq t} _ _ = false

_==_ {list t} [] [] = true
_==_ {list t} (a ∷ as) (b ∷ bs) = a == b ∧ as == bs
_==_ {list t} _ _ = false

_==_ {vector t O} [] [] = true
_==_ {vector t (S n)} (a ∷ as) (b ∷ bs) = a == b ∧ as == bs

_==_ {fin O} () () 
_==_ {fin (S n)} fO fO = true
_==_ {fin (S n)} (fS fm) (fS fn) = fm == fn
_==_ {fin (S n)} _ _ = false


_!=_ : {t : EqUni} → eqSet t → eqSet t → Bool
a != b = not (a == b)