{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators, DeriveTraversable #-}
module QuickSpec.Internal.Prop where

import Data.Bool (bool)
import Control.Monad
import qualified Data.DList as DList
import Data.Ord
import QuickSpec.Internal.Type
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Term hiding (first)
import GHC.Generics(Generic)
import qualified Data.Map.Strict as Map
import Control.Monad.Trans.State.Strict
import Data.List
import Control.Arrow (first)

data Prop a =
  (:=>:) {
    forall a. Prop a -> [Equation a]
lhs :: [Equation a],
    forall a. Prop a -> Equation a
rhs :: Equation a }
  deriving (Int -> Prop a -> ShowS
forall a. Show a => Int -> Prop a -> ShowS
forall a. Show a => [Prop a] -> ShowS
forall a. Show a => Prop a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop a] -> ShowS
$cshowList :: forall a. Show a => [Prop a] -> ShowS
show :: Prop a -> String
$cshow :: forall a. Show a => Prop a -> String
showsPrec :: Int -> Prop a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Prop a -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Prop a) x -> Prop a
forall a x. Prop a -> Rep (Prop a) x
$cto :: forall a x. Rep (Prop a) x -> Prop a
$cfrom :: forall a x. Prop a -> Rep (Prop a) x
Generic, forall a b. a -> Prop b -> Prop a
forall a b. (a -> b) -> Prop a -> Prop b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Prop b -> Prop a
$c<$ :: forall a b. a -> Prop b -> Prop a
fmap :: forall a b. (a -> b) -> Prop a -> Prop b
$cfmap :: forall a b. (a -> b) -> Prop a -> Prop b
Functor, Functor Prop
Foldable Prop
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Prop (m a) -> m (Prop a)
forall (f :: * -> *) a. Applicative f => Prop (f a) -> f (Prop a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Prop a -> m (Prop b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Prop a -> f (Prop b)
sequence :: forall (m :: * -> *) a. Monad m => Prop (m a) -> m (Prop a)
$csequence :: forall (m :: * -> *) a. Monad m => Prop (m a) -> m (Prop a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Prop a -> m (Prop b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Prop a -> m (Prop b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Prop (f a) -> f (Prop a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Prop (f a) -> f (Prop a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Prop a -> f (Prop b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Prop a -> f (Prop b)
Traversable, forall a. Eq a => a -> Prop a -> Bool
forall a. Num a => Prop a -> a
forall a. Ord a => Prop a -> a
forall m. Monoid m => Prop m -> m
forall a. Prop a -> Bool
forall a. Prop a -> Int
forall a. Prop a -> [a]
forall a. (a -> a -> a) -> Prop a -> a
forall m a. Monoid m => (a -> m) -> Prop a -> m
forall b a. (b -> a -> b) -> b -> Prop a -> b
forall a b. (a -> b -> b) -> b -> Prop a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Prop a -> a
$cproduct :: forall a. Num a => Prop a -> a
sum :: forall a. Num a => Prop a -> a
$csum :: forall a. Num a => Prop a -> a
minimum :: forall a. Ord a => Prop a -> a
$cminimum :: forall a. Ord a => Prop a -> a
maximum :: forall a. Ord a => Prop a -> a
$cmaximum :: forall a. Ord a => Prop a -> a
elem :: forall a. Eq a => a -> Prop a -> Bool
$celem :: forall a. Eq a => a -> Prop a -> Bool
length :: forall a. Prop a -> Int
$clength :: forall a. Prop a -> Int
null :: forall a. Prop a -> Bool
$cnull :: forall a. Prop a -> Bool
toList :: forall a. Prop a -> [a]
$ctoList :: forall a. Prop a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Prop a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Prop a -> a
foldr1 :: forall a. (a -> a -> a) -> Prop a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Prop a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Prop a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Prop a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Prop a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Prop a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Prop a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Prop a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Prop a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Prop a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Prop a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Prop a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Prop a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Prop a -> m
fold :: forall m. Monoid m => Prop m -> m
$cfold :: forall m. Monoid m => Prop m -> m
Foldable)

instance Symbolic f a => Symbolic f (Prop a) where
  termsDL :: Prop a -> DList (Term f)
termsDL ([Equation a]
lhs :=>: Equation a
rhs) =
    forall f a. Symbolic f a => a -> DList (Term f)
termsDL Equation a
rhs forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall f a. Symbolic f a => a -> DList (Term f)
termsDL [Equation a]
lhs
  subst :: (Var -> Term f) -> Prop a -> Prop a
subst Var -> Term f
sub ([Equation a]
lhs :=>: Equation a
rhs) =
    forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub [Equation a]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub Equation a
rhs

instance Ord a => Eq (Prop a) where
  Prop a
x == :: Prop a -> Prop a -> Bool
== Prop a
y = Prop a
x forall a. Ord a => a -> a -> Ordering
`compare` Prop a
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord a => Ord (Prop a) where
  compare :: Prop a -> Prop a -> Ordering
compare = forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (\Prop a
p -> (forall a. Ord a => [a] -> [a]
usort (forall a. Prop a -> [Equation a]
lhs Prop a
p), forall a. Prop a -> Equation a
rhs Prop a
p))

infix 4 :=>:

literals :: Prop a -> [Equation a]
literals :: forall a. Prop a -> [Equation a]
literals Prop a
p = forall a. Prop a -> Equation a
rhs Prop a
pforall a. a -> [a] -> [a]
:forall a. Prop a -> [Equation a]
lhs Prop a
p

unitProp :: Equation a -> Prop a
unitProp :: forall a. Equation a -> Prop a
unitProp Equation a
p = [] forall a. [Equation a] -> Equation a -> Prop a
:=>: Equation a
p

mapFun :: (fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapFun :: forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapFun fun1 -> fun2
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap fun1 -> fun2
f)

mapTerm :: (Term fun1 -> Term fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapTerm :: forall fun1 fun2.
(Term fun1 -> Term fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapTerm Term fun1 -> Term fun2
f ([Equation (Term fun1)]
lhs :=>: Equation (Term fun1)
rhs) = forall a b. (a -> b) -> [a] -> [b]
map (forall {t} {a}. (t -> a) -> Equation t -> Equation a
both Term fun1 -> Term fun2
f) [Equation (Term fun1)]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: forall {t} {a}. (t -> a) -> Equation t -> Equation a
both Term fun1 -> Term fun2
f Equation (Term fun1)
rhs
  where
    both :: (t -> a) -> Equation t -> Equation a
both t -> a
f (t
t :=: t
u) = t -> a
f t
t forall a. a -> a -> Equation a
:=: t -> a
f t
u

instance Typed a => Typed (Prop a) where
  typ :: Prop a -> Type
typ Prop a
_ = forall a. Typeable a => a -> Type
typeOf Bool
True
  otherTypesDL :: Prop a -> DList Type
otherTypesDL Prop a
p = forall a. [a] -> DList a
DList.fromList (forall a. Prop a -> [Equation a]
literals Prop a
p) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Typed a => a -> DList Type
typesDL
  typeSubst_ :: (Var -> Builder TyCon) -> Prop a -> Prop a
typeSubst_ Var -> Builder TyCon
sub ([Equation a]
lhs :=>: Equation a
rhs) =
    forall a b. (a -> b) -> [a] -> [b]
map (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub) [Equation a]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Equation a
rhs

instance Pretty a => Pretty (Prop a) where
  pPrint :: Prop a -> Doc
pPrint ([] :=>: Equation a
rhs) = forall a. Pretty a => a -> Doc
pPrint Equation a
rhs
  pPrint Prop a
p =
    [Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" &") (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pPrint (forall a. Prop a -> [Equation a]
lhs Prop a
p))) Doc -> Doc -> Doc
<+> String -> Doc
text String
"=>" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint (forall a. Prop a -> Equation a
rhs Prop a
p)

data Equation a = a :=: a deriving (Int -> Equation a -> ShowS
forall a. Show a => Int -> Equation a -> ShowS
forall a. Show a => [Equation a] -> ShowS
forall a. Show a => Equation a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Equation a] -> ShowS
$cshowList :: forall a. Show a => [Equation a] -> ShowS
show :: Equation a -> String
$cshow :: forall a. Show a => Equation a -> String
showsPrec :: Int -> Equation a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Equation a -> ShowS
Show, Equation a -> Equation a -> Bool
forall a. Eq a => Equation a -> Equation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Equation a -> Equation a -> Bool
$c/= :: forall a. Eq a => Equation a -> Equation a -> Bool
== :: Equation a -> Equation a -> Bool
$c== :: forall a. Eq a => Equation a -> Equation a -> Bool
Eq, Equation a -> Equation a -> Bool
Equation a -> Equation a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Equation a)
forall a. Ord a => Equation a -> Equation a -> Bool
forall a. Ord a => Equation a -> Equation a -> Ordering
forall a. Ord a => Equation a -> Equation a -> Equation a
min :: Equation a -> Equation a -> Equation a
$cmin :: forall a. Ord a => Equation a -> Equation a -> Equation a
max :: Equation a -> Equation a -> Equation a
$cmax :: forall a. Ord a => Equation a -> Equation a -> Equation a
>= :: Equation a -> Equation a -> Bool
$c>= :: forall a. Ord a => Equation a -> Equation a -> Bool
> :: Equation a -> Equation a -> Bool
$c> :: forall a. Ord a => Equation a -> Equation a -> Bool
<= :: Equation a -> Equation a -> Bool
$c<= :: forall a. Ord a => Equation a -> Equation a -> Bool
< :: Equation a -> Equation a -> Bool
$c< :: forall a. Ord a => Equation a -> Equation a -> Bool
compare :: Equation a -> Equation a -> Ordering
$ccompare :: forall a. Ord a => Equation a -> Equation a -> Ordering
Ord, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Equation a) x -> Equation a
forall a x. Equation a -> Rep (Equation a) x
$cto :: forall a x. Rep (Equation a) x -> Equation a
$cfrom :: forall a x. Equation a -> Rep (Equation a) x
Generic, forall a b. a -> Equation b -> Equation a
forall {t} {a}. (t -> a) -> Equation t -> Equation a
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Equation b -> Equation a
$c<$ :: forall a b. a -> Equation b -> Equation a
fmap :: forall {t} {a}. (t -> a) -> Equation t -> Equation a
$cfmap :: forall {t} {a}. (t -> a) -> Equation t -> Equation a
Functor, Functor Equation
Foldable Equation
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Equation (m a) -> m (Equation a)
forall (f :: * -> *) a.
Applicative f =>
Equation (f a) -> f (Equation a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Equation a -> m (Equation b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Equation a -> f (Equation b)
sequence :: forall (m :: * -> *) a. Monad m => Equation (m a) -> m (Equation a)
$csequence :: forall (m :: * -> *) a. Monad m => Equation (m a) -> m (Equation a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Equation a -> m (Equation b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Equation a -> m (Equation b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Equation (f a) -> f (Equation a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Equation (f a) -> f (Equation a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Equation a -> f (Equation b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Equation a -> f (Equation b)
Traversable, forall a. Eq a => a -> Equation a -> Bool
forall a. Num a => Equation a -> a
forall a. Ord a => Equation a -> a
forall m. Monoid m => Equation m -> m
forall a. Equation a -> Bool
forall a. Equation a -> Int
forall a. Equation a -> [a]
forall a. (a -> a -> a) -> Equation a -> a
forall m a. Monoid m => (a -> m) -> Equation a -> m
forall b a. (b -> a -> b) -> b -> Equation a -> b
forall a b. (a -> b -> b) -> b -> Equation a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Equation a -> a
$cproduct :: forall a. Num a => Equation a -> a
sum :: forall a. Num a => Equation a -> a
$csum :: forall a. Num a => Equation a -> a
minimum :: forall a. Ord a => Equation a -> a
$cminimum :: forall a. Ord a => Equation a -> a
maximum :: forall a. Ord a => Equation a -> a
$cmaximum :: forall a. Ord a => Equation a -> a
elem :: forall a. Eq a => a -> Equation a -> Bool
$celem :: forall a. Eq a => a -> Equation a -> Bool
length :: forall a. Equation a -> Int
$clength :: forall a. Equation a -> Int
null :: forall a. Equation a -> Bool
$cnull :: forall a. Equation a -> Bool
toList :: forall a. Equation a -> [a]
$ctoList :: forall a. Equation a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Equation a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Equation a -> a
foldr1 :: forall a. (a -> a -> a) -> Equation a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Equation a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Equation a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Equation a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Equation a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Equation a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Equation a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Equation a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Equation a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Equation a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Equation a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Equation a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Equation a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Equation a -> m
fold :: forall m. Monoid m => Equation m -> m
$cfold :: forall m. Monoid m => Equation m -> m
Foldable)

instance Symbolic f a => Symbolic f (Equation a) where
  termsDL :: Equation a -> DList (Term f)
termsDL (a
t :=: a
u) = forall f a. Symbolic f a => a -> DList (Term f)
termsDL a
t forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall f a. Symbolic f a => a -> DList (Term f)
termsDL a
u
  subst :: (Var -> Term f) -> Equation a -> Equation a
subst Var -> Term f
sub (a
t :=: a
u) = forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub a
t forall a. a -> a -> Equation a
:=: forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub a
u

infix 5 :=:

instance Typed a => Typed (Equation a) where
  typ :: Equation a -> Type
typ (a
t :=: a
_) = forall a. Typed a => a -> Type
typ a
t
  otherTypesDL :: Equation a -> DList Type
otherTypesDL (a
t :=: a
u) = forall a. Typed a => a -> DList Type
otherTypesDL a
t forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList Type
typesDL a
u
  typeSubst_ :: (Var -> Builder TyCon) -> Equation a -> Equation a
typeSubst_ Var -> Builder TyCon
sub (a
x :=: a
y) = forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub a
x forall a. a -> a -> Equation a
:=: forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub a
y

instance Pretty a => Pretty (Equation a) where
  pPrintPrec :: PrettyLevel -> Rational -> Equation a -> Doc
pPrintPrec PrettyLevel
_ Rational
_ (a
x :=: a
y)
    | forall {a}. Pretty a => a -> Bool
isTrue a
x = forall a. Pretty a => a -> Doc
pPrint a
y
    | forall {a}. Pretty a => a -> Bool
isTrue a
y = forall a. Pretty a => a -> Doc
pPrint a
x
    | Bool
otherwise = forall a. Pretty a => a -> Doc
pPrint a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint a
y
    where
      -- XXX this is a hack
      isTrue :: a -> Bool
isTrue a
x = forall a. Show a => a -> String
show (forall a. Pretty a => a -> Doc
pPrint a
x) forall a. Eq a => a -> a -> Bool
== String
"True"

infix 4 ===
(===) :: a -> a -> Prop a
a
x === :: forall a. a -> a -> Prop a
=== a
y = [] forall a. [Equation a] -> Equation a -> Prop a
:=>: a
x forall a. a -> a -> Equation a
:=: a
y

----------------------------------------------------------------------
-- Making properties look pretty (naming variables, etc.)
----------------------------------------------------------------------

prettyProp ::
  (Typed fun, Apply (Term fun), PrettyTerm fun) =>
  (Type -> [String]) -> Prop (Term fun) -> Doc
prettyProp :: forall fun.
(Typed fun, Apply (Term fun), PrettyTerm fun) =>
(Type -> [String]) -> Prop (Term fun) -> Doc
prettyProp Type -> [String]
cands = forall a. Pretty a => a -> Doc
pPrint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun.
(Type -> [String])
-> Prop (Term fun) -> (Map String Type, Prop (Term (Named fun)))
nameVars Type -> [String]
cands

prettyPropQC ::
  (Typed fun, Apply (Term fun), PrettyTerm fun) =>
  Type -> (Type -> Bool) -> Int -> (Type -> [String]) -> Prop (Term fun) -> Doc
prettyPropQC :: forall fun.
(Typed fun, Apply (Term fun), PrettyTerm fun) =>
Type
-> (Type -> Bool)
-> Int
-> (Type -> [String])
-> Prop (Term fun)
-> Doc
prettyPropQC Type
default_to Type -> Bool
was_observed Int
nth Type -> [String]
cands Prop (Term fun)
x
  = Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
first_char Doc -> Doc -> Doc
<+> String -> Doc
text String
"(" Doc -> Doc -> Doc
<+> ((String -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pPrint Prop (Term (Named fun))
law))) Int
2
  forall a b. (a -> b) -> a -> b
$ Doc -> Int -> Doc -> Doc
hang ([Doc] -> Doc
hsep [String -> Doc
text String
",", String -> Doc
text String
"property", String -> Doc
text String
"$"]) Int
4
  forall a b. (a -> b) -> a -> b
$ Doc -> Int -> Doc -> Doc
hang Doc
ppr_binds Int
4
  forall a b. (a -> b) -> a -> b
$ (Doc
ppr_ctx Doc -> Doc -> Doc
<+> Term (Named fun) -> Type -> Doc
with_sig Term (Named fun)
lhs Type
lhs_type Doc -> Doc -> Doc
<+> Doc
eq_fn Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Term (Named fun)
rhs) forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")"
  where
    eq :: String
eq = String
"==="
    obs_eq :: String
obs_eq = String
"=~="
    eq_fn :: Doc
eq_fn = String -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> Bool -> a
bool String
eq String
obs_eq forall a b. (a -> b) -> a -> b
$ Type -> Bool
was_observed Type
lhs_type
    lhs_type :: Type
lhs_type = forall a. Typed a => a -> Type
typ Term fun
lhs_for_type

    first_char :: String
first_char =
      case Int
nth of
        Int
1 -> String
"["
        Int
_ -> String
","
    ppr_ctx :: Doc
ppr_ctx =
      case forall (t :: * -> *) a. Foldable t => t a -> Int
length [Equation (Term (Named fun))]
ctx of
        Int
0 -> Doc
pPrintEmpty
        Int
_ -> ([Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" &&") forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pPrint) [Equation (Term (Named fun))]
ctx) Doc -> Doc -> Doc
<+> String -> Doc
text String
"==>"

    ([Equation (Term fun)]
_ :=>: (Term fun
lhs_for_type :=: Term fun
_)) = Prop (Term fun)
x
    (Map String Type
var_defs, law :: Prop (Term (Named fun))
law@([Equation (Term (Named fun))]
ctx :=>: (Term (Named fun)
lhs :=: Term (Named fun)
rhs))) = forall fun.
(Type -> [String])
-> Prop (Term fun) -> (Map String Type, Prop (Term (Named fun)))
nameVars Type -> [String]
cands Prop (Term fun)
x
    with_sig :: Term (Named fun) -> Type -> Doc
with_sig Term (Named fun)
expr Type
ty = Doc -> Type -> Doc
print_sig (forall a. Pretty a => a -> Doc
pPrint Term (Named fun)
expr) Type
ty
    print_sig :: Doc -> Type -> Doc
print_sig Doc
doc Type
ty = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ Doc
doc Doc -> Doc -> Doc
<+> String -> Doc
text String
"::" Doc -> Doc -> Doc
<+> Type -> Doc
pPrintType (forall a. Typed a => Type -> a -> a
defaultTo Type
default_to Type
ty)
    ppr_binds :: Doc
ppr_binds =
      case forall k a. Map k a -> Int
Map.size Map String Type
var_defs of
        Int
0 -> Doc
pPrintEmpty
        Int
_ -> (String -> Doc
text String
"\\ " forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
sep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Doc -> Type -> Doc
print_sig) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first String -> Doc
text) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.assocs Map String Type
var_defs))) Doc -> Doc -> Doc
<+> String -> Doc
text String
"->"


data Named fun = Name String | Ordinary fun
instance Pretty fun => Pretty (Named fun) where
  pPrintPrec :: PrettyLevel -> Rational -> Named fun -> Doc
pPrintPrec PrettyLevel
_ Rational
_ (Name String
name) = String -> Doc
text String
name
  pPrintPrec PrettyLevel
l Rational
p (Ordinary fun
fun) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun
fun
instance PrettyTerm fun => PrettyTerm (Named fun) where
  termStyle :: Named fun -> TermStyle
termStyle Name{} = TermStyle
curried
  termStyle (Ordinary fun
fun) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun
fun

nameVars :: (Type -> [String]) -> Prop (Term fun) -> (Map.Map String Type, Prop (Term (Named fun)))
nameVars :: forall fun.
(Type -> [String])
-> Prop (Term fun) -> (Map String Type, Prop (Term (Named fun)))
nameVars Type -> [String]
cands Prop (Term fun)
p =
  (Map String Type
var_defs, forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst (\Var
x -> forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
undefined Var
x Map Var (Term (Named fun))
sub) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall fun. fun -> Named fun
Ordinary) Prop (Term fun)
p))
  where
    sub :: Map Var (Term (Named fun))
sub = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var, Term (Named fun))]
sub_map
    ([(Var, Term (Named fun))]
sub_map, Map String Type
var_defs) = (forall s a. State s a -> s -> (a, s)
runState (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Var -> StateT (Map String Type) Identity (Var, Term (Named fun))
assign (forall a. Eq a => [a] -> [a]
nub (forall f a. Symbolic f a => a -> [Var]
vars Prop (Term fun)
p))) forall k a. Map k a
Map.empty)
    assign :: Var -> StateT (Map String Type) Identity (Var, Term (Named fun))
assign Var
x = do
      Map String Type
s <- forall (m :: * -> *) s. Monad m => StateT s m s
get
      let ty :: Type
ty = forall a. Typed a => a -> Type
typ Var
x
          names :: [String]
names = [String] -> [String]
supply (Type -> [String]
cands Type
ty)
          name :: String
name = forall a. [a] -> a
head (forall a. (a -> Bool) -> [a] -> [a]
filter (forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map String Type
s) [String]
names)
      forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
name Type
ty)
      forall (m :: * -> *) a. Monad m => a -> m a
return (Var
x, forall f. f -> Term f
Fun (forall fun. String -> Named fun
Name String
name))