PNat.hs

{-# LANGUAGE RankNTypes #-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--typeclass" @-}
{-@ LIQUID "--aux-inline" @-}
{-@ LIQUID "--ple" @-}

module PNat where

import           Prelude                 hiding ( Semigroup(..)
                                                , Monoid(..)
                                                , foldr
                                                , head
                                                , flip
                                                , tail
                                                , Maybe (..)
                                                , Foldable (..)
                                                )

import Semigroup
import Lib

data PNat = Z | S PNat

instance Semigroup PNat where
  mappend Z     n = n
  mappend (S m) n = S (mappend m n)

  sconcat (NonEmpty h t) = foldlList mappend h t

instance VSemigroup PNat where
  lawAssociative Z     _ _ = ()
  lawAssociative (S p) m n = lawAssociative p m n
  lawSconcat (NonEmpty h t) = ()

instance Monoid PNat where
  mempty = Z
  mconcat xs = foldrList mappend mempty xs

instance VMonoid PNat where
  lawEmpty Z     = ()
  lawEmpty (S m) = lawEmpty m
  lawMconcat _ = ()



instance Semigroup (List a) where
  mappend Nil l2 = l2
  mappend (Cons h l1) l2 = Cons h (mappend l1 l2)
  sconcat (NonEmpty h t) = foldlList mappend h t

instance VSemigroup (List a) where
  lawAssociative Nil y z = ()
  lawAssociative (Cons _ x) y z = lawAssociative x y z
  lawSconcat (NonEmpty h t) = ()

instance Monoid (List a) where
  mempty = Nil
  mconcat xs = foldrList mappend mempty xs

instance VMonoid (List a) where
  lawEmpty Nil = ()
  lawEmpty (Cons _ t) = lawEmpty t
  lawMconcat _ = ()