T1649WorkTypes.hs

{-# LANGUAGE RankNTypes      #-}
{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-@ LIQUID "--reflection" @-} 
-- Z3 encoding cannot be used until this is fixed: 
-- https://github.com/Z3Prover/z3/issues/3930
{- LIQUID "--no-adt"         @-} 
{-@ LIQUID "--ple-local"      @-} 

module Properties where 


{-@ assume injectiveEqRTFun :: x:(a->b) -> y:(a->b) -> d:{EqRT (a->b) {x} {y} | isEqFun d} 
                         -> {x = eqFunX d && y = eqFunY d} @-}
injectiveEqRTFun :: (a->b) -> (a->b) -> EqT (a->b) -> () 
injectiveEqRTFun _ _ _ = () 

{-@ measure isEqFun @-}
isEqFun :: EqT a -> Bool 
isEqFun (EqFun _ _ _) = True 
isEqFun _             = False 

{-@ reflect eqFunX @-}
{-@ eqFunX :: {d:EqT (a -> b) | isEqFun d} -> (a -> b) @-}
eqFunX :: EqT (a -> b) ->  (a -> b) 
eqFunX (EqFun x _ _) = x 

{-@ reflect eqFunY @-}
{-@ eqFunY :: {d:EqT (a -> b) | isEqFun d} -> (a -> b) @-}
eqFunY :: EqT (a -> b) ->  (a -> b) 
eqFunY (EqFun _ y _) = y 


{-@ ple     eqFunP @-}
{- reflect eqFunP @-}
-- STATUS: assertion passes, but result type still fails 
{-@ eqFunP :: d:{EqT (a -> b) | isEqFun d} -> x:a -> EqT b @-}
eqFunP :: EqT (a -> b) ->  a -> EqT b
eqFunP (EqFun f g p) x = assert (eqT (f x) (g x)) (p x)  


assert :: Bool -> a -> a 
{-@ assert :: {b:Bool | b} -> x:a -> {v:a | v == x && b} @-}
assert _ x = x 

{-@ assume eqT :: x:a -> y:a -> {v:Bool | v <=> eqT x y} @-}
eqT :: a -> a -> Bool 
eqT = undefined 


{-@ measure eqT :: a -> a -> Bool @-}
{-@ type EqRT a E1 E2 = {v:EqT a | eqT E1 E2} @-}


data EqT  :: * -> *  where 
   EqSMT  :: Eq a => a -> a -> (a -> [a]) -> EqT a 
   EqFun  :: (a -> b) -> (a -> b) -> (a -> EqT b) -> EqT (a -> b)

{-@ data EqT  :: * -> *  where 
        EqSMT  :: Eq a => x:a -> y:a -> (a -> {v:[a] | 0 < len v}) -> EqRT a {x} {y}
      | EqFun  :: ff:(a -> b) -> gg:(a -> b) -> (x:a -> {d:EqT b | eqT (ff x) (gg x)}) -> EqRT (a -> b) {ff} {gg}
@-}