{- |
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 _ _ = \case
instance TestEqualityFC EmptyExprExtension where
  testEqualityFC _ = \case
instance OrdFC EmptyExprExtension where
  compareFC _ = \case
instance HashableFC EmptyExprExtension where
  hashWithSaltFC _ _ = \case
instance FunctorFC EmptyExprExtension where
  fmapFC _ = \case
instance FoldableFC EmptyExprExtension where
  foldMapFC _ = \case
instance TraversableFC EmptyExprExtension where
  traverseFC _ = \case
instance PrettyApp EmptyExprExtension where
  ppApp _ = \case
instance TypeApp EmptyExprExtension where
  appType = \case

instance ShowFC EmptyStmtExtension where
  showsPrecFC _ _ = \case
instance TestEqualityFC EmptyStmtExtension where
  testEqualityFC _ = \case
instance OrdFC EmptyStmtExtension where
  compareFC _ = \case
instance HashableFC EmptyStmtExtension where
  hashWithSaltFC _ _ = \case
instance FunctorFC EmptyStmtExtension where
  fmapFC _ = \case
instance FoldableFC EmptyStmtExtension where
  foldMapFC _ = \case
instance TraversableFC EmptyStmtExtension where
  traverseFC _ = \case
instance PrettyApp EmptyStmtExtension where
  ppApp _ = \case
instance TypeApp EmptyStmtExtension where
  appType = \case

instance IsSyntaxExtension ()