-------------------------------------------------------------------------------
-- | 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 DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ViewPatterns #-}

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

    -- * Raw Query
  , Tag (..)
  , TagVar
  , TagQuery

    -- * accessing constraint labels
  , cLabel

    -- * invariants (refinements) on constraints
  , okCstr

    -- * extract qualifiers
  , quals

    -- * SMTLIB style render
  , ToHornSMT (..)
  )
  where

import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)
import           Control.DeepSeq ( NFData )
import qualified Data.Text               as T
import           Data.Maybe (fromMaybe)
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
import           Data.Aeson
import           Data.Aeson.Types

-------------------------------------------------------------------------------
-- | @HVar@ is a Horn variable
-------------------------------------------------------------------------------
data Var a = HVar
  { forall a. Var a -> Symbol
hvName :: !F.Symbol                         -- ^ name of the variable $k1, $k2 etc.
  , forall a. Var a -> [Sort]
hvArgs :: ![F.Sort] {- len hvArgs > 0 -}    -- ^ sorts of its parameters i.e. of the relation defined by the @HVar@
  , forall a. 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
$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
/= :: 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
$ccompare :: forall a. Ord a => Var a -> Var a -> Ordering
compare :: Var a -> Var a -> Ordering
$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
>= :: Var a -> Var a -> Bool
$cmax :: forall a. Ord a => Var a -> Var a -> Var a
max :: Var a -> Var a -> Var a
$cmin :: forall a. Ord a => Var a -> Var a -> Var a
min :: Var a -> Var a -> Var a
Ord, Typeable (Var a)
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 -> Constr
Var a -> DataType
(forall b. Data b => b -> b) -> Var a -> Var a
forall a. Data a => Typeable (Var a)
forall a. Data a => Var a -> Constr
forall a. Data a => Var a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
$ctoConstr :: forall a. Data a => Var a -> Constr
toConstr :: Var a -> Constr
$cdataTypeOf :: forall a. Data a => Var a -> DataType
dataTypeOf :: Var a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
$cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a
gmapT :: (forall b. Data b => b -> b) -> Var a -> Var a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
gmapM :: forall (m :: * -> *).
Monad m =>
(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)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var a -> m (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
$cfrom :: forall a x. Var a -> Rep (Var a) x
from :: forall x. Var a -> Rep (Var a) x
$cto :: forall a x. Rep (Var a) x -> Var a
to :: forall x. Rep (Var a) x -> Var a
Generic, (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
$cfmap :: forall a b. (a -> b) -> Var a -> Var b
fmap :: forall a b. (a -> b) -> Var a -> Var b
$c<$ :: forall a b. a -> Var b -> Var a
<$ :: forall a b. a -> Var b -> Var a
Functor, [Var a] -> Value
[Var a] -> Encoding
Var a -> Bool
Var a -> Value
Var a -> Encoding
(Var a -> Value)
-> (Var a -> Encoding)
-> ([Var a] -> Value)
-> ([Var a] -> Encoding)
-> (Var a -> Bool)
-> ToJSON (Var a)
forall a. ToJSON a => [Var a] -> Value
forall a. ToJSON a => [Var a] -> Encoding
forall a. ToJSON a => Var a -> Bool
forall a. ToJSON a => Var a -> Value
forall a. ToJSON a => Var a -> Encoding
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: forall a. ToJSON a => Var a -> Value
toJSON :: Var a -> Value
$ctoEncoding :: forall a. ToJSON a => Var a -> Encoding
toEncoding :: Var a -> Encoding
$ctoJSONList :: forall a. ToJSON a => [Var a] -> Value
toJSONList :: [Var a] -> Value
$ctoEncodingList :: forall a. ToJSON a => [Var a] -> Encoding
toEncodingList :: [Var a] -> Encoding
$comitField :: forall a. ToJSON a => Var a -> Bool
omitField :: Var a -> Bool
ToJSON, Maybe (Var a)
Value -> Parser [Var a]
Value -> Parser (Var a)
(Value -> Parser (Var a))
-> (Value -> Parser [Var a]) -> Maybe (Var a) -> FromJSON (Var a)
forall a. FromJSON a => Maybe (Var a)
forall a. FromJSON a => Value -> Parser [Var a]
forall a. FromJSON a => Value -> Parser (Var a)
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: forall a. FromJSON a => Value -> Parser (Var a)
parseJSON :: Value -> Parser (Var a)
$cparseJSONList :: forall a. FromJSON a => Value -> Parser [Var a]
parseJSONList :: Value -> Parser [Var a]
$comittedField :: forall a. FromJSON a => Maybe (Var a)
omittedField :: Maybe (Var a)
FromJSON)

-------------------------------------------------------------------------------
-- | @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
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 -> Constr
Pred -> DataType
(forall b. Data b => b -> b) -> Pred -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
$ctoConstr :: Pred -> Constr
toConstr :: Pred -> Constr
$cdataTypeOf :: Pred -> DataType
dataTypeOf :: Pred -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
$cgmapT :: (forall b. Data b => b -> b) -> Pred -> Pred
gmapT :: (forall b. Data b => b -> b) -> Pred -> Pred
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Pred -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Pred -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m 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
$cfrom :: forall x. Pred -> Rep Pred x
from :: forall x. Pred -> Rep Pred x
$cto :: forall x. Rep Pred x -> Pred
to :: forall x. Rep Pred x -> Pred
Generic, Pred -> Pred -> Bool
(Pred -> Pred -> Bool) -> (Pred -> Pred -> Bool) -> Eq Pred
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pred -> Pred -> Bool
== :: Pred -> Pred -> Bool
$c/= :: Pred -> Pred -> Bool
/= :: Pred -> Pred -> Bool
Eq, [Pred] -> Value
[Pred] -> Encoding
Pred -> Bool
Pred -> Value
Pred -> Encoding
(Pred -> Value)
-> (Pred -> Encoding)
-> ([Pred] -> Value)
-> ([Pred] -> Encoding)
-> (Pred -> Bool)
-> ToJSON Pred
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: Pred -> Value
toJSON :: Pred -> Value
$ctoEncoding :: Pred -> Encoding
toEncoding :: Pred -> Encoding
$ctoJSONList :: [Pred] -> Value
toJSONList :: [Pred] -> Value
$ctoEncodingList :: [Pred] -> Encoding
toEncodingList :: [Pred] -> Encoding
$comitField :: Pred -> Bool
omitField :: Pred -> Bool
ToJSON, Maybe Pred
Value -> Parser [Pred]
Value -> Parser Pred
(Value -> Parser Pred)
-> (Value -> Parser [Pred]) -> Maybe Pred -> FromJSON Pred
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser Pred
parseJSON :: Value -> Parser Pred
$cparseJSONList :: Value -> Parser [Pred]
parseJSONList :: Value -> Parser [Pred]
$comittedField :: Maybe Pred
omittedField :: Maybe Pred
FromJSON)


instance F.Subable Pred where
  syms :: Pred -> [Symbol]
syms (Reft ExprV Symbol
e)   = ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms ExprV Symbol
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 ExprV Symbol
e)   = ExprV Symbol -> Pred
Reft  ((Symbol -> Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f      ExprV Symbol
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 :: SubstV Symbol -> Pred -> Pred
subst SubstV Symbol
su (Reft  ExprV Symbol
e)  = ExprV Symbol -> Pred
Reft  (SubstV Symbol -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => SubstV Symbol -> a -> a
F.subst SubstV Symbol
su      ExprV Symbol
e)
  subst SubstV Symbol
su (PAnd  [Pred]
ps) = [Pred] -> Pred
PAnd  (SubstV Symbol -> Pred -> Pred
forall a. Subable a => SubstV Symbol -> a -> a
F.subst SubstV Symbol
su (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  subst SubstV Symbol
su (Var Symbol
k [Symbol]
xs) = Symbol -> [Symbol] -> Pred
Var Symbol
k (SubstV Symbol -> Symbol -> Symbol
forall a. Subable a => SubstV Symbol -> a -> a
F.subst SubstV Symbol
su (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)

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

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

-------------------------------------------------------------------------------
quals :: Cstr a -> [F.Qualifier]
-------------------------------------------------------------------------------
quals :: forall a. Cstr a -> [Qualifier]
quals = [Char] -> [Qualifier] -> [Qualifier]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"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 :: forall a. 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 a
b Cstr a
c)  = SEnv Sort -> Bind a -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Bind a -> Cstr a -> [Qualifier]
bindQuals SEnv Sort
env Bind a
b Cstr a
c
    go SEnv Sort
env Symbol
_ (Any  Bind a
b Cstr a
c)  = SEnv Sort -> Bind a -> Cstr a -> [Qualifier]
forall a. SEnv Sort -> Bind a -> Cstr a -> [Qualifier]
bindQuals SEnv Sort
env Bind a
b Cstr a
c

bindQuals  :: F.SEnv F.Sort -> Bind a -> Cstr a -> [F.Qualifier]
bindQuals :: forall a. SEnv Sort -> Bind a -> Cstr a -> [Qualifier]
bindQuals SEnv Sort
env Bind a
b Cstr a
c = SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env' Symbol
bx (Bind a -> Pred
forall a. Bind a -> Pred
bPred Bind a
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 a -> Symbol
forall a. Bind a -> Symbol
bSym Bind a
b
    bt :: Sort
bt            = Bind a -> Sort
forall a. Bind a -> Sort
bSort Bind a
b

predQuals :: F.SEnv F.Sort -> F.Symbol -> Pred -> [F.Qualifier]
predQuals :: SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env Symbol
v (Reft ExprV Symbol
p)  = SEnv Sort -> Symbol -> ExprV Symbol -> [Qualifier]
exprQuals SEnv Sort
env Symbol
v ExprV Symbol
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 -> ExprV Symbol -> [Qualifier]
exprQuals SEnv Sort
env Symbol
v ExprV Symbol
e = SEnv Sort -> Symbol -> ExprV Symbol -> Qualifier
mkQual SEnv Sort
env Symbol
v (ExprV Symbol -> Qualifier) -> [ExprV Symbol] -> [Qualifier]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprV Symbol -> [ExprV Symbol]
forall v. Eq v => ExprV v -> [ExprV v]
F.conjuncts ExprV Symbol
e

mkQual :: F.SEnv F.Sort -> F.Symbol -> F.Expr -> F.Qualifier
mkQual :: SEnv Sort -> Symbol -> ExprV Symbol -> Qualifier
mkQual SEnv Sort
env Symbol
v ExprV Symbol
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)] -> ExprV Symbol -> SourcePos -> Qualifier
F.mkQ Symbol
"Auto" ((Symbol
v, Sort
so) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) ExprV Symbol
p SourcePos
junk
                   [(Symbol, Sort)]
_          -> [Char] -> Qualifier
forall a. [Char] -> a
F.panic [Char]
"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. Ord k => [k] -> [k]
Misc.setNub (ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms ExprV Symbol
p)
    junk :: SourcePos
junk       = [Char] -> SourcePos
F.dummyPos [Char]
"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
_      -> [Char] -> (Symbol, Sort)
forall a. [Char] -> a
F.panic ([Char] -> (Symbol, Sort)) -> [Char] -> (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ [Char]
"unbound symbol in scrape: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. PPrint a => a -> [Char]
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 a = Bind
  { forall a. Bind a -> Symbol
bSym  :: !F.Symbol
  , forall a. Bind a -> Sort
bSort :: !F.Sort
  , forall a. Bind a -> Pred
bPred :: !Pred
  , forall a. Bind a -> a
bMeta :: !a
  }
  deriving (Typeable (Bind a)
Typeable (Bind a) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Bind a -> c (Bind a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Bind a))
-> (Bind a -> Constr)
-> (Bind a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Bind a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Bind a)))
-> ((forall b. Data b => b -> b) -> Bind a -> Bind a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Bind a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Bind a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bind a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Bind a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Bind a -> m (Bind a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bind a -> m (Bind a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bind a -> m (Bind a))
-> Data (Bind a)
Bind a -> Constr
Bind a -> DataType
(forall b. Data b => b -> b) -> Bind a -> Bind a
forall a. Data a => Typeable (Bind a)
forall a. Data a => Bind a -> Constr
forall a. Data a => Bind a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> Bind a -> Bind a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Bind a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Bind a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bind a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind a -> c (Bind a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bind a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Bind 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) -> Bind a -> u
forall u. (forall d. Data d => d -> u) -> Bind a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bind a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind a -> c (Bind a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Bind a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Bind a))
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind a -> c (Bind a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind a -> c (Bind a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bind a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bind a)
$ctoConstr :: forall a. Data a => Bind a -> Constr
toConstr :: Bind a -> Constr
$cdataTypeOf :: forall a. Data a => Bind a -> DataType
dataTypeOf :: Bind a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bind a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Bind a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Bind a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Bind a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Bind a -> Bind a
gmapT :: (forall b. Data b => b -> b) -> Bind a -> Bind a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Bind a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Bind a -> [u]
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Bind a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bind a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
Data, Typeable, (forall x. Bind a -> Rep (Bind a) x)
-> (forall x. Rep (Bind a) x -> Bind a) -> Generic (Bind a)
forall x. Rep (Bind a) x -> Bind a
forall x. Bind a -> Rep (Bind a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Bind a) x -> Bind a
forall a x. Bind a -> Rep (Bind a) x
$cfrom :: forall a x. Bind a -> Rep (Bind a) x
from :: forall x. Bind a -> Rep (Bind a) x
$cto :: forall a x. Rep (Bind a) x -> Bind a
to :: forall x. Rep (Bind a) x -> Bind a
Generic, (forall a b. (a -> b) -> Bind a -> Bind b)
-> (forall a b. a -> Bind b -> Bind a) -> Functor Bind
forall a b. a -> Bind b -> Bind a
forall a b. (a -> b) -> Bind a -> Bind b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Bind a -> Bind b
fmap :: forall a b. (a -> b) -> Bind a -> Bind b
$c<$ :: forall a b. a -> Bind b -> Bind a
<$ :: forall a b. a -> Bind b -> Bind a
Functor, Bind a -> Bind a -> Bool
(Bind a -> Bind a -> Bool)
-> (Bind a -> Bind a -> Bool) -> Eq (Bind a)
forall a. Eq a => Bind a -> Bind a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Bind a -> Bind a -> Bool
== :: Bind a -> Bind a -> Bool
$c/= :: forall a. Eq a => Bind a -> Bind a -> Bool
/= :: Bind a -> Bind a -> Bool
Eq, [Bind a] -> Value
[Bind a] -> Encoding
Bind a -> Bool
Bind a -> Value
Bind a -> Encoding
(Bind a -> Value)
-> (Bind a -> Encoding)
-> ([Bind a] -> Value)
-> ([Bind a] -> Encoding)
-> (Bind a -> Bool)
-> ToJSON (Bind a)
forall a. ToJSON a => [Bind a] -> Value
forall a. ToJSON a => [Bind a] -> Encoding
forall a. ToJSON a => Bind a -> Bool
forall a. ToJSON a => Bind a -> Value
forall a. ToJSON a => Bind a -> Encoding
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: forall a. ToJSON a => Bind a -> Value
toJSON :: Bind a -> Value
$ctoEncoding :: forall a. ToJSON a => Bind a -> Encoding
toEncoding :: Bind a -> Encoding
$ctoJSONList :: forall a. ToJSON a => [Bind a] -> Value
toJSONList :: [Bind a] -> Value
$ctoEncodingList :: forall a. ToJSON a => [Bind a] -> Encoding
toEncodingList :: [Bind a] -> Encoding
$comitField :: forall a. ToJSON a => Bind a -> Bool
omitField :: Bind a -> Bool
ToJSON, Maybe (Bind a)
Value -> Parser [Bind a]
Value -> Parser (Bind a)
(Value -> Parser (Bind a))
-> (Value -> Parser [Bind a])
-> Maybe (Bind a)
-> FromJSON (Bind a)
forall a. FromJSON a => Maybe (Bind a)
forall a. FromJSON a => Value -> Parser [Bind a]
forall a. FromJSON a => Value -> Parser (Bind a)
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: forall a. FromJSON a => Value -> Parser (Bind a)
parseJSON :: Value -> Parser (Bind a)
$cparseJSONList :: forall a. FromJSON a => Value -> Parser [Bind a]
parseJSONList :: Value -> Parser [Bind a]
$comittedField :: forall a. FromJSON a => Maybe (Bind a)
omittedField :: Maybe (Bind a)
FromJSON)

instance F.Subable (Bind a) where
    syms :: Bind a -> [Symbol]
syms     (Bind Symbol
x Sort
_ Pred
p a
_) = Symbol
x Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: Pred -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Pred
p
    substa :: (Symbol -> Symbol) -> Bind a -> Bind a
substa Symbol -> Symbol
f (Bind Symbol
v Sort
t Pred
p a
a) = Symbol -> Sort -> Pred -> a -> Bind a
forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind (Symbol -> Symbol
f Symbol
v) Sort
t ((Symbol -> Symbol) -> Pred -> Pred
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f Pred
p) a
a
    substf :: (Symbol -> ExprV Symbol) -> Bind a -> Bind a
substf Symbol -> ExprV Symbol
f (Bind Symbol
v Sort
t Pred
p a
a) = Symbol -> Sort -> Pred -> a -> Bind a
forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind Symbol
v Sort
t ((Symbol -> ExprV Symbol) -> Pred -> Pred
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
F.substf ((Symbol -> ExprV Symbol) -> [Symbol] -> Symbol -> ExprV Symbol
F.substfExcept Symbol -> ExprV Symbol
f [Symbol
v]) Pred
p) a
a
    subst :: SubstV Symbol -> Bind a -> Bind a
subst SubstV Symbol
su (Bind Symbol
v Sort
t Pred
p a
a)  = Symbol -> Sort -> Pred -> a -> Bind a
forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind Symbol
v Sort
t (SubstV Symbol -> Pred -> Pred
forall a. Subable a => SubstV Symbol -> a -> a
F.subst (SubstV Symbol -> [Symbol] -> SubstV Symbol
F.substExcept SubstV Symbol
su [Symbol
v]) Pred
p) a
a
    subst1 :: Bind a -> (Symbol, ExprV Symbol) -> Bind a
subst1 (Bind Symbol
v Sort
t Pred
p a
a) (Symbol, ExprV Symbol)
su = Symbol -> Sort -> Pred -> a -> Bind a
forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind Symbol
v Sort
t ([Symbol] -> Pred -> (Symbol, ExprV Symbol) -> Pred
forall a. Subable a => [Symbol] -> a -> (Symbol, ExprV Symbol) -> a
F.subst1Except [Symbol
v] Pred
p (Symbol, ExprV Symbol)
su) a
a

-- Can we enforce the invariant that CAnd has len > 1?
data Cstr a
  = Head  !Pred !a                  -- ^ p
  | CAnd  ![Cstr a]                 -- ^ c1 /\ ... /\ cn
  | All   !(Bind a)  !(Cstr a)      -- ^ \all x:t. p => c
  | Any   !(Bind a)  !(Cstr a)      -- ^ \exi x:t. p /\ c or is it \exi x:t. p => c?
  deriving (Typeable (Cstr a)
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 -> Constr
Cstr a -> DataType
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
forall a. Data a => Typeable (Cstr a)
forall a. Data a => Cstr a -> Constr
forall a. Data a => Cstr a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
$ctoConstr :: forall a. Data a => Cstr a -> Constr
toConstr :: Cstr a -> Constr
$cdataTypeOf :: forall a. Data a => Cstr a -> DataType
dataTypeOf :: Cstr a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
gmapT :: (forall b. Data b => b -> b) -> Cstr a -> Cstr a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Cstr a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Cstr a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
gmapM :: forall (m :: * -> *).
Monad m =>
(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)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Cstr a -> m (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
$cfrom :: forall a x. Cstr a -> Rep (Cstr a) x
from :: forall x. Cstr a -> Rep (Cstr a) x
$cto :: forall a x. Rep (Cstr a) x -> Cstr a
to :: forall x. Rep (Cstr a) x -> Cstr a
Generic, (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
$cfmap :: forall a b. (a -> b) -> Cstr a -> Cstr b
fmap :: forall a b. (a -> b) -> Cstr a -> Cstr b
$c<$ :: forall a b. a -> Cstr b -> Cstr a
<$ :: forall a b. a -> Cstr b -> Cstr a
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
$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
/= :: Cstr a -> Cstr a -> Bool
Eq, [Cstr a] -> Value
[Cstr a] -> Encoding
Cstr a -> Bool
Cstr a -> Value
Cstr a -> Encoding
(Cstr a -> Value)
-> (Cstr a -> Encoding)
-> ([Cstr a] -> Value)
-> ([Cstr a] -> Encoding)
-> (Cstr a -> Bool)
-> ToJSON (Cstr a)
forall a. ToJSON a => [Cstr a] -> Value
forall a. ToJSON a => [Cstr a] -> Encoding
forall a. ToJSON a => Cstr a -> Bool
forall a. ToJSON a => Cstr a -> Value
forall a. ToJSON a => Cstr a -> Encoding
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: forall a. ToJSON a => Cstr a -> Value
toJSON :: Cstr a -> Value
$ctoEncoding :: forall a. ToJSON a => Cstr a -> Encoding
toEncoding :: Cstr a -> Encoding
$ctoJSONList :: forall a. ToJSON a => [Cstr a] -> Value
toJSONList :: [Cstr a] -> Value
$ctoEncodingList :: forall a. ToJSON a => [Cstr a] -> Encoding
toEncodingList :: [Cstr a] -> Encoding
$comitField :: forall a. ToJSON a => Cstr a -> Bool
omitField :: Cstr a -> Bool
ToJSON, Maybe (Cstr a)
Value -> Parser [Cstr a]
Value -> Parser (Cstr a)
(Value -> Parser (Cstr a))
-> (Value -> Parser [Cstr a])
-> Maybe (Cstr a)
-> FromJSON (Cstr a)
forall a. FromJSON a => Maybe (Cstr a)
forall a. FromJSON a => Value -> Parser [Cstr a]
forall a. FromJSON a => Value -> Parser (Cstr a)
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: forall a. FromJSON a => Value -> Parser (Cstr a)
parseJSON :: Value -> Parser (Cstr a)
$cparseJSONList :: forall a. FromJSON a => Value -> Parser [Cstr a]
parseJSONList :: Value -> Parser [Cstr a]
$comittedField :: forall a. FromJSON a => Maybe (Cstr a)
omittedField :: Maybe (Cstr a)
FromJSON)

cLabel :: Cstr a -> a
cLabel :: forall a. Cstr a -> a
cLabel Cstr a
cstr = case Cstr a -> [a]
forall {a}. Cstr a -> [a]
go Cstr a
cstr of
  [] -> [Char] -> a
forall a. [Char] -> a
F.panic [Char]
"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 a
_ Cstr a
c)    = Cstr a -> [a]
go Cstr a
c
    go (Any Bind a
_ 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 :: forall a. 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
  { forall a. Query a -> [Qualifier]
qQuals :: ![F.Qualifier]             -- ^ qualifiers over which to solve cstrs
  , forall a. Query a -> [Var a]
qVars  :: ![Var a]                   -- ^ kvars, with parameter-sorts
  , forall a. Query a -> Cstr a
qCstr  :: !(Cstr a)                  -- ^ list of constraints
  , forall a. Query a -> HashMap Symbol Sort
qCon   :: M.HashMap F.Symbol F.Sort  -- ^ list of constants (uninterpreted functions)
  , forall a. Query a -> HashMap Symbol Sort
qDis   :: M.HashMap F.Symbol F.Sort  -- ^ list of *distinct* constants (uninterpreted functions)
  , forall a. Query a -> [Equation]
qEqns  :: ![F.Equation]              -- ^ list of equations
  , forall a. Query a -> [Rewrite]
qMats  :: ![F.Rewrite]               -- ^ list of match-es
  , forall a. Query a -> [DataDecl]
qData  :: ![F.DataDecl]              -- ^ list of data-declarations
  , forall a. Query a -> [[Char]]
qOpts  :: ![String]                  -- ^ list of fixpoint options
  , forall a. Query a -> [Symbol]
qNums  :: ![F.Symbol]                -- ^ list of numeric TyCon (?)
  }
  deriving (Typeable (Query a)
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 -> Constr
Query a -> DataType
(forall b. Data b => b -> b) -> Query a -> Query a
forall a. Data a => Typeable (Query a)
forall a. Data a => Query a -> Constr
forall a. Data a => Query a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
$ctoConstr :: forall a. Data a => Query a -> Constr
toConstr :: Query a -> Constr
$cdataTypeOf :: forall a. Data a => Query a -> DataType
dataTypeOf :: Query a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Query a -> Query a
gmapT :: (forall b. Data b => b -> b) -> Query a -> Query a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Query a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Query a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
gmapM :: forall (m :: * -> *).
Monad m =>
(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)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Query a -> m (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
$cfrom :: forall a x. Query a -> Rep (Query a) x
from :: forall x. Query a -> Rep (Query a) x
$cto :: forall a x. Rep (Query a) x -> Query a
to :: forall x. Rep (Query a) x -> Query a
Generic, (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
$cfmap :: forall a b. (a -> b) -> Query a -> Query b
fmap :: forall a b. (a -> b) -> Query a -> Query b
$c<$ :: forall a b. a -> Query b -> Query a
<$ :: forall a b. a -> Query b -> Query a
Functor, [Query a] -> Value
[Query a] -> Encoding
Query a -> Bool
Query a -> Value
Query a -> Encoding
(Query a -> Value)
-> (Query a -> Encoding)
-> ([Query a] -> Value)
-> ([Query a] -> Encoding)
-> (Query a -> Bool)
-> ToJSON (Query a)
forall a. ToJSON a => [Query a] -> Value
forall a. ToJSON a => [Query a] -> Encoding
forall a. ToJSON a => Query a -> Bool
forall a. ToJSON a => Query a -> Value
forall a. ToJSON a => Query a -> Encoding
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: forall a. ToJSON a => Query a -> Value
toJSON :: Query a -> Value
$ctoEncoding :: forall a. ToJSON a => Query a -> Encoding
toEncoding :: Query a -> Encoding
$ctoJSONList :: forall a. ToJSON a => [Query a] -> Value
toJSONList :: [Query a] -> Value
$ctoEncodingList :: forall a. ToJSON a => [Query a] -> Encoding
toEncodingList :: [Query a] -> Encoding
$comitField :: forall a. ToJSON a => Query a -> Bool
omitField :: Query a -> Bool
ToJSON, Maybe (Query a)
Value -> Parser [Query a]
Value -> Parser (Query a)
(Value -> Parser (Query a))
-> (Value -> Parser [Query a])
-> Maybe (Query a)
-> FromJSON (Query a)
forall a. FromJSON a => Maybe (Query a)
forall a. FromJSON a => Value -> Parser [Query a]
forall a. FromJSON a => Value -> Parser (Query a)
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: forall a. FromJSON a => Value -> Parser (Query a)
parseJSON :: Value -> Parser (Query a)
$cparseJSONList :: forall a. FromJSON a => Value -> Parser [Query a]
parseJSONList :: Value -> Parser [Query a]
$comittedField :: forall a. FromJSON a => Maybe (Query a)
omittedField :: Maybe (Query a)
FromJSON)

-- | Tag each query with a possible string denoting "provenance"

type TagVar   = Var Tag
type TagQuery = Query Tag
data Tag      = NoTag | Tag String
  deriving (Typeable Tag
Typeable Tag =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Tag -> c Tag)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Tag)
-> (Tag -> Constr)
-> (Tag -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Tag))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag))
-> ((forall b. Data b => b -> b) -> Tag -> Tag)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r)
-> (forall u. (forall d. Data d => d -> u) -> Tag -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Tag -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Tag -> m Tag)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Tag -> m Tag)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Tag -> m Tag)
-> Data Tag
Tag -> Constr
Tag -> DataType
(forall b. Data b => b -> b) -> Tag -> Tag
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) -> Tag -> u
forall u. (forall d. Data d => d -> u) -> Tag -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Tag
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tag -> c Tag
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Tag)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tag -> c Tag
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tag -> c Tag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Tag
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Tag
$ctoConstr :: Tag -> Constr
toConstr :: Tag -> Constr
$cdataTypeOf :: Tag -> DataType
dataTypeOf :: Tag -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Tag)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Tag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag)
$cgmapT :: (forall b. Data b => b -> b) -> Tag -> Tag
gmapT :: (forall b. Data b => b -> b) -> Tag -> Tag
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Tag -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Tag -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Tag -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Tag -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
Data, Typeable, (forall x. Tag -> Rep Tag x)
-> (forall x. Rep Tag x -> Tag) -> Generic Tag
forall x. Rep Tag x -> Tag
forall x. Tag -> Rep Tag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Tag -> Rep Tag x
from :: forall x. Tag -> Rep Tag x
$cto :: forall x. Rep Tag x -> Tag
to :: forall x. Rep Tag x -> Tag
Generic, Int -> Tag -> [Char] -> [Char]
[Tag] -> [Char] -> [Char]
Tag -> [Char]
(Int -> Tag -> [Char] -> [Char])
-> (Tag -> [Char]) -> ([Tag] -> [Char] -> [Char]) -> Show Tag
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Tag -> [Char] -> [Char]
showsPrec :: Int -> Tag -> [Char] -> [Char]
$cshow :: Tag -> [Char]
show :: Tag -> [Char]
$cshowList :: [Tag] -> [Char] -> [Char]
showList :: [Tag] -> [Char] -> [Char]
Show)

instance NFData Tag

instance F.Loc Tag where
  srcSpan :: Tag -> SrcSpan
srcSpan Tag
_ = SrcSpan
F.dummySpan

instance F.Fixpoint Tag where
  toFix :: Tag -> Doc
toFix Tag
NoTag   = Doc
"\"\""
  toFix (Tag [Char]
s) = Doc
"\"" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc
P.text [Char]
s Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"\""

instance F.PPrint Tag where
  pprintPrec :: Int -> Tidy -> Tag -> Doc
pprintPrec Int
_ Tidy
_ Tag
NoTag   = Doc
forall a. Monoid a => a
mempty
  pprintPrec Int
_ Tidy
_ (Tag [Char]
s) = [Char] -> Doc
P.ptext [Char]
s

instance ToJSON Tag where
  toJSON :: Tag -> Value
toJSON Tag
NoTag   = Value
Null
  toJSON (Tag [Char]
s) = Text -> Value
String ([Char] -> Text
T.pack [Char]
s)

instance FromJSON Tag where
  parseJSON :: Value -> Parser Tag
parseJSON Value
Null       = Tag -> Parser Tag
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
NoTag
  parseJSON (String Text
t) = Tag -> Parser Tag
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> Tag
Tag (Text -> [Char]
T.unpack Text
t))
  parseJSON Value
invalid    = [Char] -> Parser Tag -> Parser Tag
forall a. [Char] -> Parser a -> Parser a
prependFailure [Char]
"parsing `Tag` failed, " ([Char] -> Value -> Parser Tag
forall a. [Char] -> Value -> Parser a
typeMismatch [Char]
"Object" Value
invalid)





instance F.PPrint (Query a) where
  pprintPrec :: Int -> Tidy -> Query a -> Doc
pprintPrec Int
prec Tidy
t Query a
q = [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse Doc
" "
    [ [Doc] -> Doc
P.vcat   (Qualifier -> Doc
ppQual (Qualifier -> Doc) -> [Qualifier] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [Qualifier]
forall a. Query a -> [Qualifier]
qQuals Query a
q)
    , [Doc] -> Doc
P.vcat   [Var a -> Doc
forall a. Var a -> Doc
ppVar Var a
k   | Var a
k <- Query a -> [Var a]
forall a. Query a -> [Var a]
qVars Query a
q]
    , [Doc] -> Doc
P.vcat   [Symbol -> Doc -> Doc
ppCon Symbol
x (Sort -> Doc
forall a. PPrint a => a -> Doc
F.pprint Sort
sort') | (Symbol
x, Sort
sort') <- HashMap Symbol Sort -> [(Symbol, Sort)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Query a -> HashMap Symbol Sort
forall a. Query a -> HashMap Symbol Sort
qCon Query a
q)]
    , Maybe Doc -> [Equation] -> Doc
forall a. PPrint a => Maybe Doc -> [a] -> Doc
ppThings Maybe Doc
forall a. Maybe a
Nothing (Query a -> [Equation]
forall a. Query a -> [Equation]
qEqns  Query a
q)
    , Maybe Doc -> [DataDecl] -> Doc
forall a. PPrint a => Maybe Doc -> [a] -> Doc
ppThings (Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"data ") (Query a -> [DataDecl]
forall a. Query a -> [DataDecl]
qData  Query a
q)
    , Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat [Doc
"constraint", Int -> Tidy -> Cstr a -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
precInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Tidy
t (Query a -> Cstr a
forall a. Query a -> Cstr a
qCstr Query a
q)])
    ]




ppThings :: F.PPrint a => Maybe P.Doc -> [a] -> P.Doc
ppThings :: forall a. PPrint a => Maybe Doc -> [a] -> Doc
ppThings Maybe Doc
pfx [a]
qs = [Doc] -> Doc
P.vcat [ Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
prefix Doc -> Doc -> Doc
P.<-> a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
q | a
q <- [a]
qs]
  where
    prefix :: Doc
prefix      = Doc -> Maybe Doc -> Doc
forall a. a -> Maybe a -> a
fromMaybe Doc
"" Maybe Doc
pfx

ppCon :: F.Symbol -> P.Doc -> P.Doc
ppCon :: Symbol -> Doc -> Doc
ppCon Symbol
x Doc
td = Doc -> Doc
P.parens (Doc
"constant" Doc -> Doc -> Doc
P.<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
x Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens Doc
td)

ppQual :: F.Qualifier -> P.Doc
ppQual :: Qualifier -> Doc
ppQual (F.Q Symbol
n [QualParam]
xts ExprV Symbol
p SourcePos
_) =  Doc -> Doc
P.parens (Doc
"qualif" Doc -> Doc -> Doc
P.<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
n Doc -> Doc -> Doc
P.<+> [Doc] -> Doc
ppBlanks (QualParam -> Doc
ppArg (QualParam -> Doc) -> [QualParam] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
xts) Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens (ExprV Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprV Symbol
p))
  where
    ppArg :: QualParam -> Doc
ppArg QualParam
qp    = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint (QualParam -> Symbol
F.qpSym QualParam
qp) Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens (Sort -> Doc
forall a. PPrint a => a -> Doc
F.pprint (QualParam -> Sort
F.qpSort QualParam
qp))

ppVar :: Var a -> P.Doc
ppVar :: forall a. Var a -> Doc
ppVar (HVar Symbol
k [Sort]
ts a
_)  = Doc -> Doc
P.parens (Doc
"var" Doc -> Doc -> Doc
P.<+> Doc
"$" Doc -> Doc -> Doc
P.<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
k Doc -> Doc -> Doc
P.<+> [Doc] -> Doc
ppBlanks (Doc -> Doc
P.parens (Doc -> Doc) -> (Sort -> Doc) -> Sort -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Sort -> Doc) -> [Sort] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts))


ppBlanks :: [P.Doc] -> P.Doc
ppBlanks :: [Doc] -> Doc
ppBlanks [Doc]
ds = Doc -> Doc
P.parens ([Doc] -> Doc
P.hcat (Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse Doc
" " [Doc]
ds))

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

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

instance Show Pred where
  show :: Pred -> [Char]
show (Reft ExprV Symbol
p)   = [Char] -> [Char]
parens ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ExprV Symbol
p
  show (Var Symbol
x [Symbol]
xs) = [Char] -> [Char]
parens ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"$" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords (Symbol -> [Char]
F.symbolString (Symbol -> [Char]) -> [Symbol] -> [[Char]]
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)  = [Char] -> [Char]
parens ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"and"[Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Pred -> [Char]) -> [Pred] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> [Char]
forall a. Show a => a -> [Char]
show [Pred]
ps

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

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

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

instance F.PPrint Pred where
  pprintPrec :: Int -> Tidy -> Pred -> Doc
pprintPrec Int
k Tidy
t (Reft ExprV Symbol
p)   = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Tidy -> ExprV Symbol -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec Int
k Tidy
t ExprV Symbol
p
  pprintPrec Int
_ Tidy
_ (Var Symbol
x [Symbol]
xs) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
P.ptext [Char]
"$" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
P.hsep ([Char] -> Doc
P.ptext ([Char] -> Doc) -> (Symbol -> [Char]) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
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
$ [Char] -> Doc
P.ptext [Char]
"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 a
b Cstr a
c)  = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [ [Char] -> Doc
P.ptext [Char]
"forall" Doc -> Doc -> Doc
P.<+> Int -> Tidy -> Bind 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 Bind a
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 a
b Cstr a
c)  = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [[Char] -> Doc
P.ptext [Char]
"exists" Doc -> Doc -> Doc
P.<+> Int -> Tidy -> Bind 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 Bind a
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
$ [Char] -> Doc
P.ptext [Char]
"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 a) where
  pprintPrec :: Int -> Tidy -> Bind a -> Doc
pprintPrec Int
_ Tidy
_ Bind a
b = [Char] -> Doc
P.ptext ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Bind a -> [Char]
forall a. Show a => a -> [Char]
show Bind a
b


-----------------------------------------------------------------------------------------------------------------
-- Human readable but robustly parseable SMT-LIB format pretty printer
-----------------------------------------------------------------------------------------------------------------
class ToHornSMT a where
  toHornSMT :: a -> P.Doc

instance ToHornSMT Tag where
  toHornSMT :: Tag -> Doc
toHornSMT Tag
NoTag   = Doc
forall a. Monoid a => a
mempty
  toHornSMT (Tag [Char]
s) = [Char] -> Doc
P.text [Char]
s

instance ToHornSMT F.Symbol where
  toHornSMT :: Symbol -> Doc
toHornSMT Symbol
s = Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
s

instance ToHornSMT (Var a) where
  toHornSMT :: Var a -> Doc
toHornSMT (HVar Symbol
k [Sort]
ts a
_) = Doc -> Doc
P.parens (Doc
"var" Doc -> Doc -> Doc
P.<+> Doc
"$" Doc -> Doc -> Doc
P.<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
k Doc -> Doc -> Doc
P.<+> [Sort] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [Sort]
ts)

instance ToHornSMT (Query a) where
  toHornSMT :: Query a -> Doc
toHornSMT Query a
q = [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse Doc
" "
    [ [Doc] -> Doc
P.vcat   ([Char] -> Doc
toHornOpt ([Char] -> Doc) -> [[Char]] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [[Char]]
forall a. Query a -> [[Char]]
qOpts Query a
q)
    , [Doc] -> Doc
P.vcat   (Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornNum (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [Symbol]
forall a. Query a -> [Symbol]
qNums Query a
q)
    , [Doc] -> Doc
P.vcat   (Qualifier -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Qualifier -> Doc) -> [Qualifier] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [Qualifier]
forall a. Query a -> [Qualifier]
qQuals Query a
q)
    , [Doc] -> Doc
P.vcat   (Var a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Var a -> Doc) -> [Var a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [Var a]
forall a. Query a -> [Var a]
qVars Query a
q)
    , [Doc] -> Doc
P.vcat   [Symbol -> Sort -> Doc
forall {a} {a}. (ToHornSMT a, ToHornSMT a) => a -> a -> Doc
toHornCon Symbol
x Sort
t | (Symbol
x, Sort
t) <- HashMap Symbol Sort -> [(Symbol, Sort)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Query a -> HashMap Symbol Sort
forall a. Query a -> HashMap Symbol Sort
qCon Query a
q)]
    , [Doc] -> Doc
P.vcat   (Equation -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Equation -> Doc) -> [Equation] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [Equation]
forall a. Query a -> [Equation]
qEqns Query a
q)
    , [Doc] -> Doc
P.vcat   (DataDecl -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (DataDecl -> Doc) -> [DataDecl] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [DataDecl]
forall a. Query a -> [DataDecl]
qData Query a
q)
    , [Doc] -> Doc
P.vcat   (Rewrite -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Rewrite -> Doc) -> [Rewrite] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query a -> [Rewrite]
forall a. Query a -> [Rewrite]
qMats Query a
q)
    , Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat [Doc
"constraint", Int -> Doc -> Doc
P.nest Int
1 (Cstr a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Query a -> Cstr a
forall a. Query a -> Cstr a
qCstr Query a
q))])
    ]
    where
      toHornNum :: a -> Doc
toHornNum a
x   = [Doc] -> Doc
toHornMany [Doc
"numeric", a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT a
x]
      toHornOpt :: [Char] -> Doc
toHornOpt [Char]
str = [Doc] -> Doc
toHornMany [Doc
"fixpoint", [Char] -> Doc
P.text ([Char]
"\"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
str [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\"")]
      toHornCon :: a -> a -> Doc
toHornCon a
x a
t = [Doc] -> Doc
toHornMany [Doc
"constant", a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT a
x, a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT a
t]

instance ToHornSMT F.Rewrite where
  toHornSMT :: Rewrite -> Doc
toHornSMT (F.SMeasure Symbol
f Symbol
d [Symbol]
xs ExprV Symbol
e) =  Doc -> Doc
P.parens (Doc
"match" Doc -> Doc -> Doc
P.<+> Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
f Doc -> Doc -> Doc
P.<+> [Symbol] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol
dSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs) Doc -> Doc -> Doc
P.<+> ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e)

instance ToHornSMT F.Qualifier where
  toHornSMT :: Qualifier -> Doc
toHornSMT (F.Q Symbol
n [QualParam]
xts ExprV Symbol
p SourcePos
_) =  Doc -> Doc
P.parens (Doc
"qualif" Doc -> Doc -> Doc
P.<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
n Doc -> Doc -> Doc
P.<+> [QualParam] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [QualParam]
xts Doc -> Doc -> Doc
P.<+> ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
p)

instance ToHornSMT F.QualParam where
  toHornSMT :: QualParam -> Doc
toHornSMT QualParam
qp = (Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (QualParam -> Symbol
F.qpSym QualParam
qp, QualParam -> Sort
F.qpSort QualParam
qp)

instance ToHornSMT a => ToHornSMT (F.Symbol, a) where
  toHornSMT :: (Symbol, a) -> Doc
toHornSMT (Symbol
x, a
t) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
x Doc -> Doc -> Doc
P.<+> a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT a
t

instance ToHornSMT a => ToHornSMT [a] where
  toHornSMT :: [a] -> Doc
toHornSMT = [Doc] -> Doc
toHornMany ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT

toHornMany :: [P.Doc] -> P.Doc
toHornMany :: [Doc] -> Doc
toHornMany = Doc -> Doc
P.parens (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
P.sep -- Misc.intersperse " "

toHornAnd :: (a -> P.Doc) -> [a] -> P.Doc
toHornAnd :: forall a. (a -> Doc) -> [a] -> Doc
toHornAnd a -> Doc
f [a]
xs = Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat (Doc
"and" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Int -> Doc -> Doc
P.nest Int
1 (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
f (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)))

instance ToHornSMT F.Equation where
  toHornSMT :: Equation -> Doc
toHornSMT (F.Equ Symbol
f [(Symbol, Sort)]
xs ExprV Symbol
e Sort
s Bool
_) = Doc -> Doc
P.parens (Doc
"define" Doc -> Doc -> Doc
P.<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
f Doc -> Doc -> Doc
P.<+> [(Symbol, Sort)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, Sort)]
xs Doc -> Doc -> Doc
P.<+> Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
s Doc -> Doc -> Doc
P.<+> ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e)

instance ToHornSMT F.DataDecl where
  toHornSMT :: DataDecl -> Doc
toHornSMT (F.DDecl FTycon
tc Int
n [DataCtor]
ctors) =
    Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [
      [Char] -> Doc
P.text [Char]
"datatype" Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens (FTycon -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT FTycon
tc Doc -> Doc -> Doc
P.<+> Int -> Doc
P.int Int
n)
    , Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat (DataCtor -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (DataCtor -> Doc) -> [DataCtor] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
ctors))
    ]

instance ToHornSMT F.FTycon where
  toHornSMT :: FTycon -> Doc
toHornSMT FTycon
c
    | FTycon
c FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon
F.listFTyCon = Doc
"list"
    | Bool
otherwise         = Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol FTycon
c)

instance ToHornSMT a => ToHornSMT (F.Located a) where
  toHornSMT :: Located a -> Doc
toHornSMT = a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (a -> Doc) -> (Located a -> a) -> Located a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
F.val
instance ToHornSMT F.DataCtor where
  toHornSMT :: DataCtor -> Doc
toHornSMT (F.DCtor LocSymbol
x [DataField]
flds) = Doc -> Doc
P.parens (LocSymbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT LocSymbol
x Doc -> Doc -> Doc
P.<+> [DataField] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [DataField]
flds)

instance ToHornSMT F.DataField where
  toHornSMT :: DataField -> Doc
toHornSMT (F.DField LocSymbol
x Sort
t) = (Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
x, Sort
t)

instance ToHornSMT F.Sort where
  toHornSMT :: Sort -> Doc
toHornSMT = Sort -> Doc
toHornSort

toHornSort :: F.Sort -> P.Doc
toHornSort :: Sort -> Doc
toHornSort (F.FVar Int
i)     = Doc
"@" Doc -> Doc -> Doc
P.<-> Doc -> Doc
P.parens (Int -> Doc
P.int Int
i)
toHornSort Sort
F.FInt         = Doc
"Int"
toHornSort Sort
F.FReal        = Doc
"Real"
toHornSort Sort
F.FFrac        = Doc
"Frac"
toHornSort (F.FObj Symbol
x)     = Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
x -- P.parens ("obj" P.<+> toHornSMT x)
toHornSort Sort
F.FNum         = Doc
"num"
toHornSort t :: Sort
t@(F.FAbs Int
_ Sort
_) = Sort -> Doc
toHornAbsApp Sort
t
toHornSort t :: Sort
t@(F.FFunc Sort
_ Sort
_)= Sort -> Doc
toHornAbsApp Sort
t
toHornSort (F.FTC FTycon
c)      = FTycon -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT FTycon
c
toHornSort t :: Sort
t@(F.FApp Sort
_ Sort
_) = [Sort] -> Doc
toHornFApp (Sort -> [Sort]
F.unFApp Sort
t)

toHornAbsApp :: F.Sort -> P.Doc
toHornAbsApp :: Sort -> Doc
toHornAbsApp (Sort -> Maybe ([Int], [Sort], Sort)
F.functionSort -> Just ([Int]
vs, [Sort]
ss, Sort
s)) = Doc -> Doc
P.parens (Doc
"func" Doc -> Doc -> Doc
P.<+> Int -> Doc
P.int ([Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
vs) Doc -> Doc -> Doc
P.<+> [Sort] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [Sort]
ss Doc -> Doc -> Doc
P.<+> Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
s )
toHornAbsApp Sort
_                                    = [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error [Char]
"Unexpected nothing function sort"

toHornFApp     :: [F.Sort] -> P.Doc
toHornFApp :: [Sort] -> Doc
toHornFApp [Sort
t] = Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
t
toHornFApp [Sort]
ts  = [Sort] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [Sort]
ts

instance ToHornSMT F.Subst where
  toHornSMT :: SubstV Symbol -> Doc
toHornSMT (F.Su HashMap Symbol (ExprV Symbol)
m) = [(Symbol, ExprV Symbol)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (HashMap Symbol (ExprV Symbol) -> [(Symbol, ExprV Symbol)]
forall a b. Ord a => HashMap a b -> [(a, b)]
Misc.hashMapToAscList HashMap Symbol (ExprV Symbol)
m)

instance ToHornSMT (Bind a) where
  toHornSMT :: Bind a -> Doc
toHornSMT (Bind Symbol
x Sort
t Pred
p a
_) = Doc -> Doc
P.parens ((Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol
x, Sort
t) Doc -> Doc -> Doc
P.<+> Pred -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Pred
p)

instance ToHornSMT Pred where
  toHornSMT :: Pred -> Doc
toHornSMT (Reft ExprV Symbol
p)   = Doc -> Doc
P.parens (ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
p)
  toHornSMT (Var Symbol
k [Symbol]
xs) = [Doc] -> Doc
toHornMany (KVar -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol -> KVar
F.KV Symbol
k) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))
  toHornSMT (PAnd [Pred]
ps)  = [Doc] -> Doc
toHornMany (Doc
"and" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Pred -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Pred -> Doc) -> [Pred] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps))

instance ToHornSMT F.KVar where
  toHornSMT :: KVar -> Doc
toHornSMT (F.KV Symbol
k) = Doc
"$" Doc -> Doc -> Doc
P.<-> Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
k

instance ToHornSMT F.Expr where
  toHornSMT :: ExprV Symbol -> Doc
toHornSMT = ExprV Symbol -> Doc
toHornExpr

toHornExpr :: F.Expr -> P.Doc
toHornExpr :: ExprV Symbol -> Doc
toHornExpr (F.ESym SymConst
c)        = SymConst -> Doc
forall a. PPrint a => a -> Doc
F.pprint SymConst
c
toHornExpr (F.ECon Constant
c)        = Constant -> Doc
forall a. PPrint a => a -> Doc
F.pprint Constant
c
toHornExpr (F.EVar Symbol
s)        = Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
s
toHornExpr (F.ENeg ExprV Symbol
e)        = Doc -> Doc
P.parens (Doc
"-" Doc -> Doc -> Doc
P.<+> ExprV Symbol -> Doc
toHornExpr ExprV Symbol
e)
toHornExpr (F.EApp ExprV Symbol
e1 ExprV Symbol
e2)    = [ExprV Symbol] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.EBin Bop
o ExprV Symbol
e1 ExprV Symbol
e2)  = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp   (Bop -> Doc
forall a. Fixpoint a => a -> Doc
F.toFix Bop
o) [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.EIte ExprV Symbol
e1 ExprV Symbol
e2 ExprV Symbol
e3) = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"if"  [ExprV Symbol
e1, ExprV Symbol
e2, ExprV Symbol
e3]
toHornExpr (F.ECst ExprV Symbol
e Sort
t)      = [Doc] -> Doc
toHornMany [Doc
"cast", ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
t]
toHornExpr (F.PNot ExprV Symbol
p)        = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"not"  [ExprV Symbol
p]
toHornExpr (F.PImp ExprV Symbol
e1 ExprV Symbol
e2)    = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"=>"   [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.PIff ExprV Symbol
e1 ExprV Symbol
e2)    = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"<=>"  [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr e :: ExprV Symbol
e@ExprV Symbol
F.PTrue         = ExprV Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprV Symbol
e
toHornExpr e :: ExprV Symbol
e@ExprV Symbol
F.PFalse        = ExprV Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprV Symbol
e
toHornExpr (F.PAnd [ExprV Symbol]
es)       = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"and" [ExprV Symbol]
es
toHornExpr (F.POr  [ExprV Symbol]
es)       = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"or"  [ExprV Symbol]
es
toHornExpr (F.PAtom Brel
r ExprV Symbol
e1 ExprV Symbol
e2) = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp (Brel -> Doc
forall a. Fixpoint a => a -> Doc
F.toFix Brel
r) [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.PAll [(Symbol, Sort)]
xts ExprV Symbol
p)    = [Doc] -> Doc
toHornMany [Doc
"forall", [(Symbol, Sort)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, Sort)]
xts, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
p]
toHornExpr (F.PExist [(Symbol, Sort)]
xts ExprV Symbol
p)  = [Doc] -> Doc
toHornMany [Doc
"exists", [(Symbol, Sort)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, Sort)]
xts, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
p]
toHornExpr (F.ELam (Symbol, Sort)
b ExprV Symbol
e)      = [Doc] -> Doc
toHornMany [Doc
"lam", (Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol, Sort)
b, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e]
toHornExpr (F.ECoerc Sort
a Sort
t ExprV Symbol
e)  = [Doc] -> Doc
toHornMany [Doc
"coerce", Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
a, Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
t, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e]
toHornExpr (F.PKVar KVar
k SubstV Symbol
su)    = [Doc] -> Doc
toHornMany [KVar -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT KVar
k, SubstV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT SubstV Symbol
su]
toHornExpr (F.ETApp ExprV Symbol
e Sort
s)     = [Doc] -> Doc
toHornMany [Doc
"ETApp" , ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
s]
toHornExpr (F.ETAbs ExprV Symbol
e Symbol
s)     = [Doc] -> Doc
toHornMany [Doc
"ETAbs" , ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
s]
toHornExpr (F.PGrad KVar
k SubstV Symbol
_ GradInfo
_ ExprV Symbol
e) = [Doc] -> Doc
toHornMany [Doc
"&&", ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, KVar -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT KVar
k]

toHornOp :: ToHornSMT a => P.Doc -> [a] -> P.Doc
toHornOp :: forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
op [a]
es = [Doc] -> Doc
toHornMany (Doc
op Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
es))

instance ToHornSMT (Cstr a) where
  toHornSMT :: Cstr a -> Doc
toHornSMT = Cstr a -> Doc
forall a. Cstr a -> Doc
toHornCstr

toHornCstr :: Cstr a -> P.Doc
toHornCstr :: forall a. Cstr a -> Doc
toHornCstr (Head Pred
p a
_) = Pred -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Pred
p
toHornCstr (CAnd [Cstr a]
cs)  = (Cstr a -> Doc) -> [Cstr a] -> Doc
forall a. (a -> Doc) -> [a] -> Doc
toHornAnd Cstr a -> Doc
forall a. Cstr a -> Doc
toHornCstr [Cstr a]
cs
toHornCstr (All Bind a
b Cstr a
c)  = Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat [Doc
"forall" Doc -> Doc -> Doc
P.<+> Bind a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Bind a
b
                                         , Int -> Doc -> Doc
P.nest Int
1 (Cstr a -> Doc
forall a. Cstr a -> Doc
toHornCstr Cstr a
c)])
toHornCstr (Any Bind a
b Cstr a
c)  = Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat [Doc
"exists" Doc -> Doc -> Doc
P.<+> Bind a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Bind a
b
                                         , Int -> Doc -> Doc
P.nest Int
1 (Cstr a -> Doc
forall a. Cstr a -> Doc
toHornCstr Cstr a
c)])