diff --git a/prover.hs b/prover.hs
index 12551c8..a0b3665 100644
--- a/prover.hs
+++ b/prover.hs
@@ -124,11 +124,64 @@ data Atom = Var VarName | Con ConName [Expr]
 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)
+    = showParen (p>0) (showSep " . " (showsPrec 1) as)
 
 compose :: [ShowS] -> ShowS
 compose = foldr (.) id
@@ -154,48 +207,3 @@ 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