0 | -- Port of https://hackage.haskell.org/package/parsec-3.1.13.0/docs/Text-Parsec-Expr.html
  1 | -- Original License BSD-style: https://hackage.haskell.org/package/parsec-3.1.13.0/src/LICENSE
  2 |
  3 | module Data.String.Parser.Expression
  4 |
  5 | import Data.String.Parser
  6 |
  7 | public export
  8 | data Assoc = AssocNone
  9 |            | AssocLeft
 10 |            | AssocRight
 11 |
 12 | public export
 13 | data Operator a = Infix (Parser (a -> a -> a)) Assoc
 14 |                 | Prefix (Parser (a -> a))
 15 |                 | Postfix (Parser (a -> a))
 16 |
 17 | public export
 18 | OperatorTable : Type -> Type
 19 | OperatorTable a = List (List (Operator a))
 20 |
 21 | public export
 22 | BinaryOperator : Type -> Type
 23 | BinaryOperator a = List (Parser (a -> a -> a))
 24 |
 25 | public export
 26 | UnaryOperator : Type -> Type
 27 | UnaryOperator a = List (Parser (a -> a))
 28 |
 29 | public export
 30 | data Ops a = BinOp (BinaryOperator a) | UnOp (UnaryOperator a)
 31 |
 32 | public export
 33 | ReturnType : Type -> Type
 34 | ReturnType a = (BinaryOperator a, BinaryOperator a, BinaryOperator a, UnaryOperator a, UnaryOperator a)
 35 |
 36 | toParserBin : BinaryOperator a -> Parser (a -> a -> a)
 37 | toParserBin [] = fail "couldn't create binary parser"
 38 | toParserBin (x :: xs) = x <|> toParserBin xs
 39 |
 40 | toParserUn : UnaryOperator a -> Parser (a -> a)
 41 | toParserUn [] = fail "couldn't create unary parser"
 42 | toParserUn (x :: xs) = x <|> toParserUn xs
 43 |
 44 | ambiguous : (assoc : String) -> (op : Parser (a -> a -> a)) -> Parser a
 45 | ambiguous assoc op = do ignore op
 46 |                         fail ("ambiguous use of a " ++ assoc ++ " associative operator")
 47 |
 48 | mutual
 49 |   mkRassocP : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
 50 |   mkRassocP amLeft amNon rassocOp termP x =
 51 |    (do f <- rassocOp
 52 |        y <- do z <- termP ; mkRassocP1 amLeft amNon rassocOp termP z
 53 |        pure (f x y))
 54 |    <|> (amLeft)
 55 |    <|> (amNon)
 56 |
 57 |   mkRassocP1 : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
 58 |   mkRassocP1 amLeft amNon rassocOp termP x = (mkRassocP amLeft amNon rassocOp termP x) <|> pure x
 59 |
 60 | mutual
 61 |   mkLassocP : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
 62 |   mkLassocP amRight amNon lassocOp termP x =
 63 |     (do f <- lassocOp
 64 |         y <- termP
 65 |         mkLassocP1 amRight amNon lassocOp termP (f x y))
 66 |     <|> amRight
 67 |     <|> amNon
 68 |
 69 |   mkLassocP1 : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
 70 |   mkLassocP1 amRight amNon lassocOp termP x = mkLassocP amRight amNon lassocOp termP x <|> pure x
 71 |
 72 | mkNassocP : (amRight, amLeft, amNon : Parser a) ->
 73 |             (nassocOp : Parser (a -> a -> a)) ->
 74 |             (termP : Parser a) -> (x : a) -> Parser a
 75 | mkNassocP amRight amLeft amNon nassocOp termP x =
 76 |   do f <- nassocOp
 77 |      y <- termP
 78 |      ignore (amRight <|> amLeft <|> amNon)
 79 |      pure (f x y)
 80 |
 81 | public export
 82 | buildExpressionParser : (a : Type) -> OperatorTable a -> Parser a -> Parser a
 83 | buildExpressionParser a operators simpleExpr =
 84 |   foldl (makeParser a) simpleExpr operators
 85 |   where
 86 |     splitOp : (a : Type) -> Operator a -> ReturnType a -> ReturnType a
 87 |     splitOp x (Infix op AssocNone) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, op :: nassoc, prefixx, postfix)
 88 |     splitOp x (Infix op AssocLeft) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, op :: lassoc, nassoc, prefixx, postfix)
 89 |     splitOp x (Infix op AssocRight) (rassoc, lassoc, nassoc, prefixx, postfix) = (op :: rassoc, lassoc, nassoc, prefixx, postfix)
 90 |     splitOp x (Prefix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, op :: prefixx, postfix)
 91 |     splitOp x (Postfix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, prefixx, op :: postfix)
 92 |
 93 |     makeParser : (a : Type) -> Parser a -> List (Operator a) -> Parser a
 94 |     makeParser a term ops =
 95 |       let (rassoc,lassoc,nassoc
 96 |                ,prefixx,postfix) = foldr (splitOp a) ([],[],[],[],[]) ops
 97 |           rassocOp = toParserBin rassoc
 98 |           lassocOp = toParserBin lassoc
 99 |           nassocOp = toParserBin nassoc
100 |           prefixxOp = toParserUn prefixx
101 |           postfixOp = toParserUn postfix
102 |
103 |           amRight = ambiguous "right" rassocOp
104 |           amLeft = ambiguous "left" lassocOp
105 |           amNon = ambiguous "non" nassocOp
106 |
107 |           prefixxP = prefixxOp <|> pure (\x => x)
108 |
109 |           postfixP = postfixOp <|> pure (\x => x)
110 |
111 |           termP = do pre <- prefixxP
112 |                      x <- term
113 |                      post <- postfixP
114 |                      pure (post (pre x))
115 |
116 |           rassocP = mkRassocP amLeft amNon rassocOp termP
117 |           lassocP = mkLassocP amRight amNon lassocOp termP
118 |           nassocP = mkNassocP amRight amLeft amNon nassocOp termP
119 |       in
120 |           do x <- termP
121 |              rassocP x <|> lassocP x <|> nassocP x <|> pure x <?> "operator"
122 |