{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
-- For `axiom`
{-# OPTIONS_GHC -Wno-deprecations #-}

module Logic.Theory.List (
  type ListNil (),
  listNil,
  type ListCons (),
  listCons,
  listSingleton,
  type ListHead,
  listHead,
  type ListNull,
  listNull,
  type ListLength (),
  listLength,
  type ListConcat (),
  listConcat,
  type ListReverse (),
  listReverse,
) where

import Control.Applicative (Applicative (..))
import Data.Bool (Bool)
import Data.Bool qualified as Bool
import Data.Either (Either (..))
import Data.Int (Int)
import Data.List qualified as List

import Logic.Kernel
import Logic.Theory.Arithmetic
import Logic.Theory.Eq
import Logic.Theory.Ord

data ListNil = ListNilAxiom
listNil :: ListNil ::: [a]
listNil = ListNilAxiom ... []
{-# INLINE listNil #-}

instance Axiom (ListLength ListNil <-> Zero)

data ListCons x xs = ListConsAxiom
type role ListCons nominal nominal
listCons :: x ::: a -> xs ::: [a] -> ListCons x xs ::: [a]
listCons (Named x) (Named xs) = ListConsAxiom ... (x : xs)
{-# INLINE listCons #-}

listSingleton :: x ::: a -> ListCons x ListNil ::: [a]
listSingleton x = listCons x listNil
{-# INLINE listSingleton #-}

type ListConsLength x xs a = ListLength (ListCons x xs ::: [a]) == Succ (ListLength xs)
instance Axiom (ListConsLength x xs a)

data ListHead xs = ListHeadAxiom
listHead :: xs ::: [a] / (Zero < ListLength xs) -> ListHead xs ::: a
listHead (Named xs) = ListHeadAxiom ... List.head xs
{-# INLINE listHead #-}

data ListNull xs = ListNullAxiom
data ListFull xs = ListFullAxiom

type role ListNull nominal
listNull :: xs ::: [a] -> ListNull xs ::: Bool
listNull (Named xs) = ListNullAxiom ... List.null xs
{-# INLINE listNull #-}

instance Axiom (ListNull xs <-> ListLength xs == Zero)
instance Axiom (ListFull xs <-> ListLength xs > Zero)

instance Provable (ListNull xs ::: Bool) where
  type
    ProofOf (ListNull xs ::: Bool) =
      Either
        (Proof (ListLength xs > Zero))
        (Proof (ListLength xs == Zero))
  prove (Named b) = case b of
    Bool.False ->
      Left
        ( liftA2
            (-->)
            (axiom @(ListFull xs <-> ListLength xs > Zero))
            (proven ListFullAxiom)
        )
    Bool.True ->
      Right
        ( liftA2
            (-->)
            (axiom @(ListNull xs <-> ListLength xs == Zero))
            (proven ListNullAxiom)
        )

data ListLength xs = ListLengthAxiom
type role ListLength nominal
listLength :: xs ::: [a] -> ListLength xs ::: Int
listLength (Named xs) = ListLengthAxiom ... List.length xs
{-# INLINE listLength #-}
instance Axiom (ListLength xs ::: Int -> ListLength xs >= Zero)

data ListConcat xs ys = ListConcatAxiom
type role ListConcat nominal nominal
listConcat :: xs ::: [a] -> ys ::: [a] -> ListConcat xs ys ::: [a]
listConcat (Named xs) (Named ys) = ListConcatAxiom ... xs List.++ ys
{-# INLINE listConcat #-}
instance Axiom (Associative ListConcat xs ys zs)

data ListReverse xs = ListReverseAxiom
type role ListReverse nominal
listReverse :: xs ::: [a] -> ListReverse xs ::: [a]
listReverse (Named xs) = ListReverseAxiom ... List.reverse xs
{-# INLINE listReverse #-}
instance Axiom (ListReverse (ListReverse xs) <-> xs)