{-# 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
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
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))