{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

module Language.Haskell.Liquid.UX.QuasiQuoter
-- (
--     -- * LiquidHaskell Specification QuasiQuoter
--     lq

--     -- * QuasiQuoter Annotations
--   , LiquidQuote(..)
--   )
  where

import Data.Data

import qualified Data.Text as T

import Language.Haskell.TH.Lib
import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Quote

import Language.Fixpoint.Types hiding (Error, Loc, SrcSpan, panic)
import qualified Language.Fixpoint.Types as F

import Language.Haskell.Liquid.GHC.Misc (fSrcSpan)
import Liquid.GHC.API  (SrcSpan)
import qualified Liquid.GHC.API as GHC
import qualified GHC.Types.Name.Occurrence
import Language.Haskell.Liquid.Parse
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RTypeOp
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.Types

import System.IO
import Text.Megaparsec.Error

--------------------------------------------------------------------------------
-- LiquidHaskell Specification QuasiQuoter -------------------------------------
--------------------------------------------------------------------------------

lq :: QuasiQuoter
lq :: QuasiQuoter
lq = QuasiQuoter
  { quoteExp :: [Char] -> Q Exp
quoteExp  = [Char] -> Q Exp
forall {a}. a
bad
  , quotePat :: [Char] -> Q Pat
quotePat  = [Char] -> Q Pat
forall {a}. a
bad
  , quoteType :: [Char] -> Q Type
quoteType = [Char] -> Q Type
forall {a}. a
bad
  , quoteDec :: [Char] -> Q [Dec]
quoteDec  = [Char] -> Q [Dec]
lqDec
  }
  where
    -- FIME(adinapoli) Should we preserve 'fail' here?
    bad :: a
bad = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"`lq` quasiquoter can only be used as a top-level declaration"

lqDec :: String -> Q [Dec]
lqDec :: [Char] -> Q [Dec]
lqDec [Char]
src = do
  pos <- Loc -> SourcePos
locSourcePos (Loc -> SourcePos) -> Q Loc -> Q SourcePos
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Q Loc
location
  case singleSpecP pos src of
    Left ParseErrorBundle [Char] Void
peb -> do
      IO () -> Q ()
forall a. IO a -> Q a
runIO (Handle -> [Char] -> IO ()
hPutStrLn Handle
stderr (ParseErrorBundle [Char] Void -> [Char]
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> [Char]
errorBundlePretty ParseErrorBundle [Char] Void
peb))
      [Char] -> Q [Dec]
forall a. [Char] -> Q a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"LH quasiquoter parse error"
    Right BPspec
spec -> do
      prg <- AnnTarget -> Q Exp -> Q Dec
forall (m :: * -> *). Quote m => AnnTarget -> m Exp -> m Dec
pragAnnD AnnTarget
ModuleAnnotation (Q Exp -> Q Dec) -> Q Exp -> Q Dec
forall a b. (a -> b) -> a -> b
$
               Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
conE 'LiquidQuote Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`appE` BPspec -> Q Exp
forall a. Data a => a -> Q Exp
dataToExpQ' BPspec
spec
      case mkSpecDecs spec of
        Left UserError
uerr ->
          UserError -> Q [Dec]
forall a. UserError -> Q a
throwErrorInQ UserError
uerr
        Right [Dec]
decs ->
          [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ Dec
prg Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
: [Dec]
decs

throwErrorInQ :: UserError -> Q a
throwErrorInQ :: forall a. UserError -> Q a
throwErrorInQ UserError
uerr =
  [Char] -> Q a
forall a. [Char] -> Q a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> Q a)
-> ([CtxError Doc] -> [Char]) -> [CtxError Doc] -> Q a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CtxError Doc] -> [Char]
forall a. PPrint a => a -> [Char]
showpp ([CtxError Doc] -> Q a) -> Q [CtxError Doc] -> Q a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO [CtxError Doc] -> Q [CtxError Doc]
forall a. IO a -> Q a
runIO ([UserError] -> IO [CtxError Doc]
errorsWithContext [UserError
uerr])

--------------------------------------------------------------------------------
-- Liquid Haskell to Template Haskell ------------------------------------------
--------------------------------------------------------------------------------

-- Spec to Dec -----------------------------------------------------------------

mkSpecDecs :: BPspec -> Either UserError [Dec]
mkSpecDecs :: BPspec -> Either UserError [Dec]
mkSpecDecs (Asrt (Located LHName
name, LocBareTypeParsed
ty)) =
  Dec -> [Dec]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Dec -> [Dec]) -> (Type -> Dec) -> Type -> [Dec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type -> Dec
SigD (Located LHName -> Name
lhNameToName Located LHName
name)
    (Type -> [Dec]) -> Either UserError Type -> Either UserError [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BareTypeV Symbol -> BareTypeV Symbol)
-> Located LHName -> BareTypeV Symbol -> Either UserError Type
forall a v.
PPrint a =>
(BareTypeV v -> BareTypeV Symbol)
-> Located a -> BareTypeV v -> Either UserError Type
simplifyBareType BareTypeV Symbol -> BareTypeV Symbol
forall a. a -> a
id Located LHName
name (BareTypeV Symbol -> BareTypeV Symbol
forall r tv v c.
(Monoid r, Eq tv) =>
RTypeV v c tv r -> RTypeV v c tv r
quantifyFreeRTy (BareTypeV Symbol -> BareTypeV Symbol)
-> BareTypeV Symbol -> BareTypeV Symbol
forall a b. (a -> b) -> a -> b
$ BareTypeParsed -> BareTypeV Symbol
parsedToBareType (BareTypeParsed -> BareTypeV Symbol)
-> BareTypeParsed -> BareTypeV Symbol
forall a b. (a -> b) -> a -> b
$ LocBareTypeParsed -> BareTypeParsed
forall a. Located a -> a
val LocBareTypeParsed
ty)
mkSpecDecs (Asrts ([Located LHName]
names, (LocBareTypeParsed
ty, Maybe [Located (ExprV LocSymbol)]
_))) =
  (\Type
t -> (Name -> Type -> Dec
`SigD` Type
t) (Name -> Dec) -> (Located LHName -> Name) -> Located LHName -> Dec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> Name
lhNameToName (Located LHName -> Dec) -> [Located LHName] -> [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located LHName]
names)
    (Type -> [Dec]) -> Either UserError Type -> Either UserError [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BareTypeV Symbol -> BareTypeV Symbol)
-> Located LHName -> BareTypeV Symbol -> Either UserError Type
forall a v.
PPrint a =>
(BareTypeV v -> BareTypeV Symbol)
-> Located a -> BareTypeV v -> Either UserError Type
simplifyBareType BareTypeV Symbol -> BareTypeV Symbol
forall a. a -> a
id ([Located LHName] -> Located LHName
forall a. HasCallStack => [a] -> a
head [Located LHName]
names) (BareTypeV Symbol -> BareTypeV Symbol
forall r tv v c.
(Monoid r, Eq tv) =>
RTypeV v c tv r -> RTypeV v c tv r
quantifyFreeRTy (BareTypeV Symbol -> BareTypeV Symbol)
-> BareTypeV Symbol -> BareTypeV Symbol
forall a b. (a -> b) -> a -> b
$ BareTypeParsed -> BareTypeV Symbol
parsedToBareType (BareTypeParsed -> BareTypeV Symbol)
-> BareTypeParsed -> BareTypeV Symbol
forall a b. (a -> b) -> a -> b
$ LocBareTypeParsed -> BareTypeParsed
forall a. Located a -> a
val LocBareTypeParsed
ty)
mkSpecDecs (Alias Located (RTAlias Symbol BareTypeParsed)
rta) =
  Dec -> [Dec]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Dec -> [Dec]) -> (Type -> Dec) -> Type -> [Dec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [TyVarBndr BndrVis] -> Type -> Dec
TySynD Name
name [TyVarBndr BndrVis]
tvs (Type -> [Dec]) -> Either UserError Type -> Either UserError [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BareTypeParsed -> BareTypeV Symbol)
-> LocSymbol -> BareTypeParsed -> Either UserError Type
forall a v.
PPrint a =>
(BareTypeV v -> BareTypeV Symbol)
-> Located a -> BareTypeV v -> Either UserError Type
simplifyBareType BareTypeParsed -> BareTypeV Symbol
parsedToBareType LocSymbol
lsym (RTAlias Symbol BareTypeParsed -> BareTypeParsed
forall x a. RTAlias x a -> a
rtBody (Located (RTAlias Symbol BareTypeParsed)
-> RTAlias Symbol BareTypeParsed
forall a. Located a -> a
val Located (RTAlias Symbol BareTypeParsed)
rta))
  where
    lsym :: LocSymbol
lsym = Located (RTAlias Symbol BareTypeParsed) -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc Located (RTAlias Symbol BareTypeParsed)
rta Symbol
n
    name :: Name
name = Symbol -> Name
forall s. Symbolic s => s -> Name
symbolName Symbol
n
    n :: Symbol
n    = RTAlias Symbol BareTypeParsed -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (Located (RTAlias Symbol BareTypeParsed)
-> RTAlias Symbol BareTypeParsed
forall a. Located a -> a
val Located (RTAlias Symbol BareTypeParsed)
rta)
    tvs :: [TyVarBndr BndrVis]
tvs  = (\Symbol
a -> Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
PlainTV (Symbol -> Name
forall s. Symbolic s => s -> Name
symbolName Symbol
a) BndrVis
BndrReq) (Symbol -> TyVarBndr BndrVis) -> [Symbol] -> [TyVarBndr BndrVis]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTAlias Symbol BareTypeParsed -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs (Located (RTAlias Symbol BareTypeParsed)
-> RTAlias Symbol BareTypeParsed
forall a. Located a -> a
val Located (RTAlias Symbol BareTypeParsed)
rta)
mkSpecDecs BPspec
_ =
  [Dec] -> Either UserError [Dec]
forall a b. b -> Either a b
Right []

-- Symbol to TH Name -----------------------------------------------------------

symbolName :: Symbolic s => s -> Name
symbolName :: forall s. Symbolic s => s -> Name
symbolName = [Char] -> Name
mkName ([Char] -> Name) -> (s -> [Char]) -> s -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
symbolString (Symbol -> [Char]) -> (s -> Symbol) -> s -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Symbol
forall a. Symbolic a => a -> Symbol
symbol

lhNameToName :: Located LHName -> Name
lhNameToName :: Located LHName -> Name
lhNameToName Located LHName
lname = case Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname of
    LHNUnresolved LHNameSpace
_ Symbol
s -> Symbol -> Name
forall s. Symbolic s => s -> Name
symbolName Symbol
s
    LHNResolved LHResolvedName
rn Symbol
_ -> case LHResolvedName
rn of
      LHRGHC Name
n -> case Name -> Maybe Module
GHC.nameModule_maybe Name
n of
        Maybe Module
Nothing -> [Char] -> Name
mkName (Name -> [Char]
forall a. NamedThing a => a -> [Char]
GHC.getOccString Name
n)
        Just Module
m ->
          NameSpace -> [Char] -> [Char] -> [Char] -> Name
mkNameG
            (NameSpace -> NameSpace
toTHNameSpace (NameSpace -> NameSpace) -> NameSpace -> NameSpace
forall a b. (a -> b) -> a -> b
$ Name -> NameSpace
GHC.nameNameSpace Name
n)
            (Unit -> [Char]
forall u. IsUnitId u => u -> [Char]
GHC.unitString (Unit -> [Char]) -> Unit -> [Char]
forall a b. (a -> b) -> a -> b
$ Module -> Unit
forall unit. GenModule unit -> unit
GHC.moduleUnit Module
m)
            (ModuleName -> [Char]
GHC.moduleNameString (ModuleName -> [Char]) -> ModuleName -> [Char]
forall a b. (a -> b) -> a -> b
$ Module -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName Module
m)
            (Name -> [Char]
forall a. NamedThing a => a -> [Char]
GHC.getOccString Name
n)
      LHRLocal Symbol
s -> Symbol -> Name
forall s. Symbolic s => s -> Name
symbolName Symbol
s
      LHRIndex Word
i -> Maybe SrcSpan -> [Char] -> Name
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located LHName
lname) ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot produce a TH Name for a LHRIndex " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word -> [Char]
forall a. Show a => a -> [Char]
show Word
i
      LHRLogic LogicName
_ ->
        Maybe SrcSpan -> [Char] -> Name
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located LHName
lname) ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot produce a TH Name for a LogicName: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname)

  where
    toTHNameSpace :: GHC.NameSpace -> NameSpace
    toTHNameSpace :: NameSpace -> NameSpace
toTHNameSpace NameSpace
ns
      | NameSpace
ns NameSpace -> NameSpace -> Bool
forall a. Eq a => a -> a -> Bool
== NameSpace
GHC.dataName = NameSpace
DataName
      | NameSpace
ns NameSpace -> NameSpace -> Bool
forall a. Eq a => a -> a -> Bool
== NameSpace
GHC.tcName = NameSpace
TcClsName
      | NameSpace
ns NameSpace -> NameSpace -> Bool
forall a. Eq a => a -> a -> Bool
== NameSpace
GHC.Types.Name.Occurrence.varName = NameSpace
VarName
      | NameSpace -> Bool
GHC.isFieldNameSpace NameSpace
ns = Maybe SrcSpan -> [Char] -> NameSpace
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located LHName
lname) [Char]
"lhNameToName: Unimplemented case for FieldName NameSpace"
      | Bool
otherwise = Maybe SrcSpan -> [Char] -> NameSpace
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located LHName
lname) [Char]
"lhNameToName: Unknown GHC.NameSpace"


-- BareType to TH Type ---------------------------------------------------------

simplifyBareType
  :: PPrint a => (BareTypeV v -> BareType) -> Located a -> BareTypeV v -> Either UserError Type
simplifyBareType :: forall a v.
PPrint a =>
(BareTypeV v -> BareTypeV Symbol)
-> Located a -> BareTypeV v -> Either UserError Type
simplifyBareType BareTypeV v -> BareTypeV Symbol
toBareType Located a
s BareTypeV v
t = case BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' BareTypeV v
t of
  Simplified Type
t' ->
    Type -> Either UserError Type
forall a b. b -> Either a b
Right Type
t'
  FoundExprArg SrcSpan
l ->
    UserError -> Either UserError Type
forall a b. a -> Either a b
Left (UserError -> Either UserError Type)
-> UserError -> Either UserError Type
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Maybe Doc -> Doc -> Doc -> Doc -> UserError
forall t. SrcSpan -> Maybe Doc -> Doc -> t -> Doc -> TError t
ErrTySpec SrcSpan
l Maybe Doc
forall a. Maybe a
Nothing (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
s) (BareTypeV Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (BareTypeV Symbol -> Doc) -> BareTypeV Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ BareTypeV v -> BareTypeV Symbol
toBareType BareTypeV v
t)
      Doc
"Found expression argument in bad location in type"
  Simpl Type
FoundHole ->
    UserError -> Either UserError Type
forall a b. a -> Either a b
Left (UserError -> Either UserError Type)
-> UserError -> Either UserError Type
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Maybe Doc -> Doc -> Doc -> Doc -> UserError
forall t. SrcSpan -> Maybe Doc -> Doc -> t -> Doc -> TError t
ErrTySpec (Located a -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located a
s) Maybe Doc
forall a. Maybe a
Nothing (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
s) (BareTypeV Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (BareTypeV Symbol -> Doc) -> BareTypeV Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ BareTypeV v -> BareTypeV Symbol
toBareType BareTypeV v
t)
      Doc
"Can't write LiquidHaskell type with hole in a quasiquoter"

simplifyBareType' :: BareTypeV v -> Simpl Type
simplifyBareType' :: forall v. BareTypeV v -> Simpl Type
simplifyBareType' = ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([], [])

simplifyBareType'' :: ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type

simplifyBareType'' :: forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([], []) (RVar BTyVar
v RReftV v
_) =
  Type -> Simpl Type
forall a. a -> Simpl a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Simpl Type) -> Type -> Simpl Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT (Name -> Type) -> Name -> Type
forall a b. (a -> b) -> a -> b
$ BTyVar -> Name
forall s. Symbolic s => s -> Name
symbolName BTyVar
v
simplifyBareType'' ([], []) (RAppTy BareTypeV v
t1 BareTypeV v
t2 RReftV v
_) =
  Type -> Type -> Type
AppT (Type -> Type -> Type) -> Simpl Type -> Simpl (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' BareTypeV v
t1 Simpl (Type -> Type) -> Simpl Type -> Simpl Type
forall a b. Simpl (a -> b) -> Simpl a -> Simpl b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' BareTypeV v
t2
simplifyBareType'' ([], []) (RFun Symbol
_ RFInfo
_ BareTypeV v
i BareTypeV v
o RReftV v
_) =
  (\Type
x Type
y -> Type
ArrowT Type -> Type -> Type
`AppT` Type
x Type -> Type -> Type
`AppT` Type
y)
    (Type -> Type -> Type) -> Simpl Type -> Simpl (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' BareTypeV v
i Simpl (Type -> Type) -> Simpl Type -> Simpl Type
forall a b. Simpl (a -> b) -> Simpl a -> Simpl b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' BareTypeV v
o
simplifyBareType'' ([], []) (RApp BTyCon
cc [BareTypeV v]
as [RTPropV v BTyCon BTyVar (RReftV v)]
_ RReftV v
_) =
  let c' :: Type
c' | BTyCon -> Bool
forall c. TyConable c => c -> Bool
isFun   BTyCon
cc = Type
ArrowT
         | BTyCon -> Bool
forall c. TyConable c => c -> Bool
isTuple BTyCon
cc = Int -> Type
TupleT ([BareTypeV v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BareTypeV v]
as)
         | BTyCon -> Bool
forall c. TyConable c => c -> Bool
isList  BTyCon
cc = Type
ListT
         | Bool
otherwise = Name -> Type
ConT (Name -> Type) -> Name -> Type
forall a b. (a -> b) -> a -> b
$ Located LHName -> Name
lhNameToName (BTyCon -> Located LHName
btc_tc BTyCon
cc)
  in  (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppT Type
c' ([Type] -> Type) -> Simpl [Type] -> Simpl Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Simpl Type] -> Simpl [Type]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA ([Simpl Type] -> [Simpl Type]
forall a. [Simpl a] -> [Simpl a]
filterExprArgs ([Simpl Type] -> [Simpl Type]) -> [Simpl Type] -> [Simpl Type]
forall a b. (a -> b) -> a -> b
$ BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' (BareTypeV v -> Simpl Type) -> [BareTypeV v] -> [Simpl Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareTypeV v]
as)

simplifyBareType'' ([BTyVar], [BareTypeV v])
_ (RExprArg Located (ExprV v)
e) =
  SrcSpan -> Simpl Type
forall a. SrcSpan -> Simpl a
FoundExprArg (SrcSpan -> Simpl Type) -> SrcSpan -> Simpl Type
forall a b. (a -> b) -> a -> b
$ Located (ExprV v) -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located (ExprV v)
e
simplifyBareType'' ([BTyVar], [BareTypeV v])
_ (RHole RReftV v
_) =
  Simpl Type
forall a. Simpl a
FoundHole

simplifyBareType'' ([BTyVar], [BareTypeV v])
s(RAllP PVUV v BTyCon BTyVar
_ BareTypeV v
t) =
  ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([BTyVar], [BareTypeV v])
s BareTypeV v
t
simplifyBareType'' ([BTyVar], [BareTypeV v])
s (RAllE Symbol
_ BareTypeV v
_ BareTypeV v
t) =
  ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([BTyVar], [BareTypeV v])
s BareTypeV v
t
simplifyBareType'' ([BTyVar], [BareTypeV v])
s (REx Symbol
_ BareTypeV v
_ BareTypeV v
t) =
  ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([BTyVar], [BareTypeV v])
s BareTypeV v
t
simplifyBareType'' ([BTyVar], [BareTypeV v])
s (RRTy [(Symbol, BareTypeV v)]
_ RReftV v
_ Oblig
_ BareTypeV v
t) =
  ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([BTyVar], [BareTypeV v])
s BareTypeV v
t

simplifyBareType'' ([BTyVar]
tvs, [BareTypeV v]
cls) (RFun Symbol
_ RFInfo
_ BareTypeV v
i BareTypeV v
o RReftV v
_)
  | BareTypeV v -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType BareTypeV v
i = ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' ([BTyVar]
tvs, BareTypeV v
i BareTypeV v -> [BareTypeV v] -> [BareTypeV v]
forall a. a -> [a] -> [a]
: [BareTypeV v]
cls) BareTypeV v
o
simplifyBareType'' ([BTyVar]
tvs, [BareTypeV v]
cls) (RAllT RTVUV v BTyCon BTyVar
tv BareTypeV v
t RReftV v
_) =
  ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
forall v. ([BTyVar], [BareTypeV v]) -> BareTypeV v -> Simpl Type
simplifyBareType'' (RTVUV v BTyCon BTyVar -> BTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVUV v BTyCon BTyVar
tv BTyVar -> [BTyVar] -> [BTyVar]
forall a. a -> [a] -> [a]
: [BTyVar]
tvs, [BareTypeV v]
cls) BareTypeV v
t

simplifyBareType'' ([BTyVar]
tvs, [BareTypeV v]
cls) BareTypeV v
bt =
  [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT ((\BTyVar
t -> Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV (BTyVar -> Name
forall s. Symbolic s => s -> Name
symbolName BTyVar
t) Specificity
SpecifiedSpec) (BTyVar -> TyVarBndr Specificity)
-> [BTyVar] -> [TyVarBndr Specificity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BTyVar] -> [BTyVar]
forall a. [a] -> [a]
reverse [BTyVar]
tvs)
    ([Type] -> Type -> Type) -> Simpl [Type] -> Simpl (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BareTypeV v -> Simpl Type) -> [BareTypeV v] -> Simpl [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' ([BareTypeV v] -> [BareTypeV v]
forall a. [a] -> [a]
reverse [BareTypeV v]
cls)
    Simpl (Type -> Type) -> Simpl Type -> Simpl Type
forall a b. Simpl (a -> b) -> Simpl a -> Simpl b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeV v -> Simpl Type
forall v. BareTypeV v -> Simpl Type
simplifyBareType' BareTypeV v
bt


data Simpl a = Simplified a
             | FoundExprArg SrcSpan
             | FoundHole
               deriving ((forall a b. (a -> b) -> Simpl a -> Simpl b)
-> (forall a b. a -> Simpl b -> Simpl a) -> Functor Simpl
forall a b. a -> Simpl b -> Simpl a
forall a b. (a -> b) -> Simpl a -> Simpl b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Simpl a -> Simpl b
fmap :: forall a b. (a -> b) -> Simpl a -> Simpl b
$c<$ :: forall a b. a -> Simpl b -> Simpl a
<$ :: forall a b. a -> Simpl b -> Simpl a
Functor)

instance Applicative Simpl where
  pure :: forall a. a -> Simpl a
pure = a -> Simpl a
forall a. a -> Simpl a
Simplified

  Simplified   a -> b
f <*> :: forall a b. Simpl (a -> b) -> Simpl a -> Simpl b
<*> Simplified   a
x = b -> Simpl b
forall a. a -> Simpl a
Simplified (b -> Simpl b) -> b -> Simpl b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
  Simpl (a -> b)
_              <*> FoundExprArg SrcSpan
l = SrcSpan -> Simpl b
forall a. SrcSpan -> Simpl a
FoundExprArg SrcSpan
l
  Simpl (a -> b)
_              <*> Simpl a
FoundHole      = Simpl b
forall a. Simpl a
FoundHole
  FoundExprArg SrcSpan
l <*> Simpl a
_              = SrcSpan -> Simpl b
forall a. SrcSpan -> Simpl a
FoundExprArg SrcSpan
l
  Simpl (a -> b)
FoundHole      <*> Simpl a
_              = Simpl b
forall a. Simpl a
FoundHole

instance Monad Simpl where
  Simplified   a
x >>= :: forall a b. Simpl a -> (a -> Simpl b) -> Simpl b
>>= a -> Simpl b
f = a -> Simpl b
f a
x
  FoundExprArg SrcSpan
l >>= a -> Simpl b
_ = SrcSpan -> Simpl b
forall a. SrcSpan -> Simpl a
FoundExprArg SrcSpan
l
  Simpl a
FoundHole      >>= a -> Simpl b
_ = Simpl b
forall a. Simpl a
FoundHole

filterExprArgs :: [Simpl a] -> [Simpl a]
filterExprArgs :: forall a. [Simpl a] -> [Simpl a]
filterExprArgs = (Simpl a -> Bool) -> [Simpl a] -> [Simpl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Simpl a -> Bool
forall {a}. Simpl a -> Bool
check
  where
    check :: Simpl a -> Bool
check (FoundExprArg SrcSpan
_) = Bool
False
    check Simpl a
_ = Bool
True

--------------------------------------------------------------------------------
-- QuasiQuoter Annotations -----------------------------------------------------
--------------------------------------------------------------------------------

newtype LiquidQuote = LiquidQuote { LiquidQuote -> BPspec
liquidQuoteSpec :: BPspec }
                      deriving (Typeable LiquidQuote
Typeable LiquidQuote =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LiquidQuote -> c LiquidQuote)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LiquidQuote)
-> (LiquidQuote -> Constr)
-> (LiquidQuote -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LiquidQuote))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LiquidQuote))
-> ((forall b. Data b => b -> b) -> LiquidQuote -> LiquidQuote)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r)
-> (forall u. (forall d. Data d => d -> u) -> LiquidQuote -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LiquidQuote -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote)
-> Data LiquidQuote
LiquidQuote -> Constr
LiquidQuote -> DataType
(forall b. Data b => b -> b) -> LiquidQuote -> LiquidQuote
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LiquidQuote -> u
forall u. (forall d. Data d => d -> u) -> LiquidQuote -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiquidQuote
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiquidQuote -> c LiquidQuote
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiquidQuote)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LiquidQuote)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiquidQuote -> c LiquidQuote
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiquidQuote -> c LiquidQuote
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiquidQuote
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiquidQuote
$ctoConstr :: LiquidQuote -> Constr
toConstr :: LiquidQuote -> Constr
$cdataTypeOf :: LiquidQuote -> DataType
dataTypeOf :: LiquidQuote -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiquidQuote)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiquidQuote)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LiquidQuote)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LiquidQuote)
$cgmapT :: (forall b. Data b => b -> b) -> LiquidQuote -> LiquidQuote
gmapT :: (forall b. Data b => b -> b) -> LiquidQuote -> LiquidQuote
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiquidQuote -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LiquidQuote -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LiquidQuote -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LiquidQuote -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LiquidQuote -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiquidQuote -> m LiquidQuote
Data, Typeable)

--------------------------------------------------------------------------------
-- Template Haskell Utility Functions ------------------------------------------
--------------------------------------------------------------------------------

locSourcePos :: Loc -> SourcePos
locSourcePos :: Loc -> SourcePos
locSourcePos Loc
loc =
  (Int -> Int -> SourcePos) -> (Int, Int) -> SourcePos
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([Char] -> Int -> Int -> SourcePos
safeSourcePos (Loc -> [Char]
loc_filename Loc
loc)) (Loc -> (Int, Int)
loc_start Loc
loc)

dataToExpQ' :: Data a => a -> Q Exp
dataToExpQ' :: forall a. Data a => a -> Q Exp
dataToExpQ' = (forall b. Data b => b -> Maybe (Q Exp)) -> a -> Q Exp
forall (m :: * -> *) a.
(Quote m, Data a) =>
(forall b. Data b => b -> Maybe (m Exp)) -> a -> m Exp
dataToExpQ (Maybe (Q Exp) -> b -> Maybe (Q Exp)
forall a b. a -> b -> a
const Maybe (Q Exp)
forall a. Maybe a
Nothing (b -> Maybe (Q Exp))
-> (Text -> Maybe (Q Exp)) -> b -> Maybe (Q Exp)
forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
`extQ` Text -> Maybe (Q Exp)
textToExpQ)

textToExpQ :: T.Text -> Maybe ExpQ
textToExpQ :: Text -> Maybe (Q Exp)
textToExpQ Text
text = Q Exp -> Maybe (Q Exp)
forall a. a -> Maybe a
Just (Q Exp -> Maybe (Q Exp)) -> Q Exp -> Maybe (Q Exp)
forall a b. (a -> b) -> a -> b
$ Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE 'T.pack Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`appE` [Char] -> Q Exp
forall (m :: * -> *). Quote m => [Char] -> m Exp
stringE (Text -> [Char]
T.unpack Text
text)

extQ :: (Typeable a, Typeable b) => (a -> q) -> (b -> q) -> a -> q
extQ :: forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
extQ a -> q
f b -> q
g a
a = q -> (b -> q) -> Maybe b -> q
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> q
f a
a) b -> q
g (a -> Maybe b
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
a)