{-# LANGUAGE TemplateHaskell, FlexibleContexts, PolyKinds #-}
module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where
import Language.Haskell.TH.Syntax as TH
import Language.Haskell.TH.Ppr as TH
import Language.Haskell.TH.Quote
import qualified Data.Generics as SYB
import Control.Monad.Writer (runWriterT, tell)
import Data.Monoid (Any(..))
import qualified Data.Binding.Hobbits.Internal.Utilities as IU
import Data.Binding.Hobbits.Internal.Mb
import Data.Binding.Hobbits.Internal.Closed
import Data.Binding.Hobbits.PatternParser (parsePattern)
import Data.Binding.Hobbits.NuMatching
appEMulti :: Exp -> [Exp] -> Exp
appEMulti :: Exp -> [Exp] -> Exp
appEMulti = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE
compose :: Exp -> Exp -> Exp
compose :: Exp -> Exp -> Exp
compose Exp
f Exp
g = Name -> Exp
VarE '(.) Exp -> Exp -> Exp
`AppE` Exp
f Exp -> Exp -> Exp
`AppE` Exp
g
patQQ :: String -> (String -> Q Pat) -> QuasiQuoter
patQQ :: String -> (String -> Q Pat) -> QuasiQuoter
patQQ String
n String -> Q Pat
pat = (String -> Q Exp)
-> (String -> Q Pat)
-> (String -> Q Type)
-> (String -> Q [Dec])
-> QuasiQuoter
QuasiQuoter (String -> String -> Q Exp
forall a. String -> a
err String
"Exp") String -> Q Pat
pat (String -> String -> Q Type
forall a. String -> a
err String
"Type") (String -> String -> Q [Dec]
forall a. String -> a
err String
"Decs")
where err :: String -> a
err String
s = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"QQ `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' is for patterns, not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
data WrapKit =
WrapKit {WrapKit -> Exp
_varView :: Exp, WrapKit -> Pat -> Pat
_asXform :: Pat -> Pat, WrapKit -> Bool -> Pat -> Pat
_topXform :: Bool -> Pat -> Pat}
combineWrapKits :: WrapKit -> WrapKit -> WrapKit
combineWrapKits :: WrapKit -> WrapKit -> WrapKit
combineWrapKits (WrapKit {_varView :: WrapKit -> Exp
_varView = Exp
varViewO, _asXform :: WrapKit -> Pat -> Pat
_asXform = Pat -> Pat
asXformO, _topXform :: WrapKit -> Bool -> Pat -> Pat
_topXform = Bool -> Pat -> Pat
topXformO})
(WrapKit {_varView :: WrapKit -> Exp
_varView = Exp
varViewI, _asXform :: WrapKit -> Pat -> Pat
_asXform = Pat -> Pat
asXformI, _topXform :: WrapKit -> Bool -> Pat -> Pat
_topXform = Bool -> Pat -> Pat
topXformI}) =
WrapKit :: Exp -> (Pat -> Pat) -> (Bool -> Pat -> Pat) -> WrapKit
WrapKit {_varView :: Exp
_varView = Exp
varViewO Exp -> Exp -> Exp
`compose` Exp
varViewI,
_asXform :: Pat -> Pat
_asXform = Pat -> Pat
asXformO (Pat -> Pat) -> (Pat -> Pat) -> Pat -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat -> Pat
asXformI,
_topXform :: Bool -> Pat -> Pat
_topXform = \Bool
b -> Bool -> Pat -> Pat
topXformO Bool
b (Pat -> Pat) -> (Pat -> Pat) -> Pat -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Pat -> Pat
topXformI Bool
b}
wrapVars :: MonadFail m => WrapKit -> Pat -> m Pat
wrapVars :: WrapKit -> Pat -> m Pat
wrapVars (WrapKit {_varView :: WrapKit -> Exp
_varView = Exp
varView, _asXform :: WrapKit -> Pat -> Pat
_asXform = Pat -> Pat
asXform, _topXform :: WrapKit -> Bool -> Pat -> Pat
_topXform = Bool -> Pat -> Pat
topXform}) Pat
pat = do
(Pat
pat', Any Bool
usedVarView) <- WriterT Any m Pat -> m (Pat, Any)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT Any m Pat
m
Pat -> m Pat
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat -> m Pat) -> Pat -> m Pat
forall a b. (a -> b) -> a -> b
$ Bool -> Pat -> Pat
topXform Bool
usedVarView Pat
pat'
where
m :: WriterT Any m Pat
m = GenericQ Bool
-> GenericM (WriterT Any m) -> Pat -> WriterT Any m Pat
forall (m :: * -> *).
Monad m =>
GenericQ Bool -> GenericM m -> GenericM m
IU.everywhereButM (Bool -> (Exp -> Bool) -> a -> Bool
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
SYB.mkQ Bool
False Exp -> Bool
isExp) ((Pat -> WriterT Any m Pat) -> a -> WriterT Any m a
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
SYB.mkM Pat -> WriterT Any m Pat
forall (m :: * -> *).
(MonadWriter Any m, MonadFail m) =>
Pat -> m Pat
w) Pat
pat
where isExp :: Exp -> Bool
isExp :: Exp -> Bool
isExp Exp
_ = Bool
True
hit :: b -> m b
hit b
x = Any -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True) m () -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
x
w :: Pat -> m Pat
w p :: Pat
p@VarP{} = Pat -> m Pat
forall (m :: * -> *) b. MonadWriter Any m => b -> m b
hit (Pat -> m Pat) -> Pat -> m Pat
forall a b. (a -> b) -> a -> b
$ Exp -> Pat -> Pat
ViewP Exp
varView Pat
p
w (AsP Name
v Pat
p) = Pat -> m Pat
forall (m :: * -> *) b. MonadWriter Any m => b -> m b
hit (Pat -> m Pat) -> Pat -> m Pat
forall a b. (a -> b) -> a -> b
$ Exp -> Pat -> Pat
ViewP Exp
varView (Pat -> Pat) -> Pat -> Pat
forall a b. (a -> b) -> a -> b
$ Name -> Pat -> Pat
AsP Name
v (Pat -> Pat) -> Pat -> Pat
forall a b. (a -> b) -> a -> b
$ Pat -> Pat
asXform Pat
p
w (ViewP (VarE Name
n) Pat
p) = Pat -> m Pat
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat -> m Pat) -> Pat -> m Pat
forall a b. (a -> b) -> a -> b
$ Exp -> Pat -> Pat
ViewP (Name -> Exp
VarE 'unClosed Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
n) Pat
p
w (ViewP Exp
e Pat
_) = String -> m Pat
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m Pat) -> String -> m Pat
forall a b. (a -> b) -> a -> b
$ String
"view function must be a single name: `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Exp -> Doc
forall a. Ppr a => a -> Doc
TH.ppr Exp
e) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'"
w Pat
p = Pat -> m Pat
forall (m :: * -> *) a. Monad m => a -> m a
return Pat
p
parseHere :: String -> Q Pat
parseHere :: String -> Q Pat
parseHere String
s = do
String
fn <- Loc -> String
loc_filename (Loc -> String) -> Q Loc -> Q String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Q Loc
location
case String -> String -> Either String Pat
parsePattern String
fn String
s of
Left String
e -> String -> Q Pat
forall a. HasCallStack => String -> a
error (String -> Q Pat) -> String -> Q Pat
forall a b. (a -> b) -> a -> b
$ String
"Parse error: `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"'\n\n\t when parsing pattern: `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."
Right Pat
p -> Pat -> Q Pat
forall (m :: * -> *) a. Monad m => a -> m a
return Pat
p
same_ctx :: Mb ctx a -> Mb ctx b -> Mb ctx b
same_ctx :: Mb ctx a -> Mb ctx b -> Mb ctx b
same_ctx Mb ctx a
_ Mb ctx b
x = Mb ctx b
x
nuKit :: TH.Name -> TH.Name -> WrapKit
nuKit :: Name -> Name -> WrapKit
nuKit Name
topVar Name
namesVar = WrapKit :: Exp -> (Pat -> Pat) -> (Bool -> Pat -> Pat) -> WrapKit
WrapKit {_varView :: Exp
_varView = Exp
varView, _asXform :: Pat -> Pat
_asXform = Pat -> Pat
asXform, _topXform :: Bool -> Pat -> Pat
_topXform = Bool -> Pat -> Pat
topXform} where
varView :: Exp
varView = (Name -> Exp
VarE 'same_ctx Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
topVar) Exp -> Exp -> Exp
`compose`
(Exp -> [Exp] -> Exp
appEMulti (Name -> Exp
ConE 'MkMbPair) [Name -> Exp
VarE 'nuMatchingProof, Name -> Exp
VarE Name
namesVar])
asXform :: Pat -> Pat
asXform Pat
p = Exp -> Pat -> Pat
ViewP (Name -> Exp
VarE 'ensureFreshPair) ([Pat] -> Pat
TupP [Pat
WildP, Pat
p])
topXform :: Bool -> Pat -> Pat
topXform Bool
b Pat
p = if Bool
b then Name -> Pat -> Pat
AsP Name
topVar (Pat -> Pat) -> Pat -> Pat
forall a b. (a -> b) -> a -> b
$ Exp -> Pat -> Pat
ViewP (Name -> Exp
VarE 'ensureFreshPair) ([Pat] -> Pat
TupP [Name -> Pat
VarP Name
namesVar, Pat
p]) else Pat -> Pat
asXform Pat
p
nuP :: QuasiQuoter
nuP = String -> (String -> Q Pat) -> QuasiQuoter
patQQ String
"nuP" ((String -> Q Pat) -> QuasiQuoter)
-> (String -> Q Pat) -> QuasiQuoter
forall a b. (a -> b) -> a -> b
$ \String
s -> do
Name
topVar <- String -> Q Name
newName String
"topMb"
Name
namesVar <- String -> Q Name
newName String
"topNames"
String -> Q Pat
parseHere String
s Q Pat -> (Pat -> Q Pat) -> Q Pat
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= WrapKit -> Pat -> Q Pat
forall (m :: * -> *). MonadFail m => WrapKit -> Pat -> m Pat
wrapVars (Name -> Name -> WrapKit
nuKit Name
topVar Name
namesVar)
clKit :: WrapKit
clKit = WrapKit :: Exp -> (Pat -> Pat) -> (Bool -> Pat -> Pat) -> WrapKit
WrapKit {_varView :: Exp
_varView = Name -> Exp
ConE 'Closed, _asXform :: Pat -> Pat
_asXform = Pat -> Pat
asXform, _topXform :: Bool -> Pat -> Pat
_topXform = (Pat -> Pat) -> Bool -> Pat -> Pat
forall a b. a -> b -> a
const Pat -> Pat
asXform}
where asXform :: Pat -> Pat
asXform Pat
p = Name -> [Pat] -> Pat
ConP 'Closed [Pat
p]
clP :: QuasiQuoter
clP = String -> (String -> Q Pat) -> QuasiQuoter
patQQ String
"clP" ((String -> Q Pat) -> QuasiQuoter)
-> (String -> Q Pat) -> QuasiQuoter
forall a b. (a -> b) -> a -> b
$ (Q Pat -> (Pat -> Q Pat) -> Q Pat
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= WrapKit -> Pat -> Q Pat
forall (m :: * -> *). MonadFail m => WrapKit -> Pat -> m Pat
wrapVars WrapKit
clKit) (Q Pat -> Q Pat) -> (String -> Q Pat) -> String -> Q Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Q Pat
parseHere
clNuP :: QuasiQuoter
clNuP = String -> (String -> Q Pat) -> QuasiQuoter
patQQ String
"clNuP" ((String -> Q Pat) -> QuasiQuoter)
-> (String -> Q Pat) -> QuasiQuoter
forall a b. (a -> b) -> a -> b
$ \String
s -> do
Name
topVar <- String -> Q Name
newName String
"topMb"
Name
namesVar <- String -> Q Name
newName String
"topNames"
String -> Q Pat
parseHere String
s Q Pat -> (Pat -> Q Pat) -> Q Pat
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= WrapKit -> Pat -> Q Pat
forall (m :: * -> *). MonadFail m => WrapKit -> Pat -> m Pat
wrapVars (WrapKit
clKit WrapKit -> WrapKit -> WrapKit
`combineWrapKits` Name -> Name -> WrapKit
nuKit Name
topVar Name
namesVar)