content: {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE QuasiQuotes #-}
  
  --
  -- Ivory pre/post conditions quasiquoter.
  --
  -- Copyright (C) 2014, Galois, Inc.
  -- All rights reserved.
  --
  
  module Ivory.Language.Syntax.Concrete.QQ.CondQQ where
  
  import           Prelude hiding (exp)
  
  import           Language.Haskell.TH       hiding (Stmt, Exp, Type)
  import qualified Language.Haskell.TH       as T
  import           Language.Haskell.TH.Quote()
  
  import qualified Ivory.Language.Cond as I
  
  import Ivory.Language.Syntax.Concrete.ParseAST
  
  import Ivory.Language.Syntax.Concrete.QQ.BindExp
  import Ivory.Language.Syntax.Concrete.QQ.Common
  
  --------------------------------------------------------------------------------
  -- Assertions, e.g.,
  --
  -- requires (checkStored (pid ~> pid_err) (\err -> err <? 1)) ensures (\res ->
  -- checkStored (pid ~> pid_err) (\err -> err <? res))
  --------------------------------------------------------------------------------
  
  mkPrePostConds :: [PrePost] -> T.Exp -> Q T.Exp
  mkPrePostConds conds procBody = do
    condFns <- mapM mkCond conds
    -- Apply conditions to the proc body in the Q monad.
    return (foldr AppE procBody condFns)
  
    where
    mkCond :: PrePost -> Q T.Exp
    mkCond cond = case cond of
      PreCond  exp -> appE (varE 'I.requires) (runExp exp)
      PostCond exp -> appE (varE 'I.ensures)  (lamE [varP $ mkName "return"]
                                                    (runExp exp))
  
    runExp :: Exp -> Q T.Exp
    runExp exp = do
      (e, derefs) <- runToQ (fromExpCond exp)
      return (foldr go e derefs)
      where
      go :: (T.Exp, T.Name) -> T.Exp -> T.Exp
      go (deref, nm) acc =
        AppE (AppE (VarE 'I.checkStored) deref) (LamE [VarP nm] acc)
  
  --------------------------------------------------------------------------------
  
  fromExpCond :: Exp -> QStM (T.Exp, Name) T.Exp
  fromExpCond = fromExp insertDerefCond
  
  insertDerefCond :: Insert (T.Exp, Name)
  insertDerefCond key nm exp
    | isArea key
    = insert (exp, nm)
    | otherwise
    = error $ "Cannot insert " ++ show exp ++ " in pre/post conditions!"
  