From 549fecacfc49e70cc1466201344bf9a298682c29 Mon Sep 17 00:00:00 2001
From: Pranshu Sharma <pranshu@bauherren.ovh>
Date: Sat, 17 May 2025 21:45:37 +1000
Subject: [PATCH] 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