-
Notifications
You must be signed in to change notification settings - Fork 0
/
LogicTemplates.hs
53 lines (42 loc) · 1.31 KB
/
LogicTemplates.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
{-# LANGUAGE TemplateHaskell, QuasiQuotes #-}
module LogicTemplates where
import LogicType
import Parser
import Utils
import Data.Generics
import qualified Language.Haskell.TH as TH
import Language.Haskell.TH.Quote
import Data.ByteString.Char8 (pack)
type FilePos = (String, Int, Int)
type VarTrans a = Logic -> Maybe (TH.Q a)
quoteLogicProof :: String -> TH.Q TH.Exp
quoteLogicProof s = do
pos <- getPosition
e <- parseLogicProof pos (pack s)
dataToExpQ (const Nothing `extQ` takeExpVar) e
quoteLogicPat :: String -> TH.Q TH.Pat
quoteLogicPat s = do
pos <- getPosition
e <- parseLogicExp pos (pack s)
dataToPatQ (const Nothing `extQ` takePatternVar) e
takeVar :: (TH.Name -> TH.Q a) -> VarTrans a
takeVar namef (Pred (VarID name es))
| length es == 0 = Just $ namef (TH.mkName $ lowercase name)
takeVar _ _ = Nothing
takePatternVar = takeVar TH.varP
takeExpVar = takeVar TH.varE
getPosition :: TH.Q FilePos
getPosition = fmap transPos TH.location where
transPos loc = (TH.loc_filename loc,
fst (TH.loc_start loc),
snd (TH.loc_start loc))
parseLogicProof = parseT proof
parseLogicExp = parseT expr
logic :: QuasiQuoter
logic = QuasiQuoter
{ quoteExp = quoteLogicProof
, quotePat = quoteLogicPat
, quoteDec = undefined
, quoteType = undefined
}
logicF = quoteFile logic