-- For `proven`
{-# LANGUAGE BangPatterns #-}
-- For `Exists`
{-# LANGUAGE ExistentialQuantification #-}
-- For `Exists` instances
{-# LANGUAGE QuantifiedConstraints #-}
-- For `(=:)`
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
-- For `UnNamed` and `Exists` instances
{-# LANGUAGE UndecidableInstances #-}
-- For `letSymbol`
-- {-# LANGUAGE AllowAmbiguousTypes #-}
-- For pattern `Named`
{-# LANGUAGE ViewPatterns #-}

module Logic.Kernel (
  type (:::) (),
  pattern Named,
  (...),
  unitName,
  type UnNamed,
  type UnName,
  unName,
  letName,
  letName2,
  letName3,
  letName4,
  liftName,
  liftName2,
  liftName3,
  liftName4,
  -- letSymbol,
  namedAs,
  (=:),
  type Proof (),
  proven,
  implies,
  unImplies,
  type Provable (..),
  type Axiom (..),
  type Lemma (..),
  type SuchThat (),
  type (/),
  (/),
  suchThatProof,
  type That (..),
  type (<->),
  (-->),
  (<--),
  type Exists (..),
  type EqUnNamed,
  type Commutative,
  type Associative,
  type RefHoTTBook,
) where

import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Data.Eq (Eq (..))
import Data.Function ((.))
import Data.Functor (Functor (..))
import Data.Ord (Ord (..))
import Data.Tuple (fst, snd)
import Text.Show (Show (..), showParen, showString)
import Type.Reflection (Typeable, typeRep)

-- | A value of type @(a `:::` name)@ has the same runtime
-- representation as a value of type @a@, with a nominal "name" attached.
--
-- The newtype constructor of `(:::)` is not exported
-- as it would break the "smart constructor" confidence.
newtype (:::) name a = NameAxiom a
  deriving (Eq, Ord)

instance Show a => Show (name ::: a) where
  showsPrec p (NameAxiom a) = showsPrec p a

type role (:::) nominal representational
infixr 9 :::

-- | A safe pattern matcher to unwrap a name attached with `(:::)`.
pattern Named :: UnName a => UnNamed a -> a
pattern Named x <- (unName -> x)

{-# COMPLETE Named #-}

-- | Attach a name to a value of type @(a)@.
-- This name must be inhabited,
-- it means that if it's a data or newtype constructor,
-- attaching such a name can be restricted to a module's boundary
-- by not exporting that constructor out of that module.
(...) :: name -> a -> name ::: a
(...) _ = NameAxiom

infix 0 ...

{-# INLINE (...) #-}

unitName :: a -> () ::: a
unitName = NameAxiom
{-# INLINE unitName #-}

-- | Unwrap `(:::)` at the type-level.
--
-- This is not recursive like `coerce` would.
type family UnNamed a where
  UnNamed (n ::: a) = a
  UnNamed (SuchThat a p) = UnNamed a
  UnNamed (That a pred x) = UnNamed (() ::: a `SuchThat` pred ())
  UnNamed a = a

-- | Unwrap `(:::)` at the value-level.
--
-- Note: this is not recursive like `Data.Coerce.coerce`.
class UnName a where
  unName :: a -> UnNamed a

instance {-# OVERLAPS #-} UnName (n ::: a) where
  unName (NameAxiom a) = a
  {-# INLINE unName #-}
instance {-# OVERLAPS #-} UnName a => UnName (SuchThat a p) where
  unName (SuchThat a) = unName a
  {-# INLINE unName #-}
instance {-# OVERLAPS #-} UnName a => UnName (That a pred x) where
  unName (That a) = unName a
  {-# INLINE unName #-}
instance UnNamed a ~ a => UnName a where
  unName a = a
  {-# INLINE unName #-}

-- | Introduce a name for the argument,
-- and pass the named argument into the given function.
letName :: a -> (forall x. x ::: a -> res) -> res
letName x k = k (NameAxiom x)
{-# INLINE letName #-}

infixr 0 `letName`

-- | Introduce names for two arguments,
-- and pass the named arguments into the given function.
letName2 :: a -> b -> (forall x y. x ::: a -> y ::: b -> res) -> res
letName2 x y k = k (NameAxiom x) (NameAxiom y)
{-# INLINE letName2 #-}

infixr 0 `letName2`

-- | Introduce names for three arguments,
-- and pass the named arguments into the given function.
letName3 :: a -> b -> c -> (forall x y z. x ::: a -> y ::: b -> z ::: c -> res) -> res
letName3 x y z k = k (NameAxiom x) (NameAxiom y) (NameAxiom z)
{-# INLINE letName3 #-}

infixr 0 `letName3`

-- | Introduce names for four arguments,
-- and pass the named arguments into the given function.
letName4 :: a -> b -> c -> d -> (forall x y z w. x ::: a -> y ::: b -> z ::: c -> w ::: d -> res) -> res
letName4 x y z w k = k (NameAxiom x) (NameAxiom y) (NameAxiom z) (NameAxiom w)
{-# INLINE letName4 #-}

infixr 0 `letName4`

-- \| Injects a `Symbol` into a `Type` for `letSymbol`.
-- data Name (s :: Symbol)

-- \| Like `letName` but with a `Symbol` hint and a `Typeable` constraint
-- enabling to `show` @(name)@.
-- letSymbol :: forall (s :: Symbol) a res. KnownSymbol s => a -> (forall name. Typeable name => name ::: a -> res) -> res
-- letSymbol a k =
--  let n = hashUnique (unsafePerformIO newUnique)
--  in case someSymbolVal (symbolVal (Proxy @s) <> show n) of
--      SomeSymbol (Proxy :: Proxy n) ->
--        k @(Name n) (NameAxiom a)

-- | Infix alias to `letName`.
namedAs :: a -> (forall name. name ::: a -> res) -> res
namedAs a k = k (NameAxiom a)
{-# INLINE namedAs #-}

infixr 0 `namedAs`

-- | Introduce a name for the argument,
-- and pass the named argument into the given function.
liftName :: (forall x. x ::: a -> res) -> a -> res
liftName k x = k (NameAxiom x)
{-# INLINE liftName #-}

infixr 0 `liftName`

-- | Introduce names for two arguments,
-- and pass the named arguments into the given function.
liftName2 :: (forall x y. x ::: a -> y ::: b -> res) -> a -> b -> res
liftName2 k x y = k (NameAxiom x) (NameAxiom y)
{-# INLINE liftName2 #-}

infixr 0 `liftName2`

-- | Introduce names for three arguments,
-- and pass the named arguments into the given function.
liftName3 :: (forall x y z. x ::: a -> y ::: b -> z ::: c -> res) -> a -> b -> c -> res
liftName3 k x y z = k (NameAxiom x) (NameAxiom y) (NameAxiom z)
{-# INLINE liftName3 #-}

infixr 0 `liftName3`

-- | Introduce names for four arguments,
-- and pass the named arguments into the given function.
liftName4 :: (forall x y z w. x ::: a -> y ::: b -> z ::: c -> w ::: d -> res) -> a -> b -> c -> d -> res
liftName4 k x y z w = k (NameAxiom x) (NameAxiom y) (NameAxiom z) (NameAxiom w)
{-# INLINE liftName4 #-}

infixr 0 `liftName4`

-- | Operator version of `letName`.
(=:) :: a -> (forall name. name ::: a -> res) -> res
(=:) a k = k (NameAxiom a)
{-# INLINE (=:) #-}

infixr 0 =:

-- | Here, a proposition in the logic side,
-- is a type in the programming side.
-- And a proven proposition is an inhabited type.
--
-- * `Logic.Name.RefHoTTBook`
-- * https://groups.seas.harvard.edu/courses/cs152/2016sp/lectures/lec16-curryhoward.pdf
-- * https://en.wikipedia.org/wiki/Type_inhabitation_problem
-- * https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
-- * https://ncatlab.org/nlab/show/propositions+as+types
data Proof proposition = ProofAxiom

instance Typeable p => Show (Proof p) where
  showsPrec p _ =
    showParen
      (prec < p)
      ( showString "Proof "
          . showsPrec prec (typeRep @p)
      )
    where
      prec = 10

proven :: a -> Proof a
proven !_ = ProofAxiom
{-# INLINE proven #-}

type role Proof nominal

instance Functor Proof where
  fmap _f !_ = ProofAxiom

instance Applicative Proof where
  -- Observing an instance of 'a'
  -- Therefore, an instance of 'a' exists.
  pure !_ = ProofAxiom
  (<*>) !_ !_ = ProofAxiom

instance Monad Proof where
  -- There exist a proof that proves the existence of a proof of 'a'
  -- Therefore, a proof of 'a' exists.
  !_ >>= !_ = ProofAxiom

-- | The implication in the logic side,
-- is the function type of the programming side.
implies :: (Proof p -> Proof q) -> Proof (p -> q)
implies !_ = ProofAxiom
{-# INLINE implies #-}

-- | modus ponens
unImplies :: Proof (p -> q) -> (Proof p -> Proof q)
unImplies = (<*>)
{-# INLINE unImplies #-}

-- | Reify a `Proof` or `(:::)` to inspect it.
class Provable a where
  type ProofOf a
  prove :: a -> ProofOf a

-- nameProof :: ProofOf n a -> n ::: a

class Axiom p where
  -- | CorrectnessWarning: the default definition declares an axiom.
  -- This is the only way to declare an axiom out of this module
  -- (except through `undefined` or `TemplateHaskell` if LANGUAGE Safe is not used).
  --
  -- Beware that `Axiom` instances can be hidden from the documentation
  -- when not exporting a type involved in defining them,
  -- however their do appear in:
  --
  -- @
  -- ghci> :info! Axiom
  -- @
  axiom :: Proof p
  axiom = ProofAxiom
{-# WARNING axiom "x-logic-axiom" #-}

class Lemma p where
  lemma :: Proof p

type (<->) p q = ((p -> q), (q -> p))
infix 0 <->

(-->) :: (<->) p q -> p -> q
(-->) = fst
infix 9 -->
{-# INLINE (-->) #-}

(<--) :: (<->) p q -> q -> p
(<--) = snd
infix 9 <--
{-# INLINE (<--) #-}

type Commutative op x y = op x y <-> op y x
type Associative op x y z = op (op x y) z <-> op x (op y z)

-- | Existential quantification.
data Exists p = forall x. Exists (p x)

instance (forall x. Show (p x)) => Show (Exists p) where
  showsPrec p (Exists px) = showsPrec p px

-- | Class alias working around the impossibility
-- to refer to the type family `UnNamed`
-- in the quantified constraint of the @(`Eq` (`Exists` p))@ instance.
--
-- IssueRef: https://gitlab.haskell.org/ghc/ghc/-/issues/14860#note_495352
class (Eq (UnNamed (p x)), UnName (p x), UnNamed (p x) ~ UnNamed (p y)) => EqUnNamed p x y

instance (Eq (UnNamed (p x)), UnName (p x), UnNamed (p x) ~ UnNamed (p y)) => EqUnNamed p x y

instance (forall x y. EqUnNamed p x y) => Eq (Exists p) where
  (==) (Exists (Named px)) (Exists (Named py)) = (==) px py

newtype SuchThat a p = SuchThat a
  deriving (Eq, Ord)
type role SuchThat representational nominal
infixr 0 `SuchThat`
instance Show a => Show (SuchThat a p) where
  showsPrec p (SuchThat a) = showsPrec p a

-- | Convenient alias to `SuchThat`.
type (/) = SuchThat

infixr 0 /

(/) :: a -> Proof p -> a `SuchThat` p
(/) a ProofAxiom = SuchThat a
{-# INLINE (/) #-}

suchThatProof :: a `SuchThat` p -> Proof p
suchThatProof SuchThat{} = ProofAxiom
{-# INLINE suchThatProof #-}

newtype That a p x = That (x ::: a `SuchThat` p x)
  deriving (Eq, Ord)
type role That representational nominal nominal
instance Show a => Show (That a p x) where
  showsPrec p (That a) = showsPrec p a

data RefHoTTBook
-- ^ Reference to [Homotopy Type Theory: Univalent Foundations of Mathematics](https://homotopytypetheory.org/book)
--
-- > [
-- >   {
-- >     "author": [
-- >       {
-- >         "family": "Univalent Foundations Program",
-- >         "given": "The"
-- >       }
-- >     ],
-- >     "id": "hottbook",
-- >     "issued": {
-- >       "date-parts": [
-- >         [
-- >           2013
-- >         ]
-- >       ]
-- >     },
-- >     "publisher": "https://homotopytypetheory.org/book",
-- >     "publisher-place": "Institute for Advanced Study",
-- >     "title": "Homotopy Type Theory: Univalent Foundations of Mathematics",
-- >     "title-short": "Homotopy Type Theory",
-- >     "type": "book"
-- >   }
-- > ]