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
                        [] -> []
-                       [(v, out)] -> apply (f v) out)
+                       [(g, left)] -> apply (f g) left)
 
 (<|>) :: 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 (\x -> case x of
+item = P (\case
             []     -> []
             (x:xs) -> [(x,xs)])
 
@@ -54,156 +54,25 @@ 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)
 
-char :: Char -> Parser Char
+some p = p >>= (\x -> some p >>= (\xs -> return (x : xs)))
-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)
 
-spaces :: Parser [Char]
+many :: Parser a -> Parser [a]
-spaces = many (sat isSpace)
+many = optional . some
-
-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]
+newtype Expr = Compose [Atom] deriving Eq
-  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