Fixme.hs

{-@ LIQUID "--reflection"  @-}
{-@ LIQUID "--ple"         @-}
{-@ LIQUID "--no-totality" @-} 

module Fixme where 

import Language.Haskell.Liquid.ProofCombinators


bool1, bool2 :: Bool 
bool1 = undefined -- not supported by the plugin, but ok for the old LH
bool2 = undefined -- if changed to True it is ok by the plugin as well

{-
bool1 = True 
bool2 = True
-}

class Eq a => EqAdequate a where 
  toSMT :: a -> a -> PBEq a -> () 

{-@ class Eq a => EqAdequate a where 
  toSMT :: x:a -> y:a -> PEq a {x} {y} -> {x = y} @-}

instance EqAdequate Bool where 

data PBEq a
{-@ measure eqT :: a -> a -> Bool @-}
{-@ type PEq a E1 E2 = {v:PBEq a | eqT E1 E2} @-}
{-@ cEq  :: x:a -> y:a -> PEq a {x} {y} -> ctx:(a -> b) -> PEq b {ctx x} {ctx y} @-}
cEq  :: a -> a -> PBEq a -> (a -> b) -> PBEq b
cEq = undefined 

{-@ critical :: {x:a | slowSpec x } -> a @-}
critical :: a -> a 
critical x = x 

{-@ bar :: PEq (a -> Bool) {fastSpec} {slowSpec} -> a -> Maybe a @-}
bar :: PBEq (a -> Bool) -> a -> Maybe a 
bar pf x = if fastSpec x ? toSMT (fastSpec x) (slowSpec x) (unExt fastSpec slowSpec  pf x)
            then Just (critical x)
            else Nothing 

{-@ unExt :: f:(a -> b) -> g:(a -> b) -> PEq (a -> b) {f} {g} -> x:a -> PEq b {f x} {g x} @-}
unExt :: (a -> b) -> (a -> b) -> PBEq (a -> b) -> a -> PBEq b 
unExt f g p x = cEq f g p (flip' x) ? flip' x f ? flip' x g 

{-@ reflect flip' @-}
flip' :: a -> (a -> b) -> b
flip' x f = f x  


{-@ reflect fastSpec @-}
fastSpec :: a -> Bool
fastSpec _ = bool1

{-@ reflect slowSpec @-}
slowSpec :: a -> Bool
slowSpec _ = bool2