src/Logic/Theory/List.hs

   1 {-# LANGUAGE RankNTypes #-}
   2 {-# LANGUAGE Safe #-}
   3 -- For `axiom`
   4 {-# OPTIONS_GHC -Wno-deprecations #-}
   5
   6 module Logic.Theory.List (
   7   type ListNil (),
   8   listNil,
   9   type ListCons (),
  10   listCons,
  11   listSingleton,
  12   type ListHead,
  13   listHead,
  14   type ListNull,
  15   listNull,
  16   type ListLength (),
  17   listLength,
  18   type ListConcat (),
  19   listConcat,
  20   type ListReverse (),
  21   listReverse,
  22 ) where
  23
  24 import Control.Applicative (Applicative (..))
  25 import Data.Bool (Bool)
  26 import Data.Bool qualified as Bool
  27 import Data.Either (Either (..))
  28 import Data.Int (Int)
  29 import Data.List qualified as List
  30
  31 import Logic.Kernel
  32 import Logic.Theory.Arithmetic
  33 import Logic.Theory.Eq
  34 import Logic.Theory.Ord
  35
  36 data ListNil = ListNilAxiom
  37 listNil :: ListNil ::: [a]
  38 listNil = ListNilAxiom ... []
  39 {-# INLINE listNil #-}
  40
  41 instance Axiom (ListLength ListNil <-> Zero)
  42
  43 data ListCons x xs = ListConsAxiom
  44 type role ListCons nominal nominal
  45 listCons :: x ::: a -> xs ::: [a] -> ListCons x xs ::: [a]
  46 listCons (Named x) (Named xs) = ListConsAxiom ... (x : xs)
  47 {-# INLINE listCons #-}
  48
  49 listSingleton :: x ::: a -> ListCons x ListNil ::: [a]
  50 listSingleton x = listCons x listNil
  51 {-# INLINE listSingleton #-}
  52
  53 type ListConsLength x xs a = ListLength (ListCons x xs ::: [a]) == Succ (ListLength xs)
  54 instance Axiom (ListConsLength x xs a)
  55
  56 data ListHead xs = ListHeadAxiom
  57 listHead :: xs ::: [a] / (Zero < ListLength xs) -> ListHead xs ::: a
  58 listHead (Named xs) = ListHeadAxiom ... List.head xs
  59 {-# INLINE listHead #-}
  60
  61 data ListNull xs = ListNullAxiom
  62 data ListFull xs = ListFullAxiom
  63
  64 type role ListNull nominal
  65 listNull :: xs ::: [a] -> ListNull xs ::: Bool
  66 listNull (Named xs) = ListNullAxiom ... List.null xs
  67 {-# INLINE listNull #-}
  68
  69 instance Axiom (ListNull xs <-> ListLength xs == Zero)
  70 instance Axiom (ListFull xs <-> ListLength xs > Zero)
  71
  72 instance Provable (ListNull xs ::: Bool) where
  73   type
  74     ProofOf (ListNull xs ::: Bool) =
  75       Either
  76         (Proof (ListLength xs > Zero))
  77         (Proof (ListLength xs == Zero))
  78   prove (Named b) = case b of
  79     Bool.False ->
  80       Left
  81         ( liftA2
  82             (-->)
  83             (axiom @(ListFull xs <-> ListLength xs > Zero))
  84             (proven ListFullAxiom)
  85         )
  86     Bool.True ->
  87       Right
  88         ( liftA2
  89             (-->)
  90             (axiom @(ListNull xs <-> ListLength xs == Zero))
  91             (proven ListNullAxiom)
  92         )
  93
  94 data ListLength xs = ListLengthAxiom
  95 type role ListLength nominal
  96 listLength :: xs ::: [a] -> ListLength xs ::: Int
  97 listLength (Named xs) = ListLengthAxiom ... List.length xs
  98 {-# INLINE listLength #-}
  99 instance Axiom (ListLength xs ::: Int -> ListLength xs >= Zero)
 100
 101 data ListConcat xs ys = ListConcatAxiom
 102 type role ListConcat nominal nominal
 103 listConcat :: xs ::: [a] -> ys ::: [a] -> ListConcat xs ys ::: [a]
 104 listConcat (Named xs) (Named ys) = ListConcatAxiom ... xs List.++ ys
 105 {-# INLINE listConcat #-}
 106 instance Axiom (Associative ListConcat xs ys zs)
 107
 108 data ListReverse xs = ListReverseAxiom
 109 type role ListReverse nominal
 110 listReverse :: xs ::: [a] -> ListReverse xs ::: [a]
 111 listReverse (Named xs) = ListReverseAxiom ... List.reverse xs
 112 {-# INLINE listReverse #-}
 113 instance Axiom (ListReverse (ListReverse xs) <-> xs)