content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE TemplateHaskell #-}
  
  {- |
  Module      : Verifier.SAW.ParserUtils
  Copyright   : Galois, Inc. 2012-2015
  License     : BSD3
  Maintainer  : jhendrix@galois.com
  Stability   : experimental
  Portability : non-portable (language extensions)
  -}
  
  module Verifier.SAW.ParserUtils
   ( module Verifier.SAW.TypedAST
     -- * Parser utilities.
   , readModuleFromFile
     -- * Template haskell utilities.
   , DecWriter
   , runDecWriter
   , defineModuleFromFile
   , declareSharedModuleFns
   , defineModuleFromFileWithFns
   , tcInsertModule -- re-exported for code using defineModuleFromFileWithFns
   ) where
  
  #if !MIN_VERSION_base(4,8,0)
  import Control.Applicative
  #endif
  import Control.Monad.State
  import qualified Data.ByteString.Lazy as BL
  #if !MIN_VERSION_template_haskell(2,8,0)
  import qualified Data.ByteString.Lazy.UTF8 as UTF8
  #endif
  import Data.Text (Text)
  import qualified Data.Text as Text
  import Language.Haskell.TH
  #if MIN_VERSION_template_haskell(2,7,0)
  import Language.Haskell.TH.Syntax (qAddDependentFile)
  #endif
  import System.Directory
  import qualified Language.Haskell.TH.Syntax as TH (lift)
  
  import qualified Verifier.SAW.UntypedAST as Un
  import qualified Verifier.SAW.Grammar as Un
  import Verifier.SAW.SharedTerm
  import Verifier.SAW.TypedAST
  import Verifier.SAW.Typechecker (tcInsertModule)
  
  -- | Parse an untyped module declaration from a byte-string
  readModule :: FilePath -> FilePath -> BL.ByteString -> Un.Module
  readModule base path b =
    case Un.parseSAW base path b of
      Right m -> m
      Left err -> error $ "Module parsing failed:\n" ++ show err
  
  -- | Parse an untyped module from file
  readModuleFromFile :: FilePath -> IO Un.Module
  readModuleFromFile path = do
    base <- getCurrentDirectory
    b <- BL.readFile path
    return $ readModule base path b
  
  
  -- | Monad for defining TH declarations
  type DecWriter = StateT [Dec] Q
  
  -- | Run declaration writer returning list of TH declarations
  runDecWriter :: DecWriter () -> Q [Dec]
  runDecWriter m = execStateT m []
  
  -- | Emit a list of TH declarations, adding them to the current list
  addDecs :: [Dec] -> DecWriter ()
  addDecs decs = modify (++ decs)
  
  -- | Record @path@ as a dependency for this compilation
  addDep :: FilePath -> DecWriter ()
  #if MIN_VERSION_template_haskell(2,7,0)
  addDep path = lift $ qAddDependentFile path
  #else
  addDep path = return ()
  #endif
  
  -- | @defineModuleFromFile str file@ reads an untyped module from @file@, adds a
  -- TH declaration of the name @str@ that is bound to that module at runtime, and
  -- also returns the module at TH time
  defineModuleFromFile :: String -> FilePath -> DecWriter Un.Module
  defineModuleFromFile decNameStr path = do
    addDep path
    m <- lift $ runIO $ readModuleFromFile path
    let decName = mkName decNameStr
    moduleTp <- lift $ [t| Un.Module |]
    body <- lift $ TH.lift m
    addDecs [ SigD decName moduleTp
            , FunD decName [ Clause [] (NormalB body) [] ]]
    return m
  
  
  -- | Return the type
  --
  -- > 'SharedContext' -> 'Term' -> .. -> 'Term' -> 'IO' 'Term'
  --
  -- that takes in @n@ 'Term's
  termFunctionType :: Int -> Q Type
  termFunctionType n = [t| SharedContext -> $(go n) |]
    where
      go 0 = [t| IO Term |]
      go i = [t| Term -> $(go (i-1)) |]
  
  -- | @declareTermApplyFun nm t n@ declares a Haskell function
  --
  -- > nm :: SharedContext -> Term -> ... -> Term -> IO Term
  --
  -- that takes in @n@ 'Term's and applies (the 'Term' generated at runtime by the
  -- expression) @t@ to them
  declareTermApplyFun :: String -> Int -> (Name -> Q Exp -> Q Exp) -> DecWriter ()
  declareTermApplyFun nm n tf =
    do let decName = mkName nm
       sc <- lift $ newName "sc"
       tp <- lift $ termFunctionType n
       vars <- lift $ mapM newName (map (("t"++) . show) [1 .. n])
       body <- lift $ tf sc (listE $ map varE vars)
       addDecs [ SigD decName tp
               , FunD decName [ Clause (VarP sc : map VarP vars) (NormalB body) [] ]
               ]
  
  -- | @declareTypedNameFun sc_fun mnm nm apply_p tp@ declares a Haskell function
  --
  -- > scXXXmnm_nm :: SharedContext -> Term -> ... -> Term -> IO Term
  --
  -- where @XXX@ is @"Apply"@ if @apply_p@ is 'True', and empty otherwise. This
  -- function will fully apply the constructor, datatype, or declared name
  -- specified by @nm@ in module @mnm@, using the shared term constructor function
  -- @sc_fun@, which should have type
  --
  -- > SharedContext -> Ident -> [Term] -> IO Term
  --
  -- The number of 'Term's to take as arguments is given by the arity of @tp@,
  -- i.e., the number of nested pi-abstractions it contains at top level.
  declareTypedNameFun :: Q Exp -> ModuleName -> Text -> Bool -> Un.Term ->
                         DecWriter ()
  declareTypedNameFun sc_fun mnm nm apply_p tp =
    let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ Text.unpack nm in
    declareTermApplyFun th_nm (length $ fst $ Un.asPiList tp) $ \sc ts ->
    [| $(sc_fun) $(varE sc)
     (mkIdent mnm $(stringE (Text.unpack nm)))
     $(ts) |]
  
  -- | Declare a Haskell function
  --
  -- > scApplyMMM_d :: SharedContext -> Term -> ... -> Term -> IO Term
  --
  -- for declared name (primitive, axiom, or definition) @d@ with type @tp@ in
  -- module @MMM@
  declareDefFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
  declareDefFun mnm d tp =
    declareTypedNameFun [| scGlobalApply |] mnm d True tp
  
  -- | Declare a Haskell function
  --
  -- > scMMM_d :: SharedContext -> Term -> ... -> Term -> IO Term
  --
  -- for datatype @d@ with parameters @p_ctx@ and type @tp@ in module @MMM@
  declareDataTypeFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
  declareDataTypeFun mnm d tp =
    declareTypedNameFun [| scDataTypeApp |] mnm d False tp
  
  -- | Declare a Haskell function
  --
  -- > scApplyMMM_c :: SharedContext -> Term -> ... -> Term -> IO Term
  --
  -- for constructor @c@ with type (including parameters) @tp@ in module @MMM@
  declareCtorFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
  declareCtorFun mnm c tp =
    declareTypedNameFun [| scCtorApp |] mnm c True tp
  
  
  -- | Declare Haskell functions, via 'declareTermApplyFun', that build shared
  -- terms for each of the definitions, datatypes, and constructors in a
  -- module. Each datatype @d@ gets a function
  --
  -- > scMMM_d :: SharedContext -> Term -> ... -> Term -> IO Term
  --
  -- where @MMM@ is the name of the module. Similarly, each constructor or
  -- definition @d@ gets
  --
  -- > scApplyMMM_d :: SharedContext -> Term -> ... -> Term -> IO Term
  declareSharedModuleFns :: Un.Module -> DecWriter ()
  declareSharedModuleFns m =
    do forM_ (Un.moduleTypedDecls m) $ \(d,tp) ->
         declareDefFun (Un.moduleName m) d tp
       forM_ (Un.moduleTypedDataDecls m) $ \(d,tp) ->
         declareDataTypeFun (Un.moduleName m) d tp
       forM_ (Un.moduleTypedCtorDecls m) $ \(c,tp) ->
         declareCtorFun (Un.moduleName m) c tp
  
  
  -- | @defineModuleFromFileWithFns str str2 file@ reads an untyped module from
  -- @file@, adds a TH declaration of the name @str@ that is bound to that module
  -- at runtime, and then calls 'declareSharedModuleFns' to add declarations of
  -- Haskell term-building functions for each definition, constructor, and
  -- datatype declared in the module that is loaded. It also defines the function
  --
  -- > str2 :: SharedContext -> IO ()
  --
  -- that will load the module @str@ into the current 'SharedContext'.
  defineModuleFromFileWithFns :: String -> String -> FilePath -> Q [Dec]
  defineModuleFromFileWithFns mod_name mod_loader path =
    runDecWriter $
    do m <- defineModuleFromFile mod_name path
       declareSharedModuleFns m
       let sc = mkName "sc"
       load_tp <- lift $ [t| SharedContext -> IO () |]
       load_body <-
         lift $ [e| tcInsertModule $(varE sc) $(varE $ mkName mod_name) |]
       addDecs [ SigD (mkName mod_loader) load_tp
               , FunD (mkName mod_loader) [ Clause [VarP sc] (NormalB load_body) [] ]
               ]
  