From 549fecacfc49e70cc1466201344bf9a298682c29 Mon Sep 17 00:00:00 2001 From: Pranshu Sharma Date: Sat, 17 May 2025 21:45:37 +1000 Subject: [PATCH 1/2] parser works good now --- prover.hs | 143 ++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 133 insertions(+), 10 deletions(-) diff --git a/prover.hs b/prover.hs index c469fea..12551c8 100644 --- a/prover.hs +++ b/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 From 953c0d2298683d65de8aa4e14cbb93f61ba80265 Mon Sep 17 00:00:00 2001 From: Pranshu Sharma Date: Mon, 19 May 2025 22:54:13 +1000 Subject: [PATCH 2/2] Massive: completed parser and show Now parse and show finally works properly. Now I have to do the laws, fun part. --- prover.hs | 100 +++++++++++++++++++++++++++++------------------------- 1 file changed, 54 insertions(+), 46 deletions(-) diff --git a/prover.hs b/prover.hs index 12551c8..a0b3665 100644 --- a/prover.hs +++ b/prover.hs @@ -124,11 +124,64 @@ data Atom = Var VarName | Con ConName [Expr] 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) + = showParen (p>0) (showSep " . " (showsPrec 1) as) compose :: [ShowS] -> ShowS compose = foldr (.) id @@ -154,48 +207,3 @@ 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