content: ------------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.LLVM.QQ
  -- Description      : QuasiQuoters for a subset of LLVM assembly syntax
  -- Copyright        : (c) Galois, Inc 2019
  -- License          : BSD3
  -- Maintainer       : Rob Dockins <rdockins@galois.com>
  -- Stability        : provisional
  ------------------------------------------------------------------------
  
  {-# LANGUAGE DeriveDataTypeable #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Lang.Crucible.LLVM.QQ
   ( llvmType
   , llvmDecl
   , llvmOvr
   ) where
  
  import Control.Monad (void)
  import qualified Data.Attoparsec.Text as AT
  import Data.Char
  import Data.Data
  import Data.Int
  import qualified Data.Text as T
  import qualified Text.LLVM.AST as L
  
  import Language.Haskell.TH
  import Language.Haskell.TH.Syntax
  import Language.Haskell.TH.Quote
  
  import qualified Data.Parameterized.Context as Ctx
  import           Lang.Crucible.Types
  import qualified Lang.Crucible.LLVM.Intrinsics.Common as IC
  import           Lang.Crucible.LLVM.Types
  
  -- | This type closely mirrors the type syntax from llvm-pretty,
  --   but adds several additional constructors to represent
  --   quasiquoter metavariables.
  data QQType
    = QQVar String     -- ^ This constructor represents a type metavariable, e.g. @$var@
    | QQIntVar String  -- ^ This constructor represents a integer type metavariable, e.g. @#var@
    | QQVectorVar String QQType -- ^ This constructor represents a vector type with a metavariable for its size, e.g. @<#var x ty>@
    | QQSizeT          -- ^ This constructor represents an integer type that is the same width as a pointer
    | QQSSizeT          -- ^ This constructor represents a signed integer type that is the same width as a pointer
    | QQPrim L.PrimType
    | QQPtrTo QQType
    | QQPtrOpaque
    | QQAlias L.Ident
    | QQArray Int32 QQType
    | QQFunTy QQType [QQType] Bool
    | QQStruct [QQType]
    | QQPackedStruct [QQType]
    | QQVector Int32 QQType
    | QQOpaque
   deriving (Show, Eq, Ord, Data)
  
  -- | This type closely mirrors the function declaration syntax from llvm-pretty,
  --   except that the types and the name of the declaration may be metavarables.
  data QQDeclare =
    QQDeclare
    { qqDecRet     :: QQType
    , qqDecName    :: Either String L.Symbol -- ^ a @Left@ value is a metavariable; @Right@ is a symbol
    , qqDecArgs    :: [QQType]
    , qqDecVarArgs :: Bool
    }
   deriving (Show, Eq, Ord, Data)
  
  parseIdent :: AT.Parser L.Ident
  parseIdent = L.Ident <$> (AT.char '%' *> AT.choice
    [ T.unpack <$> AT.takeWhile1 isDigit
    , (:) <$> AT.satisfy (AT.inClass "-a-zA-Z$._")
          <*> (T.unpack <$> (AT.takeWhile (AT.inClass "-a-zA-Z$._0-9")))
    ])
  
  
  parseSymbol :: AT.Parser L.Symbol
  parseSymbol = L.Symbol <$> (AT.char '@' *>
    ( (:) <$> AT.satisfy (AT.inClass "-a-zA-Z$._")
          <*> (T.unpack <$> (AT.takeWhile (AT.inClass "-a-zA-Z$._0-9")))
    ))
  
  parseFloatType :: AT.Parser L.FloatType
  parseFloatType = AT.choice
    [ pure L.Half      <* AT.string "half"
    , pure L.Float     <* AT.string "float"
    , pure L.Double    <* AT.string "double"
    , pure L.Fp128     <* AT.string "fp128"
    , pure L.X86_fp80  <* AT.string "x86_fp80"
    , pure L.PPC_fp128 <* AT.string "ppc_fp128"
    ]
  
  parsePrimType :: AT.Parser L.PrimType
  parsePrimType = AT.choice
    [ pure L.Label    <* AT.string "label"
    , pure L.Void     <* AT.string "void"
    , pure L.Metadata <* AT.string "metadata"
    , pure L.X86mmx   <* AT.string "x86_mmx"
    , L.Integer <$> (AT.char 'i' *> AT.decimal)
    , L.FloatType <$> parseFloatType
    ]
  
  parseSeqType ::
    Char ->
    Char ->
    AT.Parser seqSz ->
    (seqSz -> QQType -> QQType) ->
    AT.Parser QQType
  parseSeqType start end parseSz cnstr =
    do void $ AT.char start
       AT.skipSpace
       n <- parseSz
       AT.skipSpace
       void $ AT.char 'x'
       AT.skipSpace
       tp <- parseType
       AT.skipSpace
       void $ AT.char end
       return $! cnstr n tp
  
  parseVectorType :: AT.Parser QQType
  parseVectorType = parseSeqType '<' '>' AT.decimal QQVector
  
  parseVectorVar :: AT.Parser QQType
  parseVectorVar = parseSeqType '<' '>' parseIntVar QQVectorVar
  
  parseArrayType :: AT.Parser QQType
  parseArrayType = parseSeqType '[' ']' AT.decimal QQArray
  
  parseCommaSeparatedTypes :: AT.Parser [QQType]
  parseCommaSeparatedTypes = AT.choice
    [ do AT.skipSpace
         f  <- parseType
         fs <- AT.many' (AT.skipSpace *> AT.char ',' *> AT.skipSpace *> parseType)
         return (f:fs)
    , return []
    ]
  
  parseStructType :: AT.Parser QQType
  parseStructType =
    do void $ AT.char '{'
       fs <- parseCommaSeparatedTypes
       AT.skipSpace
       void $ AT.char '}'
       return $ QQStruct fs
  
  parsePackedStructType :: AT.Parser QQType
  parsePackedStructType =
    do void $ AT.string "<{"
       fs <- parseCommaSeparatedTypes
       AT.skipSpace
       void $ AT.string "}>"
       return $ QQPackedStruct fs
  
  parseArgList :: AT.Parser ([QQType], Bool)
  parseArgList =
    do void $ AT.char '('
       tps <- parseCommaSeparatedTypes
       AT.skipSpace
       varargs <- AT.choice
                  [ do void $ AT.char ','
                       AT.skipSpace
                       void $ AT.string "..."
                       AT.skipSpace
                       void $ AT.char ')'
                       return True
                  , do void $ AT.char ')'
                       return False
                  ]
       return (tps, varargs)
  
  parseVar :: AT.Parser String
  parseVar = T.unpack <$> (AT.char '$' *> AT.takeWhile1 varChar)
   where
   varChar c = isAlpha c || isDigit c || c == '\'' || c == '_'
  
  parseIntVar :: AT.Parser String
  parseIntVar = T.unpack <$> (AT.char '#' *> AT.takeWhile1 varChar)
   where
   varChar c = isAlpha c || isDigit c || c == '\'' || c == '_'
  
  parseType :: AT.Parser QQType
  parseType =
    do base <- AT.choice
               [ parseVectorType
               , parseVectorVar
               , parseArrayType
               , parseStructType
               , parsePackedStructType
               , QQVar <$> parseVar
               , QQIntVar <$> parseIntVar
               , QQAlias <$> parseIdent
               , QQPrim <$> parsePrimType
               , pure QQOpaque <* AT.string "opaque"
               , pure QQSizeT  <* AT.string "size_t"
               , pure QQSSizeT  <* AT.string "ssize_t"
               , pure QQPtrOpaque <* AT.string "ptr"
               ]
       base' <- AT.choice
                [ do AT.skipSpace
                     (args,varargs) <- parseArgList
                     return (QQFunTy base args varargs)
                , return base
                ]
       parseStars base'
  
    where
    parseStars x =
      AT.choice
      [ do AT.skipSpace
           void $ AT.char '*'
           parseStars (QQPtrTo x)
      , return x
      ]
  
  parseDeclare :: AT.Parser QQDeclare
  parseDeclare =
    do AT.skipSpace
       ret <- parseType
       AT.skipSpace
       sym <- AT.eitherP parseVar parseSymbol
       AT.skipSpace
       (args, varargs) <- parseArgList
       AT.skipSpace
       return
         QQDeclare
         { qqDecRet     = ret
         , qqDecName    = sym
         , qqDecArgs    = args
         , qqDecVarArgs = varargs
         }
  
  
  liftQQType :: QQType -> Q Exp
  liftQQType tp =
    case tp of
      QQVar nm     -> varE (mkName nm)
      QQIntVar nm  -> [| L.PrimType (L.Integer (fromInteger (intValue $(varE (mkName nm)) ))) |]
      QQVectorVar nm t -> [| L.Vector (fromInteger (intValue $(varE (mkName nm)))) $(liftQQType t) |]
      QQSizeT      -> varE 'IC.llvmSizeT
      QQSSizeT      -> varE 'IC.llvmSSizeT
      QQAlias nm   -> [| L.Alias nm |]
      QQPrim pt    -> [| L.PrimType pt |]
      QQPtrTo t    -> [| L.PtrTo $(liftQQType t) |]
      QQPtrOpaque  -> [| L.PtrOpaque |]
      QQArray n t  -> [| L.Array n $(liftQQType t) |]
      QQVector n t -> [| L.Vector n $(liftQQType t) |]
      QQStruct ts  -> [| L.Struct $(listE (map liftQQType ts)) |]
      QQPackedStruct ts -> [| L.PackedStruct $(listE (map liftQQType ts)) |]
      QQOpaque -> [| L.Opaque |]
      QQFunTy ret args varargs -> [| L.FunTy $(liftQQType ret) $(listE (map liftQQType args)) $(lift varargs) |]
  
  liftQQDecl :: QQDeclare -> Q Exp
  liftQQDecl (QQDeclare ret nm args varargs) =
     [| L.Declare
        { L.decLinkage    = Nothing
        , L.decVisibility = Nothing
        , L.decRetType    = $(liftQQType ret)
        , L.decName       = $(f nm)
        , L.decArgs       = $(listE (map liftQQType args))
        , L.decVarArgs    = $(lift varargs)
        , L.decAttrs      = []
        , L.decComdat     = Nothing
        }
      |]
    where
    f (Left v)    = varE (mkName v)
    f (Right sym) = lift sym
  
  liftKnownNat :: Integral a => a -> Q Exp
  liftKnownNat n = [| knownNat @($(litT (numTyLit (toInteger n)))) |]
  
  liftTypeRepr :: QQType -> Q Exp
  liftTypeRepr t = case t of
      QQVar nm      -> varE (mkName (nm++"_repr"))
      QQIntVar nm   -> [| BVRepr $(varE (mkName nm)) |]
      QQVectorVar _ t' -> [| VectorRepr $(liftTypeRepr t') |]
      QQSizeT       -> [| SizeT |]
      QQSSizeT      -> [| SSizeT |]
      QQPrim pt     -> liftPrim pt
      QQPtrTo _t    -> [| PtrRepr |]
      QQPtrOpaque   -> [| PtrRepr |]
      QQArray _ t'  -> [| VectorRepr $(liftTypeRepr t') |]
      QQVector _ t' -> [| VectorRepr $(liftTypeRepr t') |]
      QQStruct ts   -> [| StructRepr $(liftArgs ts False) |]
      QQPackedStruct ts -> [| StructRepr $(liftArgs ts False) |]
      QQAlias{} -> fail "Cannot lift alias type to repr"
      QQOpaque  -> fail "Cannot lift opaque type to repr"
      QQFunTy{} -> fail "Cannot lift function type to repr"
   where
    liftPrim pt = case pt of
      L.Void         -> [| UnitRepr |]
      L.Integer n    -> [| BVRepr $(liftKnownNat n) |]
      L.FloatType ft -> [| FloatRepr $(liftFloatType ft) |]
      L.Label    -> fail "Cannot lift label type to repr"
      L.X86mmx   -> fail "Cannot lift X86mmx type to repr"
      L.Metadata -> fail "Cannot lift metatata type to repr"
  
    liftFloatType ft = case ft of
      L.Half      -> [| HalfFloatRepr |]
      L.Float     -> [| SingleFloatRepr |]
      L.Double    -> [| DoubleFloatRepr |]
      L.Fp128     -> [| QuadFloatRepr |]
      L.X86_fp80  -> [| X86_80FloatRepr |]
      L.PPC_fp128 -> [| DoubleDoubleFloatRepr|]
  
  liftArgs :: [QQType] -> Bool -> Q Exp
  liftArgs = go [| Ctx.Empty |]
   where
   go :: Q Exp -> [QQType] -> Bool -> Q Exp
   go xs [] True  = [| $(xs) Ctx.:> VectorRepr AnyRepr |]
   go xs [] False = xs
   go xs (t:ts) varargs = go [| $(xs) Ctx.:> $(liftTypeRepr t) |] ts varargs
  
  
  liftQQDeclToOverride :: QQDeclare -> Q Exp
  liftQQDeclToOverride qqd@(QQDeclare ret _nm args varargs) =
    [| IC.LLVMOverride $(liftQQDecl qqd) $(liftArgs args varargs) $(liftTypeRepr ret) |]
  
  -- | This quasiquoter parses values in LLVM type syntax, extended
  --   with metavariables, and builds values of @Text.LLVM.AST.Type@.
  --
  --   Type metavariables start with a @$@ and splice in the named
  --   program variable, which is expected to have type @Type@.
  --
  --   Numeric metavariables start with @#@ and splice in an integer
  --   type whose width is given by the named program variable, which
  --   is expected to be a @NatRepr@.
  llvmType :: QuasiQuoter
  llvmType =
    QuasiQuoter
    { quoteExp = \str ->
         do case AT.parseOnly parseType (T.pack str) of
              Left msg -> error msg
              Right x  -> liftQQType x
  
    , quotePat = error "llvmType cannot quasiquote a pattern"
    , quoteType = error "llvmType cannot quasiquote a Haskell type"
    , quoteDec = error "llvmType cannot quasiquote a declaration"
    }
  
  -- | This quasiquoter parses values in LLVM function declaration syntax,
  --   extended with metavariables, and builds values of @Text.LLVM.AST.Declare@.
  --
  --   Type metavariables start with a @$@ and splice in the named
  --   program variable, which is expected to have type @Type@.
  --
  --   Numeric metavariables start with @#@ and splice in an integer
  --   type whose width is given by the named program variable, which
  --   is expected to be a @NatRepr@.
  --
  --   The name of the declaration may also be a @$@ metavariable, in which
  --   case the named variable is expeted to be a @Symbol@.
  llvmDecl :: QuasiQuoter
  llvmDecl =
    QuasiQuoter
    { quoteExp = \str ->
         do case AT.parseOnly parseDeclare (T.pack str) of
              Left msg -> error msg
              Right x  -> liftQQDecl x
  
    , quotePat = error "llvmDecl cannot quasiquote a pattern"
    , quoteType = error "llvmDecl cannot quasiquote a Haskell type"
    , quoteDec = error "llvmDecl cannot quasiquote a declaration"
    }
  
  -- | This quasiquoter parses values in LLVM function declaration syntax,
  --   extended with metavariables, and partially applies the
  --   @LLVMOverride@ constructor so that it expectes a single remaining
  --   argument to populate the @llvmOverride_def@ field.
  --
  --   Type metavariables start with a @$@ and splice in the named
  --   program variable, which is expected to have type @Type@.
  --   In addition a related variable must be in scope to give the
  --   crucible @TypeRepr@ associated.  For example variable @$x@
  --   should be a LLVM @Type@ and @$x_repr@ should be a Crucible @TypeRepr@.
  --
  --   Numeric metavariables start with @#@ and splice in an integer
  --   type whose width is given by the named program variable, which
  --   is expected to be a @NatRepr@.  Both the LLVM type and the Crucible
  --   @TypeRepr@ are built from the @NatRepr@.
  --
  --   The name of the declaration may also be a @$@ metavariable, in which
  --   case the named variable is expeted to be a @Symbol@.
  llvmOvr :: QuasiQuoter
  llvmOvr =
    QuasiQuoter
    { quoteExp = \str ->
         do case AT.parseOnly parseDeclare (T.pack str) of
              Left msg -> error msg
              Right x  -> liftQQDeclToOverride x
  
    , quotePat = error "llvmOvr cannot quasiquote a pattern"
    , quoteType = error "llvmOvr cannot quasiquote a Haskell type"
    , quoteDec = error "llvmOvr cannot quasiquote a declaration"
    }
  