-------------------------------------------------------------------------------
-- | This module formalizes the key datatypes needed to represent Horn NNF 
--   constraints as described in "Local Refinement Typing", ICFP 2017
-------------------------------------------------------------------------------

{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}

module Language.Fixpoint.Horn.Types 
  ( -- * Horn Constraints and their components
    Query (..)
  , Cstr  (..)
  , Pred  (..)
  , Bind  (..)
  , Var   (..) 

    -- * accessing constraint labels
  , cLabel

    -- * invariants (refinements) on constraints 
  , okCstr 
  , dummyBind

    -- * extract qualifiers 
  , quals
  ) 
  where 

import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)
import qualified Data.List               as L
import qualified Language.Fixpoint.Misc  as Misc
import qualified Language.Fixpoint.Types as F
import qualified Text.PrettyPrint.HughesPJ.Compat as P
import qualified Data.HashMap.Strict as M

-------------------------------------------------------------------------------
-- | @HVar@ is a Horn variable 
-------------------------------------------------------------------------------
data Var a = HVar
  { Var a -> Symbol
hvName :: !F.Symbol                         -- ^ name of the variable $k1, $k2 etc.
  , Var a -> [Sort]
hvArgs :: ![F.Sort] {- len hvArgs > 0 -}    -- ^ sorts of its parameters i.e. of the relation defined by the @HVar@
  , Var a -> a
hvMeta :: a                                 -- ^ meta-data
  }
  deriving (Var a -> Var a -> Bool
(Var a -> Var a -> Bool) -> (Var a -> Var a -> Bool) -> Eq (Var a)
forall a. Eq a => Var a -> Var a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var a -> Var a -> Bool
$c/= :: forall a. Eq a => Var a -> Var a -> Bool
== :: Var a -> Var a -> Bool
$c== :: forall a. Eq a => Var a -> Var a -> Bool
Eq, Eq (Var a)
Eq (Var a)
-> (Var a -> Var a -> Ordering)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Var a)
-> (Var a -> Var a -> Var a)
-> Ord (Var a)
Var a -> Var a -> Bool
Var a -> Var a -> Ordering
Var a -> Var a -> Var a
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 (Var a)
forall a. Ord a => Var a -> Var a -> Bool
forall a. Ord a => Var a -> Var a -> Ordering
forall a. Ord a => Var a -> Var a -> Var a
min :: Var a -> Var a -> Var a
$cmin :: forall a. Ord a => Var a -> Var a -> Var a
max :: Var a -> Var a -> Var a
$cmax :: forall a. Ord a => Var a -> Var a -> Var a
>= :: Var a -> Var a -> Bool
$c>= :: forall a. Ord a => Var a -> Var a -> Bool
> :: Var a -> Var a -> Bool
$c> :: forall a. Ord a => Var a -> Var a -> Bool
<= :: Var a -> Var a -> Bool
$c<= :: forall a. Ord a => Var a -> Var a -> Bool
< :: Var a -> Var a -> Bool
$c< :: forall a. Ord a => Var a -> Var a -> Bool
compare :: Var a -> Var a -> Ordering
$ccompare :: forall a. Ord a => Var a -> Var a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Var a)
Ord, Typeable (Var a)
DataType
Constr
Typeable (Var a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Var a -> c (Var a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Var a))
-> (Var a -> Constr)
-> (Var a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Var a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a)))
-> ((forall b. Data b => b -> b) -> Var a -> Var a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Var a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Var a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Var a -> m (Var a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Var a -> m (Var a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Var a -> m (Var a))
-> Data (Var a)
Var a -> DataType
Var a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
(forall b. Data b => b -> b) -> Var a -> Var a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
forall a. Data a => Typeable (Var a)
forall a. Data a => Var a -> DataType
forall a. Data a => Var a -> Constr
forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Var a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Var a -> u
forall u. (forall d. Data d => d -> u) -> Var a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
$cHVar :: Constr
$tVar :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Var a -> m (Var a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
gmapMp :: (forall d. Data d => d -> m d) -> Var a -> m (Var a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
gmapM :: (forall d. Data d => d -> m d) -> Var a -> m (Var a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Var a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Var a -> u
gmapQ :: (forall d. Data d => d -> u) -> Var a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
gmapT :: (forall b. Data b => b -> b) -> Var a -> Var a
$cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Var a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
dataTypeOf :: Var a -> DataType
$cdataTypeOf :: forall a. Data a => Var a -> DataType
toConstr :: Var a -> Constr
$ctoConstr :: forall a. Data a => Var a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
$cp1Data :: forall a. Data a => Typeable (Var a)
Data, Typeable, (forall x. Var a -> Rep (Var a) x)
-> (forall x. Rep (Var a) x -> Var a) -> Generic (Var a)
forall x. Rep (Var a) x -> Var a
forall x. Var a -> Rep (Var a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Var a) x -> Var a
forall a x. Var a -> Rep (Var a) x
$cto :: forall a x. Rep (Var a) x -> Var a
$cfrom :: forall a x. Var a -> Rep (Var a) x
Generic, a -> Var b -> Var a
(a -> b) -> Var a -> Var b
(forall a b. (a -> b) -> Var a -> Var b)
-> (forall a b. a -> Var b -> Var a) -> Functor Var
forall a b. a -> Var b -> Var a
forall a b. (a -> b) -> Var a -> Var b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Var b -> Var a
$c<$ :: forall a b. a -> Var b -> Var a
fmap :: (a -> b) -> Var a -> Var b
$cfmap :: forall a b. (a -> b) -> Var a -> Var b
Functor)

-------------------------------------------------------------------------------
-- | @HPred@ is a Horn predicate that appears as LHS (body) or RHS (head) of constraints 
-------------------------------------------------------------------------------
data Pred 
  = Reft  !F.Expr                               -- ^ r 
  | Var   !F.Symbol ![F.Symbol]                 -- ^ $k(y1..yn) 
  | PAnd  ![Pred]                               -- ^ p1 /\ .../\ pn 
  deriving (Typeable Pred
DataType
Constr
Typeable Pred
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Pred -> c Pred)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Pred)
-> (Pred -> Constr)
-> (Pred -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Pred))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred))
-> ((forall b. Data b => b -> b) -> Pred -> Pred)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r)
-> (forall u. (forall d. Data d => d -> u) -> Pred -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Pred -> m Pred)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Pred -> m Pred)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Pred -> m Pred)
-> Data Pred
Pred -> DataType
Pred -> Constr
(forall b. Data b => b -> b) -> Pred -> Pred
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
forall u. (forall d. Data d => d -> u) -> Pred -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
$cPAnd :: Constr
$cVar :: Constr
$cReft :: Constr
$tPred :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Pred -> m Pred
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapMp :: (forall d. Data d => d -> m d) -> Pred -> m Pred
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapM :: (forall d. Data d => d -> m d) -> Pred -> m Pred
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapQi :: Int -> (forall d. Data d => d -> u) -> Pred -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
gmapQ :: (forall d. Data d => d -> u) -> Pred -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Pred -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
gmapT :: (forall b. Data b => b -> b) -> Pred -> Pred
$cgmapT :: (forall b. Data b => b -> b) -> Pred -> Pred
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Pred)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
dataTypeOf :: Pred -> DataType
$cdataTypeOf :: Pred -> DataType
toConstr :: Pred -> Constr
$ctoConstr :: Pred -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
$cp1Data :: Typeable Pred
Data, Typeable, (forall x. Pred -> Rep Pred x)
-> (forall x. Rep Pred x -> Pred) -> Generic Pred
forall x. Rep Pred x -> Pred
forall x. Pred -> Rep Pred x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Pred x -> Pred
$cfrom :: forall x. Pred -> Rep Pred x
Generic, Pred -> Pred -> Bool
(Pred -> Pred -> Bool) -> (Pred -> Pred -> Bool) -> Eq Pred
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pred -> Pred -> Bool
$c/= :: Pred -> Pred -> Bool
== :: Pred -> Pred -> Bool
$c== :: Pred -> Pred -> Bool
Eq)


instance Semigroup Pred where
  Pred
p1 <> :: Pred -> Pred -> Pred
<> Pred
p2 = [Pred] -> Pred
PAnd [Pred
p1, Pred
p2]

instance Monoid Pred where 
  mempty :: Pred
mempty = Expr -> Pred
Reft Expr
forall a. Monoid a => a
mempty

instance F.Subable Pred where
  syms :: Pred -> [Symbol]
syms (Reft Expr
e)   = Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
e
  syms (Var Symbol
_ [Symbol]
xs) = [Symbol]
xs
  syms (PAnd [Pred]
ps)  = (Pred -> [Symbol]) -> [Pred] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms [Pred]
ps

  substa :: (Symbol -> Symbol) -> Pred -> Pred
substa Symbol -> Symbol
f (Reft Expr
e)   = Expr -> Pred
Reft  ((Symbol -> Symbol) -> Expr -> Expr
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f      Expr
e)
  substa Symbol -> Symbol
f (Var Symbol
k [Symbol]
xs) = Symbol -> [Symbol] -> Pred
Var Symbol
k ((Symbol -> Symbol) -> Symbol -> Symbol
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
  substa Symbol -> Symbol
f (PAnd [Pred]
ps)  = [Pred] -> Pred
PAnd  ((Symbol -> Symbol) -> Pred -> Pred
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)

  subst :: Subst -> Pred -> Pred
subst Subst
su (Reft  Expr
e)  = Expr -> Pred
Reft  (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su      Expr
e)
  subst Subst
su (PAnd  [Pred]
ps) = [Pred] -> Pred
PAnd  (Subst -> Pred -> Pred
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  subst Subst
su (Var Symbol
k [Symbol]
xs) = Symbol -> [Symbol] -> Pred
Var Symbol
k (Subst -> Symbol -> Symbol
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)

  substf :: (Symbol -> Expr) -> Pred -> Pred
substf Symbol -> Expr
f (Reft  Expr
e)  = Expr -> Pred
Reft  ((Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
f      Expr
e)
  substf Symbol -> Expr
f (PAnd  [Pred]
ps) = [Pred] -> Pred
PAnd  ((Symbol -> Expr) -> Pred -> Pred
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
f (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  substf Symbol -> Expr
f (Var Symbol
k [Symbol]
xs) = Symbol -> [Symbol] -> Pred
Var Symbol
k ((Symbol -> Expr) -> Symbol -> Symbol
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
f (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)

  subst1 :: Pred -> (Symbol, Expr) -> Pred
subst1 (Reft  Expr
e)  (Symbol, Expr)
su = Expr -> Pred
Reft  (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
e (Symbol, Expr)
su)
  subst1 (PAnd  [Pred]
ps) (Symbol, Expr)
su = [Pred] -> Pred
PAnd  [Pred -> (Symbol, Expr) -> Pred
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Pred
p (Symbol, Expr)
su | Pred
p <- [Pred]
ps]
  subst1 (Var Symbol
k [Symbol]
xs) (Symbol, Expr)
su = Symbol -> [Symbol] -> Pred
Var Symbol
k [Symbol -> (Symbol, Expr) -> Symbol
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Symbol
x (Symbol, Expr)
su | Symbol
x <- [Symbol]
xs]

-------------------------------------------------------------------------------
quals :: Cstr a -> [F.Qualifier] 
-------------------------------------------------------------------------------
quals :: Cstr a -> [Qualifier]
quals = String -> [Qualifier] -> [Qualifier]
forall a. PPrint a => String -> a -> a
F.tracepp String
"horn.quals" ([Qualifier] -> [Qualifier])
-> (Cstr a -> [Qualifier]) -> Cstr a -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
cstrQuals SEnv Sort
forall a. SEnv a
F.emptySEnv Symbol
F.vv_  

cstrQuals :: F.SEnv F.Sort -> F.Symbol -> Cstr a -> [F.Qualifier] 
cstrQuals :: SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
cstrQuals = SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
go 
  where
    go :: SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
go SEnv Sort
env Symbol
v (Head Pred
p a
_)  = SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env Symbol
v Pred
p
    go SEnv Sort
env Symbol
v (CAnd   [Cstr a]
cs) = (Cstr a -> [Qualifier]) -> [Cstr a] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
go SEnv Sort
env Symbol
v) [Cstr a]
cs
    go SEnv Sort
env Symbol
_ (All  Bind
b Cstr a
c)  = SEnv Sort -> Bind -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Bind -> Cstr a -> [Qualifier]
bindQuals SEnv Sort
env Bind
b Cstr a
c 
    go SEnv Sort
env Symbol
_ (Any  Bind
b Cstr a
c)  = SEnv Sort -> Bind -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Bind -> Cstr a -> [Qualifier]
bindQuals SEnv Sort
env Bind
b Cstr a
c

bindQuals  :: F.SEnv F.Sort -> Bind -> Cstr a -> [F.Qualifier] 
bindQuals :: SEnv Sort -> Bind -> Cstr a -> [Qualifier]
bindQuals SEnv Sort
env Bind
b Cstr a
c = SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env' Symbol
bx (Bind -> Pred
bPred Bind
b) [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
cstrQuals SEnv Sort
env' Symbol
bx Cstr a
c 
  where 
    env' :: SEnv Sort
env'          = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
bx Sort
bt SEnv Sort
env
    bx :: Symbol
bx            = Bind -> Symbol
bSym Bind
b
    bt :: Sort
bt            = Bind -> Sort
bSort Bind
b

predQuals :: F.SEnv F.Sort -> F.Symbol -> Pred -> [F.Qualifier]
predQuals :: SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env Symbol
v (Reft Expr
p)  = SEnv Sort -> Symbol -> Expr -> [Qualifier]
exprQuals SEnv Sort
env Symbol
v Expr
p
predQuals SEnv Sort
env Symbol
v (PAnd [Pred]
ps) = (Pred -> [Qualifier]) -> [Pred] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env Symbol
v) [Pred]
ps
predQuals SEnv Sort
_   Symbol
_ Pred
_         = [] 

exprQuals :: F.SEnv F.Sort -> F.Symbol -> F.Expr -> [F.Qualifier]
exprQuals :: SEnv Sort -> Symbol -> Expr -> [Qualifier]
exprQuals SEnv Sort
env Symbol
v Expr
e = SEnv Sort -> Symbol -> Expr -> Qualifier
mkQual SEnv Sort
env Symbol
v (Expr -> Qualifier) -> [Expr] -> [Qualifier]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> [Expr]
F.conjuncts Expr
e

mkQual :: F.SEnv F.Sort -> F.Symbol -> F.Expr -> F.Qualifier
mkQual :: SEnv Sort -> Symbol -> Expr -> Qualifier
mkQual SEnv Sort
env Symbol
v Expr
p = case SEnv Sort -> Symbol -> (Symbol, Sort)
envSort SEnv Sort
env (Symbol -> (Symbol, Sort)) -> [Symbol] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol
vSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs) of
                   (Symbol
_,Sort
so):[(Symbol, Sort)]
xts -> Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
F.mkQ Symbol
"Auto" ((Symbol
v, Sort
so) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) Expr
p SourcePos
junk 
                   [(Symbol, Sort)]
_          -> String -> Qualifier
forall a. String -> a
F.panic String
"impossible"
  where
    xs :: [Symbol]
xs         = Symbol -> [Symbol] -> [Symbol]
forall a. Eq a => a -> [a] -> [a]
L.delete Symbol
v ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol]
forall k. (Eq k, Hashable k) => [k] -> [k]
Misc.hashNub (Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
p)
    junk :: SourcePos
junk       = String -> SourcePos
F.dummyPos String
"mkQual" 

envSort :: F.SEnv F.Sort -> F.Symbol -> (F.Symbol, F.Sort)
envSort :: SEnv Sort -> Symbol -> (Symbol, Sort)
envSort SEnv Sort
env Symbol
x = case Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
x SEnv Sort
env of
                   Just Sort
t -> (Symbol
x, Sort
t) 
                   Maybe Sort
_      -> String -> (Symbol, Sort)
forall a. String -> a
F.panic (String -> (Symbol, Sort)) -> String -> (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ String
"unbound symbol in scrape: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
x
{- 
  | Just _ <- lookupSEnv x lEnv = Nothing
  | otherwise                   = Just (x, ai)
  where
    ai             = trace msg $ fObj $ Loc l l $ tempSymbol "LHTV" i
    msg            = "Unknown symbol in qualifier: " ++ show x
-}


--------------------------------------------------------------------------------
-- | @Cst@ is an NNF Horn Constraint. 
-------------------------------------------------------------------------------
-- Note that a @Bind@ is a simplified @F.SortedReft@ ...
data Bind = Bind 
  { Bind -> Symbol
bSym  :: !F.Symbol 
  , Bind -> Sort
bSort :: !F.Sort 
  , Bind -> Pred
bPred :: !Pred 
  }
  deriving (Typeable Bind
DataType
Constr
Typeable Bind
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Bind -> c Bind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Bind)
-> (Bind -> Constr)
-> (Bind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Bind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bind))
-> ((forall b. Data b => b -> b) -> Bind -> Bind)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Bind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Bind -> m Bind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bind -> m Bind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bind -> m Bind)
-> Data Bind
Bind -> DataType
Bind -> Constr
(forall b. Data b => b -> b) -> Bind -> Bind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind -> c Bind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bind
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Bind -> u
forall u. (forall d. Data d => d -> u) -> Bind -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bind -> m Bind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bind -> m Bind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind -> c Bind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bind)
$cBind :: Constr
$tBind :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Bind -> m Bind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bind -> m Bind
gmapMp :: (forall d. Data d => d -> m d) -> Bind -> m Bind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bind -> m Bind
gmapM :: (forall d. Data d => d -> m d) -> Bind -> m Bind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bind -> m Bind
gmapQi :: Int -> (forall d. Data d => d -> u) -> Bind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bind -> u
gmapQ :: (forall d. Data d => d -> u) -> Bind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Bind -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind -> r
gmapT :: (forall b. Data b => b -> b) -> Bind -> Bind
$cgmapT :: (forall b. Data b => b -> b) -> Bind -> Bind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Bind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bind)
dataTypeOf :: Bind -> DataType
$cdataTypeOf :: Bind -> DataType
toConstr :: Bind -> Constr
$ctoConstr :: Bind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind -> c Bind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind -> c Bind
$cp1Data :: Typeable Bind
Data, Typeable, (forall x. Bind -> Rep Bind x)
-> (forall x. Rep Bind x -> Bind) -> Generic Bind
forall x. Rep Bind x -> Bind
forall x. Bind -> Rep Bind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Bind x -> Bind
$cfrom :: forall x. Bind -> Rep Bind x
Generic, Bind -> Bind -> Bool
(Bind -> Bind -> Bool) -> (Bind -> Bind -> Bool) -> Eq Bind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bind -> Bind -> Bool
$c/= :: Bind -> Bind -> Bool
== :: Bind -> Bind -> Bool
$c== :: Bind -> Bind -> Bool
Eq)

instance F.Subable Bind where
    syms :: Bind -> [Symbol]
syms = Bind -> [Symbol]
forall a. HasCallStack => a
undefined
    substa :: (Symbol -> Symbol) -> Bind -> Bind
substa = (Symbol -> Symbol) -> Bind -> Bind
forall a. HasCallStack => a
undefined
    substf :: (Symbol -> Expr) -> Bind -> Bind
substf = (Symbol -> Expr) -> Bind -> Bind
forall a. HasCallStack => a
undefined
    subst :: Subst -> Bind -> Bind
subst Subst
su (Bind Symbol
x Sort
t Pred
p) = (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Subst -> Pred -> Pred
forall a. Subable a => Subst -> a -> a
F.subst Subst
su Pred
p))

dummyBind :: Bind 
dummyBind :: Bind
dummyBind = Symbol -> Sort -> Pred -> Bind
Bind Symbol
F.dummySymbol Sort
F.intSort ([Pred] -> Pred
PAnd []) 

-- Can we enforce the invariant that CAnd has len > 1?
data Cstr a
  = Head  !Pred a               -- ^ p
  | CAnd  ![(Cstr a)]           -- ^ c1 /\ ... /\ cn
  | All   !Bind  !(Cstr a)      -- ^ \all x:t. p => c
  | Any   !Bind  !(Cstr a)      -- ^ \exi x:t. p /\ c or is it \exi x:t. p => c?
  deriving (Typeable (Cstr a)
DataType
Constr
Typeable (Cstr a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Cstr a -> c (Cstr a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Cstr a))
-> (Cstr a -> Constr)
-> (Cstr a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Cstr a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a)))
-> ((forall b. Data b => b -> b) -> Cstr a -> Cstr a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Cstr a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Cstr a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Cstr a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Cstr a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a))
-> Data (Cstr a)
Cstr a -> DataType
Cstr a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
forall a. Data a => Typeable (Cstr a)
forall a. Data a => Cstr a -> DataType
forall a. Data a => Cstr a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Cstr a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Cstr a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Cstr a -> u
forall u. (forall d. Data d => d -> u) -> Cstr a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
$cAny :: Constr
$cAll :: Constr
$cCAnd :: Constr
$cHead :: Constr
$tCstr :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
gmapMp :: (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
gmapM :: (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Cstr a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Cstr a -> u
gmapQ :: (forall d. Data d => d -> u) -> Cstr a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Cstr a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
gmapT :: (forall b. Data b => b -> b) -> Cstr a -> Cstr a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
dataTypeOf :: Cstr a -> DataType
$cdataTypeOf :: forall a. Data a => Cstr a -> DataType
toConstr :: Cstr a -> Constr
$ctoConstr :: forall a. Data a => Cstr a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
$cp1Data :: forall a. Data a => Typeable (Cstr a)
Data, Typeable, (forall x. Cstr a -> Rep (Cstr a) x)
-> (forall x. Rep (Cstr a) x -> Cstr a) -> Generic (Cstr a)
forall x. Rep (Cstr a) x -> Cstr a
forall x. Cstr a -> Rep (Cstr a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Cstr a) x -> Cstr a
forall a x. Cstr a -> Rep (Cstr a) x
$cto :: forall a x. Rep (Cstr a) x -> Cstr a
$cfrom :: forall a x. Cstr a -> Rep (Cstr a) x
Generic, a -> Cstr b -> Cstr a
(a -> b) -> Cstr a -> Cstr b
(forall a b. (a -> b) -> Cstr a -> Cstr b)
-> (forall a b. a -> Cstr b -> Cstr a) -> Functor Cstr
forall a b. a -> Cstr b -> Cstr a
forall a b. (a -> b) -> Cstr a -> Cstr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Cstr b -> Cstr a
$c<$ :: forall a b. a -> Cstr b -> Cstr a
fmap :: (a -> b) -> Cstr a -> Cstr b
$cfmap :: forall a b. (a -> b) -> Cstr a -> Cstr b
Functor, Cstr a -> Cstr a -> Bool
(Cstr a -> Cstr a -> Bool)
-> (Cstr a -> Cstr a -> Bool) -> Eq (Cstr a)
forall a. Eq a => Cstr a -> Cstr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cstr a -> Cstr a -> Bool
$c/= :: forall a. Eq a => Cstr a -> Cstr a -> Bool
== :: Cstr a -> Cstr a -> Bool
$c== :: forall a. Eq a => Cstr a -> Cstr a -> Bool
Eq)

cLabel :: Cstr a -> a
cLabel :: Cstr a -> a
cLabel Cstr a
cstr = case Cstr a -> [a]
forall a. Cstr a -> [a]
go Cstr a
cstr of
  [] -> String -> a
forall a. String -> a
F.panic String
"everything is true!!!"
  a
label:[a]
_ -> a
label
  where
    go :: Cstr a -> [a]
go (Head Pred
_ a
l)   = [a
l]
    go (CAnd [Cstr a]
cs)    = [[a]] -> [a]
forall a. Monoid a => [a] -> a
mconcat ([[a]] -> [a]) -> [[a]] -> [a]
forall a b. (a -> b) -> a -> b
$ Cstr a -> [a]
go (Cstr a -> [a]) -> [Cstr a] -> [[a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
    go (All Bind
_ Cstr a
c)    = Cstr a -> [a]
go Cstr a
c
    go (Any Bind
_ Cstr a
c)    = Cstr a -> [a]
go Cstr a
c

-- We want all valid constraints to start with a binding at the top
okCstr :: Cstr a -> Bool 
okCstr :: Cstr a -> Bool
okCstr (All {}) = Bool
True 
okCstr (Any {}) = Bool
True 
okCstr Cstr a
_        = Bool
False 

-------------------------------------------------------------------------------
-- | @Query@ is an NNF Horn Constraint. 
-------------------------------------------------------------------------------

data Query a = Query 
  { Query a -> [Qualifier]
qQuals :: ![F.Qualifier]                    -- ^ qualifiers over which to solve cstrs
  , Query a -> [Var a]
qVars  :: ![Var a]                          -- ^ kvars, with parameter-sorts
  , Query a -> Cstr a
qCstr  :: !(Cstr a)                         -- ^ list of constraints
  , Query a -> HashMap Symbol Sort
qCon   :: M.HashMap (F.Symbol) (F.Sort)     -- ^ list of constants (uninterpreted functions
  , Query a -> HashMap Symbol Sort
qDis   :: M.HashMap (F.Symbol) (F.Sort)     -- ^ list of constants (uninterpreted functions
  }
  deriving (Typeable (Query a)
DataType
Constr
Typeable (Query a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Query a -> c (Query a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Query a))
-> (Query a -> Constr)
-> (Query a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Query a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a)))
-> ((forall b. Data b => b -> b) -> Query a -> Query a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Query a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Query a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Query a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Query a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Query a -> m (Query a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Query a -> m (Query a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Query a -> m (Query a))
-> Data (Query a)
Query a -> DataType
Query a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
(forall b. Data b => b -> b) -> Query a -> Query a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
forall a. Data a => Typeable (Query a)
forall a. Data a => Query a -> DataType
forall a. Data a => Query a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Query a -> Query a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Query a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Query a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Query a -> u
forall u. (forall d. Data d => d -> u) -> Query a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
$cQuery :: Constr
$tQuery :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Query a -> m (Query a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
gmapMp :: (forall d. Data d => d -> m d) -> Query a -> m (Query a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
gmapM :: (forall d. Data d => d -> m d) -> Query a -> m (Query a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Query a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Query a -> u
gmapQ :: (forall d. Data d => d -> u) -> Query a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Query a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
gmapT :: (forall b. Data b => b -> b) -> Query a -> Query a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Query a -> Query a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Query a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
dataTypeOf :: Query a -> DataType
$cdataTypeOf :: forall a. Data a => Query a -> DataType
toConstr :: Query a -> Constr
$ctoConstr :: forall a. Data a => Query a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
$cp1Data :: forall a. Data a => Typeable (Query a)
Data, Typeable, (forall x. Query a -> Rep (Query a) x)
-> (forall x. Rep (Query a) x -> Query a) -> Generic (Query a)
forall x. Rep (Query a) x -> Query a
forall x. Query a -> Rep (Query a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Query a) x -> Query a
forall a x. Query a -> Rep (Query a) x
$cto :: forall a x. Rep (Query a) x -> Query a
$cfrom :: forall a x. Query a -> Rep (Query a) x
Generic, a -> Query b -> Query a
(a -> b) -> Query a -> Query b
(forall a b. (a -> b) -> Query a -> Query b)
-> (forall a b. a -> Query b -> Query a) -> Functor Query
forall a b. a -> Query b -> Query a
forall a b. (a -> b) -> Query a -> Query b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Query b -> Query a
$c<$ :: forall a b. a -> Query b -> Query a
fmap :: (a -> b) -> Query a -> Query b
$cfmap :: forall a b. (a -> b) -> Query a -> Query b
Functor)


-------------------------------------------------------------------------------
-- Pretty Printing
-------------------------------------------------------------------------------
parens :: String -> String
parens :: String -> String
parens String
s = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

instance Show (Var a) where
  show :: Var a -> String
show (HVar Symbol
k [Sort]
xs a
_) = Symbol -> String
forall a. Show a => a -> String
show Symbol
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens ([String] -> String
unwords (Sort -> String
forall a. Show a => a -> String
show (Sort -> String) -> [Sort] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
xs))

instance Show Pred where
  show :: Pred -> String
show (Reft Expr
p)   = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. PPrint a => a -> String
F.showpp Expr
p
  show (Var Symbol
x [Symbol]
xs) = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords (Symbol -> String
F.symbolString (Symbol -> String) -> [Symbol] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs)
  show (PAnd [Pred]
ps)  = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"and"String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred -> String) -> [Pred] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> String
forall a. Show a => a -> String
show [Pred]
ps

instance Show (Cstr a) where
  show :: Cstr a -> String
show (Head Pred
p a
_) = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Pred -> String
forall a. Show a => a -> String
show Pred
p
  show (All Bind
b Cstr a
c)  = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"forall" , Bind -> String
forall a. Show a => a -> String
show Bind
b , Cstr a -> String
forall a. Show a => a -> String
show Cstr a
c]
  show (Any Bind
b Cstr a
c)  = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"exists" , Bind -> String
forall a. Show a => a -> String
show Bind
b , Cstr a -> String
forall a. Show a => a -> String
show Cstr a
c]
  show (CAnd [Cstr a]
cs)  = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"and" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Cstr a -> String) -> [Cstr a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Cstr a -> String
forall a. Show a => a -> String
show [Cstr a]
cs

instance Show Bind where
  show :: Bind -> String
show (Bind Symbol
x Sort
t Pred
p) = String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String -> String
parens (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [Symbol -> String
F.symbolString Symbol
x, Sort -> String
forall a. PPrint a => a -> String
F.showpp Sort
t], Pred -> String
forall a. Show a => a -> String
show Pred
p]

instance F.PPrint (Var a) where
  pprintPrec :: Int -> Tidy -> Var a -> Doc
pprintPrec Int
_ Tidy
_ Var a
v = String -> Doc
P.ptext (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Var a -> String
forall a. Show a => a -> String
show Var a
v

instance F.PPrint Pred where
  pprintPrec :: Int -> Tidy -> Pred -> Doc
pprintPrec Int
k Tidy
t (Reft Expr
p) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec Int
k Tidy
t Expr
p
  pprintPrec Int
_ Tidy
_ (Var Symbol
x [Symbol]
xs) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.hsep (String -> Doc
P.ptext (String -> Doc) -> (Symbol -> String) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
F.symbolString (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs)
  pprintPrec Int
k Tidy
t (PAnd [Pred]
ps) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.ptext String
"and" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Pred -> Doc) -> [Pred] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Tidy
t) [Pred]
ps

instance F.PPrint (Cstr a) where
  pprintPrec :: Int -> Tidy -> Cstr a -> Doc
pprintPrec Int
k Tidy
t (Head Pred
p a
_) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec Int
k Tidy
t Pred
p
  pprintPrec Int
k Tidy
t (All Bind
b Cstr a
c) =
    Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [String -> Doc
P.ptext String
"forall" Doc -> Doc -> Doc
P.<+> Int -> Tidy -> Bind -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Tidy
t Bind
b, Int -> Tidy -> Cstr a -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
t Cstr a
c]
  pprintPrec Int
k Tidy
t (Any Bind
b Cstr a
c) =
    Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [String -> Doc
P.ptext String
"exists" Doc -> Doc -> Doc
P.<+> Int -> Tidy -> Bind -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Tidy
t Bind
b, Int -> Tidy -> Cstr a -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
t Cstr a
c]
  pprintPrec Int
k Tidy
t (CAnd [Cstr a]
cs) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat  ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.ptext String
"and" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Cstr a -> Doc) -> [Cstr a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Tidy -> Cstr a -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Tidy
t) [Cstr a]
cs

instance F.PPrint Bind where
  pprintPrec :: Int -> Tidy -> Bind -> Doc
pprintPrec Int
_ Tidy
_ Bind
b = String -> Doc
P.ptext (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Bind -> String
forall a. Show a => a -> String
show Bind
b