Removed some superfluous lambdas in intermediate functions

8 files changed, 66 insertions, 65 deletions

diff --git a/Library/Object.hs b/Library/Object.hs
index 9fc3b94..dd65ded 100644
--- a/Library/Object.hs
+++ b/Library/Object.hs
@@ -55,10 +55,10 @@ instance Show Object where
 makeSubst :: [Object] -> Maybe Substitution
 makeSubst l =
     let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l
-        f = (\g h x -> (g . head $ x, h . last $ x))
+        f g h x = (g . head $ x, h . last $ x)
         check = f (map (f objName objType)) (map (f objVar objTerm)) list
         g = all (\x -> (isJust . fst $ x) && (isJust . snd $ x))
-        h = (\x -> (fromJust . fst $ x, fromJust . snd $ x))
+        h x = (fromJust . fst $ x, fromJust . snd $ x)
     in if ((g . fst $ check) && (g . snd $ check))
        then Just (map h (fst check), map h (snd check))
        else Nothing
diff --git a/Library/Parse.hs b/Library/Parse.hs
index 0e2aa25..7494822 100644
--- a/Library/Parse.hs
+++ b/Library/Parse.hs
@@ -39,9 +39,7 @@ removeQuotes = init . tail
 
 separateBy :: Char -> String -> [String]
 separateBy char list =
-	let f = (\x -> if (x == char)
-		           then ' '
-		           else x)
+	let f x = if (x == char) then ' ' else x
 	in words . (map f) $ list
 
 
diff --git a/Library/ProofGraph.hs b/Library/ProofGraph.hs
index 217e40c..0e7e80a 100644
--- a/Library/ProofGraph.hs
+++ b/Library/ProofGraph.hs
@@ -113,14 +113,12 @@ parse gs@(graph,stack,dictionary) str =
 
 checkDupe :: PGraph -> PGraph
 checkDupe graph =
-    let f = (\g n ->
-                let list = filter (\x -> (x /= n) && (nodeEquals g n x)) (Graph.nodes g)
-                in if (list == []) then g else merge g n (head list))
+    let f g n = let list = filter (\x -> (x /= n) && (nodeEquals g n x)) (Graph.nodes g)
+                in if (list == []) then g else merge g n (head list)
 
-        merge = 
-            (\g n r ->
+        merge g n r = 
                 let edgesFixed = map (\(a,b,c) -> (a,r,c)) (Graph.inn g n)
-                in (Graph.insEdges edgesFixed) . (Graph.delNode n) $ g)
+                in (Graph.insEdges edgesFixed) . (Graph.delNode n) $ g
 
     in foldl' f graph (Graph.nodes graph)
 
diff --git a/Library/Semantic.hs b/Library/Semantic.hs
index e59069e..0f08d52 100644
--- a/Library/Semantic.hs
+++ b/Library/Semantic.hs
@@ -80,7 +80,7 @@ parse n = Command (number n)
 
 
 name :: String -> (MachineState -> MachineState)
-name str = \x ->
+name str x =
     do (s,d,a,t) <- x
        n <- Com.name str
        let s' = (ObjName n) <:> s
@@ -88,7 +88,7 @@ name str = \x ->
 
 
 number :: String -> (MachineState -> MachineState)
-number n = \x ->
+number n x =
     do (s,d,a,t) <- x
        num <- Com.number n
        let s' = (ObjNum num) <:> s
diff --git a/Library/Term.hs b/Library/Term.hs
index bac25a0..be9e53b 100644
--- a/Library/Term.hs
+++ b/Library/Term.hs
@@ -27,13 +27,13 @@ import Library.TypeVar
 
 
 
-data Term = TVar { tVar :: Var }
-          | TConst { tConst :: Const
-                   , tConstType :: Type }
-          | TApp { tAppLeft :: Term
-                 , tAppRight :: Term }
-          | TAbs { tAbsVar :: Term
-                 , tAbsTerm :: Term } deriving (Ord)
+data Term   = TVar { tVar :: Var }
+            | TConst { tConst :: Const
+                     , tConstType :: Type }
+            | TApp { tAppLeft :: Term
+                   , tAppRight :: Term }
+            | TAbs { tAbsVar :: Term
+                   , tAbsTerm :: Term } deriving (Ord)
 
 type Substitution = ( [(Name,Type)], [(Var,Term)] )
 
@@ -54,7 +54,7 @@ instance Eq Term where
 
 alphaEquiv :: Term -> Term -> Bool
 alphaEquiv a b =
-    let equiv = \term1 term2 varmap1 varmap2 depth ->
+    let equiv term1 term2 varmap1 varmap2 depth =
             case (term1,term2) of
                 (TConst a1 b1, TConst a2 b2) ->
                     a1 == a2 && b1 == b2
@@ -90,16 +90,14 @@ alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b)
 
 substitute :: Substitution -> Term -> Term
 substitute (t,v) term =
-    let typesub =
-            (\x y ->
+    let typesub x y =
                 case y of
                     (TConst a ty) -> TConst a (typeVarSub x ty)
                     (TApp a b) -> TApp (typesub x a) (typesub x b)
                     (TAbs (TVar (Var n ty)) a) -> TAbs (TVar (Var n (typeVarSub x ty))) (typesub x a)
-                    (TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty)))
+                    (TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty))
 
-        varsub =
-            (\x y ->
+        varsub x y =
                 case y of
                     (TConst a ty) -> TConst a ty
                     (TApp a b) -> TApp (varsub x a) (varsub x b)
@@ -108,7 +106,7 @@ substitute (t,v) term =
                                 else TVar v
                     (TAbs v a) -> let safe = rename (TAbs v a) (Set.union (Map.keysSet x) (Set.unions . (map freeVars) . (Map.elems) $ x))
                                   in case safe of
-                                         (TAbs m n) -> TAbs m (varsub x n)) 
+                                         (TAbs m n) -> TAbs m (varsub x n)
 
         tymap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty t
         vmap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty v
@@ -132,23 +130,27 @@ freeVars (TAbs a b) = Set.delete (tVar a) (freeVars b)
 
 rename :: Term -> Set.Set Var -> Term
 rename (TAbs (TVar v) t) vars =
-    let doRename =
-            (\x y z -> case x of
-                           (TAbs (TVar a) b) -> if (a == y)
-                                         then TAbs (TVar z) (doRename b y z)
-                                         else TAbs (TVar a) (doRename b y z)
-                           (TConst a b) -> TConst a b
-                           (TApp a b) -> TApp (doRename a y z) (doRename b y z)
-                           (TVar a) -> if (a == y)
-                                         then TVar z
-                                         else TVar a)
-        findSafe =
-            (\x y -> if (Set.member x y)
-                     then case x of
-                              (Var a b) ->
-                                  case a of
-                                      (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
-                     else x)
+    let doRename x y z =
+            case x of
+                (TAbs (TVar a) b) ->
+                    if (a == y)
+                    then TAbs (TVar z) (doRename b y z)
+                    else TAbs (TVar a) (doRename b y z)
+                (TConst a b) -> TConst a b
+                (TApp a b) -> TApp (doRename a y z) (doRename b y z)
+                (TVar a) ->
+                    if (a == y)
+                    then TVar z
+                    else TVar a
+
+        findSafe x y =
+            if (Set.member x y)
+            then case x of
+                    (Var a b) ->
+                        case a of
+                            (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
+            else x
+
     in if (Set.member v vars)
        then doRename (TAbs (TVar v) t) v (findSafe v vars)
        else TAbs (TVar v) t
diff --git a/Library/TermNet.hs b/Library/TermNet.hs
index 6d87aa9..16b5446 100644
--- a/Library/TermNet.hs
+++ b/Library/TermNet.hs
@@ -33,7 +33,8 @@ import qualified Library.Stack as Stack
 
 
 
-data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)] deriving (Eq, Show)
+data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)]
+    deriving (Eq, Show)
 
 
 
@@ -72,12 +73,15 @@ getBranchList net =
 
 genThm :: PGraph -> Node -> Theorem
 genThm graph node =
-    let gen = (\g n num -> let edge = filter (\x -> (fst . thd3 $ x) == num) (Graph.out g n)
-                               node = (snd3 . head $ edge)
-                               listing = write g node
-                           in fromJust (((\(a,_,_,_) -> a) . fromJust $ (eval listing)) `at` 0))
+    let gen g n num = 
+            let edge = filter (\x -> (fst . thd3 $ x) == num) (Graph.out g n)
+                node = (snd3 . head $ edge)
+                listing = write g node
+            in fromJust (((\(a,_,_,_) -> a) . fromJust $ (eval listing)) `at` 0)
+
         hypList = map (fromJust . objTerm) (fromJust . objList $ (gen graph node 2))
         con = fromJust . objTerm $ (gen graph node 1)
+
     in Theorem (Set.fromList hypList) con
 
 
@@ -102,7 +106,7 @@ termToTermString term =
 thmToTermString :: Theorem -> [String]
 thmToTermString theorem =
     let hypList = Set.toList (thmHyp theorem)
-        f = (\soFar hyp -> soFar ++ ["hyp"] ++ (termToTermString hyp))
+        f soFar hyp = soFar ++ ["hyp"] ++ (termToTermString hyp)
     in (foldl' f [] hypList) ++ ["con"] ++ (termToTermString . thmCon $ theorem)
 
 
diff --git a/Library/Usage.hs b/Library/Usage.hs
index 58fb0e0..a307274 100644
--- a/Library/Usage.hs
+++ b/Library/Usage.hs
@@ -29,23 +29,22 @@ type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int]))
 -- will encounter the nodes of interest through.
 usageMap :: PGraph -> [Node] -> Set Node -> UsageMap
 usageMap graph order interest =
-    let unionFunc = (\a b ->
-                Map.unionWith min a b)
+    let unionFunc a b = Map.unionWith min a b
 
-        addFunc = (\index prev umap edge ->
+        addFunc index prev umap edge =
                 let node = snd3 edge
                     curIn = Graph.outdeg graph (fst3 edge)
                     prev' = (curIn - (fst . thd3 $ edge)):prev
                     toAdd = Map.singleton node (Map.singleton edge (index,prev'))
                 in if (Set.member node interest)
                    then Map.unionWith unionFunc toAdd umap
-                   else umap)
+                   else umap
 
-        f = (\umap (index,node,prev) ->
+        f umap (index,node,prev) =
                 let edgeList = Graph.out graph node
                     sucMapList = map (f Map.empty) (map (\x -> (index, snd3 x, (length edgeList - (fst . thd3 $ x)):prev)) edgeList)
                     umap' = foldl' (addFunc index prev) umap edgeList
-                in Map.unionsWith unionFunc (umap':sucMapList))
+                in Map.unionsWith unionFunc (umap':sucMapList)
 
     in foldl' f Map.empty (zip3 [1..] order (repeat []))
 
diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs
index c7e0a5f..2c15b74 100644
--- a/Library/WriteProof.hs
+++ b/Library/WriteProof.hs
@@ -148,8 +148,8 @@ next :: Int -> PGraph -> [String]
 next num graph =
     let nodeList = filter (isNumber . snd) (Graph.labNodes graph)
         numList = nub . (map (read . snd)) $ nodeList
-        f = (\x y -> if (x `elem` y) then f (x + 1) y else x)
-        g = (\x y -> if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y))
+        f x y = if (x `elem` y) then f (x + 1) y else x
+        g x y = if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y)
     in map show (g num [])
 
 
@@ -177,10 +177,10 @@ writeGraph :: PGraph -> Node -> [String]
 writeGraph graph node =
     let label = fromJust (Graph.lab graph node)
         argList = [1 .. (Graph.outdeg graph node)]
-        f = (\s a -> let arg = getArg graph node a
-                     in if (isNothing arg)
-                        then s
-                        else (writeGraph graph (fromJust arg)) ++ s)
+        f s a = let arg = getArg graph node a
+                in if (isNothing arg)
+                    then s
+                    else (writeGraph graph (fromJust arg)) ++ s
     in foldl' f [label] argList
 
 
@@ -195,9 +195,9 @@ writeAll :: PGraph -> [Node] -> [String]
 writeAll graph nodeList =
     let ordered = orderNodes graph nodeList
         resolved = resolve graph ordered
-        f = (\g n -> if (n == [])
-                     then []
-                     else (writeGraph g (head n)) ++ (f g (tail n)))
+        f g n = if (n == [])
+                then []
+                else (writeGraph g (head n)) ++ (f g (tail n))
     in f resolved ordered