{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE QuasiQuotes #-} module Data.Type.Quote where import Control.Arrow import Language.Haskell.TH import qualified Data.List as L import Data.Maybe (maybeToList) import Type.Family.Nat import Text.Read (readMaybe) import Data.Char (isSpace) import qualified Language.Haskell.Meta.Parse as P import Control.Monad ((>=>),(<=<)) failFrom :: Monad m => String -> String -> m a failFrom src msg = fail $ src ++ ": " ++ msg stub :: String -> String -> a -> Q b stub qq fn _ = failFrom qq $ fn ++ " not provided" -- Parsers {{{ parseExp :: String -> String -> Q Exp parseExp qq = eitherM qq . P.parseExp parsePat :: String -> String -> Q Pat parsePat qq = eitherM qq . P.parsePat parseType :: String -> String -> Q Type parseType qq = eitherM qq . P.parseType parseDecs :: String -> String -> Q [Dec] parseDecs qq = eitherM qq . P.parseDecs -- }}} -- Nat Util {{{ parseN :: Monad m => String -> String -> m N parseN qq = maybe (failFrom qq "couldn't parse number") (notNeg qq) . readMaybe notNeg :: Monad m => String -> Int -> m N notNeg qq n = maybe (failFrom qq $ "negative number: " ++ show n) return $ fromInt n -- }}} eitherM :: Monad m => String -> Either String a -> m a eitherM qq = either (failFrom qq) return maybeM :: Monad m => String -> String -> Maybe a -> m a maybeM qq msg = maybe (failFrom qq msg) return -- List Util {{{ readMaybeList :: Read a => String -> [a] readMaybeList = maybeToList . readMaybe commaSep :: String -> [String] commaSep = map (strip isSpace) . breakOnAll "," strip :: (a -> Bool) -> [a] -> [a] strip pr = L.dropWhileEnd pr . dropWhile pr breakOnAll :: Eq a => [a] -> [a] -> [[a]] breakOnAll b as = b1 : case rest of [] -> [] _ -> breakOnAll b rest where (b1,rest) = breakOn b as breakOn :: Eq a => [a] -> [a] -> ([a],[a]) breakOn b = \case [] -> ([],[]) as@(a : as') -> case getPrefix b as of Just sf -> ([],sf) _ -> first (a:) $ breakOn b as' getPrefix :: Eq a => [a] -> [a] -> Maybe [a] getPrefix p as | L.isPrefixOf p as = Just $ drop (length p) as | otherwise = Nothing -- }}} -- AddTerm {{{ data AddTerm a = Simple a | Add String a deriving (Eq,Ord,Show,Functor,Foldable,Traversable) instance (a ~ Int) => Read (AddTerm a) where readsPrec d s0 = [ (Add x i,s3) | (x,s1) <- lex s0 , ("+",s2) <- lex s1 , (i,s3) <- reads s2 ] ++ [ (Simple i,s1) | (i,s1) <- reads s0 ] parseAddTerm :: Monad m => String -> String -> m (AddTerm N) parseAddTerm qq = traverse (notNeg qq) <=< maybeM qq "couldn't parse AddTerm" . readMaybe fromAddTerm :: b -> (String -> b) -> (b -> a -> Q c) -> AddTerm a -> Q c fromAddTerm simp var f = \case Simple a -> f simp a Add x a -> f (var x) a parseAsNatTerm :: forall a. String -> (Name -> Q a) -> Q a -> (Q a -> Q a) -> String -> Q a parseAsNatTerm qq v z s = parseAddTerm qq >=> fromAddTerm z (v . mkName) go where go :: Q a -> N -> Q a go x = \case Z -> x S n -> s $ go x n -- }}}