summaryrefslogtreecommitdiff
path: root/Library
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2014-03-12 02:17:25 +1100
committerJed Barber <jjbarber@y7mail.com>2014-03-12 02:17:25 +1100
commitb5ff89d417c73d74a42a1756cb3ecd99b7a3e7f4 (patch)
tree97bf2d3ad4e5eac7aec320b932ccf09fdf127871 /Library
parentef81889c1eccb08acc27d47c9df652541134e3db (diff)
Removed some superfluous lambdas in intermediate functions
Diffstat (limited to 'Library')
-rw-r--r--Library/Object.hs4
-rw-r--r--Library/Parse.hs4
-rw-r--r--Library/ProofGraph.hs10
-rw-r--r--Library/Semantic.hs4
-rw-r--r--Library/Term.hs64
-rw-r--r--Library/TermNet.hs16
-rw-r--r--Library/Usage.hs11
-rw-r--r--Library/WriteProof.hs18
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