VerifiedMonoid.hs

module Data.Monoid where

{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--exactdc" @-}
{-@ LIQUID "--totality" @-}

import Prelude hiding (Monoid (..))

import Language.Haskell.Liquid.ProofCombinators


class VerifiedMonoid a where
  mempty  :: a

  mappend :: a -> a -> a

  leftId  :: a -> Proof
  rightId :: a -> Proof
  assoc   :: a -> a -> a -> Proof

{-@ class VerifiedMonoid a where
    mempty  :: a
    mappend :: a -> a -> a
    leftId  :: x:a -> {v:Proof | mappend mempty x = x }
    rightId :: x:a -> {v:Proof | mappend x mempty = x }
    assoc   :: x:a -> y:a -> z:a -> {v:Proof | mappend x (mappend y z) = mappend (mappend x y) z}
  @-}

-- TODO
-- The above should change to explicitely reflect mappend and mempty.
-- Then, each instance should generate the code at the end of this file.


{-@ data List a = N | C {hd :: a, tl :: List a} @-}
data List a = N | C a (List a)



instance VerifiedMonoid (List a) where
  mempty              = N
  mappend N ys        = ys
  mappend (C x xs) ys = C x (mappend xs ys)

  leftId  x           = mappend mempty x ==. mappend N x ==. x *** QED


  rightId N           = mappend N mempty ==. mappend N N ==. N *** QED
  rightId (C x xs)    = mappend (C x xs) mempty ==. C x (mappend xs N ) ==. C x xs ? rightId xs *** QED


  assoc N ys zs
    =   mappend N (mappend ys zs)
    ==. mappend ys zs
    ==. mappend (mappend N ys) zs
    *** QED
  assoc (C x xs) ys zs
    =   mappend (C x xs) (mappend ys zs)
    ==. C x (mappend xs (mappend ys zs))
    ==. C x (mappend (mappend xs ys) zs)
    ==. mappend (C x (mappend xs ys)) zs
    ==. mappend (mappend (C x xs) ys) zs
    *** QED



-- || Below specs should be automatically generated by the reflect annotations
-- || in the class definition

-- | 1. One uninterpreted function per class method so that proof obligations type check

{-@ measure mappend :: a -> a -> a @-}
{-@ measure mempty  :: a @-}

-- | 1. One uninterpreted function is generated for each reflected function


{-@ measure mappendList :: List a -> List a -> List a @-}
{-@ measure memptyList  :: List a @-}


-- | 2. The reflected methods are reflected in the result type as assumed types,
-- |    and the proof obligations are copied to the proof methods.

{-@ instance VerifiedMonoid (List a) where
  assume mempty  :: {v:List a | (v = N) && (v = memptyList) };
  assume mappend :: {v:(x:List a -> y:List a
                 -> {v:List a | (v = mappendList x y) && (if (is$Data.Monoid.N x) then (v == y) else (v == C (lqdc##select##C##1 x) (mappendList (lqdc##select##C##2 x) y) )) })  | v == mappendList};
  leftId  :: x:List a -> {v:Proof | mappendList memptyList x = x } ;
  rightId :: x:List a -> {v:Proof | mappendList x memptyList = x } ;
  assoc   :: x:List a -> y:List a -> z:List a -> {v:Proof | mappendList x (mappendList y z) = mappendList (mappendList x y) z}
  @-}