2b02303 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1729 from projedi/custom-syntax-optimization

2b02303Edwin Brady12 years ago

CONTRIBUTORS+2−1

compare with master

unifiedsplit

@@ -35,4 +35,5 @@ Dirk Ullrich

35Leif Warner

36Daniel Waterworth

37Jonas Westerlund

38−Alyssa Carter

38+Alyssa Carter

39+Alexander Shabalin

src/Idris/AbsSyntaxTree.hs+47−3

@@ -21,6 +21,7 @@ import System.IO

21import Control.Monad.Trans.State.Strict

22import Control.Monad.Trans.Error

24+import Data.Function (on)

24import Data.List hiding (group)

25import Data.List hiding (group)

25import Data.Char

26import Data.Char

26import qualified Data.Map as M

27import qualified Data.Map as M

@@ -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{-!

@@ -1003,6 +1007,46 @@ deriving instance Binary SSymbol

1003deriving instance NFData SSymbol

1007deriving instance NFData SSymbol

1004!-}

1008!-}

1005

1009

1010+newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }

1011+

1012+emptySyntaxRules :: SyntaxRules

1013+emptySyntaxRules = SyntaxRules []

1014+

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

1016+updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

1017+ where

1018+ newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)

1019+

1020+ ruleSort [] [] = EQ

1021+ ruleSort [] _ = LT

1022+ ruleSort _ [] = GT

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

1024+ case symCompare s1 s2 of

1025+ EQ -> ruleSort ss1 ss2

1026+ r -> r

1027+

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

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

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

1031+ symCompare (Keyword _) _ = LT

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

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

1034+ symCompare (Symbol _) _ = LT

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

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

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

1038+ symCompare (Binding _) _ = LT

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

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

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

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

1043+ symCompare (Expr _) _ = LT

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

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

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

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

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

1049+

1006initDSL = DSL (PRef f (sUN ">>="))

1050initDSL = DSL (PRef f (sUN ">>="))

1007 (PRef f (sUN "return"))

1051 (PRef f (sUN "return"))

1008 (PRef f (sUN "<$>"))

1052 (PRef f (sUN "<$>"))

src/Idris/IBC.hs+1−1

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

394

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

396pSyntax s = do i <- getIState

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

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

398

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

400pKeywords k = do i <- getIState

src/Idris/ParseExpr.hs+18−10

@@ -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

@@ -91,13 +92,13 @@ expr' syn = try (externalExpr syn)

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

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

92externalExpr :: SyntaxInfo -> IdrisParser PTerm

93externalExpr :: SyntaxInfo -> IdrisParser PTerm

93externalExpr syn = do i <- get

94externalExpr syn = do i <- get

94− extensions syn (syntax_rules i)

95+ extensions syn (syntaxRulesList $ syntax_rules i)

95 <?> "user-defined expression"

96 <?> "user-defined expression"

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

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

98simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

99simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

99simpleExternalExpr syn = do i <- get

100simpleExternalExpr syn = do i <- get

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

101+ extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))

101 where

102 where

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

103 isSimple (Rule (Expr x:xs) _ _) = False

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

104 isSimple (Rule (SimpleExpr x:xs) _ _) = False

@@ -111,7 +112,7 @@ simpleExternalExpr syn = do i <- get

111

112

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

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

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

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

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

115+extensions syn rules = extension syn [] (filter isValid rules)

115 <?> "user-defined expression"

116 <?> "user-defined expression"

116 where

117 where

117 isValid :: Syntax -> Bool

118 isValid :: Syntax -> Bool

@@ -119,16 +120,23 @@ extensions syn rules = choice (map (try . extension syn) (filter isValid rules))

119 isValid (Rule _ _ PatternSyntax) = inPattern syn

120 isValid (Rule _ _ PatternSyntax) = inPattern syn

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

121 isValid (Rule _ _ TermSyntax) = not (inPattern syn)

121

122

122−

123data SynMatch = SynTm PTerm | SynBind Name

124

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

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

125+extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

127−extension syn (Rule ssym ptm _)

126+extension syn ns rules =

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

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

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

128− = do smap <- mapM extensionSymbol ssym

130+ n <- extensionSymbol symb

129− let ns = mapMaybe id smap

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

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

133+ -- nondeterministic.

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

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

131 where

135 where

136+ ruleGroup [] [] = True

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

138+ ruleGroup _ _ = False

139+

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

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

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

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

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

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

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