diff options
| -rw-r--r-- | Library/Object.hs | 4 | ||||
| -rw-r--r-- | Library/Parse.hs | 4 | ||||
| -rw-r--r-- | Library/ProofGraph.hs | 10 | ||||
| -rw-r--r-- | Library/Semantic.hs | 4 | ||||
| -rw-r--r-- | Library/Term.hs | 64 | ||||
| -rw-r--r-- | Library/TermNet.hs | 16 | ||||
| -rw-r--r-- | Library/Usage.hs | 11 | ||||
| -rw-r--r-- | Library/WriteProof.hs | 18 |
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 |