module Interfaces.Verified

import Control.Algebra
import Control.Algebra.Lattice
import Control.Algebra.NumericImplementations
import Control.Algebra.VectorSpace
import Data.ZZ

%access public export

-- Due to these being basically unused and difficult to implement,
-- they're in contrib for a bit. Once a design is found that lets them
-- be implemented for a number of implementations, and we get those
-- implementations, then some of them can move back to base (or even
-- prelude, in the cases of Functor, Applicative, Monad, Semigroup,
-- and Monoid).

interface Functor f => VerifiedFunctor (f : Type -> Type) where
  functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x
  functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
                       (g1 : a -> b) -> (g2 : b -> c) ->
                       map (g2 . g1) x = (map g2 . map g1) x

VerifiedFunctor Maybe where
  functorIdentity Nothing = Refl
  functorIdentity (Just x) = Refl
  functorComposition Nothing g1 g2 = Refl
  functorComposition (Just x) g1 g2 = Refl

interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
  applicativeMap : (x : f a) -> (g : a -> b) ->
                   map g x = pure g <*> x
  applicativeIdentity : (x : f a) -> pure Basics.id <*> x = x
  applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
                           ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)
  applicativeHomomorphism : (x : a) -> (g : a -> b) ->
                            (<*>) {f} (pure g) (pure x) = pure {f} (g x)
  applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
                           g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g

VerifiedApplicative Maybe where
  applicativeMap Nothing g = Refl
  applicativeMap (Just x) g = Refl
  applicativeIdentity Nothing = Refl
  applicativeIdentity (Just x) = Refl
  applicativeComposition Nothing Nothing Nothing = Refl
  applicativeComposition Nothing Nothing (Just x) = Refl
  applicativeComposition Nothing (Just x) Nothing = Refl
  applicativeComposition Nothing (Just x) (Just y) = Refl
  applicativeComposition (Just x) Nothing Nothing = Refl
  applicativeComposition (Just x) Nothing (Just y) = Refl
  applicativeComposition (Just x) (Just y) Nothing = Refl
  applicativeComposition (Just x) (Just y) (Just z) = Refl
  applicativeHomomorphism x g = Refl
  applicativeInterchange x Nothing = Refl
  applicativeInterchange x (Just y) = Refl

interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
  monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
                     mf <*> mx = mf >>= \f =>
                                 mx >>= \x =>
                                        pure (f x)
  monadLeftIdentity : (x : a) -> (f : a -> m b) -> pure x >>= f = f x
  monadRightIdentity : (mx : m a) -> mx >>= Applicative.pure = mx
  monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
                       (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

VerifiedMonad Maybe where
    monadApplicative Nothing Nothing = Refl
    monadApplicative Nothing (Just x) = Refl
    monadApplicative (Just x) Nothing = Refl
    monadApplicative (Just x) (Just y) = Refl
    monadLeftIdentity x f = Refl
    monadRightIdentity Nothing = Refl
    monadRightIdentity (Just x) = Refl
    monadAssociativity Nothing f g = Refl
    monadAssociativity (Just x) f g = Refl

interface Semigroup a => VerifiedSemigroup a where
  total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

implementation VerifiedSemigroup (List a) where
  semigroupOpIsAssociative = appendAssociative

[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
  semigroupOpIsAssociative = plusAssociative

[MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where
  semigroupOpIsAssociative = multAssociative

[PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where
  semigroupOpIsAssociative = plusAssociativeZ

[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
  semigroupOpIsAssociative = multAssociativeZ

interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
  total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
  total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
   monoidNeutralIsNeutralL = plusZeroRightNeutral
   monoidNeutralIsNeutralR = plusZeroLeftNeutral

[MultNatMonoidV] VerifiedMonoid Nat using MultNatSemiV, MultNatMonoid where
  monoidNeutralIsNeutralL = multOneRightNeutral
  monoidNeutralIsNeutralR = multOneLeftNeutral

[PlusZZMonoidV] VerifiedMonoid ZZ using PlusZZSemiV, PlusZZMonoid where
   monoidNeutralIsNeutralL = plusZeroRightNeutralZ
   monoidNeutralIsNeutralR = plusZeroLeftNeutralZ

[MultZZMonoidV] VerifiedMonoid ZZ using MultZZSemiV, MultZZMonoid where
  monoidNeutralIsNeutralL = multOneRightNeutralZ
  monoidNeutralIsNeutralR = multOneLeftNeutralZ

implementation VerifiedMonoid (List a) where
  monoidNeutralIsNeutralL = appendNilRightNeutral
  monoidNeutralIsNeutralR xs = Refl

interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
  total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
  total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

VerifiedGroup ZZ using PlusZZMonoidV where
  groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
                             rewrite multNegLeftZ 0 k in
                             rewrite multOneLeftNeutralZ k in
                             plusNegateInverseLZ k
  groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
                             rewrite multNegLeftZ 0 k in
                             rewrite multOneLeftNeutralZ k in
                             plusNegateInverseRZ k

interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
  total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

VerifiedAbelianGroup ZZ where
  abelianGroupOpIsCommutative = plusCommutativeZ

interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
  total ringOpIsAssociative   : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
  total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
  total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

VerifiedRing ZZ where
  ringOpIsAssociative = multAssociativeZ
  ringOpIsDistributiveL = multDistributesOverPlusRightZ
  ringOpIsDistributiveR = multDistributesOverPlusLeftZ

interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
  total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
  total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

VerifiedRingWithUnity ZZ where
  ringWithUnityIsUnityL = multOneRightNeutralZ
  ringWithUnityIsUnityR = multOneLeftNeutralZ

interface JoinSemilattice a => VerifiedJoinSemilattice a where
  total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
  total joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l
  total joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e

interface MeetSemilattice a => VerifiedMeetSemilattice a where
  total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
  total meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l
  total meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e