-------------------------------------------------------------------------------
-- | 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          #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

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

-------------------------------------------------------------------------------
-- | @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
forall a. Eq a => Var a -> Var a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var a -> Var a -> Bool
$c/= :: forall a. Eq a => Var a -> Var a -> Bool
== :: Var a -> Var a -> Bool
$c== :: forall a. Eq a => Var a -> Var a -> Bool
Eq, Var a -> Var a -> Bool
Var a -> Var a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Var a)
forall a. Ord a => Var a -> Var a -> Bool
forall a. Ord a => Var a -> Var a -> Ordering
forall a. Ord a => Var a -> Var a -> Var a
min :: Var a -> Var a -> Var a
$cmin :: forall a. Ord a => Var a -> Var a -> Var a
max :: Var a -> Var a -> Var a
$cmax :: forall a. Ord a => Var a -> Var a -> Var a
>= :: Var a -> Var a -> Bool
$c>= :: forall a. Ord a => Var a -> Var a -> Bool
> :: Var a -> Var a -> Bool
$c> :: forall a. Ord a => Var a -> Var a -> Bool
<= :: Var a -> Var a -> Bool
$c<= :: forall a. Ord a => Var a -> Var a -> Bool
< :: Var a -> Var a -> Bool
$c< :: forall a. Ord a => Var a -> Var a -> Bool
compare :: Var a -> Var a -> Ordering
$ccompare :: forall a. Ord a => Var a -> Var a -> Ordering
Ord, Var a -> DataType
Var a -> Constr
forall {a}. Data a => Typeable (Var a)
forall a. Data a => Var a -> DataType
forall a. Data a => Var a -> Constr
forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Var a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Var a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Var a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
gmapT :: (forall b. Data b => b -> b) -> Var a -> Var a
$cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
dataTypeOf :: Var a -> DataType
$cdataTypeOf :: forall a. Data a => Var a -> DataType
toConstr :: Var a -> Constr
$ctoConstr :: forall a. Data a => Var a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
Data, Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Var a) x -> Var a
forall a x. Var a -> Rep (Var a) x
$cto :: forall a x. Rep (Var a) x -> Var a
$cfrom :: forall a x. Var a -> Rep (Var a) x
Generic, 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
<$ :: forall a b. a -> Var b -> Var a
$c<$ :: forall a b. a -> Var b -> Var a
fmap :: forall a b. (a -> b) -> Var a -> Var b
$cfmap :: forall a b. (a -> b) -> Var a -> Var b
Functor)

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


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

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

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

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

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

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

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

-------------------------------------------------------------------------------
quals :: Cstr a -> [F.Qualifier]
-------------------------------------------------------------------------------
quals :: forall a. Cstr a -> [Qualifier]
quals = forall a. PPrint a => String -> a -> a
F.tracepp String
"horn.quals" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
cstrQuals 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 = 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) = 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)  = 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)  = 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 (forall a. Bind a -> Pred
bPred Bind a
b) forall a. [a] -> [a] -> [a]
++ forall a. SEnv Sort -> Symbol -> Cstr a -> [Qualifier]
cstrQuals SEnv Sort
env' Symbol
bx Cstr a
c
  where
    env' :: SEnv Sort
env'          = forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
bx Sort
bt SEnv Sort
env
    bx :: Symbol
bx            = forall a. Bind a -> Symbol
bSym Bind a
b
    bt :: Sort
bt            = 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 Expr
p)  = SEnv Sort -> Symbol -> Expr -> [Qualifier]
exprQuals SEnv Sort
env Symbol
v Expr
p
predQuals SEnv Sort
env Symbol
v (PAnd [Pred]
ps) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SEnv Sort -> Symbol -> Pred -> [Qualifier]
predQuals SEnv Sort
env Symbol
v) [Pred]
ps
predQuals SEnv Sort
_   Symbol
_ Pred
_         = []

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

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

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


--------------------------------------------------------------------------------
-- | @Cst@ is an NNF Horn Constraint.
-------------------------------------------------------------------------------
-- Note that a @Bind@ is a simplified @F.SortedReft@ ...
data Bind 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 (Bind a -> DataType
Bind a -> Constr
forall {a}. Data a => Typeable (Bind a)
forall a. Data a => Bind a -> DataType
forall a. Data a => Bind a -> Constr
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 (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Bind a -> m (Bind a)
gmapQi :: forall u. Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> Bind a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Bind a -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r
gmapT :: (forall b. Data b => b -> b) -> Bind a -> Bind a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Bind a -> Bind a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> 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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Bind a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bind a))
dataTypeOf :: Bind a -> DataType
$cdataTypeOf :: forall a. Data a => Bind a -> DataType
toConstr :: Bind a -> Constr
$ctoConstr :: forall a. Data a => Bind a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bind a -> 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)
Data, Typeable, 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
$cto :: forall a x. Rep (Bind a) x -> Bind a
$cfrom :: forall a x. Bind a -> Rep (Bind a) x
Generic, 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
<$ :: forall a b. a -> Bind b -> Bind a
$c<$ :: forall a b. a -> Bind b -> Bind a
fmap :: forall a b. (a -> b) -> Bind a -> Bind b
$cfmap :: forall a b. (a -> b) -> Bind a -> Bind b
Functor, Bind a -> Bind a -> Bool
forall a. Eq a => Bind a -> Bind a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bind a -> Bind a -> Bool
$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
Eq)

instance F.Subable (Bind a) where
    syms :: Bind a -> [Symbol]
syms     (Bind Symbol
x Sort
_ Pred
p a
_) = Symbol
x forall a. a -> [a] -> [a]
: 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) = forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind (Symbol -> Symbol
f Symbol
v) Sort
t (forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f Pred
p) a
a
    substf :: (Symbol -> Expr) -> Bind a -> Bind a
substf Symbol -> Expr
f (Bind Symbol
v Sort
t Pred
p a
a) = forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind Symbol
v Sort
t (forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf ((Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
F.substfExcept Symbol -> Expr
f [Symbol
v]) Pred
p) a
a
    -- subst su (Bind x t p) = (Bind x t (F.subst su p))
    subst :: Subst -> Bind a -> Bind a
subst Subst
su (Bind Symbol
v Sort
t Pred
p a
a)  = forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind Symbol
v Sort
t (forall a. Subable a => Subst -> a -> a
F.subst (Subst -> [Symbol] -> Subst
F.substExcept Subst
su [Symbol
v]) Pred
p) a
a
    subst1 :: Bind a -> (Symbol, Expr) -> Bind a
subst1 (Bind Symbol
v Sort
t Pred
p a
a) (Symbol, Expr)
su = forall a. Symbol -> Sort -> Pred -> a -> Bind a
Bind Symbol
v Sort
t (forall a. Subable a => [Symbol] -> a -> (Symbol, Expr) -> a
F.subst1Except [Symbol
v] Pred
p (Symbol, Expr)
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 (Cstr a -> DataType
Cstr a -> Constr
forall {a}. Data a => Typeable (Cstr a)
forall a. Data a => Cstr a -> DataType
forall a. Data a => Cstr a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Cstr a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Cstr a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Cstr a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Cstr a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Cstr a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Cstr a -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r
gmapT :: (forall b. Data b => b -> b) -> Cstr a -> Cstr a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Cstr a -> Cstr a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Cstr a))
dataTypeOf :: Cstr a -> DataType
$cdataTypeOf :: forall a. Data a => Cstr a -> DataType
toConstr :: Cstr a -> Constr
$ctoConstr :: forall a. Data a => Cstr a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Cstr a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Cstr a -> c (Cstr a)
Data, Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Cstr a) x -> Cstr a
forall a x. Cstr a -> Rep (Cstr a) x
$cto :: forall a x. Rep (Cstr a) x -> Cstr a
$cfrom :: forall a x. Cstr a -> Rep (Cstr a) x
Generic, 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
<$ :: forall a b. a -> Cstr b -> Cstr a
$c<$ :: forall a b. a -> Cstr b -> Cstr a
fmap :: forall a b. (a -> b) -> Cstr a -> Cstr b
$cfmap :: forall a b. (a -> b) -> Cstr a -> Cstr b
Functor, Cstr a -> Cstr a -> Bool
forall a. Eq a => Cstr a -> Cstr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cstr a -> Cstr a -> Bool
$c/= :: forall a. Eq a => Cstr a -> Cstr a -> Bool
== :: Cstr a -> Cstr a -> Bool
$c== :: forall a. Eq a => Cstr a -> Cstr a -> Bool
Eq)

cLabel :: Cstr a -> a
cLabel :: forall a. Cstr a -> a
cLabel Cstr a
cstr = case forall {a}. Cstr a -> [a]
go Cstr a
cstr of
  [] -> forall a. String -> a
F.panic String
"everything is true!!!"
  a
label:[a]
_ -> a
label
  where
    go :: Cstr a -> [a]
go (Head Pred
_ a
l)   = [a
l]
    go (CAnd [Cstr a]
cs)    = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ Cstr a -> [a]
go 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 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
  }
  deriving (Query a -> DataType
Query a -> Constr
forall {a}. Data a => Typeable (Query a)
forall a. Data a => Query a -> DataType
forall a. Data a => Query a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Query a -> Query a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Query a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Query a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Query a -> m (Query a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Query a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Query a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Query a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Query a -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Query a -> r
gmapT :: (forall b. Data b => b -> b) -> Query a -> Query a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Query a -> Query a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Query a))
dataTypeOf :: Query a -> DataType
$cdataTypeOf :: forall a. Data a => Query a -> DataType
toConstr :: Query a -> Constr
$ctoConstr :: forall a. Data a => Query a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Query a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Query a -> c (Query a)
Data, Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Query a) x -> Query a
forall a x. Query a -> Rep (Query a) x
$cto :: forall a x. Rep (Query a) x -> Query a
$cfrom :: forall a x. Query a -> Rep (Query a) x
Generic, 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
<$ :: forall a b. a -> Query b -> Query a
$c<$ :: forall a b. a -> Query b -> Query a
fmap :: forall a b. (a -> b) -> Query a -> Query b
$cfmap :: forall a b. (a -> b) -> Query a -> Query b
Functor)

-- | 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
Tag -> DataType
Tag -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Tag -> m Tag
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Tag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Tag -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Tag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Tag -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r
gmapT :: (forall b. Data b => b -> b) -> Tag -> Tag
$cgmapT :: (forall b. Data b => b -> b) -> Tag -> Tag
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Tag)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Tag)
dataTypeOf :: Tag -> DataType
$cdataTypeOf :: Tag -> DataType
toConstr :: Tag -> Constr
$ctoConstr :: Tag -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Tag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Tag
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tag -> c Tag
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tag -> c Tag
Data, Typeable, 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
$cto :: forall x. Rep Tag x -> Tag
$cfrom :: forall x. Tag -> Rep Tag x
Generic, Int -> Tag -> ShowS
[Tag] -> ShowS
Tag -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tag] -> ShowS
$cshowList :: [Tag] -> ShowS
show :: Tag -> String
$cshow :: Tag -> String
showsPrec :: Int -> Tag -> ShowS
$cshowsPrec :: Int -> Tag -> ShowS
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 String
s) = Doc
"\"" forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
s forall a. Semigroup a => a -> a -> a
<> Doc
"\""

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

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

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

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

ppQual :: F.Qualifier -> P.Doc
ppQual :: Qualifier -> Doc
ppQual (F.Q Symbol
n [QualParam]
xts Expr
p SourcePos
_) =  Doc -> Doc
P.parens (Doc
"qualif" Doc -> Doc -> Doc
P.<+> forall a. PPrint a => a -> Doc
F.pprint Symbol
n Doc -> Doc -> Doc
P.<+> [Doc] -> Doc
ppBlanks (QualParam -> Doc
ppArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
xts) Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens (forall a. PPrint a => a -> Doc
F.pprint Expr
p))
  where
    ppArg :: QualParam -> Doc
ppArg QualParam
qp    = Doc -> Doc
P.parens forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
F.pprint (QualParam -> Symbol
F.qpSym QualParam
qp) Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens (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.<-> forall a. PPrint a => a -> Doc
F.pprint Symbol
k Doc -> Doc -> Doc
P.<+> [Doc] -> Doc
ppBlanks (Doc -> Doc
P.parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => a -> Doc
F.pprint 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 (forall a. a -> [a] -> [a]
L.intersperse Doc
" " [Doc]
ds))

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

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

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

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

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

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

instance F.PPrint Pred where
  pprintPrec :: Int -> Tidy -> Pred -> Doc
pprintPrec Int
k Tidy
t (Reft Expr
p)   = Doc -> Doc
P.parens forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec Int
k Tidy
t Expr
p
  pprintPrec Int
_ Tidy
_ (Var Symbol
x [Symbol]
xs) = Doc -> Doc
P.parens forall a b. (a -> b) -> a -> b
$ String -> Doc
P.ptext String
"$" forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
P.hsep (String -> Doc
P.ptext forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
F.symbolString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol
xforall a. a -> [a] -> [a]
:[Symbol]
xs)
  pprintPrec Int
k Tidy
t (PAnd [Pred]
ps)  = Doc -> Doc
P.parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat forall a b. (a -> b) -> a -> b
$ String -> Doc
P.ptext String
"and" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kforall 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [ String -> Doc
P.ptext String
"forall" Doc -> Doc -> Doc
P.<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kforall a. Num a => a -> a -> a
+Int
2) Tidy
t Bind a
b
                                                , forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kforall 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 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [String -> Doc
P.ptext String
"exists" Doc -> Doc -> Doc
P.<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kforall a. Num a => a -> a -> a
+Int
2) Tidy
t Bind a
b
                                                , forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kforall 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 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat  forall a b. (a -> b) -> a -> b
$ String -> Doc
P.ptext String
"and" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a. PPrint a => Int -> Tidy -> a -> Doc
F.pprintPrec (Int
kforall 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 = String -> Doc
P.ptext forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Bind a
b