git.iko.soy/Idris-dev
on 0cb9b4e help sign in
Idris-dev/src/Idris/Parser/Ops.hs
172 lines 6.1 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.Parser.Ops where
4import Prelude hiding (pi)
6import Text.Trifecta.Delta
7import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
8import Text.Parser.LookAhead
9import Text.Parser.Expression
10import qualified Text.Parser.Token as Tok
11import qualified Text.Parser.Char as Chr
12import qualified Text.Parser.Token.Highlight as Hi
14import Idris.AbsSyntax
15import Idris.Parser.Helpers
17import Idris.Core.TT
19import Control.Applicative
20import Control.Monad
21import Control.Monad.State.Strict
23import Data.Maybe
24import qualified Data.List.Split as Spl
25import Data.List
26import Data.Monoid
27import Data.Char
28import qualified Data.HashSet as HS
29import qualified Data.Text as T
30import qualified Data.ByteString.UTF8 as UTF8
32import Debug.Trace
34-- | Creates table for fixity declarations to build expression parser
35-- using pre-build and user-defined operator/fixity declarations
36table :: [FixDecl] -> OperatorTable IdrisParser PTerm
37table fixes
38 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++
39 toTable (reverse fixes) ++
40 [[backtick],
41 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],
42 [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],
43 [nofixityoperator]]
44 where
45 flatten :: PTerm -> PTerm -- flatten application
46 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
47 flatten t = t
50-- | Calculates table for fixity declarations
51toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
52toTable fs = map (map toBin)
53 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
54 where toBin (Fix (PrefixN _) op) = prefix op
55 (\fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x])
56 toBin (Fix f op)
57 = binary op (\fc x y -> PApp fc (PRef fc [] (sUN op)) [pexp x,pexp y]) (assoc f)
58 assoc (Infixl _) = AssocLeft
59 assoc (Infixr _) = AssocRight
60 assoc (InfixN _) = AssocNone
62-- | Binary operator
63binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
64binary name f = Infix (do indentPropHolds gtProp
65 fc <- reservedOpFC name
66 indentPropHolds gtProp
67 return (f fc))
69-- | Prefix operator
70prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
71prefix name f = Prefix (do reservedOp name
72 fc <- getFC
73 indentPropHolds gtProp
74 return (f fc))
76-- | Backtick operator
77backtick :: Operator IdrisParser PTerm
78backtick = Infix (do indentPropHolds gtProp
79 lchar '`'; (n, fc) <- fnName
80 lchar '`'
81 indentPropHolds gtProp
82 return (\x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y])) AssocNone
84-- | Operator without fixity (throws an error)
85nofixityoperator :: Operator IdrisParser PTerm
86nofixityoperator = Infix (do indentPropHolds gtProp
87 op <- try operator
88 unexpected $ "Operator without known fixity: " ++ op) AssocNone
91{- | Parses an operator in function position i.e. enclosed by `()', with an
92 optional namespace
95 OperatorFront ::=
96 '(' '=' ')'
97 | (Identifier_t '.')? '(' Operator_t ')'
98 ;
101-}
102operatorFront :: IdrisParser (Name, FC)
103operatorFront = try (do (FC f (l, c) _) <- getFC
104 op <- lchar '(' *> reservedOp "=" <* lchar ')'
105 return (eqTy, FC f (l, c) (l, c+3)))
106 <|> maybeWithNS (do (FC f (l, c) _) <- getFC
107 op <- lchar '(' *> operator
108 (FC _ _ (l', c')) <- getFC
109 lchar ')'
110 return (op, (FC f (l, c) (l', c' + 1)))) False []
112{- | Parses a function (either normal name or operator)
115 FnName ::= Name | OperatorFront;
117-}
118fnName :: IdrisParser (Name, FC)
119fnName = try operatorFront <|> name <?> "function name"
121{- | Parses a fixity declaration
123Fixity ::=
124 FixityType Natural_t OperatorList Terminator
125 ;
127-}
128fixity :: IdrisParser PDecl
129fixity = do pushIndent
130 f <- fixityType; i <- fst <$> natural;
131 ops <- sepBy1 operator (lchar ',')
132 terminator
133 let prec = fromInteger i
134 istate <- get
135 let infixes = idris_infixes istate
136 let fs = map (Fix (f prec)) ops
137 let redecls = map (alreadyDeclared infixes) fs
138 let ill = filter (not . checkValidity) redecls
139 if null ill
140 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
141 , ibc_write = map IBCFix fs ++ ibc_write istate
142 })
143 fc <- getFC
144 return (PFix fc (f prec) ops)
145 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
146 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
147 <?> "fixity declaration"
148 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
149 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
151 checkValidity :: (FixDecl, [FixDecl]) -> Bool
152 checkValidity (f, fs) = all (== f) fs
154 extractName :: FixDecl -> String
155 extractName (Fix _ n) = n
157{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
159 FixityType ::=
160 'infixl'
161 | 'infixr'
162 | 'infix'
163 | 'prefix'
164 ;
166 -}
167fixityType :: IdrisParser (Int -> Fixity)
168fixityType = do reserved "infixl"; return Infixl
169 <|> do reserved "infixr"; return Infixr
170 <|> do reserved "infix"; return InfixN
171 <|> do reserved "prefix"; return PrefixN
172 <?> "fixity type"