RefinedEquality.hs

{-@ LIQUID "--reflection" @-} 
{-@ LIQUID "--no-adt"     @-} 
{-@ LIQUID "--ple"        @-} 
{-@ LIQUID "--typeclass"  @-} 

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module RefinedEquality
--   ( EqT(..), BEq(..)
-- --   , eqRTCtx
-- --   , eqFun
--   , deqFun
--   , eqSMT
--   ) where 
  where 

import Language.Haskell.Liquid.ProofCombinators 

{-@ measure eqT :: a -> a -> Bool @-}
{-@ type EqRT a E1 E2 = {v:EqT a | eqT E1 E2} @-}
-- 
-- 
-- {-@ _eqRTCtx :: x:a -> y:a -> EqRT a {x} {y} -> ctx:(a -> b) -> EqRT b {ctx x} {ctx y}  @-}
-- _eqRTCtx ::  a -> a -> EqT a -> (a -> b) -> EqT b
-- _eqRTCtx = EqCtx  
-- 
-- 
-- {-@ ignore deqFun @-}
-- {-@ deqFun :: forall<p :: a -> b -> Bool>. f:(a -> b) -> g:(a -> b) 
--           -> (x:a -> EqRT b<p x> {f x} {g x}) -> EqRT (y:a -> b<p y>) {f} {g}  @-}
-- deqFun :: (a -> b) -> (a -> b) -> (a -> EqT b) -> EqT (a -> b)
-- deqFun = EqFun
-- 
-- {-@ _eqFun :: f:(a -> b) -> g:(a -> b) 
--           -> (x:a -> EqRT b {f x} {g x}) -> EqRT (a -> b) {f} {g}  @-}
-- _eqFun :: (a -> b) -> (a -> b) -> (a -> EqT b) -> EqT (a -> b)
-- _eqFun = EqFun
-- 
-- {-@ ignore eqSMT @-}
-- {-@ assume eqSMT :: forall <p :: a -> Bool>. BEq a => x:a<p> -> y:a<p> -> {v:() | bEq x y} -> EqRT (a<p>) {x} {y} @-}
-- eqSMT :: BEq a => a -> a -> () -> EqT a
-- eqSMT x y p = EqSMT x y p 
-- 
-- 
data EqT  :: * -> *  where 
   EqSMT  :: BEq a => a -> a -> () -> EqT a 
   EqFun  :: (a -> b) -> (a -> b) -> (a -> EqT b) -> EqT (a -> b)
   EqCtx  :: a -> a -> EqT a -> (a -> b) -> EqT b 


{-@ data EqT  :: * -> *  where 
        EqSMT  :: BEq a => x:a -> y:a -> {v:() | bEq x y} -> EqRT a {x} {y}
     |  EqFun  :: ff:(a -> b) -> gg:(a -> b) -> (x:a -> EqRT b {ff x} {gg x}) -> EqRT (a -> b) {ff} {gg}
     |  EqCtx  :: x:a -> y:a -> EqRT a {x} {y} -> ctx:(a -> b) -> EqRT b {ctx x} {ctx y} 
@-}   

-- class BEq a 
class BEq a where 
  {-@ bEq    :: x:a -> y:a -> Bool @-}
  bEq    :: a -> a -> Bool 
  {-@ reflP  :: x:a -> {bEq x x} @-}
  reflP  :: a -> ()
  symmP  :: a -> a -> ()
  {-@ symmP  :: x:a -> y:a -> { bEq x y => bEq y x } @-}
  transP :: a -> a -> a -> ()
  {-@ transP :: x:a -> y:a -> z:a -> { ( bEq x y && bEq y z) => bEq x z } @-}



-- instance BEq Integer where 
--   bEq = bEqInteger
--   reflP x = const () (bEqInteger x x)     
--   symmP x y  = () `const` (bEqInteger x y)   
--   transP x y z = () `const` (bEqInteger x y)   
-- 
-- 
-- instance BEq a => BEq [a] where 
--   bEq    = bEqList' 
--   reflP  = undefined  
--   symmP  = symmList 
--   transP = undefined 
-- 
-- 
-- {-@ assume bEqList' :: BEq a => xs:[a] -> ys:[a] -> {v:Bool | (v <=> bEq xs ys) && (v <=> bEqList xs ys) } @-}
-- bEqList' :: BEq a => [a] -> [a] -> Bool 
-- bEqList' = bEqList 
-- 
-- {-@ reflect bEqList @-}
-- bEqList :: BEq a => [a] -> [a] -> Bool 
-- bEqList [] [] = True 
-- bEqList (x:xs) (y:ys) = bEq x y && bEqList xs ys 
-- bEqList _ _ = False  
-- 
-- {-@ reflList :: BEq a => xs:[a] -> {bEq xs xs} @-}
-- reflList :: BEq a => [a] -> ()
-- reflList x@[]    = () `const` bEqList x x `const` bEqList' x x
-- {- reflList (x:xs) = undefined 
--   bEq (x:xs) (x:xs) ==. 
--   bEqList' (x:xs) (x:xs) ==. 
--   bEqList (x:xs) (x:xs) ==.
--   (bEq x x && bEqList xs xs)
--     ? reflP x ==.
--   bEqList xs xs ==. 
--   bEqList' xs xs 
--     ? reflList xs ==. 
--   True *** QED 
-- -}
-- 
-- {-@ symmList :: BEq a => xs:[a] -> ys:[a] -> {bEq xs ys => bEq ys xs} @-}
-- symmList :: BEq a => [a] -> [a] -> ()
-- symmList = undefined 
-- 
-- 
-- {-@ assume bEqInteger :: x:Integer -> y:Integer -> {v:Bool | (v <=> bEq x y) && (v <=> x = y)} @-} 
-- bEqInteger :: Integer -> Integer -> Bool 
-- bEqInteger x y = x == y