git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1729 from projedi/custom-syntax-optimization

Custom syntax optimization

commit2b02303025e44e1e61e701c70cf43cae18531008 authorEdwin Brady <edwin.brady@gmail.com> dateMon 24 Nov 2014, 11:19 (12 years ago) parent3d1b0074130476
5 files changed+70−17
compare with master
unifiedsplit
CONTRIBUTORS+2−1 src/Idris/AbsSyntaxTree.hs+47−3 src/Idris/IBC.hs+1−1 src/Idris/ParseExpr.hs+18−10 src/Idris/Parser.hs+2−2
CONTRIBUTORS+2−1
@@ -35,4 +35,5 @@ Dirk Ullrich
3535Leif Warner
3636Daniel Waterworth
3737Jonas Westerlund
38−Alyssa Carter
38+Alyssa Carter
39+Alexander Shabalin
src/Idris/AbsSyntaxTree.hs+47−3
@@ -21,6 +21,7 @@ import System.IO
2121import Control.Monad.Trans.State.Strict
2222import Control.Monad.Trans.Error
2323
24+import Data.Function (on)
2425import Data.List hiding (group)
2526import Data.Char
2627import qualified Data.Map as M
@@ -177,7 +178,7 @@ data IState = IState {
177178 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
178179 idris_coercions :: [Name],
179180 idris_errRev :: [(Term, Term)],
180− syntax_rules :: [Syntax],
181+ syntax_rules :: SyntaxRules,
181182 syntax_keywords :: [String],
182183 imported :: [FilePath], -- ^ The imported modules
183184 idris_scprims :: [(Name, (Int, PrimFn))],
@@ -290,7 +291,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
290291 emptyContext emptyContext emptyContext emptyContext
291292 emptyContext emptyContext emptyContext emptyContext
292293 emptyContext emptyContext emptyContext emptyContext
293− [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
294+ [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
294295 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
295296 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
296297 AutomaticWidth S.empty Nothing Nothing []
@@ -985,6 +986,9 @@ syntaxNames :: Syntax -> [Name]
985986syntaxNames (Rule syms _ _) = mapMaybe ename syms
986987 where ename (Keyword n) = Just n
987988 ename _ = Nothing
989+
990+syntaxSymbols :: Syntax -> [SSymbol]
991+syntaxSymbols (Rule ss _ _) = ss
988992{-!
989993deriving instance Binary Syntax
990994deriving instance NFData Syntax
@@ -995,7 +999,7 @@ data SSymbol = Keyword Name
995999 | Binding Name
9961000 | Expr Name
9971001 | SimpleExpr Name
998− deriving Show
1002+ deriving (Show, Eq)
9991003
10001004
10011005{-!
@@ -1003,6 +1007,46 @@ deriving instance Binary SSymbol
10031007deriving instance NFData SSymbol
10041008!-}
10051009
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+
10061050initDSL = DSL (PRef f (sUN ">>="))
10071051 (PRef f (sUN "return"))
10081052 (PRef f (sUN "<$>"))
src/Idris/IBC.hs+1−1
@@ -394,7 +394,7 @@ pOptimise cs = mapM_ (\ (n, c) ->
394394
395395pSyntax :: [Syntax] -> Idris ()
396396pSyntax s = do i <- getIState
397− putIState (i { syntax_rules = s ++ syntax_rules i })
397+ putIState (i { syntax_rules = updateSyntaxRules s (syntax_rules i) })
398398
399399pKeywords :: [String] -> Idris ()
400400pKeywords k = do i <- getIState
src/Idris/ParseExpr.hs+18−10
@@ -23,6 +23,7 @@ import Control.Applicative
2323import Control.Monad
2424import Control.Monad.State.Strict
2525
26+import Data.Function (on)
2627import Data.Maybe
2728import qualified Data.List.Split as Spl
2829import Data.List
@@ -91,13 +92,13 @@ expr' syn = try (externalExpr syn)
9192{- | Parses a user-defined expression -}
9293externalExpr :: SyntaxInfo -> IdrisParser PTerm
9394externalExpr syn = do i <- get
94− extensions syn (syntax_rules i)
95+ extensions syn (syntaxRulesList $ syntax_rules i)
9596 <?> "user-defined expression"
9697
9798{- | Parses a simple user-defined expression -}
9899simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
99100simpleExternalExpr syn = do i <- get
100− extensions syn (filter isSimple (syntax_rules i))
101+ extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))
101102 where
102103 isSimple (Rule (Expr x:xs) _ _) = False
103104 isSimple (Rule (SimpleExpr x:xs) _ _) = False
@@ -111,7 +112,7 @@ simpleExternalExpr syn = do i <- get
111112
112113{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
113114extensions :: 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)
115116 <?> "user-defined expression"
116117 where
117118 isValid :: Syntax -> Bool
@@ -119,16 +120,23 @@ extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
119120 isValid (Rule _ _ PatternSyntax) = inPattern syn
120121 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
121122
122−
123123data SynMatch = SynTm PTerm | SynBind Name
124124
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
125+extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
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
130+ n <- extensionSymbol symb
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.
134+ Rule [] ptm _ -> return (flatten (update (mapMaybe id ns) ptm))
131135 where
136+ ruleGroup [] [] = True
137+ ruleGroup (s1:_) (s2:_) = s1 == s2
138+ ruleGroup _ _ = False
139+
132140 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
133141 extensionSymbol (Keyword n) = do reserved (show n); return Nothing
134142 extensionSymbol (Expr n) = do tm <- expr syn
src/Idris/Parser.hs+2−2
@@ -223,7 +223,7 @@ syntaxDecl syn = do s <- syntaxRule syn
223223
224224-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
225225addSyntax :: IState -> Syntax -> IState
226−addSyntax i s = i { syntax_rules = s : rs,
226+addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
227227 syntax_keywords = ks ++ ns,
228228 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
229229 where rs = syntax_rules i
@@ -233,7 +233,7 @@ addSyntax i s = i { syntax_rules = s : rs,
233233
234234-- | Like 'addSyntax', but no effect on the IBC.
235235addReplSyntax :: IState -> Syntax -> IState
236−addReplSyntax i s = i { syntax_rules = s : rs,
236+addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,
237237 syntax_keywords = ks ++ ns }
238238 where rs = syntax_rules i
239239 ns = syntax_keywords i