9d804b5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Optimize custom syntax rules

9d804b5Alexander Shabalin12 years ago

src/Idris/AbsSyntaxTree.hs+7−3

compare with master

unifiedsplit

@@ -12,6 +12,7 @@ import IRTS.Lang

12import IRTS.CodegenCommon

13import Util.Pretty

14import Util.DynamicLinker

15+import {-# SOURCE #-} Idris.ParseExpr (SyntaxRules, emptySyntaxRules)

16import Idris.Colours

17import Idris.Colours

@@ -177,7 +178,7 @@ data IState = IState {

177 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

178 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

178 idris_coercions :: [Name],

179 idris_coercions :: [Name],

179 idris_errRev :: [(Term, Term)],

180 idris_errRev :: [(Term, Term)],

180− syntax_rules :: [Syntax],

181+ syntax_rules :: SyntaxRules,

181 syntax_keywords :: [String],

182 syntax_keywords :: [String],

182 imported :: [FilePath], -- ^ The imported modules

183 imported :: [FilePath], -- ^ The imported modules

183 idris_scprims :: [(Name, (Int, PrimFn))],

184 idris_scprims :: [(Name, (Int, PrimFn))],

@@ -290,7 +291,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

290 emptyContext emptyContext emptyContext emptyContext

291 emptyContext emptyContext emptyContext emptyContext

292 emptyContext emptyContext emptyContext emptyContext

293 emptyContext emptyContext emptyContext emptyContext

293− [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

294+ [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

294 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

295 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

295 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

296 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

296 AutomaticWidth S.empty Nothing Nothing []

297 AutomaticWidth S.empty Nothing Nothing []

@@ -985,6 +986,9 @@ syntaxNames :: Syntax -> [Name]

985syntaxNames (Rule syms _ _) = mapMaybe ename syms

986syntaxNames (Rule syms _ _) = mapMaybe ename syms

986 where ename (Keyword n) = Just n

987 where ename (Keyword n) = Just n

987 ename _ = Nothing

988 ename _ = Nothing

989+

990+syntaxSymbols :: Syntax -> [SSymbol]

991+syntaxSymbols (Rule ss _ _) = ss

988{-!

992{-!

989deriving instance Binary Syntax

993deriving instance Binary Syntax

990deriving instance NFData Syntax

994deriving instance NFData Syntax

@@ -995,7 +999,7 @@ data SSymbol = Keyword Name

995 | Binding Name

999 | Binding Name

996 | Expr Name

1000 | Expr Name

997 | SimpleExpr Name

1001 | SimpleExpr Name

998− deriving Show

1002+ deriving (Show, Eq)

999

1003

1000

1004

1001{-!

1005{-!

src/Idris/IBC.hs+2−1

@@ -12,6 +12,7 @@ import Idris.Error

12import Idris.Delaborate

13import qualified Idris.Docstrings as D

14import Idris.Docstrings (Docstring)

15+import Idris.ParseExpr (updateSyntaxRules)

15import Idris.Output

16import Idris.Output

17import qualified Cheapskate.Types as CT

18import qualified Cheapskate.Types as CT

@@ -394,7 +395,7 @@ pOptimise cs = mapM_ (\ (n, c) ->

394

395

395pSyntax :: [Syntax] -> Idris ()

396pSyntax :: [Syntax] -> Idris ()

396pSyntax s = do i <- getIState

397pSyntax s = do i <- getIState

397− putIState (i { syntax_rules = s ++ syntax_rules i })

398+ putIState (i { syntax_rules = updateSyntaxRules s (syntax_rules i) })

398

399

399pKeywords :: [String] -> Idris ()

400pKeywords :: [String] -> Idris ()

400pKeywords k = do i <- getIState

401pKeywords k = do i <- getIState

src/Idris/ParseExpr.hs+98−27

@@ -23,6 +23,7 @@ import Control.Applicative

23import Control.Monad

24import Control.Monad.State.Strict

26+import Data.Function (on)

26import Data.Maybe

27import Data.Maybe

27import qualified Data.List.Split as Spl

28import qualified Data.List.Split as Spl

28import Data.List

29import Data.List

@@ -34,6 +35,51 @@ import qualified Data.ByteString.UTF8 as UTF8

35import Debug.Trace

36import Debug.Trace

38+data SyntaxRules = SyntaxRules

39+ { rules_rules :: [Syntax]

40+ , rules_parserPattern :: (SyntaxInfo -> IdrisParser PTerm)

41+ , rules_parserTerm :: (SyntaxInfo -> IdrisParser PTerm)

42+ , rules_parserSimplePattern :: (SyntaxInfo -> IdrisParser PTerm)

43+ , rules_parserSimpleTerm :: (SyntaxInfo -> IdrisParser PTerm)

44+ }

45+

46+emptySyntaxRules :: SyntaxRules

47+emptySyntaxRules = SyntaxRules

48+ { rules_rules = []

49+ , rules_parserPattern = const empty

50+ , rules_parserTerm = const empty

51+ , rules_parserSimplePattern = const empty

52+ , rules_parserSimpleTerm = const empty

53+ }

54+

55+updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules

56+updateSyntaxRules rules sr = sr

57+ { rules_rules = newRules

58+ , rules_parserPattern = \syn -> extensions syn $ filter isPattern newRules

59+ , rules_parserTerm = \syn -> extensions syn $ filter isTerm newRules

60+ , rules_parserSimplePattern = \syn ->

61+ extensions syn $ filter isPattern $ filter isSimple $ newRules

62+ , rules_parserSimpleTerm = \syn ->

63+ extensions syn $ filter isTerm $ filter isSimple $ newRules

64+ }

65+ where

66+ newRules = rules ++ rules_rules sr

67+ isSimple (Rule (Expr x:xs) _ _) = False

68+ isSimple (Rule (SimpleExpr x:xs) _ _) = False

69+ isSimple (Rule [Keyword _] _ _) = True

70+ isSimple (Rule [Symbol _] _ _) = True

71+ isSimple (Rule (_:xs) _ _) = case last xs of

72+ Keyword _ -> True

73+ Symbol _ -> True

74+ _ -> False

75+ isSimple _ = False

76+ isPattern (Rule _ _ AnySyntax) = True

77+ isPattern (Rule _ _ PatternSyntax) = True

78+ isPattern _ = False

79+ isTerm (Rule _ _ AnySyntax) = True

80+ isTerm (Rule _ _ TermSyntax) = True

81+ isTerm _ = False

82+

37-- | Allow implicit type declarations

83-- | Allow implicit type declarations

38allowImp :: SyntaxInfo -> SyntaxInfo

84allowImp :: SyntaxInfo -> SyntaxInfo

39allowImp syn = syn { implicitAllowed = True }

85allowImp syn = syn { implicitAllowed = True }

@@ -91,44 +137,69 @@ expr' syn = try (externalExpr syn)

91{- | Parses a user-defined expression -}

137{- | Parses a user-defined expression -}

92externalExpr :: SyntaxInfo -> IdrisParser PTerm

138externalExpr :: SyntaxInfo -> IdrisParser PTerm

93externalExpr syn = do i <- get

139externalExpr syn = do i <- get

140+ if inPattern syn

141+ then rules_parserPattern (syntax_rules i) syn

94− extensions syn (syntax_rules i)

142+ else rules_parserTerm (syntax_rules i) syn

95 <?> "user-defined expression"

143 <?> "user-defined expression"

144

97{- | Parses a simple user-defined expression -}

145{- | Parses a simple user-defined expression -}

98simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

146simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

99simpleExternalExpr syn = do i <- get

147simpleExternalExpr syn = do i <- get

100− extensions syn (filter isSimple (syntax_rules i))

148+ if inPattern syn

101− where

149+ then rules_parserSimplePattern (syntax_rules i) syn

102− isSimple (Rule (Expr x:xs) _ _) = False

150+ else rules_parserSimpleTerm (syntax_rules i) syn

103− isSimple (Rule (SimpleExpr x:xs) _ _) = False

151+

104− isSimple (Rule [Keyword _] _ _) = True

152+data SynMatch = SynTm PTerm | SynBind Name

105− isSimple (Rule [Symbol _] _ _) = True

106− isSimple (Rule (_:xs) _ _) = case last xs of

107− Keyword _ -> True

108− Symbol _ -> True

109− _ -> False

110− isSimple _ = False

111

153

112{- | Tries to parse a user-defined expression given a list of syntactic extensions -}

154{- | Tries to parse a user-defined expression given a list of syntactic extensions -}

113extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm

155extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm

114−extensions syn rules = choice (map (try . extension syn) (filter isValid rules))

156+extensions syn rules = extension [] (sortBy (ruleSort `on` syntaxSymbols) rules)

115 <?> "user-defined expression"

157 <?> "user-defined expression"

116 where

158 where

117− isValid :: Syntax -> Bool

159+ extension ns rules =

118− isValid (Rule _ _ AnySyntax) = True

160+ choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

119− isValid (Rule _ _ PatternSyntax) = inPattern syn

161+ case head rs of -- can never be []

120− isValid (Rule _ _ TermSyntax) = not (inPattern syn)

162+ Rule (symb:_) _ _ -> try $ do

121−

163+ n <- extensionSymbol symb

164+ extension (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

165+ -- If we have more than one Rule in this bucket, our grammar is

166+ -- nondeterministic.

167+ Rule [] ptm _ -> return (flatten (update (mapMaybe id ns) ptm))

168+

169+ ruleGroup [] [] = True

170+ ruleGroup (s1:_) (s2:_) = s1 == s2

171+ ruleGroup _ _ = False

172+

173+ ruleSort [] [] = EQ

174+ ruleSort [] _ = LT

175+ ruleSort _ [] = GT

176+ ruleSort (s1:ss1) (s2:ss2) =

177+ case symCompare s1 s2 of

178+ EQ -> ruleSort ss1 ss2

179+ r -> r

180+

181+ -- Better than creating Ord instance for SSymbol since

182+ -- in general this ordering does not really make sense.

183+ symCompare (Keyword n1) (Keyword n2) = compare n1 n2

184+ symCompare (Keyword _) _ = LT

185+ symCompare (Symbol _) (Keyword _) = GT

186+ symCompare (Symbol s1) (Symbol s2) = compare s1 s2

187+ symCompare (Symbol _) _ = LT

188+ symCompare (Binding _) (Keyword _) = GT

189+ symCompare (Binding _) (Symbol _) = GT

190+ symCompare (Binding b1) (Binding b2) = compare b1 b2

191+ symCompare (Binding _) _ = LT

192+ symCompare (Expr _) (Keyword _) = GT

193+ symCompare (Expr _) (Symbol _) = GT

194+ symCompare (Expr _) (Binding _) = GT

195+ symCompare (Expr e1) (Expr e2) = compare e1 e2

196+ symCompare (Expr _) _ = LT

197+ symCompare (SimpleExpr _) (Keyword _) = GT

198+ symCompare (SimpleExpr _) (Symbol _) = GT

199+ symCompare (SimpleExpr _) (Binding _) = GT

200+ symCompare (SimpleExpr _) (Expr _) = GT

201+ symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2

122

202

123−data SynMatch = SynTm PTerm | SynBind Name

124−

125−{- | Tries to parse an expression given a user-defined rule -}

126−extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm

127−extension syn (Rule ssym ptm _)

128− = do smap <- mapM extensionSymbol ssym

129− let ns = mapMaybe id smap

130− return (flatten (update ns ptm)) -- updated with smap

131− where

132 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

203 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

133 extensionSymbol (Keyword n) = do reserved (show n); return Nothing

204 extensionSymbol (Keyword n) = do reserved (show n); return Nothing

134 extensionSymbol (Expr n) = do tm <- expr syn

205 extensionSymbol (Expr n) = do tm <- expr syn

src/Idris/ParseExpr.hs-bootnew file+5

@@ -0,0 +1,5 @@

1+module Idris.ParseExpr where

3+data SyntaxRules

5+emptySyntaxRules :: SyntaxRules

src/Idris/Parser.hs+2−2

@@ -223,7 +223,7 @@ syntaxDecl syn = do s <- syntaxRule syn

223

224-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.

225addSyntax :: IState -> Syntax -> IState

226−addSyntax i s = i { syntax_rules = s : rs,

226+addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,

227 syntax_keywords = ks ++ ns,

228 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }

229 where rs = syntax_rules i

@@ -233,7 +233,7 @@ addSyntax i s = i { syntax_rules = s : rs,

233

234-- | Like 'addSyntax', but no effect on the IBC.

235addReplSyntax :: IState -> Syntax -> IState

236−addReplSyntax i s = i { syntax_rules = s : rs,

236+addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,

237 syntax_keywords = ks ++ ns }

238 where rs = syntax_rules i

239 ns = syntax_keywords i