Compare commits

..

2 commits

Author SHA1 Message Date
953c0d2298 Massive: completed parser and show
Now parse and show finally works properly.  Now I have to do the laws,
fun part.
2025-05-19 22:54:13 +10:00
549fecacfc parser works good now 2025-05-17 21:45:37 +10:00

151
prover.hs
View file

@ -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,156 @@ 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
-- 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