0 | module Text.Parser.Expression
 1 |
 2 | import Text.Parser
 3 |
 4 | public export
 5 | data Assoc
 6 |    = AssocNone
 7 |    | AssocLeft
 8 |    | AssocRight
 9 |
10 | public export
11 | data Op state k a
12 |   = Prefix (Grammar state k True (a -> a))
13 |   | Postfix (Grammar state k True (a -> a))
14 |   | Infix (Grammar state k True (a -> a -> a)) Assoc
15 |
16 | public export
17 | OperatorTable : Type -> Type -> Type -> Type
18 | OperatorTable state k a = List (List (Op state k a))
19 |
20 | export
21 | buildExpressionParser :
22 |   OperatorTable state k a ->
23 |   Grammar state k True a ->
24 |   Grammar state k True a
25 | buildExpressionParser table term = foldl level term table
26 |   where
27 |     level : Grammar state k True a -> List (Op state k a) -> Grammar state k True a
28 |     level factor ops = parseThese <|> factor
29 |       where
30 |         0 BinOp, UnOp : Type
31 |         BinOp = Grammar state k True (a -> a -> a)
32 |         UnOp = Grammar state k True (a -> a)
33 |
34 |         0 SortedOps : Type
35 |         SortedOps = (List BinOp, List BinOp, List BinOp, List UnOp, List UnOp)
36 |
37 |         separate : Op state k a -> SortedOps -> SortedOps
38 |         separate op (lassoc, rassoc, nassoc, pre, post) = case op of
39 |           Infix p AssocLeft  => (p::lassoc, rassoc, nassoc, pre, post)
40 |           Infix p AssocRight => (lassoc, p::rassoc, nassoc, pre, post)
41 |           Infix p AssocNone  => (lassoc, rassoc, p::nassoc, pre, post)
42 |           Prefix p           => (lassoc, rassoc, nassoc, p::pre, post)
43 |           Postfix p          => (lassoc, rassoc, nassoc, pre, p::post)
44 |
45 |         sortedOps : SortedOps
46 |         sortedOps = foldr separate ([], [], [], [], []) ops
47 |
48 |         parseThese : Grammar state k True a
49 |         parseThese =
50 |           let (lassoc, rassoc, nassoc, pre, post) = sortedOps
51 |
52 |               termP : Grammar state k True a
53 |               prefixP : Grammar state k False (a -> a)
54 |               postfixP : Grammar state k False (a -> a)
55 |               termP = do
56 |                   f <- prefixP
57 |                   x <- factor
58 |                   g <- postfixP
59 |                   pure $ g (f x)
60 |
61 |               prefixP = choice pre <|> pure id
62 |               postfixP = choice post <|> pure id
63 |
64 |               rassocP : a -> Grammar state k True a
65 |               rassocP1 : a -> Grammar state k False a
66 |               rassocP x = do
67 |                   f <- choice rassoc
68 |                   y <- termP >>= rassocP1
69 |                   pure $ f x y
70 |               rassocP1 x = rassocP x <|> pure x
71 |
72 |               lassocP : a -> Grammar state k True a
73 |               lassocP1 : a -> Grammar state k False a
74 |               lassocP x = do
75 |                   f <- choice lassoc
76 |                   y <- termP
77 |                   lassocP1 $ f x y
78 |               lassocP1 x = lassocP x <|> pure x
79 |
80 |               nassocP : a -> Grammar state k True a
81 |               nassocP x = do
82 |                   f <- choice nassoc
83 |                   y <- termP
84 |                   pure $ f x y
85 |
86 |           in do
87 |               x <- termP
88 |               rassocP x <|> lassocP x <|> nassocP x <|> pure x
89 |