{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE DeriveTraversable         #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE NamedFieldPuns            #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeFamilies              #-}

{-# OPTIONS_GHC -Wall #-}

{-|

Defines the syntax of invariant annotations. See "Camfort.Specification.Hoare"
for a high-level overview.

In this module, the word \'primitive\' is used to refer to untyped expression
syntax (as opposed to the typed expression syntax defined in
"Language.Fortran.Model.Op").

-}
module Camfort.Specification.Hoare.Syntax where

import           Data.Data

import           Control.Lens

import qualified Language.Fortran.AST       as F

import           Language.Expression.Pretty


-- * Syntax Types

-- | A type of primitive logical operators.
data PrimLogic a
  = PLAnd a a
  | PLOr a a
  | PLImpl a a
  | PLEquiv a a
  | PLNot a
  | PLLit Bool
  deriving (Typeable, Typeable (PrimLogic a)
DataType
Constr
Typeable (PrimLogic a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PrimLogic a))
-> (PrimLogic a -> Constr)
-> (PrimLogic a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PrimLogic a)))
-> ((forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r)
-> (forall u. (forall d. Data d => d -> u) -> PrimLogic a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PrimLogic a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a))
-> Data (PrimLogic a)
PrimLogic a -> DataType
PrimLogic a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a))
(forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimLogic a)
forall a. Data a => Typeable (PrimLogic a)
forall a. Data a => PrimLogic a -> DataType
forall a. Data a => PrimLogic a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> PrimLogic a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> PrimLogic a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimLogic a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimLogic 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) -> PrimLogic a -> u
forall u. (forall d. Data d => d -> u) -> PrimLogic a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimLogic a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimLogic a))
$cPLLit :: Constr
$cPLNot :: Constr
$cPLEquiv :: Constr
$cPLImpl :: Constr
$cPLOr :: Constr
$cPLAnd :: Constr
$tPrimLogic :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
gmapMp :: (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
gmapM :: (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> PrimLogic a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> PrimLogic a -> u
gmapQ :: (forall d. Data d => d -> u) -> PrimLogic a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> PrimLogic a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
gmapT :: (forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimLogic a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimLogic a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a))
dataTypeOf :: PrimLogic a -> DataType
$cdataTypeOf :: forall a. Data a => PrimLogic a -> DataType
toConstr :: PrimLogic a -> Constr
$ctoConstr :: forall a. Data a => PrimLogic a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimLogic a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimLogic a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a)
$cp1Data :: forall a. Data a => Typeable (PrimLogic a)
Data, Int -> PrimLogic a -> ShowS
[PrimLogic a] -> ShowS
PrimLogic a -> String
(Int -> PrimLogic a -> ShowS)
-> (PrimLogic a -> String)
-> ([PrimLogic a] -> ShowS)
-> Show (PrimLogic a)
forall a. Show a => Int -> PrimLogic a -> ShowS
forall a. Show a => [PrimLogic a] -> ShowS
forall a. Show a => PrimLogic a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PrimLogic a] -> ShowS
$cshowList :: forall a. Show a => [PrimLogic a] -> ShowS
show :: PrimLogic a -> String
$cshow :: forall a. Show a => PrimLogic a -> String
showsPrec :: Int -> PrimLogic a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> PrimLogic a -> ShowS
Show, PrimLogic a -> PrimLogic a -> Bool
(PrimLogic a -> PrimLogic a -> Bool)
-> (PrimLogic a -> PrimLogic a -> Bool) -> Eq (PrimLogic a)
forall a. Eq a => PrimLogic a -> PrimLogic a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrimLogic a -> PrimLogic a -> Bool
$c/= :: forall a. Eq a => PrimLogic a -> PrimLogic a -> Bool
== :: PrimLogic a -> PrimLogic a -> Bool
$c== :: forall a. Eq a => PrimLogic a -> PrimLogic a -> Bool
Eq, a -> PrimLogic b -> PrimLogic a
(a -> b) -> PrimLogic a -> PrimLogic b
(forall a b. (a -> b) -> PrimLogic a -> PrimLogic b)
-> (forall a b. a -> PrimLogic b -> PrimLogic a)
-> Functor PrimLogic
forall a b. a -> PrimLogic b -> PrimLogic a
forall a b. (a -> b) -> PrimLogic a -> PrimLogic b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> PrimLogic b -> PrimLogic a
$c<$ :: forall a b. a -> PrimLogic b -> PrimLogic a
fmap :: (a -> b) -> PrimLogic a -> PrimLogic b
$cfmap :: forall a b. (a -> b) -> PrimLogic a -> PrimLogic b
Functor, PrimLogic a -> Bool
(a -> m) -> PrimLogic a -> m
(a -> b -> b) -> b -> PrimLogic a -> b
(forall m. Monoid m => PrimLogic m -> m)
-> (forall m a. Monoid m => (a -> m) -> PrimLogic a -> m)
-> (forall m a. Monoid m => (a -> m) -> PrimLogic a -> m)
-> (forall a b. (a -> b -> b) -> b -> PrimLogic a -> b)
-> (forall a b. (a -> b -> b) -> b -> PrimLogic a -> b)
-> (forall b a. (b -> a -> b) -> b -> PrimLogic a -> b)
-> (forall b a. (b -> a -> b) -> b -> PrimLogic a -> b)
-> (forall a. (a -> a -> a) -> PrimLogic a -> a)
-> (forall a. (a -> a -> a) -> PrimLogic a -> a)
-> (forall a. PrimLogic a -> [a])
-> (forall a. PrimLogic a -> Bool)
-> (forall a. PrimLogic a -> Int)
-> (forall a. Eq a => a -> PrimLogic a -> Bool)
-> (forall a. Ord a => PrimLogic a -> a)
-> (forall a. Ord a => PrimLogic a -> a)
-> (forall a. Num a => PrimLogic a -> a)
-> (forall a. Num a => PrimLogic a -> a)
-> Foldable PrimLogic
forall a. Eq a => a -> PrimLogic a -> Bool
forall a. Num a => PrimLogic a -> a
forall a. Ord a => PrimLogic a -> a
forall m. Monoid m => PrimLogic m -> m
forall a. PrimLogic a -> Bool
forall a. PrimLogic a -> Int
forall a. PrimLogic a -> [a]
forall a. (a -> a -> a) -> PrimLogic a -> a
forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: PrimLogic a -> a
$cproduct :: forall a. Num a => PrimLogic a -> a
sum :: PrimLogic a -> a
$csum :: forall a. Num a => PrimLogic a -> a
minimum :: PrimLogic a -> a
$cminimum :: forall a. Ord a => PrimLogic a -> a
maximum :: PrimLogic a -> a
$cmaximum :: forall a. Ord a => PrimLogic a -> a
elem :: a -> PrimLogic a -> Bool
$celem :: forall a. Eq a => a -> PrimLogic a -> Bool
length :: PrimLogic a -> Int
$clength :: forall a. PrimLogic a -> Int
null :: PrimLogic a -> Bool
$cnull :: forall a. PrimLogic a -> Bool
toList :: PrimLogic a -> [a]
$ctoList :: forall a. PrimLogic a -> [a]
foldl1 :: (a -> a -> a) -> PrimLogic a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> PrimLogic a -> a
foldr1 :: (a -> a -> a) -> PrimLogic a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> PrimLogic a -> a
foldl' :: (b -> a -> b) -> b -> PrimLogic a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
foldl :: (b -> a -> b) -> b -> PrimLogic a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
foldr' :: (a -> b -> b) -> b -> PrimLogic a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
foldr :: (a -> b -> b) -> b -> PrimLogic a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
foldMap' :: (a -> m) -> PrimLogic a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
foldMap :: (a -> m) -> PrimLogic a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
fold :: PrimLogic m -> m
$cfold :: forall m. Monoid m => PrimLogic m -> m
Foldable, Functor PrimLogic
Foldable PrimLogic
Functor PrimLogic
-> Foldable PrimLogic
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> PrimLogic a -> f (PrimLogic b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    PrimLogic (f a) -> f (PrimLogic a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> PrimLogic a -> m (PrimLogic b))
-> (forall (m :: * -> *) a.
    Monad m =>
    PrimLogic (m a) -> m (PrimLogic a))
-> Traversable PrimLogic
(a -> f b) -> PrimLogic a -> f (PrimLogic b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
PrimLogic (m a) -> m (PrimLogic a)
forall (f :: * -> *) a.
Applicative f =>
PrimLogic (f a) -> f (PrimLogic a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PrimLogic a -> m (PrimLogic b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PrimLogic a -> f (PrimLogic b)
sequence :: PrimLogic (m a) -> m (PrimLogic a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
PrimLogic (m a) -> m (PrimLogic a)
mapM :: (a -> m b) -> PrimLogic a -> m (PrimLogic b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PrimLogic a -> m (PrimLogic b)
sequenceA :: PrimLogic (f a) -> f (PrimLogic a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
PrimLogic (f a) -> f (PrimLogic a)
traverse :: (a -> f b) -> PrimLogic a -> f (PrimLogic b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PrimLogic a -> f (PrimLogic b)
$cp2Traversable :: Foldable PrimLogic
$cp1Traversable :: Functor PrimLogic
Traversable)


-- | Logical expressions over Fortran expressions.
data PrimFormula ann
  = PFExpr (F.Expression ann)
  | PFLogical (PrimLogic (PrimFormula ann))
  deriving (Typeable, Typeable (PrimFormula ann)
DataType
Constr
Typeable (PrimFormula ann)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PrimFormula ann))
-> (PrimFormula ann -> Constr)
-> (PrimFormula ann -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PrimFormula ann)))
-> ((forall b. Data b => b -> b)
    -> PrimFormula ann -> PrimFormula ann)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> PrimFormula ann -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PrimFormula ann -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PrimFormula ann -> m (PrimFormula ann))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PrimFormula ann -> m (PrimFormula ann))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PrimFormula ann -> m (PrimFormula ann))
-> Data (PrimFormula ann)
PrimFormula ann -> DataType
PrimFormula ann -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann))
(forall b. Data b => b -> b) -> PrimFormula ann -> PrimFormula ann
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimFormula ann)
forall ann. Data ann => Typeable (PrimFormula ann)
forall ann. Data ann => PrimFormula ann -> DataType
forall ann. Data ann => PrimFormula ann -> Constr
forall ann.
Data ann =>
(forall b. Data b => b -> b) -> PrimFormula ann -> PrimFormula ann
forall ann u.
Data ann =>
Int -> (forall d. Data d => d -> u) -> PrimFormula ann -> u
forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> PrimFormula ann -> [u]
forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
forall ann r r'.
Data ann =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
forall ann (c :: * -> *).
Data ann =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimFormula ann)
forall ann (c :: * -> *).
Data ann =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann)
forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann))
forall ann (t :: * -> * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimFormula ann))
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) -> PrimFormula ann -> u
forall u. (forall d. Data d => d -> u) -> PrimFormula ann -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimFormula ann)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimFormula ann))
$cPFLogical :: Constr
$cPFExpr :: Constr
$tPrimFormula :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
$cgmapMo :: forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
gmapMp :: (forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
$cgmapMp :: forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
gmapM :: (forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
$cgmapM :: forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d)
-> PrimFormula ann -> m (PrimFormula ann)
gmapQi :: Int -> (forall d. Data d => d -> u) -> PrimFormula ann -> u
$cgmapQi :: forall ann u.
Data ann =>
Int -> (forall d. Data d => d -> u) -> PrimFormula ann -> u
gmapQ :: (forall d. Data d => d -> u) -> PrimFormula ann -> [u]
$cgmapQ :: forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> PrimFormula ann -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
$cgmapQr :: forall ann r r'.
Data ann =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
$cgmapQl :: forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r
gmapT :: (forall b. Data b => b -> b) -> PrimFormula ann -> PrimFormula ann
$cgmapT :: forall ann.
Data ann =>
(forall b. Data b => b -> b) -> PrimFormula ann -> PrimFormula ann
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimFormula ann))
$cdataCast2 :: forall ann (t :: * -> * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimFormula ann))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann))
$cdataCast1 :: forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann))
dataTypeOf :: PrimFormula ann -> DataType
$cdataTypeOf :: forall ann. Data ann => PrimFormula ann -> DataType
toConstr :: PrimFormula ann -> Constr
$ctoConstr :: forall ann. Data ann => PrimFormula ann -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimFormula ann)
$cgunfold :: forall ann (c :: * -> *).
Data ann =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimFormula ann)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann)
$cgfoldl :: forall ann (c :: * -> *).
Data ann =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann)
$cp1Data :: forall ann. Data ann => Typeable (PrimFormula ann)
Data, Int -> PrimFormula ann -> ShowS
[PrimFormula ann] -> ShowS
PrimFormula ann -> String
(Int -> PrimFormula ann -> ShowS)
-> (PrimFormula ann -> String)
-> ([PrimFormula ann] -> ShowS)
-> Show (PrimFormula ann)
forall ann. Show ann => Int -> PrimFormula ann -> ShowS
forall ann. Show ann => [PrimFormula ann] -> ShowS
forall ann. Show ann => PrimFormula ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PrimFormula ann] -> ShowS
$cshowList :: forall ann. Show ann => [PrimFormula ann] -> ShowS
show :: PrimFormula ann -> String
$cshow :: forall ann. Show ann => PrimFormula ann -> String
showsPrec :: Int -> PrimFormula ann -> ShowS
$cshowsPrec :: forall ann. Show ann => Int -> PrimFormula ann -> ShowS
Show, PrimFormula ann -> PrimFormula ann -> Bool
(PrimFormula ann -> PrimFormula ann -> Bool)
-> (PrimFormula ann -> PrimFormula ann -> Bool)
-> Eq (PrimFormula ann)
forall ann. Eq ann => PrimFormula ann -> PrimFormula ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrimFormula ann -> PrimFormula ann -> Bool
$c/= :: forall ann. Eq ann => PrimFormula ann -> PrimFormula ann -> Bool
== :: PrimFormula ann -> PrimFormula ann -> Bool
$c== :: forall ann. Eq ann => PrimFormula ann -> PrimFormula ann -> Bool
Eq, a -> PrimFormula b -> PrimFormula a
(a -> b) -> PrimFormula a -> PrimFormula b
(forall a b. (a -> b) -> PrimFormula a -> PrimFormula b)
-> (forall a b. a -> PrimFormula b -> PrimFormula a)
-> Functor PrimFormula
forall a b. a -> PrimFormula b -> PrimFormula a
forall a b. (a -> b) -> PrimFormula a -> PrimFormula b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> PrimFormula b -> PrimFormula a
$c<$ :: forall a b. a -> PrimFormula b -> PrimFormula a
fmap :: (a -> b) -> PrimFormula a -> PrimFormula b
$cfmap :: forall a b. (a -> b) -> PrimFormula a -> PrimFormula b
Functor)


-- | Labels for the keyword used in @static_assert@ annotations.
data SpecKind
  = SpecPre
    -- ^ @static_assert pre(...)@
  | SpecPost
    -- ^ @static_assert post(...)@
  | SpecSeq
    -- ^ @static_assert seq(...)@
  | SpecInvariant
    -- ^ @static_assert invariant(...)@
  deriving (Int -> SpecKind -> ShowS
[SpecKind] -> ShowS
SpecKind -> String
(Int -> SpecKind -> ShowS)
-> (SpecKind -> String) -> ([SpecKind] -> ShowS) -> Show SpecKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SpecKind] -> ShowS
$cshowList :: [SpecKind] -> ShowS
show :: SpecKind -> String
$cshow :: SpecKind -> String
showsPrec :: Int -> SpecKind -> ShowS
$cshowsPrec :: Int -> SpecKind -> ShowS
Show, SpecKind -> SpecKind -> Bool
(SpecKind -> SpecKind -> Bool)
-> (SpecKind -> SpecKind -> Bool) -> Eq SpecKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SpecKind -> SpecKind -> Bool
$c/= :: SpecKind -> SpecKind -> Bool
== :: SpecKind -> SpecKind -> Bool
$c== :: SpecKind -> SpecKind -> Bool
Eq, Typeable, Typeable SpecKind
DataType
Constr
Typeable SpecKind
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SpecKind -> c SpecKind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SpecKind)
-> (SpecKind -> Constr)
-> (SpecKind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SpecKind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecKind))
-> ((forall b. Data b => b -> b) -> SpecKind -> SpecKind)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SpecKind -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SpecKind -> r)
-> (forall u. (forall d. Data d => d -> u) -> SpecKind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SpecKind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind)
-> Data SpecKind
SpecKind -> DataType
SpecKind -> Constr
(forall b. Data b => b -> b) -> SpecKind -> SpecKind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecKind -> c SpecKind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SpecKind
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) -> SpecKind -> u
forall u. (forall d. Data d => d -> u) -> SpecKind -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecKind -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecKind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SpecKind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecKind -> c SpecKind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SpecKind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecKind)
$cSpecInvariant :: Constr
$cSpecSeq :: Constr
$cSpecPost :: Constr
$cSpecPre :: Constr
$tSpecKind :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
gmapMp :: (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
gmapM :: (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SpecKind -> m SpecKind
gmapQi :: Int -> (forall d. Data d => d -> u) -> SpecKind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SpecKind -> u
gmapQ :: (forall d. Data d => d -> u) -> SpecKind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SpecKind -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecKind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecKind -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecKind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecKind -> r
gmapT :: (forall b. Data b => b -> b) -> SpecKind -> SpecKind
$cgmapT :: (forall b. Data b => b -> b) -> SpecKind -> SpecKind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecKind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecKind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SpecKind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SpecKind)
dataTypeOf :: SpecKind -> DataType
$cdataTypeOf :: SpecKind -> DataType
toConstr :: SpecKind -> Constr
$ctoConstr :: SpecKind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SpecKind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SpecKind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecKind -> c SpecKind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecKind -> c SpecKind
$cp1Data :: Typeable SpecKind
Data)


-- | A @static_assert@ annotation.
data Specification a =
  Specification
  { Specification a -> SpecKind
_specType    :: SpecKind
  , Specification a -> a
_specFormula :: a
  }
  deriving (Typeable, Typeable (Specification a)
DataType
Constr
Typeable (Specification a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Specification a -> c (Specification a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Specification a))
-> (Specification a -> Constr)
-> (Specification a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Specification a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Specification a)))
-> ((forall b. Data b => b -> b)
    -> Specification a -> Specification a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Specification a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Specification a -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> Specification a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Specification a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Specification a -> m (Specification a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Specification a -> m (Specification a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Specification a -> m (Specification a))
-> Data (Specification a)
Specification a -> DataType
Specification a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Specification a))
(forall b. Data b => b -> b) -> Specification a -> Specification a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specification a -> c (Specification a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Specification a)
forall a. Data a => Typeable (Specification a)
forall a. Data a => Specification a -> DataType
forall a. Data a => Specification a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Specification a -> Specification a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Specification a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Specification a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Specification a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specification a -> c (Specification a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Specification a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Specification 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) -> Specification a -> u
forall u. (forall d. Data d => d -> u) -> Specification a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Specification a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specification a -> c (Specification a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Specification a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Specification a))
$cSpecification :: Constr
$tSpecification :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
gmapMp :: (forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
gmapM :: (forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Specification a -> m (Specification a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Specification a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Specification a -> u
gmapQ :: (forall d. Data d => d -> u) -> Specification a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Specification a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specification a -> r
gmapT :: (forall b. Data b => b -> b) -> Specification a -> Specification a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Specification a -> Specification a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Specification a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Specification a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Specification a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Specification a))
dataTypeOf :: Specification a -> DataType
$cdataTypeOf :: forall a. Data a => Specification a -> DataType
toConstr :: Specification a -> Constr
$ctoConstr :: forall a. Data a => Specification a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Specification a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Specification a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specification a -> c (Specification a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specification a -> c (Specification a)
$cp1Data :: forall a. Data a => Typeable (Specification a)
Data, Specification a -> Specification a -> Bool
(Specification a -> Specification a -> Bool)
-> (Specification a -> Specification a -> Bool)
-> Eq (Specification a)
forall a. Eq a => Specification a -> Specification a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Specification a -> Specification a -> Bool
$c/= :: forall a. Eq a => Specification a -> Specification a -> Bool
== :: Specification a -> Specification a -> Bool
$c== :: forall a. Eq a => Specification a -> Specification a -> Bool
Eq, a -> Specification b -> Specification a
(a -> b) -> Specification a -> Specification b
(forall a b. (a -> b) -> Specification a -> Specification b)
-> (forall a b. a -> Specification b -> Specification a)
-> Functor Specification
forall a b. a -> Specification b -> Specification a
forall a b. (a -> b) -> Specification a -> Specification b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Specification b -> Specification a
$c<$ :: forall a b. a -> Specification b -> Specification a
fmap :: (a -> b) -> Specification a -> Specification b
$cfmap :: forall a b. (a -> b) -> Specification a -> Specification b
Functor)


-- | A @decl_aux@ annotation.
data AuxDecl ann =
  AuxDecl
  { AuxDecl ann -> String
_adName :: F.Name
  , AuxDecl ann -> TypeSpec ann
_adTy   :: F.TypeSpec ann
  }
  deriving (Typeable, Typeable (AuxDecl ann)
DataType
Constr
Typeable (AuxDecl ann)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (AuxDecl ann))
-> (AuxDecl ann -> Constr)
-> (AuxDecl ann -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (AuxDecl ann)))
-> ((forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r)
-> (forall u. (forall d. Data d => d -> u) -> AuxDecl ann -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> AuxDecl ann -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann))
-> Data (AuxDecl ann)
AuxDecl ann -> DataType
AuxDecl ann -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann))
(forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (AuxDecl ann)
forall ann. Data ann => Typeable (AuxDecl ann)
forall ann. Data ann => AuxDecl ann -> DataType
forall ann. Data ann => AuxDecl ann -> Constr
forall ann.
Data ann =>
(forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
forall ann u.
Data ann =>
Int -> (forall d. Data d => d -> u) -> AuxDecl ann -> u
forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> AuxDecl ann -> [u]
forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
forall ann r r'.
Data ann =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
forall ann (c :: * -> *).
Data ann =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (AuxDecl ann)
forall ann (c :: * -> *).
Data ann =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann)
forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann))
forall ann (t :: * -> * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (AuxDecl ann))
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) -> AuxDecl ann -> u
forall u. (forall d. Data d => d -> u) -> AuxDecl ann -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (AuxDecl ann)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (AuxDecl ann))
$cAuxDecl :: Constr
$tAuxDecl :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
$cgmapMo :: forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
gmapMp :: (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
$cgmapMp :: forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
gmapM :: (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
$cgmapM :: forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
gmapQi :: Int -> (forall d. Data d => d -> u) -> AuxDecl ann -> u
$cgmapQi :: forall ann u.
Data ann =>
Int -> (forall d. Data d => d -> u) -> AuxDecl ann -> u
gmapQ :: (forall d. Data d => d -> u) -> AuxDecl ann -> [u]
$cgmapQ :: forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> AuxDecl ann -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
$cgmapQr :: forall ann r r'.
Data ann =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
$cgmapQl :: forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
gmapT :: (forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
$cgmapT :: forall ann.
Data ann =>
(forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (AuxDecl ann))
$cdataCast2 :: forall ann (t :: * -> * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (AuxDecl ann))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann))
$cdataCast1 :: forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann))
dataTypeOf :: AuxDecl ann -> DataType
$cdataTypeOf :: forall ann. Data ann => AuxDecl ann -> DataType
toConstr :: AuxDecl ann -> Constr
$ctoConstr :: forall ann. Data ann => AuxDecl ann -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (AuxDecl ann)
$cgunfold :: forall ann (c :: * -> *).
Data ann =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (AuxDecl ann)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann)
$cgfoldl :: forall ann (c :: * -> *).
Data ann =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann)
$cp1Data :: forall ann. Data ann => Typeable (AuxDecl ann)
Data, Int -> AuxDecl ann -> ShowS
[AuxDecl ann] -> ShowS
AuxDecl ann -> String
(Int -> AuxDecl ann -> ShowS)
-> (AuxDecl ann -> String)
-> ([AuxDecl ann] -> ShowS)
-> Show (AuxDecl ann)
forall ann. Show ann => Int -> AuxDecl ann -> ShowS
forall ann. Show ann => [AuxDecl ann] -> ShowS
forall ann. Show ann => AuxDecl ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AuxDecl ann] -> ShowS
$cshowList :: forall ann. Show ann => [AuxDecl ann] -> ShowS
show :: AuxDecl ann -> String
$cshow :: forall ann. Show ann => AuxDecl ann -> String
showsPrec :: Int -> AuxDecl ann -> ShowS
$cshowsPrec :: forall ann. Show ann => Int -> AuxDecl ann -> ShowS
Show, AuxDecl ann -> AuxDecl ann -> Bool
(AuxDecl ann -> AuxDecl ann -> Bool)
-> (AuxDecl ann -> AuxDecl ann -> Bool) -> Eq (AuxDecl ann)
forall ann. Eq ann => AuxDecl ann -> AuxDecl ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AuxDecl ann -> AuxDecl ann -> Bool
$c/= :: forall ann. Eq ann => AuxDecl ann -> AuxDecl ann -> Bool
== :: AuxDecl ann -> AuxDecl ann -> Bool
$c== :: forall ann. Eq ann => AuxDecl ann -> AuxDecl ann -> Bool
Eq, a -> AuxDecl b -> AuxDecl a
(a -> b) -> AuxDecl a -> AuxDecl b
(forall a b. (a -> b) -> AuxDecl a -> AuxDecl b)
-> (forall a b. a -> AuxDecl b -> AuxDecl a) -> Functor AuxDecl
forall a b. a -> AuxDecl b -> AuxDecl a
forall a b. (a -> b) -> AuxDecl a -> AuxDecl b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> AuxDecl b -> AuxDecl a
$c<$ :: forall a b. a -> AuxDecl b -> AuxDecl a
fmap :: (a -> b) -> AuxDecl a -> AuxDecl b
$cfmap :: forall a b. (a -> b) -> AuxDecl a -> AuxDecl b
Functor)


-- | A specification over untyped logical expressions.
type PrimSpec ann = Specification (PrimFormula ann)


-- | A @static_assert@ or @decl_aux@ annotation.
data SpecOrDecl ann =
    SodSpec (PrimSpec ann)
  | SodDecl (AuxDecl ann)
  deriving (Typeable, Typeable (SpecOrDecl ann)
DataType
Constr
Typeable (SpecOrDecl ann)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann))
-> (SpecOrDecl ann -> Constr)
-> (SpecOrDecl ann -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (SpecOrDecl ann)))
-> ((forall b. Data b => b -> b)
    -> SpecOrDecl ann -> SpecOrDecl ann)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> SpecOrDecl ann -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SpecOrDecl ann -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> SpecOrDecl ann -> m (SpecOrDecl ann))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SpecOrDecl ann -> m (SpecOrDecl ann))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SpecOrDecl ann -> m (SpecOrDecl ann))
-> Data (SpecOrDecl ann)
SpecOrDecl ann -> DataType
SpecOrDecl ann -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann))
(forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann)
forall ann. Data ann => Typeable (SpecOrDecl ann)
forall ann. Data ann => SpecOrDecl ann -> DataType
forall ann. Data ann => SpecOrDecl ann -> Constr
forall ann.
Data ann =>
(forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
forall ann u.
Data ann =>
Int -> (forall d. Data d => d -> u) -> SpecOrDecl ann -> u
forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> SpecOrDecl ann -> [u]
forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
forall ann r r'.
Data ann =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
forall ann (c :: * -> *).
Data ann =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann)
forall ann (c :: * -> *).
Data ann =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann)
forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann))
forall ann (t :: * -> * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SpecOrDecl ann))
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) -> SpecOrDecl ann -> u
forall u. (forall d. Data d => d -> u) -> SpecOrDecl ann -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SpecOrDecl ann))
$cSodDecl :: Constr
$cSodSpec :: Constr
$tSpecOrDecl :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
$cgmapMo :: forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
gmapMp :: (forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
$cgmapMp :: forall ann (m :: * -> *).
(Data ann, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
gmapM :: (forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
$cgmapM :: forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
gmapQi :: Int -> (forall d. Data d => d -> u) -> SpecOrDecl ann -> u
$cgmapQi :: forall ann u.
Data ann =>
Int -> (forall d. Data d => d -> u) -> SpecOrDecl ann -> u
gmapQ :: (forall d. Data d => d -> u) -> SpecOrDecl ann -> [u]
$cgmapQ :: forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> SpecOrDecl ann -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
$cgmapQr :: forall ann r r'.
Data ann =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
$cgmapQl :: forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
gmapT :: (forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
$cgmapT :: forall ann.
Data ann =>
(forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SpecOrDecl ann))
$cdataCast2 :: forall ann (t :: * -> * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SpecOrDecl ann))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann))
$cdataCast1 :: forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann))
dataTypeOf :: SpecOrDecl ann -> DataType
$cdataTypeOf :: forall ann. Data ann => SpecOrDecl ann -> DataType
toConstr :: SpecOrDecl ann -> Constr
$ctoConstr :: forall ann. Data ann => SpecOrDecl ann -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann)
$cgunfold :: forall ann (c :: * -> *).
Data ann =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann)
$cgfoldl :: forall ann (c :: * -> *).
Data ann =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann)
$cp1Data :: forall ann. Data ann => Typeable (SpecOrDecl ann)
Data, Int -> SpecOrDecl ann -> ShowS
[SpecOrDecl ann] -> ShowS
SpecOrDecl ann -> String
(Int -> SpecOrDecl ann -> ShowS)
-> (SpecOrDecl ann -> String)
-> ([SpecOrDecl ann] -> ShowS)
-> Show (SpecOrDecl ann)
forall ann. Show ann => Int -> SpecOrDecl ann -> ShowS
forall ann. Show ann => [SpecOrDecl ann] -> ShowS
forall ann. Show ann => SpecOrDecl ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SpecOrDecl ann] -> ShowS
$cshowList :: forall ann. Show ann => [SpecOrDecl ann] -> ShowS
show :: SpecOrDecl ann -> String
$cshow :: forall ann. Show ann => SpecOrDecl ann -> String
showsPrec :: Int -> SpecOrDecl ann -> ShowS
$cshowsPrec :: forall ann. Show ann => Int -> SpecOrDecl ann -> ShowS
Show, SpecOrDecl ann -> SpecOrDecl ann -> Bool
(SpecOrDecl ann -> SpecOrDecl ann -> Bool)
-> (SpecOrDecl ann -> SpecOrDecl ann -> Bool)
-> Eq (SpecOrDecl ann)
forall ann. Eq ann => SpecOrDecl ann -> SpecOrDecl ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SpecOrDecl ann -> SpecOrDecl ann -> Bool
$c/= :: forall ann. Eq ann => SpecOrDecl ann -> SpecOrDecl ann -> Bool
== :: SpecOrDecl ann -> SpecOrDecl ann -> Bool
$c== :: forall ann. Eq ann => SpecOrDecl ann -> SpecOrDecl ann -> Bool
Eq, a -> SpecOrDecl b -> SpecOrDecl a
(a -> b) -> SpecOrDecl a -> SpecOrDecl b
(forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b)
-> (forall a b. a -> SpecOrDecl b -> SpecOrDecl a)
-> Functor SpecOrDecl
forall a b. a -> SpecOrDecl b -> SpecOrDecl a
forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SpecOrDecl b -> SpecOrDecl a
$c<$ :: forall a b. a -> SpecOrDecl b -> SpecOrDecl a
fmap :: (a -> b) -> SpecOrDecl a -> SpecOrDecl b
$cfmap :: forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b
Functor)


instance Show a => Pretty (PrimFormula a) where pretty :: PrimFormula a -> String
pretty = PrimFormula a -> String
forall a. Show a => a -> String
show


instance (Pretty a) => Show (Specification a) where
  show :: Specification a -> String
show Specification { SpecKind
_specType :: SpecKind
_specType :: forall a. Specification a -> SpecKind
_specType, a
_specFormula :: a
_specFormula :: forall a. Specification a -> a
_specFormula } =
    String
"Specification { " String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
"_specType = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecKind -> String
forall a. Show a => a -> String
show SpecKind
_specType String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
"_specFormula = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Pretty a => a -> String
pretty a
_specFormula String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
" }"

-- * Lenses

makeLenses ''Specification
makeLenses ''AuxDecl
makePrisms ''Specification
makePrisms ''SpecOrDecl


-- | Given a prism @p@ projecting a pair, @'refining' x p@ projects values from
-- the front left of the pair such that the right of the pair matches @x@.
--
-- >>> [1, 2, 3] ^? refining [] _Cons
-- Nothing
--
-- >>> [1] ^? refining [] _Cons
-- Just 1
--
refining :: (Eq r) => r -> APrism s t (a, r) (a, r) -> Prism s t a a
refining :: r -> APrism s t (a, r) (a, r) -> Prism s t a a
refining r
y APrism s t (a, r) (a, r)
p = APrism s t (a, r) (a, r) -> Prism s t (a, r) (a, r)
forall s t a b. APrism s t a b -> Prism s t a b
clonePrism APrism s t (a, r) (a, r)
p (p (a, r) (f (a, r)) -> p s (f t))
-> (p a (f a) -> p (a, r) (f (a, r))) -> p a (f a) -> p s (f t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. APrism' r () -> Prism' (a, r) (a, ())
forall (f :: * -> *) s a.
Traversable f =>
APrism' s a -> Prism' (f s) (f a)
below (r -> Prism' r ()
forall a. Eq a => a -> Prism' a ()
only r
y) (p (a, ()) (f (a, ())) -> p (a, r) (f (a, r)))
-> (p a (f a) -> p (a, ()) (f (a, ())))
-> p a (f a)
-> p (a, r) (f (a, r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, ()) -> a) -> (a -> (a, ())) -> Iso (a, ()) (a, ()) a a
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (a, ()) -> a
forall a b. (a, b) -> a
fst (, ())


-- | Match a @static_assert pre(...)@ annotation.
_SpecPre :: Prism' (Specification a) a
_SpecPre :: p a (f a) -> p (Specification a) (f (Specification a))
_SpecPre = SpecKind
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
-> Prism (Specification a) (Specification a) a a
forall r s t a.
Eq r =>
r -> APrism s t (a, r) (a, r) -> Prism s t a a
refining SpecKind
SpecPre (Market
  (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
-> Market
     (a, SpecKind)
     (a, SpecKind)
     (Specification a)
     (Identity (Specification a))
forall a a.
Iso (Specification a) (Specification a) (SpecKind, a) (SpecKind, a)
_Specification (Market
   (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
 -> Market
      (a, SpecKind)
      (a, SpecKind)
      (Specification a)
      (Identity (Specification a)))
-> (Market
      (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
    -> Market
         (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a)))
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
-> Market
     (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
forall (p :: * -> * -> *) a b c d.
Swapped p =>
Iso (p a b) (p c d) (p b a) (p d c)
swapped)

-- | Match a @static_assert post(...)@ annotation.
_SpecPost :: Prism' (Specification a) a
_SpecPost :: p a (f a) -> p (Specification a) (f (Specification a))
_SpecPost = SpecKind
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
-> Prism (Specification a) (Specification a) a a
forall r s t a.
Eq r =>
r -> APrism s t (a, r) (a, r) -> Prism s t a a
refining SpecKind
SpecPost (Market
  (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
-> Market
     (a, SpecKind)
     (a, SpecKind)
     (Specification a)
     (Identity (Specification a))
forall a a.
Iso (Specification a) (Specification a) (SpecKind, a) (SpecKind, a)
_Specification (Market
   (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
 -> Market
      (a, SpecKind)
      (a, SpecKind)
      (Specification a)
      (Identity (Specification a)))
-> (Market
      (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
    -> Market
         (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a)))
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
-> Market
     (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
forall (p :: * -> * -> *) a b c d.
Swapped p =>
Iso (p a b) (p c d) (p b a) (p d c)
swapped)

-- | Match a @static_assert seq(...)@ annotation.
_SpecSeq :: Prism' (Specification a) a
_SpecSeq :: p a (f a) -> p (Specification a) (f (Specification a))
_SpecSeq = SpecKind
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
-> Prism (Specification a) (Specification a) a a
forall r s t a.
Eq r =>
r -> APrism s t (a, r) (a, r) -> Prism s t a a
refining SpecKind
SpecSeq (Market
  (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
-> Market
     (a, SpecKind)
     (a, SpecKind)
     (Specification a)
     (Identity (Specification a))
forall a a.
Iso (Specification a) (Specification a) (SpecKind, a) (SpecKind, a)
_Specification (Market
   (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
 -> Market
      (a, SpecKind)
      (a, SpecKind)
      (Specification a)
      (Identity (Specification a)))
-> (Market
      (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
    -> Market
         (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a)))
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
-> Market
     (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
forall (p :: * -> * -> *) a b c d.
Swapped p =>
Iso (p a b) (p c d) (p b a) (p d c)
swapped)

-- | Match a @static_assert invariant(...)@ annotation.
_SpecInvariant :: Prism' (Specification a) a
_SpecInvariant :: p a (f a) -> p (Specification a) (f (Specification a))
_SpecInvariant = SpecKind
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
-> Prism (Specification a) (Specification a) a a
forall r s t a.
Eq r =>
r -> APrism s t (a, r) (a, r) -> Prism s t a a
refining SpecKind
SpecInvariant (Market
  (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
-> Market
     (a, SpecKind)
     (a, SpecKind)
     (Specification a)
     (Identity (Specification a))
forall a a.
Iso (Specification a) (Specification a) (SpecKind, a) (SpecKind, a)
_Specification (Market
   (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
 -> Market
      (a, SpecKind)
      (a, SpecKind)
      (Specification a)
      (Identity (Specification a)))
-> (Market
      (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
    -> Market
         (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a)))
-> APrism
     (Specification a) (Specification a) (a, SpecKind) (a, SpecKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (a, SpecKind) (a, SpecKind) (a, SpecKind) (Identity (a, SpecKind))
-> Market
     (a, SpecKind) (a, SpecKind) (SpecKind, a) (Identity (SpecKind, a))
forall (p :: * -> * -> *) a b c d.
Swapped p =>
Iso (p a b) (p c d) (p b a) (p d c)
swapped)