@@ -35,51 +35,6 @@ import qualified Data.ByteString.UTF8 as UTF8
36import 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)
46−emptySyntaxRules :: SyntaxRules
47−emptySyntaxRules = SyntaxRules
49− , rules_parserPattern = const empty
50− , rules_parserTerm = const empty
51− , rules_parserSimplePattern = const empty
52− , rules_parserSimpleTerm = const empty
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
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
76− isPattern (Rule _ _ AnySyntax) = True
77− isPattern (Rule _ _ PatternSyntax) = True
79− isTerm (Rule _ _ AnySyntax) = True
80− isTerm (Rule _ _ TermSyntax) = True
83-- | Allow implicit type declarations
38-- | Allow implicit type declarations
84allowImp :: SyntaxInfo -> SyntaxInfo
39allowImp :: SyntaxInfo -> SyntaxInfo
85allowImp syn = syn { implicitAllowed = True }
40allowImp syn = syn { implicitAllowed = True }
@@ -137,69 +92,51 @@ expr' syn = try (externalExpr syn)
137{- | Parses a user-defined expression -}
92{- | Parses a user-defined expression -}
138externalExpr :: SyntaxInfo -> IdrisParser PTerm
93externalExpr :: SyntaxInfo -> IdrisParser PTerm
139externalExpr syn = do i <- get
94externalExpr syn = do i <- get
140− if inPattern syn
95+ extensions syn (syntaxRulesList $ syntax_rules i)
141− then rules_parserPattern (syntax_rules i) syn
142− else rules_parserTerm (syntax_rules i) syn
143 <?> "user-defined expression"
96 <?> "user-defined expression"
145{- | Parses a simple user-defined expression -}
98{- | Parses a simple user-defined expression -}
146simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
99simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
147simpleExternalExpr syn = do i <- get
100simpleExternalExpr syn = do i <- get
148− if inPattern syn
101+ extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))
149− then rules_parserSimplePattern (syntax_rules i) syn
102+ where
150− else rules_parserSimpleTerm (syntax_rules i) syn
103+ isSimple (Rule (Expr x:xs) _ _) = False
151−
104+ isSimple (Rule (SimpleExpr x:xs) _ _) = False
152−data SynMatch = SynTm PTerm | SynBind Name
105+ isSimple (Rule [Keyword _] _ _) = True
106+ isSimple (Rule [Symbol _] _ _) = True
107+ isSimple (Rule (_:xs) _ _) = case last xs of
154{- | 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 -}
155extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
114extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
156−extensions syn rules = extension [] (sortBy (ruleSort `on` syntaxSymbols) rules)
115+extensions syn rules = extension syn [] (filter isValid rules)
157 <?> "user-defined expression"
116 <?> "user-defined expression"
159− extension ns rules =
118+ isValid :: Syntax -> Bool
160− choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
119+ isValid (Rule _ _ AnySyntax) = True
161− case head rs of -- can never be []
120+ isValid (Rule _ _ PatternSyntax) = inPattern syn
162− Rule (symb:_) _ _ -> try $ do
121+ isValid (Rule _ _ TermSyntax) = not (inPattern syn)
163− n <- extensionSymbol symb
122+
164− extension (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]
123+data SynMatch = SynTm PTerm | SynBind Name
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))
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))
169 ruleGroup [] [] = True
136 ruleGroup [] [] = True
170 ruleGroup (s1:_) (s2:_) = s1 == s2
137 ruleGroup (s1:_) (s2:_) = s1 == s2
171 ruleGroup _ _ = False
138 ruleGroup _ _ = False
176− ruleSort (s1:ss1) (s2:ss2) =
177− case symCompare s1 s2 of
178− EQ -> ruleSort ss1 ss2
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
203 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
140 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
204 extensionSymbol (Keyword n) = do reserved (show n); return Nothing
141 extensionSymbol (Keyword n) = do reserved (show n); return Nothing
205 extensionSymbol (Expr n) = do tm <- expr syn
142 extensionSymbol (Expr n) = do tm <- expr syn