diff --git a/Calculator.hs b/Calculator.hs new file mode 100644 index 0000000..b228664 --- /dev/null +++ b/Calculator.hs @@ -0,0 +1,22 @@ +module Calculator where + +import Utils +import Expr +import Parser + +data Law = Law LawName Equation + deriving Show + +type LawName = String +type Equation = (Expr,Expr) + +law :: Parser Law +law = do name <- upto ':' + eqn <- equation + return (Law name eqn) + +equation :: Parser Equation +equation = do lh <- expr + symbol "=" + rh <- expr + return (lh, rh) diff --git a/Expr.hs b/Expr.hs new file mode 100644 index 0000000..088055d --- /dev/null +++ b/Expr.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE LambdaCase #-} + +module Expr where + +import Data.Char +import Utils + +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 diff --git a/prover.hs b/Parser.hs similarity index 76% rename from prover.hs rename to Parser.hs index a0b3665..b021445 100644 --- a/prover.hs +++ b/Parser.hs @@ -1,5 +1,9 @@ {-# LANGUAGE LambdaCase #-} +module Parser where +import Expr +import Utils + import Data.Char ---------------- Parser declerations --------------------------- @@ -113,17 +117,19 @@ nat = do ds <- some digit return (foldl1 shiftl ds) where shiftl m n = 10*m+n +upto :: Char -> Parser String +upto c = P (\s -> let (xs, ys) = break (==c) s in + if null ys then [] + else [(xs, tail ys)]) + +-- TODO look into why this didn't work +-- upto x = do c <- (sat (/= x)) +-- cs <- upto x +-- return (c:cs) + ----------------- Calculator ----------------------------------- -newtype Expr = Compose [Atom] - deriving Eq -data Atom = Var VarName | Con ConName [Expr] - deriving Eq - -type VarName = String -type ConName = String - -- Main parsing {- @@ -145,9 +151,6 @@ 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)) @@ -174,36 +177,4 @@ 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 diff --git a/Utils.hs b/Utils.hs new file mode 100644 index 0000000..d62a525 --- /dev/null +++ b/Utils.hs @@ -0,0 +1,5 @@ +module Utils where + + +symbolic = (`elem` symbolic_ops) +symbolic_ops = "!@#$%^&*+./<=>?\\^|:-~"