parser works good now
This commit is contained in:
parent
473d26ff0e
commit
549fecacfc
1 changed files with 133 additions and 10 deletions
143
prover.hs
143
prover.hs
|
@ -30,7 +30,7 @@ instance Monad Parser where
|
|||
-- (>>=) :: Parser a -> (a -> Parser b) -> Parser b
|
||||
p >>= f = P (\s -> case apply p s of
|
||||
[] -> []
|
||||
[(g, left)] -> apply (f g) left)
|
||||
[(v, out)] -> apply (f v) out)
|
||||
|
||||
(<|>) :: Parser a -> Parser a -> Parser a
|
||||
p <|> q = P (\s -> let ps = apply p s in
|
||||
|
@ -39,7 +39,7 @@ p <|> q = P (\s -> let ps = apply p s in
|
|||
else ps)
|
||||
|
||||
item :: Parser Char
|
||||
item = P (\case
|
||||
item = P (\x -> case x of
|
||||
[] -> []
|
||||
(x:xs) -> [(x,xs)])
|
||||
|
||||
|
@ -54,25 +54,148 @@ sat p = do x <- item
|
|||
parse_fail :: Parser a
|
||||
parse_fail = P (const [])
|
||||
|
||||
some :: Parser a -> Parser [a]
|
||||
-- some p = do x <- p
|
||||
-- xs <- some p
|
||||
-- return (x:xs)
|
||||
|
||||
some p = p >>= (\x -> some p >>= (\xs -> return (x : xs)))
|
||||
char :: Char -> Parser Char
|
||||
char x = sat (== x)
|
||||
|
||||
string :: String -> Parser ()
|
||||
string [] = return ()
|
||||
string (x:xs) = do char x
|
||||
string xs
|
||||
return ()
|
||||
|
||||
some, many :: Parser a -> Parser [a]
|
||||
|
||||
some a = do c <- a
|
||||
cs <- many a
|
||||
return (c:cs)
|
||||
|
||||
many = optional . some
|
||||
|
||||
optional :: Parser [a] -> Parser [a]
|
||||
optional = (<|> none)
|
||||
|
||||
many :: Parser a -> Parser [a]
|
||||
many = optional . some
|
||||
spaces :: Parser [Char]
|
||||
spaces = many (sat isSpace)
|
||||
|
||||
token :: Parser a -> Parser a
|
||||
token = (spaces >>)
|
||||
|
||||
guard True = return ()
|
||||
guard False = parse_fail
|
||||
|
||||
paren :: Parser a -> Parser a
|
||||
paren p = do symbol "("
|
||||
c <- p
|
||||
symbol ")"
|
||||
return c
|
||||
|
||||
symbol :: String -> Parser ()
|
||||
symbol = token . string
|
||||
|
||||
somewith, manywith :: Parser a -> Parser b -> Parser [b]
|
||||
somewith s p = do c <- p
|
||||
cs <- many (s >> p)
|
||||
return (c:cs)
|
||||
|
||||
manywith s = optional . somewith s
|
||||
|
||||
|
||||
digit :: Parser Int
|
||||
digit = sat isDigit >>= \d -> return (cvt d)
|
||||
where cvt d = fromEnum d - fromEnum '0'
|
||||
|
||||
|
||||
natural, nat :: Parser Int
|
||||
|
||||
natural = token nat
|
||||
nat = do ds <- some digit
|
||||
return (foldl1 shiftl ds)
|
||||
where shiftl m n = 10*m+n
|
||||
|
||||
|
||||
----------------- Calculator -----------------------------------
|
||||
|
||||
newtype Expr = Compose [Atom] deriving Eq
|
||||
newtype Expr = Compose [Atom]
|
||||
deriving Eq
|
||||
data Atom = Var VarName | Con ConName [Expr]
|
||||
deriving Eq
|
||||
|
||||
type VarName = String
|
||||
type ConName = String
|
||||
|
||||
instance Show Expr where
|
||||
showsPrec p (Compose []) = showString "id"
|
||||
showsPrec p (Compose [a]) = showsPrec p a
|
||||
showsPrec p (Compose as)
|
||||
= showParen (p>0) (showSep " . " (showsPrec 1) as)
|
||||
|
||||
compose :: [ShowS] -> ShowS
|
||||
compose = foldr (.) id
|
||||
|
||||
showSep :: String -> (a -> ShowS) -> [a] -> ShowS
|
||||
showSep sep f
|
||||
= compose . intersperse (showString sep) . map f
|
||||
|
||||
instance Show Atom where
|
||||
showsPrec p (Var v) = showString v
|
||||
showsPrec p (Con f []) = showString f
|
||||
showsPrec p (Con f [l,r])
|
||||
| isOp f = showParen (p>0) (showsPrec 1 l . showSpace
|
||||
. showString f . showSpace . showsPrec 1 r)
|
||||
showsPrec p (Con f es)
|
||||
= showParen (p>1) (showString f . showSpace . showSep " " (showsPrec 2) es)
|
||||
|
||||
showSpace = showChar ' '
|
||||
|
||||
isOp f = all symbolic f
|
||||
|
||||
intersperse :: a -> [a] -> [a]
|
||||
intersperse _ [x] = [x]
|
||||
intersperse s (x : xs)
|
||||
= x : s : intersperse s xs
|
||||
|
||||
|
||||
-- Main parsing
|
||||
|
||||
expr :: Parser Expr
|
||||
expr = simple >>= rest
|
||||
where
|
||||
rest l = do op <- operator
|
||||
r <- simple
|
||||
return (Compose [Con op [l, r]])
|
||||
<|> return l
|
||||
|
||||
operator :: Parser String
|
||||
operator = do op <- token (some (sat symbolic))
|
||||
guard (op /= "." && op /= "=")
|
||||
return op
|
||||
|
||||
symbolic = (`elem` symbolic_ops)
|
||||
symbolic_ops = "!@#$%^&*+./<=>?\\^|:-~"
|
||||
|
||||
simple :: Parser Expr
|
||||
simple = do es <- somewith (symbol ".") term
|
||||
return (Compose (concatMap deCompose es))
|
||||
|
||||
term :: Parser Expr
|
||||
term = ident args <|> paren expr
|
||||
args = many (ident none <|> paren expr)
|
||||
|
||||
deCompose :: Expr -> [Atom]
|
||||
deCompose (Compose at) = at
|
||||
|
||||
ident :: Parser [Expr] -> Parser Expr
|
||||
ident args =
|
||||
do x <- token (some (sat isAlphaNum))
|
||||
guard (isAlpha (head x))
|
||||
if isVar x
|
||||
then return (Compose [Var x])
|
||||
else if (x == "id")
|
||||
then return (Compose [])
|
||||
else do as <- args
|
||||
return (Compose [Con x as])
|
||||
|
||||
isVar [x] = True
|
||||
isVar [x,d] = isDigit d
|
||||
isVar _ = False
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue