hs-equational-calculator/prover.hs

{-# 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
                       [] -> []
                       [(v, out)] -> apply (f v) out)

(<|>) :: 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 (\x -> case x of
            []     -> []
            (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 [])


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)

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
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