Compare commits
2 commits
473d26ff0e
...
953c0d2298
Author | SHA1 | Date | |
---|---|---|---|
953c0d2298 | |||
549fecacfc |
1 changed files with 141 additions and 10 deletions
151
prover.hs
151
prover.hs
|
@ -30,7 +30,7 @@ instance Monad Parser where
|
||||||
-- (>>=) :: Parser a -> (a -> Parser b) -> Parser b
|
-- (>>=) :: Parser a -> (a -> Parser b) -> Parser b
|
||||||
p >>= f = P (\s -> case apply p s of
|
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
|
(<|>) :: Parser a -> Parser a -> Parser a
|
||||||
p <|> q = P (\s -> let ps = apply p s in
|
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)
|
else ps)
|
||||||
|
|
||||||
item :: Parser Char
|
item :: Parser Char
|
||||||
item = P (\case
|
item = P (\x -> case x of
|
||||||
[] -> []
|
[] -> []
|
||||||
(x:xs) -> [(x,xs)])
|
(x:xs) -> [(x,xs)])
|
||||||
|
|
||||||
|
@ -54,25 +54,156 @@ sat p = do x <- item
|
||||||
parse_fail :: Parser a
|
parse_fail :: Parser a
|
||||||
parse_fail = P (const [])
|
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 :: Parser [a] -> Parser [a]
|
||||||
optional = (<|> none)
|
optional = (<|> none)
|
||||||
|
|
||||||
many :: Parser a -> Parser [a]
|
spaces :: Parser [Char]
|
||||||
many = optional . some
|
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 -----------------------------------
|
----------------- Calculator -----------------------------------
|
||||||
|
|
||||||
newtype Expr = Compose [Atom] deriving Eq
|
newtype Expr = Compose [Atom]
|
||||||
|
deriving Eq
|
||||||
data Atom = Var VarName | Con ConName [Expr]
|
data Atom = Var VarName | Con ConName [Expr]
|
||||||
deriving Eq
|
deriving Eq
|
||||||
|
|
||||||
type VarName = String
|
type VarName = String
|
||||||
type ConName = String
|
type ConName = String
|
||||||
|
|
||||||
|
-- Main parsing
|
||||||
|
|
||||||
|
{-
|
||||||
|
Example:
|
||||||
|
map (f . g) . foo f g . (bar * bar)
|
||||||
|
|
||||||
|
-}
|
||||||
|
|
||||||
|
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))
|
||||||
|
|
||||||
|
deCompose :: Expr -> [Atom]
|
||||||
|
deCompose (Compose at) = at
|
||||||
|
|
||||||
|
term :: Parser Expr
|
||||||
|
term = ident args <|> paren expr
|
||||||
|
args = many (ident none <|> paren expr)
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
-- Showing
|
||||||
|
|
||||||
|
|
||||||
|
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
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue