module Ty where

open import Data.Bool                  using (Bool; false; _∨_; if_then_else_)
open import Data.Nat                   using (ℕ; zero; suc; pred; _+_; _≟_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.List                  using (List; []; [_]; _∷_; length; concat; map; sum)
open import Data.Product               using (_×_; _,_)
open import Relation.Binary.Core       using (Decidable; refl; _≡_)
open import Relation.Nullary.Core      using (yes; no)
open import Function                   using (_∘_)

𝕍ar  : Set 
𝕍ar = ℕ

𝕍ars : Set
𝕍ars = List ℕ

mem : ℕ → 𝕍ars → Bool
mem _ []      = false
mem a (b ∷ x) = ⌊ a ≟ b ⌋ ∨ mem a x

union : 𝕍ars → 𝕍ars → 𝕍ars
union []      y = y
union (a ∷ x) y = if mem a y then union x y else a ∷ union x y

data 𝕋 : Set where
 Con : ℕ → 𝕋     {- type constructor -}
 Var : ℕ → 𝕋     {- type variable -}
 _⇒_ : 𝕋 → 𝕋 → 𝕋 {- function type -}

𝕋𝕋 = 𝕋 × 𝕋
𝕋𝕋s = List 𝕋𝕋

data Σ : Set  where 
 Simple : 𝕋 → Σ        {- simple type is a type -}
 Gen    : ℕ → Σ → Σ    {- type with outermost quantifier -}

invCon : ∀ {n m} → (Con n ≡ Con m) → n ≡ m
invCon refl = refl 

invVar : ∀ {n m} → (Var n ≡ Var m) → n ≡ m
invVar refl = refl 

inv⇒L : ∀ {a b c d} → (a ⇒ b ≡ c ⇒ d) → a ≡ c
inv⇒L {a} {b} {.a} {.b} refl = refl

inv⇒R : ∀ {a b c d} → (a ⇒ b ≡ c ⇒ d) → b ≡ d
inv⇒R {a} {b} {.a} {.b} refl = refl

_≟t_ : Decidable {A = 𝕋} _≡_
Con c1  ≟t Con c2 with c1 ≟ c2 
Con c1  ≟t Con .c1 | yes refl = yes refl
Con c1  ≟t Con c2  | no prf   = no (prf ∘ invCon)
Con _   ≟t Var _   = no (λ ())
Con _   ≟t (_ ⇒ _) = no (λ ())

Var v1  ≟t Var v2 with v1 ≟ v2 
Var v1  ≟t Var .v1 | yes refl = yes refl 
Var v1  ≟t Var v2  | no prf   = no (prf ∘ invVar)
Var _   ≟t Con _   = no (λ ())
Var _  ≟t (_ ⇒ _)  = no (λ ())

(ta ⇒ tb) ≟t (tc ⇒ td)  with ta ≟t tc
(ta ⇒ tb) ≟t (.ta ⇒ td)  | yes refl with tb ≟t td
(ta ⇒ tb) ≟t (.ta ⇒ .tb) | yes refl | yes refl = yes refl
(ta ⇒ tb) ≟t (.ta ⇒ td)  | yes refl | no prf   = no (prf ∘ inv⇒R)
(ta ⇒ tb) ≟t (tc ⇒ td)   | no prf = no (prf ∘ inv⇒L)
(ta ⇒ tb) ≟t Con _ = no (λ ())
(ta ⇒ tb) ≟t Var _ = no (λ ())

vars : 𝕋 → 𝕍ars
vars (Con _)   = []
vars (Var v)   = [ v ]
vars (ta ⇒ tb) = union (vars ta) (vars tb)

varsP : 𝕋𝕋 → 𝕍ars
varsP (t , t') = union (vars t) (vars t')

numVars : 𝕋 → ℕ
numVars = length ∘ vars

numVarsP : 𝕋𝕋 → ℕ
numVarsP (Var _ , _)     = 1
numVarsP (_     , Var _) = 1
numVarsP _               = 0

numVarsL : 𝕋𝕋s → ℕ 
-- numVarsL = length ∘ concat ∘ map varsP 
numVarsL [] = 0
numVarsL (p ∷ x) = numVarsP p + numVarsL x

numConstructors : 𝕋 → ℕ
numConstructors (Con _)   = 1
numConstructors (Var _)   = 0
numConstructors (ta ⇒ tb) = 1 + numConstructors ta + numConstructors tb

numConstructorsP : 𝕋𝕋 → ℕ
numConstructorsP (Con _ , Con _)       = 1
numConstructorsP (Con _ , _)           = 0
numConstructorsP (Var _ , _)           = 0
numConstructorsP (ta ⇒ tb , ta' ⇒ tb') = 1 + numConstructorsP (ta , ta') + numConstructorsP (tb , tb')
numConstructorsP (_ ⇒ _ , _)           = 0

numConstructorsLP : 𝕋𝕋s → ℕ
-- numConstructorsLP = sum ∘ map numConstructorsP 
numConstructorsLP []              = 0
numConstructorsLP ((t , t') ∷ x)  = numConstructorsP (t , t') + numConstructorsLP x