git.iko.soy/Idris-dev
on 2a68244 help sign in
Idris-dev/src/Idris/Parser/Ops.hs
199 lines 7.5 kB history raw
1{-|
2Module : Idris.Parser.Ops
3Description : Parser for operators and fixity declarations.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
9module Idris.Parser.Ops where
11import Idris.AbsSyntax
12import Idris.Core.TT
13import Idris.Parser.Helpers
15import Prelude hiding (pi)
17import Control.Applicative
18import Control.Monad
19import Control.Monad.State.Strict
20import qualified Data.ByteString.UTF8 as UTF8
21import Data.Char
22import qualified Data.HashSet as HS
23import Data.List
24import qualified Data.List.Split as Spl
25import Data.Maybe
26import Data.Monoid
27import qualified Data.Text as T
28import Debug.Trace
29import qualified Text.Parser.Char as Chr
30import Text.Parser.Expression
31import Text.Parser.LookAhead
32import qualified Text.Parser.Token as Tok
33import qualified Text.Parser.Token.Highlight as Hi
34import Text.Trifecta hiding (char, charLiteral, natural, span, string,
35 stringLiteral, symbol, whiteSpace)
36import Text.Trifecta.Delta
38-- | Creates table for fixity declarations to build expression parser
39-- using pre-build and user-defined operator/fixity declarations
40table :: [FixDecl] -> OperatorTable IdrisParser PTerm
41table fixes
42 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++
43 toTable (reverse fixes) ++
44 [[backtick],
45 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],
46 [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],
47 [nofixityoperator]]
48 where
49 flatten :: PTerm -> PTerm -- flatten application
50 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
51 flatten t = t
54-- | Calculates table for fixity declarations
55toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
56toTable fs = map (map toBin)
57 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
58 where toBin (Fix (PrefixN _) op) = prefix op
59 (\fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x])
60 toBin (Fix f op)
61 = binary op (\fc x y -> PApp fc (PRef fc [] (sUN op)) [pexp x,pexp y]) (assoc f)
62 assoc (Infixl _) = AssocLeft
63 assoc (Infixr _) = AssocRight
64 assoc (InfixN _) = AssocNone
66-- | Binary operator
67binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
68binary name f = Infix (do indentPropHolds gtProp
69 fc <- reservedOpFC name
70 indentPropHolds gtProp
71 return (f fc))
73-- | Prefix operator
74prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
75prefix name f = Prefix (do reservedOp name
76 fc <- getFC
77 indentPropHolds gtProp
78 return (f fc))
80-- | Backtick operator
81backtick :: Operator IdrisParser PTerm
82backtick = Infix (do indentPropHolds gtProp
83 lchar '`'; (n, fc) <- fnName
84 lchar '`'
85 indentPropHolds gtProp
86 return (\x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y])) AssocNone
88-- | Operator without fixity (throws an error)
89nofixityoperator :: Operator IdrisParser PTerm
90nofixityoperator = Infix (do indentPropHolds gtProp
91 op <- try operator
92 unexpected $ "Operator without known fixity: " ++ op) AssocNone
95{- | Parses an operator in function position i.e. enclosed by `()', with an
96 optional namespace
99 OperatorFront ::=
100 '(' '=' ')'
101 | (Identifier_t '.')? '(' Operator_t ')'
102 ;
105-}
106operatorFront :: IdrisParser (Name, FC)
107operatorFront = try (do (FC f (l, c) _) <- getFC
108 op <- lchar '(' *> reservedOp "=" <* lchar ')'
109 return (eqTy, FC f (l, c) (l, c+3)))
110 <|> maybeWithNS (do (FC f (l, c) _) <- getFC
111 op <- lchar '(' *> operator
112 (FC _ _ (l', c')) <- getFC
113 lchar ')'
114 return (op, (FC f (l, c) (l', c' + 1)))) False []
116{- | Parses a function (either normal name or operator)
119 FnName ::= Name | OperatorFront;
121-}
122fnName :: IdrisParser (Name, FC)
123fnName = try operatorFront <|> name <?> "function name"
125{- | Parses a fixity declaration
127Fixity ::=
128 FixityType Natural_t OperatorList Terminator
129 ;
131-}
132fixity :: IdrisParser PDecl
133fixity = do pushIndent
134 f <- fixityType; i <- fst <$> natural;
135 ops <- sepBy1 operator (lchar ',')
136 terminator
137 let prec = fromInteger i
138 istate <- get
139 let infixes = idris_infixes istate
140 let fs = map (Fix (f prec)) ops
141 let redecls = map (alreadyDeclared infixes) fs
142 let ill = filter (not . checkValidity) redecls
143 if null ill
144 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
145 , ibc_write = map IBCFix fs ++ ibc_write istate
146 })
147 fc <- getFC
148 return (PFix fc (f prec) ops)
149 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
150 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
151 <?> "fixity declaration"
152 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
153 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
155 checkValidity :: (FixDecl, [FixDecl]) -> Bool
156 checkValidity (f, fs) = all (== f) fs
158 extractName :: FixDecl -> String
159 extractName (Fix _ n) = n
161-- | Check that a declaration of an operator also has fixity declared
162checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
163checkDeclFixity p = do decl <- p
164 case getDeclName decl of
165 Nothing -> return decl
166 Just n -> do checkNameFixity n
167 return decl
168 where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n
169 getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n
170 getDeclName _ = Nothing
172-- | Checks that an operator name also has a fixity declaration
173checkNameFixity :: Name -> IdrisParser ()
174checkNameFixity n = do fOk <- fixityOk n
175 unless fOk . fail $
176 "Missing fixity declaration for " ++ show n
177 where fixityOk (NS n' _) = fixityOk n'
178 fixityOk (UN n') | all (flip elem opChars) (str n') =
179 do fixities <- fmap idris_infixes get
180 return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities
181 | otherwise = return True
182 fixityOk _ = return True
184{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
186 FixityType ::=
187 'infixl'
188 | 'infixr'
189 | 'infix'
190 | 'prefix'
191 ;
193 -}
194fixityType :: IdrisParser (Int -> Fixity)
195fixityType = do reserved "infixl"; return Infixl
196 <|> do reserved "infixr"; return Infixr
197 <|> do reserved "infix"; return InfixN
198 <|> do reserved "prefix"; return PrefixN
199 <?> "fixity type"