mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
Merge pull request #526 from alexhumphreys/feat/buildExpressionParser
Add BuildExpressionParser to contrib
This commit is contained in:
commit
93ecb72012
@ -1,10 +1,11 @@
|
|||||||
||| A simple parser combinator library for strings. Inspired by attoparsec zepto.
|
||| A simple parser combinator library for strings. Inspired by attoparsec zepto.
|
||||||
module Data.String.Parser
|
module Data.String.Parser
|
||||||
|
|
||||||
import Control.Monad.Identity
|
import Control.Monad.Identity
|
||||||
import Control.Monad.Trans
|
import Control.Monad.Trans
|
||||||
|
|
||||||
import Data.Strings
|
import Data.Strings
|
||||||
|
import Data.Fin
|
||||||
|
import Data.List
|
||||||
|
|
||||||
%default partial
|
%default partial
|
||||||
|
|
||||||
@ -153,3 +154,81 @@ option def p = p <|> pure def
|
|||||||
export
|
export
|
||||||
optional : Monad m => ParseT m a -> ParseT m (Maybe a)
|
optional : Monad m => ParseT m a -> ParseT m (Maybe a)
|
||||||
optional p = (p >>= \res => pure $ Just res) <|> pure Nothing
|
optional p = (p >>= \res => pure $ Just res) <|> pure Nothing
|
||||||
|
|
||||||
|
||| Discards the result of a parser
|
||||||
|
export
|
||||||
|
skip : Parser a -> Parser ()
|
||||||
|
skip = ignore
|
||||||
|
|
||||||
|
||| Parses a space character
|
||||||
|
export
|
||||||
|
space : Parser Char
|
||||||
|
space = satisfy isSpace
|
||||||
|
|
||||||
|
||| Parses one or more space characters
|
||||||
|
export
|
||||||
|
spaces : Parser ()
|
||||||
|
spaces = skip (many space) <?> "white space"
|
||||||
|
|
||||||
|
||| Discards whitespace after a matching parser
|
||||||
|
export
|
||||||
|
lexeme : Parser a -> Parser a
|
||||||
|
lexeme p = p <* spaces
|
||||||
|
|
||||||
|
||| Matches a specific string, then skips following whitespace
|
||||||
|
export
|
||||||
|
token : String -> Parser ()
|
||||||
|
token s = lexeme (skip (string s)) <?> "token " ++ show s
|
||||||
|
|
||||||
|
||| Fail with some error message
|
||||||
|
export
|
||||||
|
fail : Monad m => String -> ParseT m a
|
||||||
|
fail x = P $ \s => do pure $ Fail s.pos x
|
||||||
|
|
||||||
|
||| Matches a single digit
|
||||||
|
export
|
||||||
|
digit : Parser (Fin 10)
|
||||||
|
digit = do x <- satisfy isDigit
|
||||||
|
case lookup x digits of
|
||||||
|
Nothing => P $ \s => do pure $ Fail s.pos "not a digit"
|
||||||
|
Just y => P $ \s => Id (OK y s)
|
||||||
|
where
|
||||||
|
digits : List (Char, Fin 10)
|
||||||
|
digits = [ ('0', 0)
|
||||||
|
, ('1', 1)
|
||||||
|
, ('2', 2)
|
||||||
|
, ('3', 3)
|
||||||
|
, ('4', 4)
|
||||||
|
, ('5', 5)
|
||||||
|
, ('6', 6)
|
||||||
|
, ('7', 7)
|
||||||
|
, ('8', 8)
|
||||||
|
, ('9', 9)
|
||||||
|
]
|
||||||
|
|
||||||
|
fromDigits : Num a => ((Fin 10) -> a) -> List (Fin 10) -> a
|
||||||
|
fromDigits f xs = foldl (addDigit) 0 xs
|
||||||
|
where
|
||||||
|
addDigit : a -> (Fin 10) -> a
|
||||||
|
addDigit num d = 10*num + (f d)
|
||||||
|
|
||||||
|
intFromDigits : List (Fin 10) -> Integer
|
||||||
|
intFromDigits = fromDigits finToInteger
|
||||||
|
|
||||||
|
natFromDigits : List (Fin 10) -> Nat
|
||||||
|
natFromDigits = fromDigits finToNat
|
||||||
|
|
||||||
|
||| Matches a natural number
|
||||||
|
export
|
||||||
|
natural : Parser Nat
|
||||||
|
natural = do x <- some digit
|
||||||
|
pure (natFromDigits x)
|
||||||
|
|
||||||
|
||| Matches an integer, eg. "12", "-4"
|
||||||
|
export
|
||||||
|
integer : Parser Integer
|
||||||
|
integer = do minus <- optional (char '-')
|
||||||
|
x <- some digit
|
||||||
|
case minus of
|
||||||
|
Nothing => pure (intFromDigits x)
|
||||||
|
(Just y) => pure ((intFromDigits x)*(-1))
|
||||||
|
125
libs/contrib/Data/String/Parser/Expression.idr
Normal file
125
libs/contrib/Data/String/Parser/Expression.idr
Normal file
@ -0,0 +1,125 @@
|
|||||||
|
-- Port of https://hackage.haskell.org/package/parsec-3.1.13.0/docs/Text-Parsec-Expr.html
|
||||||
|
-- Original License BSD-style: https://hackage.haskell.org/package/parsec-3.1.13.0/src/LICENSE
|
||||||
|
|
||||||
|
module Data.String.Parser.Expression
|
||||||
|
|
||||||
|
import Control.Monad.Identity
|
||||||
|
import Data.String.Parser
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Assoc = AssocNone
|
||||||
|
| AssocLeft
|
||||||
|
| AssocRight
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Operator a = Infix (Parser (a -> a -> a)) Assoc
|
||||||
|
| Prefix (Parser (a -> a))
|
||||||
|
| Postfix (Parser (a -> a))
|
||||||
|
|
||||||
|
public export
|
||||||
|
OperatorTable : Type -> Type
|
||||||
|
OperatorTable a = List (List (Operator a))
|
||||||
|
|
||||||
|
public export
|
||||||
|
BinaryOperator : Type -> Type
|
||||||
|
BinaryOperator a = List (Parser (a -> a -> a))
|
||||||
|
|
||||||
|
public export
|
||||||
|
UnaryOperator : Type -> Type
|
||||||
|
UnaryOperator a = List (Parser (a -> a))
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Ops a = BinOp (BinaryOperator a) | UnOp (UnaryOperator a)
|
||||||
|
|
||||||
|
public export
|
||||||
|
ReturnType : Type -> Type
|
||||||
|
ReturnType a = (BinaryOperator a, BinaryOperator a, BinaryOperator a, UnaryOperator a, UnaryOperator a)
|
||||||
|
|
||||||
|
toParserBin : BinaryOperator a -> Parser (a -> a -> a)
|
||||||
|
toParserBin [] = fail "couldn't create binary parser"
|
||||||
|
toParserBin (x :: xs) = x <|> toParserBin xs
|
||||||
|
|
||||||
|
toParserUn : UnaryOperator a -> Parser (a -> a)
|
||||||
|
toParserUn [] = fail "couldn't create unary parser"
|
||||||
|
toParserUn (x :: xs) = x <|> toParserUn xs
|
||||||
|
|
||||||
|
ambigious : (assoc : String) -> (op : Parser (a -> a -> a)) -> Parser a
|
||||||
|
ambigious assoc op = do op
|
||||||
|
fail ("ambiguous use of a " ++ assoc ++ " associative operator")
|
||||||
|
|
||||||
|
mutual
|
||||||
|
mkRassocP : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
|
||||||
|
mkRassocP amLeft amNon rassocOp termP x =
|
||||||
|
(do f <- rassocOp
|
||||||
|
y <- do z <- termP ; mkRassocP1 amLeft amNon rassocOp termP z
|
||||||
|
pure (f x y))
|
||||||
|
<|> (amLeft)
|
||||||
|
<|> (amNon)
|
||||||
|
|
||||||
|
mkRassocP1 : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
|
||||||
|
mkRassocP1 amLeft amNon rassocOp termP x = (mkRassocP amLeft amNon rassocOp termP x) <|> pure x
|
||||||
|
|
||||||
|
mutual
|
||||||
|
mkLassocP : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
|
||||||
|
mkLassocP amRight amNon lassocOp termP x =
|
||||||
|
(do f <- lassocOp
|
||||||
|
y <- termP
|
||||||
|
mkLassocP1 amRight amNon lassocOp termP (f x y))
|
||||||
|
<|> amRight
|
||||||
|
<|> amNon
|
||||||
|
|
||||||
|
mkLassocP1 : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
|
||||||
|
mkLassocP1 amRight amNon lassocOp termP x = mkLassocP amRight amNon lassocOp termP x <|> pure x
|
||||||
|
|
||||||
|
mkNassocP : (amRight : Parser a) -> (amLeft : Parser a) -> (amNon : Parser a) -> (nassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
|
||||||
|
mkNassocP amRight amLeft amNon nassocOp termP x =
|
||||||
|
do f <- nassocOp
|
||||||
|
y <- termP
|
||||||
|
amRight <|> amLeft <|> amNon
|
||||||
|
pure (f x y)
|
||||||
|
|
||||||
|
public export
|
||||||
|
buildExpressionParser : (a : Type) -> OperatorTable a -> Parser a -> Parser a
|
||||||
|
buildExpressionParser a operators simpleExpr =
|
||||||
|
foldl (makeParser a) simpleExpr operators
|
||||||
|
where
|
||||||
|
splitOp : (a : Type) -> Operator a -> ReturnType a -> ReturnType a
|
||||||
|
splitOp x (Infix op AssocNone) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, op :: nassoc, prefixx, postfix)
|
||||||
|
splitOp x (Infix op AssocLeft) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, op :: lassoc, nassoc, prefixx, postfix)
|
||||||
|
splitOp x (Infix op AssocRight) (rassoc, lassoc, nassoc, prefixx, postfix) = (op :: rassoc, lassoc, nassoc, prefixx, postfix)
|
||||||
|
splitOp x (Prefix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, op :: prefixx, postfix)
|
||||||
|
splitOp x (Postfix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, prefixx, op :: postfix)
|
||||||
|
|
||||||
|
makeParser : (a : Type) -> Parser a -> List (Operator a) -> Parser a
|
||||||
|
makeParser a term ops =
|
||||||
|
let (rassoc,lassoc,nassoc
|
||||||
|
,prefixx,postfix) = foldr (splitOp a) ([],[],[],[],[]) ops
|
||||||
|
rassocOp = toParserBin rassoc
|
||||||
|
lassocOp = toParserBin lassoc
|
||||||
|
nassocOp = toParserBin nassoc
|
||||||
|
prefixxOp = toParserUn prefixx
|
||||||
|
postfixOp = toParserUn postfix
|
||||||
|
|
||||||
|
amRight = ambigious "right" rassocOp
|
||||||
|
amLeft = ambigious "left" lassocOp
|
||||||
|
amNon = ambigious "non" nassocOp
|
||||||
|
|
||||||
|
prefixxP = prefixxOp <|> pure (\x => x)
|
||||||
|
|
||||||
|
postfixP = postfixOp <|> pure (\x => x)
|
||||||
|
|
||||||
|
termP = do pre <- prefixxP
|
||||||
|
x <- term
|
||||||
|
post <- postfixP
|
||||||
|
pure (post (pre x))
|
||||||
|
|
||||||
|
rassocP = mkRassocP amLeft amNon rassocOp termP
|
||||||
|
rassocP1 = mkRassocP1 amLeft amNon rassocOp termP
|
||||||
|
|
||||||
|
lassocP = mkLassocP amRight amNon lassocOp termP
|
||||||
|
lassocP1 = mkLassocP1 amRight amNon lassocOp termP
|
||||||
|
|
||||||
|
nassocP = mkNassocP amRight amLeft amNon nassocOp termP
|
||||||
|
in
|
||||||
|
do x <- termP
|
||||||
|
rassocP x <|> lassocP x <|> nassocP x <|> pure x <?> "operator"
|
@ -41,6 +41,7 @@ modules = Control.ANSI,
|
|||||||
Data.String.Extra,
|
Data.String.Extra,
|
||||||
Data.String.Interpolation,
|
Data.String.Interpolation,
|
||||||
Data.String.Parser,
|
Data.String.Parser,
|
||||||
|
Data.String.Parser.Expression,
|
||||||
|
|
||||||
Data.Vect.Sort,
|
Data.Vect.Sort,
|
||||||
|
|
||||||
|
@ -125,7 +125,7 @@ chezTests
|
|||||||
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
||||||
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
|
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
|
||||||
"chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
|
"chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
|
||||||
"chez025", "chez026", "chez027",
|
"chez025", "chez026", "chez027", "chez028",
|
||||||
"reg001"]
|
"reg001"]
|
||||||
|
|
||||||
nodeTests : List String
|
nodeTests : List String
|
||||||
|
55
tests/chez/chez028/ExpressionParser.idr
Normal file
55
tests/chez/chez028/ExpressionParser.idr
Normal file
@ -0,0 +1,55 @@
|
|||||||
|
module Main
|
||||||
|
|
||||||
|
import Control.Monad.Identity
|
||||||
|
import Control.Monad.Trans
|
||||||
|
|
||||||
|
import Data.Nat
|
||||||
|
import Data.String.Parser
|
||||||
|
import Data.String.Parser.Expression
|
||||||
|
|
||||||
|
%default partial
|
||||||
|
|
||||||
|
table : OperatorTable Nat
|
||||||
|
table =
|
||||||
|
[ [Infix (do token "^"; pure (power) ) AssocRight]
|
||||||
|
, [ Infix (do token "*"; pure (*) ) AssocLeft ]
|
||||||
|
, [ Infix (do token "+"; pure (+) ) AssocLeft ]
|
||||||
|
]
|
||||||
|
|
||||||
|
table' : OperatorTable Integer
|
||||||
|
table' =
|
||||||
|
[ [ Infix (do token "*"; pure (*) ) AssocLeft
|
||||||
|
, Infix (do token "/"; pure (div) ) AssocLeft
|
||||||
|
]
|
||||||
|
, [ Infix (do token "+"; pure (+) ) AssocLeft
|
||||||
|
, Infix (do token "-"; pure (-) ) AssocLeft
|
||||||
|
]
|
||||||
|
]
|
||||||
|
|
||||||
|
mutual
|
||||||
|
term : Parser Nat
|
||||||
|
term = (natural <|> expr) <* spaces
|
||||||
|
<?> "simple expression"
|
||||||
|
|
||||||
|
expr : Parser Nat
|
||||||
|
expr = buildExpressionParser Nat table term
|
||||||
|
|
||||||
|
mutual
|
||||||
|
term' : Parser Integer
|
||||||
|
term' = (integer <|> expr') <* spaces
|
||||||
|
<?> "simple expression"
|
||||||
|
|
||||||
|
expr' : Parser Integer
|
||||||
|
expr' = buildExpressionParser Integer table' term'
|
||||||
|
|
||||||
|
showRes : Show a => Either String (a, Int) -> IO ()
|
||||||
|
showRes res = case res of
|
||||||
|
Left err => putStrLn err
|
||||||
|
Right (xs, rem) => printLn xs
|
||||||
|
|
||||||
|
main : IO ()
|
||||||
|
main = do showRes (parse natural "5678")
|
||||||
|
showRes (parse integer "-3")
|
||||||
|
showRes (parse expr "1+4^3^2^1")
|
||||||
|
showRes (parse expr' "4 + 2 * 3")
|
||||||
|
showRes (parse expr' "13-3+1*2-10/2")
|
7
tests/chez/chez028/expected
Normal file
7
tests/chez/chez028/expected
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
5678
|
||||||
|
-3
|
||||||
|
262145
|
||||||
|
10
|
||||||
|
7
|
||||||
|
1/1: Building ExpressionParser (ExpressionParser.idr)
|
||||||
|
Main> Main> Bye for now!
|
2
tests/chez/chez028/input
Normal file
2
tests/chez/chez028/input
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
:exec main
|
||||||
|
:q
|
3
tests/chez/chez028/run
Normal file
3
tests/chez/chez028/run
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
$1 --no-banner -p contrib ExpressionParser.idr < input
|
||||||
|
|
||||||
|
rm -rf build
|
Loading…
Reference in New Issue
Block a user