content: {-# 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, Data, Show, Eq, Functor, Foldable, Traversable)
  
  
  -- | Logical expressions over Fortran expressions.
  data PrimFormula ann
    = PFExpr (F.Expression ann)
    | PFLogical (PrimLogic (PrimFormula ann))
    deriving (Typeable, Data, Show, Eq, 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 (Show, Eq, Typeable, Data)
  
  
  -- | A @static_assert@ annotation.
  data Specification a =
    Specification
    { _specType    :: SpecKind
    , _specFormula :: a
    }
    deriving (Typeable, Data, Eq, Functor)
  
  
  -- | A @decl_aux@ annotation.
  data AuxDecl ann =
    AuxDecl
    { _adName :: F.Name
    , _adTy   :: F.TypeSpec ann
    }
    deriving (Typeable, Data, Show, Eq, 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, Data, Show, Eq, Functor)
  
  
  instance Show a => Pretty (PrimFormula a) where pretty = show
  
  
  instance (Pretty a) => Show (Specification a) where
    show Specification { _specType, _specFormula } =
      "Specification { " ++
      "_specType = " ++ show _specType ++ ", " ++
      "_specFormula = " ++ pretty _specFormula ++
      " }"
  
  -- * 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 y p = clonePrism p . below (only y) . iso fst (, ())
  
  
  -- | Match a @static_assert pre(...)@ annotation.
  _SpecPre :: Prism' (Specification a) a
  _SpecPre = refining SpecPre (_Specification . swapped)
  
  -- | Match a @static_assert post(...)@ annotation.
  _SpecPost :: Prism' (Specification a) a
  _SpecPost = refining SpecPost (_Specification . swapped)
  
  -- | Match a @static_assert seq(...)@ annotation.
  _SpecSeq :: Prism' (Specification a) a
  _SpecSeq = refining SpecSeq (_Specification . swapped)
  
  -- | Match a @static_assert invariant(...)@ annotation.
  _SpecInvariant :: Prism' (Specification a) a
  _SpecInvariant = refining SpecInvariant (_Specification . swapped)
  
  