From 6d18e0c1fb6819557ab31bc332a323bc00a3c9ba Mon Sep 17 00:00:00 2001
From: Pranshu Sharma <pranshu@bauherren.ovh>
Date: Wed, 14 May 2025 23:27:45 +1000
Subject: [PATCH] Inital commit

---
 prover.hs | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 prover.hs

diff --git a/prover.hs b/prover.hs
new file mode 100644
index 0000000..c469fea
--- /dev/null
+++ b/prover.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE LambdaCase #-}
+
+import Data.Char
+
+---------------- Parser declerations ---------------------------
+
+
+newtype Parser a = P (String -> [(a,String)])
+
+apply :: Parser a -> String -> [(a,String)]
+apply (P p) = p
+
+instance Functor Parser where
+  -- fmap :: (a -> b) -> Parser a -> Parser b
+  fmap g p = P (\s -> case apply p s of
+                        []        -> []
+                        [(v,out)] -> [(g v, out)])
+
+
+instance Applicative Parser where
+  -- pure :: a -> Parser a
+  pure v = P (\inp -> [(v,inp)])
+
+  -- <*> :: Parser (a -> b) -> Parser a -> Parser b
+  pg <*> px = P (\inp -> case apply pg inp of
+                           []        -> []
+                           [(g,out)] -> apply (fmap g px) out)
+
+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)
+
+(<|>) :: Parser a -> Parser a -> Parser a
+p <|> q = P (\s -> let ps = apply p s in
+                     if null ps
+                       then apply q s
+                       else ps)
+
+item :: Parser Char
+item = P (\case
+            []     -> []
+            (x:xs) -> [(x,xs)])
+
+
+none :: Parser [a]
+none = return []
+
+sat :: (Char -> Bool) -> Parser Char
+sat p = do x <- item
+           if p x then return x else parse_fail
+
+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)))
+
+optional :: Parser [a] -> Parser [a]
+optional = (<|> none)
+
+many :: Parser a -> Parser [a]
+many = optional . some
+
+----------------- Calculator -----------------------------------
+
+newtype Expr = Compose [Atom] deriving Eq
+data Atom = Var VarName | Con ConName [Expr]
+  deriving Eq
+
+type VarName = String
+type ConName = String
+