{-# 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)
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 -> Constr
PrimLogic a -> DataType
(forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
forall {a}. Data a => Typeable (PrimLogic a)
forall a. Data a => PrimLogic a -> Constr
forall a. Data a => PrimLogic a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PrimLogic a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PrimLogic a)
$ctoConstr :: forall a. Data a => PrimLogic a -> Constr
toConstr :: PrimLogic a -> Constr
$cdataTypeOf :: forall a. Data a => PrimLogic a -> DataType
dataTypeOf :: PrimLogic a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PrimLogic a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
gmapT :: (forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> PrimLogic a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PrimLogic a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a)
gmapM :: forall (m :: * -> *).
Monad m =>
(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)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PrimLogic a -> m (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
$cshowsPrec :: forall a. Show a => Int -> PrimLogic a -> ShowS
showsPrec :: Int -> PrimLogic a -> ShowS
$cshow :: forall a. Show a => PrimLogic a -> String
show :: PrimLogic a -> String
$cshowList :: forall a. Show a => [PrimLogic a] -> ShowS
showList :: [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
$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
/= :: PrimLogic a -> PrimLogic a -> Bool
Eq, (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
$cfmap :: forall a b. (a -> b) -> PrimLogic a -> PrimLogic b
fmap :: forall a b. (a -> b) -> PrimLogic a -> PrimLogic b
$c<$ :: forall a b. a -> PrimLogic b -> PrimLogic a
<$ :: forall a b. a -> PrimLogic b -> PrimLogic a
Functor, (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
$cfold :: forall m. Monoid m => PrimLogic m -> m
fold :: forall m. Monoid m => PrimLogic m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> PrimLogic a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
foldr :: forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> PrimLogic a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
foldl :: forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> PrimLogic a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> PrimLogic a -> a
foldr1 :: forall a. (a -> a -> a) -> PrimLogic a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> PrimLogic a -> a
foldl1 :: forall a. (a -> a -> a) -> PrimLogic a -> a
$ctoList :: forall a. PrimLogic a -> [a]
toList :: forall a. PrimLogic a -> [a]
$cnull :: forall a. PrimLogic a -> Bool
null :: forall a. PrimLogic a -> Bool
$clength :: forall a. PrimLogic a -> Int
length :: forall a. PrimLogic a -> Int
$celem :: forall a. Eq a => a -> PrimLogic a -> Bool
elem :: forall a. Eq a => a -> PrimLogic a -> Bool
$cmaximum :: forall a. Ord a => PrimLogic a -> a
maximum :: forall a. Ord a => PrimLogic a -> a
$cminimum :: forall a. Ord a => PrimLogic a -> a
minimum :: forall a. Ord a => PrimLogic a -> a
$csum :: forall a. Num a => PrimLogic a -> a
sum :: forall a. Num a => PrimLogic a -> a
$cproduct :: forall a. Num a => PrimLogic a -> a
product :: forall a. Num a => PrimLogic a -> a
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
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PrimLogic a -> f (PrimLogic b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PrimLogic a -> f (PrimLogic b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
PrimLogic (f a) -> f (PrimLogic a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
PrimLogic (f a) -> f (PrimLogic a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PrimLogic a -> m (PrimLogic b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PrimLogic a -> m (PrimLogic b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
PrimLogic (m a) -> m (PrimLogic a)
sequence :: forall (m :: * -> *) a.
Monad m =>
PrimLogic (m a) -> m (PrimLogic a)
Traversable)


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


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


-- | A @decl_aux@ annotation.
data AuxDecl ann =
  AuxDecl
  { forall ann. AuxDecl ann -> String
_adName :: F.Name
  , forall ann. AuxDecl ann -> TypeSpec ann
_adTy   :: F.TypeSpec ann
  }
  deriving (Typeable, Typeable (AuxDecl ann)
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 -> Constr
AuxDecl ann -> DataType
(forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
forall {ann}. Data ann => Typeable (AuxDecl ann)
forall ann. Data ann => AuxDecl ann -> Constr
forall ann. Data ann => AuxDecl ann -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AuxDecl ann -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (AuxDecl ann)
$ctoConstr :: forall ann. Data ann => AuxDecl ann -> Constr
toConstr :: AuxDecl ann -> Constr
$cdataTypeOf :: forall ann. Data ann => AuxDecl ann -> DataType
dataTypeOf :: AuxDecl ann -> DataType
$cdataCast1 :: forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (AuxDecl ann))
$cgmapT :: forall ann.
Data ann =>
(forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
gmapT :: (forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann
$cgmapQl :: forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r
$cgmapQ :: forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> AuxDecl ann -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AuxDecl ann -> u
$cgmapM :: forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann)
gmapM :: forall (m :: * -> *).
Monad m =>
(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)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AuxDecl ann -> m (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
$cshowsPrec :: forall ann. Show ann => Int -> AuxDecl ann -> ShowS
showsPrec :: Int -> AuxDecl ann -> ShowS
$cshow :: forall ann. Show ann => AuxDecl ann -> String
show :: AuxDecl ann -> String
$cshowList :: forall ann. Show ann => [AuxDecl ann] -> ShowS
showList :: [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
$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
/= :: AuxDecl ann -> AuxDecl ann -> Bool
Eq, (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
$cfmap :: forall a b. (a -> b) -> AuxDecl a -> AuxDecl b
fmap :: forall a b. (a -> b) -> AuxDecl a -> AuxDecl b
$c<$ :: forall a b. a -> AuxDecl b -> AuxDecl a
<$ :: forall a b. a -> AuxDecl b -> AuxDecl a
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)
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 -> Constr
SpecOrDecl ann -> DataType
(forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
forall {ann}. Data ann => Typeable (SpecOrDecl ann)
forall ann. Data ann => SpecOrDecl ann -> Constr
forall ann. Data ann => SpecOrDecl ann -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SpecOrDecl ann -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann)
$ctoConstr :: forall ann. Data ann => SpecOrDecl ann -> Constr
toConstr :: SpecOrDecl ann -> Constr
$cdataTypeOf :: forall ann. Data ann => SpecOrDecl ann -> DataType
dataTypeOf :: SpecOrDecl ann -> DataType
$cdataCast1 :: forall ann (t :: * -> *) (c :: * -> *).
(Data ann, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SpecOrDecl ann))
$cgmapT :: forall ann.
Data ann =>
(forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
gmapT :: (forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann
$cgmapQl :: forall ann r r'.
Data ann =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r
$cgmapQ :: forall ann u.
Data ann =>
(forall d. Data d => d -> u) -> SpecOrDecl ann -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SpecOrDecl ann -> u
$cgmapM :: forall ann (m :: * -> *).
(Data ann, Monad m) =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (SpecOrDecl ann)
gmapM :: forall (m :: * -> *).
Monad m =>
(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)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SpecOrDecl ann -> m (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
$cshowsPrec :: forall ann. Show ann => Int -> SpecOrDecl ann -> ShowS
showsPrec :: Int -> SpecOrDecl ann -> ShowS
$cshow :: forall ann. Show ann => SpecOrDecl ann -> String
show :: SpecOrDecl ann -> String
$cshowList :: forall ann. Show ann => [SpecOrDecl ann] -> ShowS
showList :: [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
$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
/= :: SpecOrDecl ann -> SpecOrDecl ann -> Bool
Eq, (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
$cfmap :: forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b
fmap :: forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b
$c<$ :: forall a b. a -> SpecOrDecl b -> SpecOrDecl a
<$ :: forall a b. a -> SpecOrDecl b -> SpecOrDecl a
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 :: forall a. Specification a -> SpecKind
_specType :: SpecKind
_specType, a
_specFormula :: forall a. Specification a -> a
_specFormula :: 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 :: forall r s t a.
Eq r =>
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 :: forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
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 (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (SpecKind, a) (f (SpecKind, a))
-> p (Specification a) (f (Specification 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.
Swap p =>
Iso (p a b) (p c d) (p b a) (p d c)
Iso (SpecKind, a) (SpecKind, a) (a, SpecKind) (a, SpecKind)
swapped)

-- | Match a @static_assert post(...)@ annotation.
_SpecPost :: Prism' (Specification a) a
_SpecPost :: forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
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 (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (SpecKind, a) (f (SpecKind, a))
-> p (Specification a) (f (Specification 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.
Swap p =>
Iso (p a b) (p c d) (p b a) (p d c)
Iso (SpecKind, a) (SpecKind, a) (a, SpecKind) (a, SpecKind)
swapped)

-- | Match a @static_assert seq(...)@ annotation.
_SpecSeq :: Prism' (Specification a) a
_SpecSeq :: forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
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 (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (SpecKind, a) (f (SpecKind, a))
-> p (Specification a) (f (Specification 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.
Swap p =>
Iso (p a b) (p c d) (p b a) (p d c)
Iso (SpecKind, a) (SpecKind, a) (a, SpecKind) (a, SpecKind)
swapped)

-- | Match a @static_assert invariant(...)@ annotation.
_SpecInvariant :: Prism' (Specification a) a
_SpecInvariant :: forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
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 (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (SpecKind, a) (f (SpecKind, a))
-> p (Specification a) (f (Specification 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.
Swap p =>
Iso (p a b) (p c d) (p b a) (p d c)
Iso (SpecKind, a) (SpecKind, a) (a, SpecKind) (a, SpecKind)
swapped)