{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}

-- |

-- Module      : OAlg.Data.EqualExtensional

-- Description : extensional equality.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- extensional equality.

module OAlg.Data.EqualExtensional
  ( EqExt(..), prpEqualExt
  )
  where

import OAlg.Data.Show
import OAlg.Data.X
import OAlg.Data.Equal
import OAlg.Data.Statement.Definition

--------------------------------------------------------------------------------

-- EqExt -


infix 4 .=.

-- | extensional equality for two parameterized types.

--

-- __Properties__ Let @'EqExt' __c__@ then for all @__x__@, @__y__@ holds:

--

-- (1) For all @f@ in @__c x y__@ holdst: @f '.=.' f@.

--

-- (2) For all @f@, @g@ in @__c x y__@ holdst: If @f '.=.' g@ then holds

-- @g '.=.' f@.

--

-- (3) For all @f@, @g@ and @h@ in @__c x y__@ holds: If @f '.=.' g@ and @g '.=.' h@ then

-- @f '.=.' h@.

class EqExt c where
  -- | equality statement of two objects.

  (.=.) :: c x y -> c x y -> Statement
  default (.=.) :: Eq2 c => c x y -> c x y -> Statement
  c x y
f .=. c x y
g = c x y -> c x y -> Bool
forall x y. c x y -> c x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 c x y
f c x y
g Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []

--------------------------------------------------------------------------------

-- prpEqualExt -


-- | validity for two functions being __/extensional equal/__, i.e. for all @f@ and @g@ in

-- @__x__ -> __y__@ and @x@ in @__x__@ holds: @f x '==' g y@.

prpEqualExt :: (Show x, Eq y) => X x -> (x -> y) -> (x -> y) -> Statement
prpEqualExt :: forall x y.
(Show x, Eq y) =>
X x -> (x -> y) -> (x -> y) -> Statement
prpEqualExt X x
xx x -> y
f x -> y
g = String -> Label
Prp String
"ExtensionalEqual" Label -> Statement -> Statement
:<=>: X x -> (x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X x
xx
  (\x
x -> (x -> y
f x
x y -> y -> Bool
forall a. Eq a => a -> a -> Bool
== x -> y
g x
x) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
  )