{- |
Module           : Lang.Crucible.CFG.Extension
Description      : Support infrastructure for syntax extensions
Copyright        : (c) Galois, Inc 2017
License          : BSD3
Maintainer       : Rob Dockins <rdockins@galois.com>

This module provides basic definitions necessary for handling syntax extensions
in Crucible.  Syntax extensions provide a mechanism for users of the Crucible library
to add new syntactic forms to the base control-flow-graph representation of programs.

Syntax extensions are more flexible and less tedious for some use cases than other
extension methods (e.g., override functions).
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.CFG.Extension
( ExprExtension
, StmtExtension
, IsSyntaxExtension
, PrettyApp(..)
, TypeApp(..)
, PrettyExt
, TraverseExt

  -- * Empty extension
, EmptyExprExtension
, EmptyStmtExtension
) where

import           Data.Kind (Type)
import           Data.Parameterized.TraversableFC
import           Prettyprinter (Doc)

import           Lang.Crucible.Types


class PrettyApp (app :: (k -> Type) -> k -> Type) where
  ppApp :: forall f ann. (forall x. f x -> Doc ann) -> (forall x. app f x -> Doc ann)

class TypeApp (app :: (CrucibleType -> Type) -> CrucibleType -> Type) where
  appType :: app f x -> TypeRepr x

type family ExprExtension (ext :: Type) :: (CrucibleType -> Type) -> (CrucibleType -> Type)
type family StmtExtension (ext :: Type) :: (CrucibleType -> Type) -> (CrucibleType -> Type)

type PrettyExt ext =
  ( PrettyApp (ExprExtension ext)
  , PrettyApp (StmtExtension ext)
  )

type TraverseExt ext =
  ( TraversableFC (ExprExtension ext)
  , TraversableFC (StmtExtension ext)
  )

-- | This class captures all the grungy technical capabilities
--   that are needed for syntax extensions.  These capabilities
--   allow syntax to be tested for equality, ordered, put into
--   hashtables, traversed and printed, etc.
--
--   The actual meat of implementing the semantics of syntax
--   extensions is left to a later phase.  See the @ExtensionImpl@
--   record defined in "Lang.Crucible.Simulator.ExecutionTree".
class
   ( OrdFC (ExprExtension ext)
   , TraversableFC (ExprExtension ext)
   , PrettyApp (ExprExtension ext)
   , TypeApp (ExprExtension ext)
   --
   , TraversableFC (StmtExtension ext)
   , PrettyApp (StmtExtension ext)
   , TypeApp (StmtExtension ext)
   ) =>
   IsSyntaxExtension ext

-- | The empty expression syntax extension, which adds no new syntactic forms.
data EmptyExprExtension :: (CrucibleType -> Type) -> (CrucibleType -> Type)

deriving instance Show (EmptyExprExtension f tp)

type instance ExprExtension () = EmptyExprExtension

-- | The empty statement syntax extension, which adds no new syntactic forms.
data EmptyStmtExtension :: (CrucibleType -> Type) -> (CrucibleType -> Type) where

deriving instance Show (EmptyStmtExtension f tp)

type instance StmtExtension () = EmptyStmtExtension

instance ShowFC EmptyExprExtension where
  showsPrecFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType). Int -> f x -> ShowS)
-> forall (x :: CrucibleType).
   Int -> EmptyExprExtension f x -> ShowS
showsPrecFC forall (x :: CrucibleType). Int -> f x -> ShowS
_ Int
_ = EmptyExprExtension f x -> ShowS
\case
instance TestEqualityFC EmptyExprExtension where
  testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
   EmptyExprExtension f x -> EmptyExprExtension f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
_ = EmptyExprExtension f x -> EmptyExprExtension f y -> Maybe (x :~: y)
\case
instance OrdFC EmptyExprExtension where
  compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
   EmptyExprExtension f x -> EmptyExprExtension f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
_ = EmptyExprExtension f x -> EmptyExprExtension f y -> OrderingF x y
\case
instance HashableFC EmptyExprExtension where
  hashWithSaltFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType). Int -> f x -> Int)
-> forall (x :: CrucibleType). Int -> EmptyExprExtension f x -> Int
hashWithSaltFC forall (x :: CrucibleType). Int -> f x -> Int
_ Int
_ = EmptyExprExtension f x -> Int
\case
instance FunctorFC EmptyExprExtension where
  fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType).
   EmptyExprExtension f x -> EmptyExprExtension g x
fmapFC forall (x :: CrucibleType). f x -> g x
_ = EmptyExprExtension f x -> EmptyExprExtension g x
\case
instance FoldableFC EmptyExprExtension where
  foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). EmptyExprExtension f x -> m
foldMapFC forall (x :: CrucibleType). f x -> m
_ = EmptyExprExtension f x -> m
\case
instance TraversableFC EmptyExprExtension where
  traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
   EmptyExprExtension f x -> m (EmptyExprExtension g x)
traverseFC forall (x :: CrucibleType). f x -> m (g x)
_ = EmptyExprExtension f x -> m (EmptyExprExtension g x)
\case
instance PrettyApp EmptyExprExtension where
  ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). EmptyExprExtension f x -> Doc ann
ppApp forall (x :: CrucibleType). f x -> Doc ann
_ = EmptyExprExtension f x -> Doc ann
\case
instance TypeApp EmptyExprExtension where
  appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType).
EmptyExprExtension f x -> TypeRepr x
appType = EmptyExprExtension f x -> TypeRepr x
\case

instance ShowFC EmptyStmtExtension where
  showsPrecFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType). Int -> f x -> ShowS)
-> forall (x :: CrucibleType).
   Int -> EmptyStmtExtension f x -> ShowS
showsPrecFC forall (x :: CrucibleType). Int -> f x -> ShowS
_ Int
_ = EmptyStmtExtension f x -> ShowS
\case
instance TestEqualityFC EmptyStmtExtension where
  testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
   EmptyStmtExtension f x -> EmptyStmtExtension f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
_ = EmptyStmtExtension f x -> EmptyStmtExtension f y -> Maybe (x :~: y)
\case
instance OrdFC EmptyStmtExtension where
  compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
   EmptyStmtExtension f x -> EmptyStmtExtension f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
_ = EmptyStmtExtension f x -> EmptyStmtExtension f y -> OrderingF x y
\case
instance HashableFC EmptyStmtExtension where
  hashWithSaltFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType). Int -> f x -> Int)
-> forall (x :: CrucibleType). Int -> EmptyStmtExtension f x -> Int
hashWithSaltFC forall (x :: CrucibleType). Int -> f x -> Int
_ Int
_ = EmptyStmtExtension f x -> Int
\case
instance FunctorFC EmptyStmtExtension where
  fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType).
   EmptyStmtExtension f x -> EmptyStmtExtension g x
fmapFC forall (x :: CrucibleType). f x -> g x
_ = EmptyStmtExtension f x -> EmptyStmtExtension g x
\case
instance FoldableFC EmptyStmtExtension where
  foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). EmptyStmtExtension f x -> m
foldMapFC forall (x :: CrucibleType). f x -> m
_ = EmptyStmtExtension f x -> m
\case
instance TraversableFC EmptyStmtExtension where
  traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
   EmptyStmtExtension f x -> m (EmptyStmtExtension g x)
traverseFC forall (x :: CrucibleType). f x -> m (g x)
_ = EmptyStmtExtension f x -> m (EmptyStmtExtension g x)
\case
instance PrettyApp EmptyStmtExtension where
  ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). EmptyStmtExtension f x -> Doc ann
ppApp forall (x :: CrucibleType). f x -> Doc ann
_ = EmptyStmtExtension f x -> Doc ann
\case
instance TypeApp EmptyStmtExtension where
  appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType).
EmptyStmtExtension f x -> TypeRepr x
appType = EmptyStmtExtension f x -> TypeRepr x
\case

instance IsSyntaxExtension ()