@@ -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
@@ -34,6 +35,51 @@ import qualified Data.ByteString.UTF8 as UTF8
3435
3536import Debug.Trace
3637
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+
3783-- | Allow implicit type declarations
3884allowImp :: SyntaxInfo -> SyntaxInfo
3985allowImp syn = syn { implicitAllowed = True }
@@ -91,44 +137,69 @@ expr' syn = try (externalExpr syn)
91137{- | Parses a user-defined expression -}
92138externalExpr :: SyntaxInfo -> IdrisParser PTerm
93139externalExpr syn = do i <- get
94− extensions syn (syntax_rules i)
140+ if inPattern syn
141+ then rules_parserPattern (syntax_rules i) syn
142+ else rules_parserTerm (syntax_rules i) syn
95143 <?> "user-defined expression"
96144
97145{- | Parses a simple user-defined expression -}
98146simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
99147simpleExternalExpr syn = do i <- get
100− extensions syn (filter isSimple (syntax_rules i))
101− where
102− isSimple (Rule (Expr x:xs) _ _) = False
103− isSimple (Rule (SimpleExpr x:xs) _ _) = False
104− isSimple (Rule [Keyword _] _ _) = True
105− isSimple (Rule [Symbol _] _ _) = True
106− isSimple (Rule (_:xs) _ _) = case last xs of
107− Keyword _ -> True
108− Symbol _ -> True
109− _ -> False
110− isSimple _ = False
148+ if inPattern syn
149+ then rules_parserSimplePattern (syntax_rules i) syn
150+ else rules_parserSimpleTerm (syntax_rules i) syn
151+
152+data SynMatch = SynTm PTerm | SynBind Name
111153
112154{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
113155extensions :: 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)
115157 <?> "user-defined expression"
116158 where
117− isValid :: Syntax -> Bool
118− isValid (Rule _ _ AnySyntax) = True
119− isValid (Rule _ _ PatternSyntax) = inPattern syn
120− isValid (Rule _ _ TermSyntax) = not (inPattern syn)
121−
159+ extension ns rules =
160+ choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
161+ case head rs of -- can never be []
162+ Rule (symb:_) _ _ -> try $ do
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
122202
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
132203 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
133204 extensionSymbol (Keyword n) = do reserved (show n); return Nothing
134205 extensionSymbol (Expr n) = do tm <- expr syn