From 03d38eb3190eb5e51fb18847fe0792013285bde5 Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Tue, 8 Apr 2014 15:06:40 +1000 Subject: Reorganising source code --- Library/Command.hs | 203 --------------------- Library/Cost.hs | 29 --- Library/Generator.hs | 82 --------- Library/GraphPart.hs | 161 ----------------- Library/Object.hs | 128 ------------- Library/Parse.hs | 75 -------- Library/ProofGraph.hs | 159 ---------------- Library/Semantic.hs | 360 ------------------------------------- Library/Stack.hs | 50 ------ Library/Term.hs | 193 -------------------- Library/TermNet.hs | 214 ---------------------- Library/Theorem.hs | 19 -- Library/TypeVar.hs | 99 ---------- Library/Usage.hs | 80 --------- Library/WriteProof.hs | 211 ---------------------- Library/alternate_multi_command.hs | 315 -------------------------------- 16 files changed, 2378 deletions(-) delete mode 100644 Library/Command.hs delete mode 100644 Library/Cost.hs delete mode 100644 Library/Generator.hs delete mode 100644 Library/GraphPart.hs delete mode 100644 Library/Object.hs delete mode 100644 Library/Parse.hs delete mode 100644 Library/ProofGraph.hs delete mode 100644 Library/Semantic.hs delete mode 100644 Library/Stack.hs delete mode 100644 Library/Term.hs delete mode 100644 Library/TermNet.hs delete mode 100644 Library/Theorem.hs delete mode 100644 Library/TypeVar.hs delete mode 100644 Library/Usage.hs delete mode 100644 Library/WriteProof.hs delete mode 100644 Library/alternate_multi_command.hs (limited to 'Library') diff --git a/Library/Command.hs b/Library/Command.hs deleted file mode 100644 index 47f0537..0000000 --- a/Library/Command.hs +++ /dev/null @@ -1,203 +0,0 @@ -module Library.Command ( - name, - number, - absTerm, - absThm, - appTerm, - appThm, - assume, - axiom, - betaConv, - constant, - constTerm, - deductAntisym, - defineConst, - defineTypeOp, - eqMp, - opType, - refl, - subst, - thm, - typeOp, - var, - varTerm, - varType - ) where - --- deliberately not included: --- cons, nil, def, ref, remove, pop - --- all functions here deal exclusively with arguments --- and results from/to the stack - -import Control.Monad -import Data.List -import Data.Maybe -import qualified Data.Set as Set -import qualified Data.Map as Map -import Library.TypeVar -import Library.Term -import Library.Theorem -import Library.Object -import Library.Parse - - -name :: String -> Maybe Name -name str = - do guard (isName str) - let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str - return (Name (init wordlist) (last wordlist)) - - -number :: String -> Maybe Number -number num = - do guard (isNumber num) - return (read num) - - -absTerm :: Term -> Var -> Term -absTerm term var = - TAbs (TVar var) term - - -absThm :: Theorem -> Var -> Maybe Theorem -absThm thm var = - do guard (not (Set.member (TVar var) (thmHyp thm))) - return (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm)) - (TAbs (TVar var) (getrhs . thmCon $ thm)))) - - -appTerm :: Term -> Term -> Term -appTerm term1 term2 = - TApp term2 term1 - - -appThm :: Theorem -> Theorem -> Theorem -appThm thm1 thm2 = - Theorem (Set.union (thmHyp thm1) (thmHyp thm2)) - (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1)) - (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1))) - - -assume :: Term -> Maybe Theorem -assume term = - do guard (typeOf term == typeBool) - return (Theorem (Set.singleton term) term) - - -axiom :: Term -> [Term] -> Maybe Theorem -axiom term termlist = - do guard (all ((== typeBool) . typeOf) termlist) - return (Theorem (Set.fromList termlist) term) - - -betaConv :: Term -> Theorem -betaConv term = - Theorem (Set.empty) - (mkEquals term - (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)]) - (tAbsTerm . tAppLeft $ term))) - - -constant :: Name -> Const -constant name = - Const name - - -constTerm :: Type -> Const -> Term -constTerm ty c = - TConst c ty - - -deductAntisym :: Theorem -> Theorem -> Theorem -deductAntisym x y = - Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y)) - (Set.delete (thmCon $ y) (thmHyp $ x))) - (mkEquals (thmCon $ y) (thmCon $ x)) - - -defineConst :: Term -> Name -> Maybe (Theorem, Const) -defineConst term name = - do guard ((freeVars term == Set.empty) && (typeVarsInTerm term == typeVarsInType (typeOf term))) - let constant = Const name - constTerm = TConst constant (typeOf term) - theorem = Theorem Set.empty (mkEquals constTerm term) - return (theorem, constant) - - -defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp) -defineTypeOp thm namelist r a n = - do guard ((typeVarsInTerm . tAppLeft . thmCon $ thm) == (Set.fromList . map (TypeVar) $ namelist) && - (length namelist) == (length . nub $ namelist)) - let rep = Const r - abst = Const a - op = TypeOp n - rtype = typeOf . tAppRight . thmCon $ thm - atype = AType (map (TypeVar) namelist) op - r' = TVar (Var (Name [] "r'") rtype) - a' = TVar (Var (Name [] "a'") atype) - reptype = typeFunc atype rtype - abstype = typeFunc rtype atype - repTerm = TConst rep reptype - absTerm = TConst abst abstype - rthm = Theorem Set.empty - (mkEquals (TApp (tAppLeft . thmCon $ thm) r') - (mkEquals (TApp repTerm (TApp absTerm r')) r')) - athm = Theorem Set.empty - (mkEquals (TApp absTerm (TApp repTerm a')) a') - return (rthm, athm, rep, abst, op) - - -eqMp :: Theorem -> Theorem -> Maybe Theorem -eqMp thm1 thm2 = - do guard (thmCon thm1 == (getlhs . thmCon $ thm2)) - return (Theorem (Set.union (thmHyp thm1) (thmHyp thm2)) - (getrhs . thmCon $ thm2)) - - -opType :: [Type] -> TypeOp -> Type -opType typelist tyOp = - AType typelist tyOp - - -refl :: Term -> Theorem -refl term = - Theorem Set.empty (mkEquals term term) - - -subst :: Theorem -> [Object] -> Maybe Theorem -subst thm list = - do s <- makeSubst list - return (Theorem (Set.map (substitute s) (thmHyp thm)) - (substitute s (thmCon thm))) - - -thm :: Term -> [Term] -> Theorem -> Maybe Theorem -thm term termlist oldthm = - do guard ((term == thmCon oldthm) && (Set.fromList termlist == thmHyp oldthm)) - return (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist)) - (alphaConvert (thmCon oldthm) term)) - - -typeOp :: Name -> TypeOp -typeOp name = - TypeOp name - - -var :: Type -> Name -> Maybe Var -var ty name = - do guard ((nameSpace name) == []) - return (Var name ty) - - -varTerm :: Var -> Term -varTerm var = - TVar var - - -varType :: Name -> Maybe Type -varType name = - do guard ((nameSpace name) == []) - return (TypeVar name) - - diff --git a/Library/Cost.hs b/Library/Cost.hs deleted file mode 100644 index 86cabdc..0000000 --- a/Library/Cost.hs +++ /dev/null @@ -1,29 +0,0 @@ -module Library.Cost( - cost, - nodeCost, - listCost - ) where - - - -import Data.Maybe -import Data.Graph.Inductive.Graph( Node ) -import qualified Data.Graph.Inductive.Graph as Graph -import Library.ProofGraph - - - -cost :: String -> Int -cost x = 1 - - -nodeCost :: PGraph -> Node -> Int -nodeCost graph node = - let label = fromJust (Graph.lab graph node) - nextCostLayer = map (nodeCost graph) (Graph.suc graph node) - in (cost label) + (sum nextCostLayer) - - -listCost :: [String] -> Int -listCost = sum . (map cost) - diff --git a/Library/Generator.hs b/Library/Generator.hs deleted file mode 100644 index ef9dfe2..0000000 --- a/Library/Generator.hs +++ /dev/null @@ -1,82 +0,0 @@ -module Library.Generator ( - listGen, - substitutionGen, - termGen, - varGen, - typeGen, - typeOpGen, - constGen, - nameGen - ) where - - -import Data.List -import Library.Term -import Library.TypeVar - - - -listGen :: (a -> [String]) -> [a] -> [String] -listGen f list = - concat (map f list) ++ ["nil"] ++ replicate (length list) "cons" - - - -substitutionGen :: Substitution -> [String] -substitutionGen sub = - let varTermList = listGen varTermPair (snd sub) - nameTypeList = listGen nameTypePair (fst sub) - in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"] - - - -varTermPair :: (Var, Term) -> [String] -varTermPair (var, term) = - (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"] - - - -nameTypePair :: (Name, Type) -> [String] -nameTypePair (name, ty) = - (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"] - - - -termGen :: Term -> [String] -termGen (TVar v) = (varGen v) ++ ["varTerm"] -termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"] -termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"] -termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"] - - - -varGen :: Var -> [String] -varGen var = - (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"] - - - -typeGen :: Type -> [String] -typeGen (TypeVar v) = (nameGen v) ++ ["varType"] -typeGen (AType ty op) = - let list = listGen typeGen ty - in (typeOpGen op) ++ list ++ ["opType"] - - - -typeOpGen :: TypeOp -> [String] -typeOpGen op = - (nameGen . tyOp $ op) ++ ["typeOp"] - - - -constGen :: Const -> [String] -constGen c = - (nameGen . constName $ c) ++ ["const"] - - - -nameGen :: Name -> [String] -nameGen name = - ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""] - diff --git a/Library/GraphPart.hs b/Library/GraphPart.hs deleted file mode 100644 index 02a95c0..0000000 --- a/Library/GraphPart.hs +++ /dev/null @@ -1,161 +0,0 @@ -module Library.GraphPart ( - GraphPart, - - graphPart, - makeGraphPart, - - nodes, - edges, - inputNode, - outputNode, - inputLab, - outputLab, - - graphAdd, - graphAddList, - graphDel, - size, - addedSize, - overlap, - join - ) where - - - -import Data.Maybe -import Data.List -import Data.Map( Map ) -import qualified Data.Map as Map -import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree -import Library.ProofGraph - - -data GraphPart = GraphPart { getGraph :: Gr String (Int,Int) - , getInput :: Maybe (Node,Int) - , getOutput :: Maybe (Node,Int) } - - -graphPart :: [LNode String] -> [LEdge (Int,Int)] -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart -graphPart nodes edges = - let graph = checkDupe (Graph.mkGraph nodes edges) - in GraphPart graph - - -makeGraphPart :: PGraph -> Maybe (Node,Int) -> Maybe (Node,Int) -> GraphPart -makeGraphPart = GraphPart - - -nodes :: GraphPart -> [LNode String] -nodes = Graph.labNodes . getGraph - - -edges :: GraphPart -> [LEdge (Int,Int)] -edges = Graph.labEdges . getGraph - - -inputNode :: GraphPart -> Maybe Node -inputNode gpart = do - input <- getInput gpart - return (fst input) - - -outputNode :: GraphPart -> Maybe Node -outputNode gpart = do - output <- getOutput gpart - return (fst output) - - -inputLab :: GraphPart -> Maybe Int -inputLab gpart = do - input <- getInput gpart - return (snd input) - - -outputLab :: GraphPart -> Maybe Int -outputLab gpart = do - output <- getOutput gpart - return (snd output) - - - -graphAddImp :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph -graphAddImp gpart i o graph = - let (resolved, dict) = resolveNodeClash graph (getGraph gpart) - base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) $ graph - - inputAdded = if (isNothing i || isNothing (getInput gpart)) - then base - else Graph.insEdge (fromJust (Map.lookup (fst . fromJust . getInput $ gpart) dict), - fst . fromJust $ i, - (snd . fromJust . getInput $ gpart, snd . fromJust $ i)) base - - outputAdded = if (o == [] || isNothing (getOutput gpart)) - then inputAdded - else let outEdge = map (\(x,y) -> (x, fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict), - (y, snd . fromJust . getOutput $ gpart))) o - in Graph.insEdges outEdge inputAdded - - graph' = outputAdded - in graph' - - - -graphAdd :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph -graphAdd gpart i o graph = - let graph' = graphAddImp gpart i o graph - in checkDupe graph' - - - -graphAddList :: [(GraphPart, Maybe (Node,Int), [(Node,Int)])] -> PGraph -> PGraph -graphAddList partList graph = - let graph' = foldl' (\g (x,y,z) -> graphAddImp x y z g) graph partList - in checkDupe graph' - - - -graphDel :: GraphPart -> PGraph -> PGraph -graphDel gpart graph = - let n = map fst . nodes $ gpart - e = map (\(a,b,_) -> (a,b)) . edges $ gpart - in (Graph.delNodes n) . (Graph.delEdges e) $ graph - - - -size :: GraphPart -> Int -size = Graph.noNodes . getGraph - - - -addedSize :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> Int -addedSize gpart i o graph = - let oldSize = Graph.noNodes graph - newSize = Graph.noNodes (graphAdd gpart i o graph) - in newSize - oldSize - - - -overlap :: GraphPart -> GraphPart -> Int -overlap one two = - let added = Graph.noNodes (graphAdd one Nothing [] (getGraph two)) - total = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two) - in total - added - - - -join :: GraphPart -> GraphPart -> GraphPart -join one two | (isJust (getOutput one) && isJust (getInput two)) = - let (resolved, dict) = resolveNodeClash (getGraph one) (getGraph two) - base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) . getGraph $ one - - from = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getInput $ two - to = fromJust . getOutput $ one - ioEdge = (fst from, fst to, (snd from, snd to)) - - newOutput = (\(x,y) -> (fromJust (Map.lookup x dict), y)) . fromJust . getOutput $ two - - in makeGraphPart (checkDupe (Graph.insEdge ioEdge base)) (getInput one) (Just newOutput) - - diff --git a/Library/Object.hs b/Library/Object.hs deleted file mode 100644 index dd65ded..0000000 --- a/Library/Object.hs +++ /dev/null @@ -1,128 +0,0 @@ -module Library.Object ( - Object(..), - objNum, - objName, - objList, - objTyOp, - objType, - objConst, - objVar, - objTerm, - objThm, - - List, - - makeSubst - ) where - - - -import Data.Maybe -import Data.List -import Library.TypeVar -import Library.Term -import Library.Theorem - - - -data Object = ObjNum Number - | ObjName Name - | ObjList List - | ObjTyOp TypeOp - | ObjType Type - | ObjConst Const - | ObjVar Var - | ObjTerm Term - | ObjThm Theorem deriving (Eq, Ord) - -type List = [Object] - - - -instance Show Object where - show (ObjNum a) = show a - show (ObjName a) = show a - show (ObjList a) = show a - show (ObjTyOp a) = show a - show (ObjType a) = show a - show (ObjConst a) = show a - show (ObjVar a) = show a - show (ObjTerm a) = show a - show (ObjThm a) = show a - - - -makeSubst :: [Object] -> Maybe Substitution -makeSubst l = - let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l - 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) - in if ((g . fst $ check) && (g . snd $ check)) - then Just (map h (fst check), map h (snd check)) - else Nothing - - -objNum :: Object -> Maybe Number -objNum obj = - case (obj) of - (ObjNum n) -> Just n - (_) -> Nothing - - -objName :: Object -> Maybe Name -objName obj = - case (obj) of - (ObjName n) -> Just n - (_) -> Nothing - - -objList :: Object -> Maybe List -objList obj = - case (obj) of - (ObjList l) -> Just l - (_) -> Nothing - - -objTyOp :: Object -> Maybe TypeOp -objTyOp obj = - case (obj) of - (ObjTyOp tyop) -> Just tyop - (_) -> Nothing - - -objType :: Object -> Maybe Type -objType obj = - case (obj) of - (ObjType ty) -> Just ty - (_) -> Nothing - - -objConst :: Object -> Maybe Const -objConst obj = - case (obj) of - (ObjConst c) -> Just c - (_) -> Nothing - - -objVar :: Object -> Maybe Var -objVar obj = - case (obj) of - (ObjVar var) -> Just var - (_) -> Nothing - - -objTerm :: Object -> Maybe Term -objTerm obj = - case (obj) of - (ObjTerm term) -> Just term - (_) -> Nothing - - -objThm :: Object -> Maybe Theorem -objThm obj = - case (obj) of - (ObjThm thm) -> Just thm - (_) -> Nothing - diff --git a/Library/Parse.hs b/Library/Parse.hs deleted file mode 100644 index 7494822..0000000 --- a/Library/Parse.hs +++ /dev/null @@ -1,75 +0,0 @@ -module Library.Parse ( - getLines, - stripReturn, - removeEscChars, - removeQuotes, - separateBy, - isComment, - isNumber, - isName, - output, - fst3, - snd3, - thd3 - ) where - -import Control.Monad( liftM ) -import qualified Data.Char as Char - - -getLines :: FilePath -> IO [String] -getLines = liftM lines . readFile - - -stripReturn :: String -> String -stripReturn s = if (last s == '\r') then init s else s - - -removeEscChars :: String -> String -removeEscChars [] = [] -removeEscChars (x:[]) = [x] -removeEscChars x = if (head x == '\\') - then (x!!1) : (removeEscChars . (drop 2) $ x) - else (head x) : (removeEscChars . tail $ x) - - -removeQuotes :: String -> String -removeQuotes = init . tail - - -separateBy :: Char -> String -> [String] -separateBy char list = - let f x = if (x == char) then ' ' else x - in words . (map f) $ list - - -isComment :: String -> Bool -isComment = (==) '#' . head - - -isNumber :: String -> Bool -isNumber ('0':[]) = True -isNumber ('-':ns) - | (ns /= [] && head ns /= '0') = isNumber ns -isNumber n = all (Char.isNumber) n - - -isName :: String -> Bool -isName s = all ((==) '"') [head s, last s] - - -output :: [String] -> IO () -output [] = return () -output list = do - putStrLn (head list) - output (tail list) - - -fst3 :: (a,b,c) -> a -fst3 (a,_,_) = a - -snd3 :: (a,b,c) -> b -snd3 (_,b,_) = b - -thd3 :: (a,b,c) -> c -thd3 (_,_,c) = c diff --git a/Library/ProofGraph.hs b/Library/ProofGraph.hs deleted file mode 100644 index 0e7e80a..0000000 --- a/Library/ProofGraph.hs +++ /dev/null @@ -1,159 +0,0 @@ -module Library.ProofGraph ( - PGraph, - doGraphGen, - - checkDupe, - nodeEquals, - resolveNodeClash, - - argMap - ) where - - - -import Data.Maybe -import Data.List -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.Map( Map, (!) ) -import qualified Data.Map as Map - -import Data.Graph.Inductive.Graph( Node, LNode, LEdge, (&) ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree - -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack -import Library.Parse( isNumber, isName ) - - - -type PGraph = Gr String (Int,Int) -type PStack = Stack (Int, LNode String) -type PMap = Map Int (Int, LNode String) - - -data CommandIO = IO { args :: Int - , results :: Int } - - -argMap :: String -> CommandIO -argMap "absTerm" = IO 2 1 -argMap "absThm" = IO 2 1 -argMap "appTerm" = IO 2 1 -argMap "appThm" = IO 2 1 -argMap "assume" = IO 1 1 -argMap "axiom" = IO 2 1 -argMap "betaConv" = IO 1 1 -argMap "cons" = IO 2 1 -argMap "const" = IO 1 1 -argMap "constTerm" = IO 2 1 -argMap "deductAntisym" = IO 2 1 -argMap "defineConst" = IO 2 2 -argMap "defineTypeOp" = IO 5 5 -argMap "eqMp" = IO 2 1 -argMap "nil" = IO 0 1 -argMap "opType" = IO 2 1 -argMap "refl" = IO 1 1 -argMap "subst" = IO 2 1 -argMap "thm" = IO 3 0 -argMap "typeOp" = IO 1 1 -argMap "var" = IO 2 1 -argMap "varTerm" = IO 1 1 -argMap "varType" = IO 1 1 -argMap x | (isName x) = IO 0 1 - - - -process :: String -> CommandIO -> PGraph -> PStack -> (PGraph, PStack) -process str io graph stack = - let argList = map (\x -> fromJust (stack `at` x)) [0..((args io) - 1)] - nextNum = head (Graph.newNodes 1 graph) - node = (nextNum, str) - edgeList = map (\x -> (nextNum, (fst . snd . snd $ x), (fst x, fst . snd $ x))) (zip [1..(args io)] argList) - graph' = (Graph.insEdges edgeList) . (Graph.insNode node) $ graph - nodeList = map (\x -> (x, node)) [1..(results io)] - stack' = foldr (<:>) (Stack.pop (args io) stack) nodeList - in (graph', stack') - - - -parse :: (PGraph,PStack,PMap) -> String -> (PGraph,PStack,PMap) -parse gs@(graph,stack,dictionary) str = - case str of - "def" -> let num = fst . fromJust $ stack `at` 0 - node = fromJust $ stack `at` 1 - dictionary' = Map.insert num node dictionary - stack' = Stack.pop 1 stack - in (graph, stack', dictionary') - - "ref" -> let num = fst . fromJust $ stack `at` 0 - node = fromJust (Map.lookup num dictionary) - stack' = node <:> (Stack.pop 1 stack) - in (graph, stack', dictionary) - - "remove" -> let num = fst . fromJust $ stack `at` 0 - node = fromJust (Map.lookup num dictionary) - stack' = node <:> (Stack.pop 1 stack) - dictionary' = Map.delete num dictionary - in (graph, stack', dictionary') - - "pop" -> (graph, (Stack.pop 1 stack), dictionary) - - '#':rest -> gs - - n | (isNumber n) -> let node = (read n, (0,"")) - stack' = node <:> stack - in (graph, stack', dictionary) - - x -> let (graph', stack') = process x (argMap x) graph stack - in (graph', stack', dictionary) - - - -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) - - 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 foldl' f graph (Graph.nodes graph) - - - -nodeEquals :: Gr String (Int,Int) -> Node -> Node -> Bool -nodeEquals graph one two = - let edgesOne = sortBy sortFunc (Graph.out graph one) - edgesTwo = sortBy sortFunc (Graph.out graph two) - sortFunc = (\(_,_,x) (_,_,y) -> compare x y) - paired = zip (map (\(_,x,_) -> x) edgesOne) (map (\(_,x,_) -> x) edgesTwo) - - in (Graph.gelem one graph) && - (Graph.gelem two graph) && - (Graph.lab graph one == Graph.lab graph two) && - (length edgesOne == length edgesTwo) && - (all (\x -> nodeEquals graph (fst x) (snd x)) paired) - - - -resolveNodeClash :: Gr String (Int,Int) -> Gr String (Int,Int) -> (Gr String (Int,Int), Map Int Int) -resolveNodeClash ref graph = - let dict = Map.fromList (zip (Graph.nodes graph) (Graph.newNodes (Graph.noNodes graph) ref)) - nodeList = map (\(x,y) -> (fromJust (Map.lookup x dict), y)) (Graph.labNodes graph) - edgeList = map (\(x,y,z) -> (fromJust (Map.lookup x dict), - fromJust (Map.lookup y dict), z)) (Graph.labEdges graph) - in (Graph.mkGraph nodeList edgeList, dict) - - - -doGraphGen :: [String] -> PGraph -doGraphGen list = - let graph = Graph.empty - stack = Stack.empty - dictionary = Map.empty - result = foldl' parse (graph,stack,dictionary) list - in case result of (g,s,d) -> checkDupe g - diff --git a/Library/Semantic.hs b/Library/Semantic.hs deleted file mode 100644 index 0f08d52..0000000 --- a/Library/Semantic.hs +++ /dev/null @@ -1,360 +0,0 @@ -module Library.Semantic ( - MachineState, - machineToString, - eval, - doSemanticCheck - ) where - - - -import Data.List -import Data.Maybe -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.Map( Map, (!) ) -import qualified Data.Map as Map -import Library.TypeVar -import Library.Term -import Library.Theorem -import Library.Object -import Library.Parse -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack -import qualified Library.Command as Com - - - -type MachineState = Maybe (Stack Object, - Map Int Object, --dictionary - Set Theorem, --assumptions - Set Theorem) --theorems - - -machineToString :: MachineState -> Maybe String -machineToString x = - do (s,d,a,t) <- x - let s' = show s - d' = "Dictionary:\n" ++ intercalate "\n" (map (show) (Map.toList d)) ++ "\n\n" - a' = "Assumptions:\n" ++ intercalate "\n" (map (show) (Set.toList a)) ++ "\n\n" - t' = "Theorems:\n" ++ intercalate "\n" (map (show) (Set.toList t)) ++ "\n\n" - return (s' ++ d' ++ a' ++ t') - - -data ArticleLine = Comment { commentString :: String } - | Command { commandFunc :: (MachineState -> MachineState) } - - - -parse :: String -> ArticleLine -parse "absTerm" = Command absTerm -parse "absThm" = Command absThm -parse "appTerm" = Command appTerm -parse "appThm" = Command appThm -parse "assume" = Command assume -parse "axiom" = Command axiom -parse "betaConv" = Command betaConv -parse "cons" = Command cons -parse "const" = Command constant -parse "constTerm" = Command constTerm -parse "deductAntisym" = Command deductAntisym -parse "def" = Command def -parse "defineConst" = Command defineConst -parse "defineTypeOp" = Command defineTypeOp -parse "eqMp" = Command eqMp -parse "nil" = Command nil -parse "opType" = Command opType -parse "pop" = Command pop -parse "ref" = Command ref -parse "refl" = Command refl -parse "remove" = Command remove -parse "subst" = Command subst -parse "thm" = Command thm -parse "typeOp" = Command typeOp -parse "var" = Command var -parse "varTerm" = Command varTerm -parse "varType" = Command varType -parse s@('#':rest) = Comment s -parse s@('"':rest) = Command (name s) -parse n = Command (number n) - - - -name :: String -> (MachineState -> MachineState) -name str x = - do (s,d,a,t) <- x - n <- Com.name str - let s' = (ObjName n) <:> s - return (s',d,a,t) - - -number :: String -> (MachineState -> MachineState) -number n x = - do (s,d,a,t) <- x - num <- Com.number n - let s' = (ObjNum num) <:> s - return (s',d,a,t) - - -absTerm :: MachineState -> MachineState -absTerm x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm; v <- (s `at` 1) >>= objVar - let term = Com.absTerm te v - s' = (ObjTerm term) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -absThm :: MachineState -> MachineState -absThm x = - do (s,d,a,t) <- x - th <- (s `at` 0) >>= objThm; v <- (s `at` 1) >>= objVar - thm <- Com.absThm th v - let s' = (ObjThm thm) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -appTerm :: MachineState -> MachineState -appTerm x = - do (s,d,a,t) <- x - f <- (s `at` 0) >>= objTerm; x <- (s `at` 1) >>= objTerm - let term = Com.appTerm f x - s' = (ObjTerm term) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -appThm :: MachineState -> MachineState -appThm x = - do (s,d,a,t) <- x - t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm - let thm = Com.appThm t1 t2 - s' = (ObjThm thm) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -assume :: MachineState -> MachineState -assume x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm - thm <- Com.assume te - let s' = (ObjThm thm) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -axiom :: MachineState -> MachineState -axiom x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList - thm <- Com.axiom te (mapMaybe objTerm l) - let s' = (ObjThm thm) <:> (Stack.pop 2 s) - a' = Set.insert thm a - return (s',d,a',t) - - -betaConv :: MachineState -> MachineState -betaConv x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm - let thm = Com.betaConv te - s' = (ObjThm thm) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -cons :: MachineState -> MachineState -cons x = - do (s,d,a,t) <- x - l <- (s `at` 0) >>= objList; h <- (s `at` 1) - let s' = (ObjList $ h : l) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -constant :: MachineState -> MachineState -constant x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objName - let constant = Com.constant n - s' = (ObjConst constant) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -constTerm :: MachineState -> MachineState -constTerm x = - do (s,d,a,t) <- x - ty <- (s `at` 0) >>= objType; c <- (s `at` 1) >>= objConst - let term = Com.constTerm ty c - s' = (ObjTerm term) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -deductAntisym :: MachineState -> MachineState -deductAntisym x = - do (s,d,a,t) <- x - t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm - let thm = Com.deductAntisym t1 t2 - s' = (ObjThm thm) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -def :: MachineState -> MachineState -def x = - do (s,d,a,t) <- x - num <- (s `at` 0) >>= objNum; obj <- (s `at` 1) - let d' = Map.insert num obj d - s' = Stack.pop 1 s - return (s',d',a,t) - - -defineConst :: MachineState -> MachineState -defineConst x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm; n <- (s `at` 1) >>= objName - (thm, constant) <- Com.defineConst te n - let s' = (ObjThm thm) <:> (ObjConst constant) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -defineTypeOp :: MachineState -> MachineState -defineTypeOp x = - do (s,d,a,t) <- x - th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList; r <- (s `at` 2) >>= objName - ab <- (s `at` 3) >>= objName; y <- (s `at` 4) >>= objName - (rthm, athm, rep, abst, n) <- Com.defineTypeOp th (mapMaybe objName l) r ab y - let s' = (ObjThm rthm) <:> (ObjThm athm) <:> (ObjConst rep) <:> (ObjConst abst) <:> (ObjTyOp n) <:> (Stack.pop 5 s) - return (s',d,a,t) - - -eqMp :: MachineState -> MachineState -eqMp x = - do (s,d,a,t) <- x - t1 <- (s `at` 0) >>= objThm; t2 <- (s `at` 1) >>= objThm - thm <- Com.eqMp t1 t2 - let s' = (ObjThm thm) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -nil :: MachineState -> MachineState -nil x = - do (s,d,a,t) <- x - return (ObjList [] <:> s, d, a, t) - - -opType :: MachineState -> MachineState -opType x = - do (s,d,a,t) <- x - l <- (s `at` 0) >>= objList; to <- (s `at` 1) >>= objTyOp - let newType = Com.opType (mapMaybe objType l) to - s' = (ObjType newType) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -pop :: MachineState -> MachineState -pop x = - do (s,d,a,t) <- x - return ((Stack.pop 1 s),d,a,t) - - -ref :: MachineState -> MachineState -ref x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objNum - let object = d ! n - s' = object <:> (Stack.pop 1 s) - return (s',d,a,t) - - -refl :: MachineState -> MachineState -refl x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm - let thm = Com.refl te - s' = (ObjThm thm) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -remove :: MachineState -> MachineState -remove x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objNum - let object = d ! n - s' = object <:> (Stack.pop 1 s) - d' = Map.delete n d - return (s',d',a,t) - - -subst :: MachineState -> MachineState -subst x = - do (s,d,a,t) <- x - th <- (s `at` 0) >>= objThm; l <- (s `at` 1) >>= objList - thm <- Com.subst th l - let s' = (ObjThm thm) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -thm :: MachineState -> MachineState -thm x = - do (s,d,a,t) <- x - te <- (s `at` 0) >>= objTerm; l <- (s `at` 1) >>= objList; th <- (s `at` 2) >>= objThm - thm <- Com.thm te (mapMaybe objTerm l) th - let s' = Stack.pop 3 s - t' = Set.insert thm t - return (s',d,a,t') - - -typeOp :: MachineState -> MachineState -typeOp x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objName - let typeOp = Com.typeOp n - s' = (ObjTyOp typeOp) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -var :: MachineState -> MachineState -var x = - do (s,d,a,t) <- x - ty <- (s `at` 0) >>= objType; n <- (s `at` 1) >>= objName - v <- Com.var ty n - let s' = (ObjVar v) <:> (Stack.pop 2 s) - return (s',d,a,t) - - -varTerm :: MachineState -> MachineState -varTerm x = - do (s,d,a,t) <- x - v <- (s `at` 0) >>= objVar - let term = Com.varTerm v - s' = (ObjTerm term) <:> (Stack.pop 1 s) - return (s',d,a,t) - - -varType :: MachineState -> MachineState -varType x = - do (s,d,a,t) <- x - n <- (s `at` 0) >>= objName - newType <- Com.varType n - let s' = (ObjType newType) <:> (Stack.pop 1 s) - return (s',d,a,t) - - - -eval :: [String] -> MachineState -eval list = - let s = Stack.empty - d = Map.empty - a = Set.empty - t = Set.empty - op = (\x y -> case y of (Comment _) -> x - (Command z) -> z x) - - -- important to use foldl here so commands get applied in the correct order - result = (foldl' (op) (Just (s,d,a,t))) . (map (parse)) $ list - - in result - - - -doSemanticCheck :: [String] -> String -doSemanticCheck list = - case (machineToString (eval list)) of - Just x -> x - Nothing -> "Error\n" - diff --git a/Library/Stack.hs b/Library/Stack.hs deleted file mode 100644 index 99cd8e1..0000000 --- a/Library/Stack.hs +++ /dev/null @@ -1,50 +0,0 @@ -module Library.Stack ( - Stack, - empty, - at, - pop, - (<:>), - size, - diff - ) where - - -import Data.List - - -data Stack a = Stack [a] deriving (Eq) - - -instance Show a => Show (Stack a) where - show (Stack x) = "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n" - - -infixr 9 <:> - - -empty :: Stack a -empty = Stack [] - - -at :: Stack a -> Int -> Maybe a -at (Stack list) index = - if (index < length list && index >= 0) - then Just (list!!index) - else Nothing - - -pop :: Int -> Stack a -> Stack a -pop n (Stack list) = Stack (drop n list) - - -(<:>) :: a -> Stack a -> Stack a -x <:> (Stack list) = Stack (x : list) - - -size :: Stack a -> Int -size (Stack list) = length list - - -diff :: (Eq a) => Stack a -> Stack a -> Stack a -diff (Stack one) (Stack two) = Stack (one \\ two) - diff --git a/Library/Term.hs b/Library/Term.hs deleted file mode 100644 index be9e53b..0000000 --- a/Library/Term.hs +++ /dev/null @@ -1,193 +0,0 @@ -module Library.Term ( - Term(..), - Substitution, - - alphaEquiv, - alphaConvert, - alphaConvertList, - substitute, - boundVars, - freeVars, - rename, - typeOf, - typeVarsInTerm, - mkEquals, - isEq, - getlhs, - getrhs - ) where - - - -import Data.List -import Data.Maybe -import qualified Data.Set as Set -import qualified Data.Map as Map -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) - -type Substitution = ( [(Name,Type)], [(Var,Term)] ) - - -instance Show Term where - show (TVar v) = (show v) - show (TConst a _) = (show a) - show (TApp (TApp eq lhs) rhs) - | isEq eq = "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")" - show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")" - show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")" - - -instance Eq Term where - a == b = a `alphaEquiv` b - - - -alphaEquiv :: Term -> Term -> Bool -alphaEquiv a b = - let equiv term1 term2 varmap1 varmap2 depth = - case (term1,term2) of - (TConst a1 b1, TConst a2 b2) -> - a1 == a2 && b1 == b2 - - (TApp a1 b1, TApp a2 b2) -> - equiv a1 a2 varmap1 varmap2 depth && - equiv b1 b2 varmap1 varmap2 depth - - (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) -> - equiv b1 b2 newmap1 newmap2 (depth+1) - where newmap1 = Map.insert (Var name1 type1) depth varmap1 - newmap2 = Map.insert (Var name2 type2) depth varmap2 - - (TVar (Var name1 type1), TVar (Var name2 type2)) -> - type1 == type2 && ((name1 == name2 && Map.notMember (Var name1 type1) varmap1 && Map.notMember (Var name2 type2) varmap2) || - Map.lookup (Var name1 type1) varmap1 == Map.lookup (Var name2 type2) varmap2) - - (_,_) -> False - - in equiv a b Map.empty Map.empty 0 - - -alphaConvert :: Term -> Term -> Term -alphaConvert (TConst _ _) (TConst a ty) = TConst a ty -alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) -alphaConvert (TVar _) (TVar v) = TVar v -alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b)) - - -alphaConvertList :: [Term] -> [Term] -> [Term] -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 = - 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)) - - varsub x y = - case y of - (TConst a ty) -> TConst a ty - (TApp a b) -> TApp (varsub x a) (varsub x b) - (TVar v) -> if (Map.member v x) - then fromJust (Map.lookup v x) - 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) - - 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 - - in (varsub vmap) . (typesub tymap) $ term - - -boundVars :: Term -> Set.Set Var -boundVars (TConst a b) = Set.empty -boundVars (TApp a b) = Set.union (boundVars a) (boundVars b) -boundVars (TVar a) = Set.empty -boundVars (TAbs a b) = Set.insert (tVar a) (boundVars b) - - -freeVars :: Term -> Set.Set Var -freeVars (TConst a b) = Set.empty -freeVars (TApp a b) = Set.union (freeVars a) (freeVars b) -freeVars (TVar a) = Set.singleton a -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 - - in if (Set.member v vars) - then doRename (TAbs (TVar v) t) v (findSafe v vars) - else TAbs (TVar v) t - - -typeOf :: Term -> Type -typeOf (TConst _ ty) = ty -typeOf (TVar v) = varTy v -typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t) -typeOf (TApp f _) = - -- type of f is of the form [[a,b], "->"] - last . aType . typeOf $ f - - -typeVarsInTerm :: Term -> Set.Set Type -typeVarsInTerm (TConst _ ty) = typeVarsInType ty -typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v -typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy . tVar $ v) (typeVarsInTerm t) -typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x) - - -mkEquals :: Term -> Term -> Term -mkEquals lhs rhs = - let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs)) - in TApp (TApp eqConst lhs) rhs - - -getlhs :: Term -> Term -getlhs (TApp (TApp eq lhs) _) - | (isEq eq) = lhs - - -getrhs :: Term -> Term -getrhs (TApp (TApp eq _) rhs) - | (isEq eq) = rhs - - -isEq :: Term -> Bool -isEq (TConst (Const (Name [] "=")) _) = True -isEq _ = False diff --git a/Library/TermNet.hs b/Library/TermNet.hs deleted file mode 100644 index 16b5446..0000000 --- a/Library/TermNet.hs +++ /dev/null @@ -1,214 +0,0 @@ -module Library.TermNet( - TermNet, - - empty, - getLeafList, - getBranchList, - - genThm, - termToTermString, - thmToTermString, - - addThm, - addThmFromNode, - matchThm - ) where - - - -import Data.Maybe -import Data.List -import qualified Data.Set as Set -import Data.Graph.Inductive.Graph( Node ) -import qualified Data.Graph.Inductive.Graph as Graph -import Library.ProofGraph -import Library.WriteProof -import Library.Object -import Library.Theorem -import Library.Term -import Library.Parse -import Library.Semantic -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack - - - -data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)] - deriving (Eq, Show) - - - -empty :: TermNet -empty = Branch [] - - - -isLeaf :: TermNet -> Bool -isLeaf (Leaf _) = True -isLeaf _ = False - - - -isBranch :: TermNet -> Bool -isBranch (Branch _) = True -isBranch _ = False - - - -getLeafList :: TermNet -> Maybe [(Theorem, Node)] -getLeafList net = - case net of - Leaf list -> Just list - Branch list -> Nothing - - - -getBranchList :: TermNet -> Maybe [(String, TermNet)] -getBranchList net = - case net of - Leaf list -> Nothing - Branch list -> Just list - - - -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) - - hypList = map (fromJust . objTerm) (fromJust . objList $ (gen graph node 2)) - con = fromJust . objTerm $ (gen graph node 1) - - in Theorem (Set.fromList hypList) con - - - -termToTermString :: Term -> [String] -termToTermString term = - case term of - (TConst _ _) -> - ["const"] - - (TApp func arg) -> - ["app"] ++ (termToTermString func) ++ (termToTermString arg) - - (TAbs var body) -> - ["abs", "var"] ++ (termToTermString body) - - (TVar var) -> - ["var"] - - - -thmToTermString :: Theorem -> [String] -thmToTermString theorem = - let hypList = Set.toList (thmHyp theorem) - f soFar hyp = soFar ++ ["hyp"] ++ (termToTermString hyp) - in (foldl' f [] hypList) ++ ["con"] ++ (termToTermString . thmCon $ theorem) - - - -addThm :: TermNet -> Theorem -> Node -> TermNet -addThm net theorem node = - addThmImp net (theorem,node) (thmToTermString theorem) - - - -addThmFromNode :: TermNet -> PGraph -> Node -> TermNet -addThmFromNode net graph node = - let theorem = genThm graph node - in addThmImp net (theorem,node) (thmToTermString theorem) - - - -addThmImp :: TermNet -> (Theorem,Node) -> [String] -> TermNet -addThmImp (Branch branchList) item (x:[]) = - let (sameKey, rest) = partition (\(y,z) -> y == x && isLeaf z) branchList - in if (sameKey == []) - then let leaf' = Leaf [item] - in Branch ((x,leaf'):rest) - else let leaf = snd . head $ sameKey - leafList = fromJust . getLeafList $ leaf - in if (item `elem` leafList) - then Branch branchList - else let leaf' = Leaf (item:leafList) - in Branch ((x,leaf'):rest) - -addThmImp (Branch branchList) item (x:xs) = - let (sameKey, rest) = partition (\(y,z) -> y == x) branchList - in if (sameKey == []) - then let net' = addThmImp empty item xs - in Branch ((x,net'):rest) - else let nextStepDown = snd . head $ sameKey - net' = addThmImp nextStepDown item xs - in Branch ((x,net'):rest) - - - -matchThm :: TermNet -> Theorem -> [(Theorem,Node)] -matchThm net theorem = - let hyp = Set.toList (thmHyp theorem) - con = thmCon theorem - (curPrefix, curTerm) = if (hyp == []) - then ("con", con) - else ("hyp", head hyp) - - r = do a <- matchImp curPrefix net - let b = matchTermImp curTerm a - (branches, leaves) = partition (\x -> isBranch x) b - - c <- if (hyp == []) - then getLeafList (foldl' unify (Leaf []) leaves) - else let theorem' = Theorem (Set.fromList (tail hyp)) con - in return (matchThm (foldl' unify empty branches) theorem') - return c - - in if (isNothing r) then [] else fromJust r - - - -matchImp :: String -> TermNet -> Maybe TermNet -matchImp key net = - do list <- getBranchList net - let result = filter (\(x,y) -> x == key) list - r <- if (result == []) then Nothing else Just (snd . head $ result) - return r - - - -matchTermImp :: Term -> TermNet -> [TermNet] -matchTermImp term net = - let list = getBranchList net - var = matchImp "var" net - result = - case term of - (TConst c ty) -> - do a <- matchImp "const" net - return [a] - - (TApp f x) -> - do a <- matchImp "app" net - let b = matchTermImp f a - return (concat (map (matchTermImp x) b)) - - (TAbs v x) -> - do a <- matchImp "abs" net - b <- matchImp "var" a - return (matchTermImp x b) - - (TVar v) -> Nothing --don't need to do anything because variables are already taken care of - - var' = if (isNothing var) then [] else [fromJust var] - result' = if (isNothing result) then [] else fromJust result - - in var' ++ result' - - - -unify :: TermNet -> TermNet -> TermNet -unify (Branch a) (Branch b) = Branch (a ++ b) -unify (Leaf a) (Leaf b) = Leaf (a ++ b) - diff --git a/Library/Theorem.hs b/Library/Theorem.hs deleted file mode 100644 index fc66cc2..0000000 --- a/Library/Theorem.hs +++ /dev/null @@ -1,19 +0,0 @@ -module Library.Theorem ( - Theorem(..), - ) where - - - -import qualified Data.Set as Set -import Library.TypeVar -import Library.Term - - - -data Theorem = Theorem { thmHyp :: Set.Set Term - , thmCon :: Term } deriving (Eq, Ord) - - - -instance Show Theorem where - show a = (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) diff --git a/Library/TypeVar.hs b/Library/TypeVar.hs deleted file mode 100644 index d2915e6..0000000 --- a/Library/TypeVar.hs +++ /dev/null @@ -1,99 +0,0 @@ -module Library.TypeVar ( - Number, - - Name(..), - - TypeOp(..), - - Type(..), - - Const(..), - - Var(..), - - mkEqualsType, - typeFunc, - typeBool, - typeVarsInType, - isTypeVar, - typeVarSub - ) where - - - -import Data.List -import Data.Maybe -import qualified Data.Set as Set -import Data.Map( Map, (!) ) -import qualified Data.Map as Map - - - -type Number = Int - -data Name = Name { nameSpace :: [String] - , nameId :: String } deriving (Eq, Ord) - -data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Ord) - -data Type = TypeVar { typeVar :: Name } - | AType { aType :: [Type] - , aTypeOp :: TypeOp } deriving (Eq, Ord) - -data Const = Const { constName :: Name } deriving (Eq, Ord) - -data Var = Var { varName :: Name - , varTy :: Type } deriving (Eq, Ord) - - - -instance Show Name where - show a = intercalate "." (nameSpace a ++ [nameId a]) - -instance Show TypeOp where - show a = "typeOp " ++ (show $ tyOp a) - -instance Show Type where - show (TypeVar tyVar) = "V " ++ (show tyVar) - show (AType [] (TypeOp (Name [] "bool"))) = "bool" - show (AType [d,r] (TypeOp (Name [] "->"))) = "(" ++ show d ++ " -> " ++ show r ++ ")" - show (AType list typeOp) = "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list) - -instance Show Const where - show (Const a) = show a - -instance Show Var where - show (Var a _) = show a - - - -mkEqualsType :: Type -> Type -mkEqualsType ty = typeFunc ty (typeFunc ty typeBool) - - -typeFunc :: Type -> Type -> Type -typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) - - -typeBool :: Type -typeBool = AType [] (TypeOp (Name [] "bool")) - - -typeVarsInType :: Type -> Set.Set Type -typeVarsInType (TypeVar t) = Set.singleton (TypeVar t) -typeVarsInType (AType list _) = Set.unions . (map typeVarsInType) $ list - - -isTypeVar :: Type -> Bool -isTypeVar (TypeVar _) = True -isTypeVar _ = False - - -typeVarSub :: Map Name Type -> Type -> Type -typeVarSub m (TypeVar a) = - if (Map.member a m) - then fromJust (Map.lookup a m) - else TypeVar a -typeVarSub m (AType list op) = - AType (map (typeVarSub m) list) op - diff --git a/Library/Usage.hs b/Library/Usage.hs deleted file mode 100644 index a307274..0000000 --- a/Library/Usage.hs +++ /dev/null @@ -1,80 +0,0 @@ -module Library.Usage( - UsageMap, - usageMap, - useSort, - nodeOutput, - getArg - ) where - - - -import Data.Map( Map ) -import qualified Data.Map as Map -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.List -import Data.Maybe -import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) -import qualified Data.Graph.Inductive.Graph as Graph -import Library.Parse -import Library.ProofGraph - - - -type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int])) - - --- Takes a graph, a starting list of nodes, a set of nodes of interest, and --- follows the starting nodes up the graph to find which edges the starting nodes --- 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 - - 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 - - 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 foldl' f Map.empty (zip3 [1..] order (repeat [])) - - - -useSort :: (LEdge a, (Int,[Int])) -> (LEdge a, (Int,[Int])) -> Ordering -useSort (_,(w,x)) (_,(y,z)) = - let check = compare w y - in if (check == EQ) - then compare (reverse x) (reverse z) - else check - - - -nodeOutput :: PGraph -> Node -> Int -nodeOutput graph node = - let label = fromJust (Graph.lab graph node) - in case label of - "thm" -> 0 - "pop" -> 0 - "defineConst" -> 2 - "defineTypeOp" -> 5 - x -> 1 - - - -getArg :: PGraph -> Node -> Int -> Maybe Node -getArg graph node arg = - let edge = filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node) - in if (edge == []) - then Nothing - else Just (snd3 . head $ edge) - diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs deleted file mode 100644 index 2c15b74..0000000 --- a/Library/WriteProof.hs +++ /dev/null @@ -1,211 +0,0 @@ -module Library.WriteProof ( - write, - writeAll, - doWriteProof, - singleCommands, - next, - genPart, - writeGraph - ) where - - - -import Data.Maybe -import Data.Graph.Inductive.Graph( LNode, LEdge, Node, Edge, (&) ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree -import Data.Map( Map, (!) ) -import qualified Data.Map as Map -import Data.Set( Set ) -import qualified Data.Set as Set -import Data.List -import Library.Stack( Stack, at, (<:>) ) -import qualified Library.Stack as Stack -import Library.Parse( isNumber, fst3, snd3, thd3 ) -import Library.Cost -import Library.ProofGraph -import Library.GraphPart -import Library.Usage - - - -orderNodes :: PGraph -> [Node] -> [Node] -orderNodes graph nodeList = nodeList ---placeholder - - - --- buggy -multiCommandsSimple :: PGraph -> UsageMap -> [Node] -> PGraph -multiCommandsSimple graph usemap nodeList = - let multiNodes = filter (\x -> nodeOutput graph x > 1 && x `notElem` nodeList) (Graph.nodes graph) - umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap - - f = (\gr node edgemap -> - let out = nodeOutput gr node - index = next out gr - - edgeList = Map.toList edgemap - edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) - - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edgeList - grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted - - defEdge = fst (minimumBy useSort edgeList) - removeEdges = map (fst . (maximumBy useSort)) grouped - refEdges = map (filter (\x -> x /= defEdge && x `notElem` removeEdges) . (map fst)) grouped - - usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeEdges)) [1..out] - - defGen = (\num -> - if (num > out) - then let reqEdges = filter (\x -> (snd . thd3 . fst $ x) == (snd . thd3 $ defEdge) && fst x /= defEdge) edgeList - refArg = (snd . thd3 $ defEdge) - 1 - in if (reqEdges == []) - then [index!!refArg, "ref"] --remove - else [index!!refArg, "ref"] - else if (num == (snd . thd3 $ defEdge) && num == out) - then if (filter (\x -> x /= defEdge && (snd . thd3 $ x) == num) (map fst edgeList) == []) - then [] - else [index!!(num-1), "def"] - else if (num `elem` usedArgs) - then [index!!(num-1), "def", "pop"] ++ defGen (num+1) - else ["pop"] ++ defGen (num+1)) - - defPart = (genPart (defGen 1) True, Just (node,1), [edgeToNode defEdge]) - - removeList = filter (\(x,y) -> y /= defEdge) (zip usedArgs removeEdges) - removeParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, [edgeToNode y])) removeList - - refList = filter (\(x,y) -> y /= []) (zip usedArgs refEdges) - refParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, map edgeToNode y)) refList - - partList = defPart:(removeParts ++ refParts) - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList - partsAdded = graphAddList partList edgesRemoved - in partsAdded) - - in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes - - - -singleCommands :: PGraph -> UsageMap -> [Node] -> PGraph -singleCommands graph usemap nodeList = - let singleNodes = filter (\x -> nodeOutput graph x == 1 && Graph.indeg graph x > 1) (Graph.nodes graph) - umap = Map.filterWithKey (\n _ -> n `elem` singleNodes) usemap - - s = (\gr node edgemap -> - let index = head (next 1 gr) - edgeList = Map.toList edgemap - - defEdge = fst (minimumBy useSort edgeList) - removeEdge = fst (maximumBy useSort edgeList) - refEdgeList = filter (\x -> x /= defEdge && x /= removeEdge) (map fst edgeList) - - defPart = genPart [index, "def"] True - refPart = genPart [index, "ref"] False - removePart = genPart [index, "ref"] False - - defNode = (fst3 defEdge, fst . thd3 $ defEdge) - removeNode = (fst3 removeEdge, fst . thd3 $ removeEdge) - refNodeList = map (\x -> (fst3 x, fst . thd3 $ x)) refEdgeList - - partList = [(defPart, Just (node, 1), [defNode]), (removePart, Nothing, [removeNode])] - partList' = if (refNodeList == []) then partList else (refPart, Nothing, refNodeList):partList - - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList - partsAdded = graphAddList partList' edgesRemoved - in partsAdded) - - f = (\gr node edgemap -> - let reuse = Graph.indeg graph node - costToStore = (nodeCost graph node) + (listCost ["def","0"]) + (reuse - 1) * (listCost ["ref","0"]) - costToIgnore = reuse * (nodeCost graph node) - in if (costToStore >= costToIgnore) - then gr - else s gr node edgemap) - - in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph singleNodes - - - -genPart :: [String] -> Bool -> GraphPart -genPart labels hasInput = - let nodeList = zip [1..] labels - edgeFunc = (\edges nodes -> - if (nodes == [] || (tail nodes) == []) - then edges - else let newEdge = (fst (nodes!!1), fst (nodes!!0), (1,1)) - in edgeFunc (newEdge:edges) (tail nodes)) - edgeList = edgeFunc [] nodeList - input = if (hasInput) then Just (1,1) else Nothing - output = Just (length labels, 1) - in graphPart nodeList edgeList input output - - - -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) - in map show (g num []) - - - -removeUnused :: PGraph -> [Node] -> PGraph -removeUnused graph nodeList = - let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph) - in if (unused == []) - then graph - else removeUnused (Graph.delNodes unused graph) nodeList - - - -resolve :: PGraph -> [Node] -> PGraph -resolve graph nodeList = - let liveGraph = removeUnused graph nodeList - umap = usageMap graph nodeList (Set.fromList (Graph.nodes liveGraph)) - singlesDone = singleCommands liveGraph umap nodeList - multisDone = multiCommandsSimple singlesDone umap nodeList - in multisDone - - - -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 - in foldl' f [label] argList - - - -write :: PGraph -> Node -> [String] -write graph node = - writeGraph (resolve graph [node]) node - - - -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)) - in f resolved ordered - - --- metric relates to minimum amount of work done not-on-top of the stack - - -doWriteProof :: PGraph -> [String] -doWriteProof graph = - let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) - in writeAll graph initList - diff --git a/Library/alternate_multi_command.hs b/Library/alternate_multi_command.hs deleted file mode 100644 index da49a7d..0000000 --- a/Library/alternate_multi_command.hs +++ /dev/null @@ -1,315 +0,0 @@ -multiCommands :: PGraph -> UsageMap -> [Node] -> PGraph -multiCommands graph usemap nodeList = - let multiNodes = filter (\x -> nodeOutput graph x > 1) (Graph.nodes graph) - umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap - - before = (\gr node edgemap arg indexList -> - let edges = filter (\x -> snd . thd3 . fst $ x < arg) edgemap - - -- sorts and groups by which output of the command each edge is using - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges - grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted - - -- makes a list of pairs of (maximum, restOfList) - maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped - - refNodeEdges = map (fst . snd) maxSplit - removeNodeEdges = concat (map (fst . fst) maxSplit) - - usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeNodeEdges)) [1..(arg-1)] - - -- creates a graphpart to define and pop all the initial outputs to get to the used one in the middle - defGen = (\num -> - if (num == arg) - then [] - else if (index!!num `elem` usedArgs) - then [index!!num, "def", "pop"] ++ defGen (num+1) - else ["pop"] ++ defGen (num+1)) - defPart = genPart (defGen 0) True - - -- creates graphparts for removing all the items stored in the dictionary, including node attachments - removeList = zip usedArgs removeNodeEdges - removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList - - -- creates graphparts to reference all the items stored in the dictionary, including node attachments - refList = zip usedArgs refNodeEdges - refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList - - in (defPart, refPart ++ removePart)) - - - after = (\gr node edgemap arg indexList -> - let -- obtain edges after the cutoff argument - edges = filter (\x -> snd . thd3 . fst $ x > arg) edgemap - - -- sort and group by which output of the command each edge is using - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges - grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted - - mins = map (minimumBy useSort) grouped - initEdge = minimumBy useSort (Map.toList edgemap) - - usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) mins)) [(arg+1)..(nodeOutput gr node)] - edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) - - -- finds the argument where you have to pop everything and store it all in the dictionary before - -- proceeding - findAttach = (\x y -> - if (x == []) - then nodeOutput gr node - else let allZero = all (=0) (snd . snd . head $ x) - headIsMin = (head x) == (minimumBy useSort x) - headThmLowestStrict = let testList = map (fst . snd) x - in all (> head testList) (tail testList) - nextUsedArg = snd . thd3 . fst . head . tail $ x - in if (allZero && headIsMin && headThmLowestStrict) - then findAttach (tail x) nextUsedArg - else y) - - argToAttach = findAttach initEdge:mins arg - - process = (\attach curArg modp ordp -> - case (compare arg argToAttach) of - LT -> - EQ -> - GT ->) - - (modParts, ordinaryParts) = process argToAttach arg [] [] - - -- calculate the def/pop/ref defPart - afterPartInit = - afterPart = - if (argToAttach == arg) - then - else - - -- calculate def nodes/parts for outputs before the argToAttach - defs = - makeDefList = - defPart = map (\(x,y) -> (genPart [index!!(x-1), "def"] False, Nothing, [edgeToNode y])) makeDefList - - -- calculate ref and remove nodes/parts - maxes = map (maximumBy useSort) grouped - refs = map (filter (\x -> x `notElem` maxes && x `notElem` defs)) grouped - - removeList = zip usedArgs maxes - removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList - - -- creates graphparts to reference all the items stored in the dictionary, including node attachments - refList = zip usedArgs refs - refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList - - in (modParts, ordinaryParts)) - - addPreserveNodeParts = (\partList graph -> - ) - - f = (\gr node edgemap -> - let edgeList = Map.toList edgemap - - out = nodeOutput gr node - index = next (out + 1) gr - - initEdge = fst (minimumBy useSort edgeList) - initArg = snd . thd3 $ initEdge - (defBefore, beforeParts) = before gr node edgemap initArg (take (initArg-1) index) - (defAfter, afterParts) = after gr node edgemap initArg (drop initArg index) - edgesToRemove = filter (\x -> x /= initEdge) (map fst edgeList) - - gr' = addPreserveNodeParts defAfter gr - - edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) gr' edgesToRemove - partsAdded = graphAddList partList edgesRemoved - in partsAdded) - - in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes - - - - - - - - - - - - - -multiCommands :: PGraph -> PGraph -> UsageMap -> [Node] -> PGraph -multiCommands graph orig usemap nodeList = - let process = (\gr stack dict workmap edge -> - let node = snd3 edge - label = fromJust (Graph.lab gr node) - in if (label == "def" || label == "ref" || label == "remove" || isNumber label) - then dictProcess gr stack dict workmap edge - else regProcess gr stack dict workmap edge - - - dictProcess = (\gr stack dict workmap edge -> - let node = snd3 edge - label = fromJust (Graph.lab gr node) - index = fromJust (Graph.lab gr (head (Graph.suc gr node))) - - in if (label == "def") - then let dict' = Map.insert index (head stack) dict - in (gr, stack, dict', workmap) - - else if (label == "ref") - then let stack' = (fromJust (Map.lookup index dict)):stack - in (gr, stack', dict, workmap) - - else if (label == "remove") - then let stack' = (fromJust (Map.lookup index dict)):stack - dict' = Map.delete index dict - in (gr, stack', dict', workmap) - else -- isNumber label - (gr, stack, dict, workmap) - - - regProcess = (\gr stack dict workmap edge -> - let node = snd3 edge - label = fromJust (Graph.lab gr node) - - io = argMap label - sortedIns = sortBy (\x y -> compare (fst . thd3 $ x) (fst . thd3 $ y)) (Graph.out orig node) - expectedInput = map (\(a,b,(c,d)) -> (b,d)) sortedIns - - consume = (\(g,s,d,w) inList -> - if (inList == []) - then if (nodeOutput == 1) - then (g, (node,1):s, d, w) - else initial (g,s,d,w) - else let i = head inList - in if (head s == i) - then consume (g, tail s, d, w) (tail inList) - else store (g, s, d, w) inList) - - initial = (\(g,s,d,w) inList -> - let edgemap = Map.toList (fromJust (Map.lookup node usemap)) - sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ b)) edgemap - grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted - minimals = map (minimumBy useSort) grouped - usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) minimals)) [1..nodeOutput] - atArg = snd . thd3 $ edge - atArgReuse = length (filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap) - fromStart = fst . snd $ (head (filter (\x -> ((snd . thd3 . fst $ x) == atArg)) minimals)) - edgesToRemove = filter (\x -> (snd . thd3 $ x) < upTo) (map fst edgemap) - - upTo = let shortList = filter (\x -> (snd . thd3 . fst $ x) > atArg && (fst . snd $ x) > fromStart) minimals - in if (shortList == []) - then nodeOutput + 1 - else let shortNum = snd . thd3 . fst . head $ shortList - calc = (\num -> - if (filter (\x -> (snd . thd3 . fst $ x) == num - 1) edgemap == []) - then calc (num - 1) - else num) - in calc shortNum - index = next upTo g - - defPartGen = (\num -> - if (num == upTo) - then if (atArg + 1 < upTo) - then if (atArgReuse > 1) - then [index!!atArg, "ref"] - else [index!!atArg, "remove"] - else [] - else if (num `elem` usedArgs) - then if (num + 1 == atArg &&) - else if (num == atArg) - then if (atArgReuse <= 1 && atArg + 1 == upTo) - then defPartGen (num+1) - else if (atArg + 1 < upTo) - then [index!!num, "def", "pop"] ++ (defPartGen (num+1)) - else [index!!num, "def"] ++ (defPartGen (num+1)) - else [index!!num, "def", "pop"] ++ (defPartGen (num+1)) - else ["pop"] ++ (defPartGen (num+1))) - defPart = genPart (defPartGen 1) True - - maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped - refNodeEdges = map (fst . snd) maxSplit - removeNodeEdges = concat (map (fst . fst) maxSplit) - - removeList = zip usedArgs removeNodeEdges - removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList - - refList = zip usedArgs refNodeEdges - refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refPart - - workingEdge = - let atArgEdges = filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap - initEdge = fst . head $ (filter (\x -> (snd . thd3 $ x) == atArg && - (x `notElem` (delete (minimumBy useSort atArgEdges) - atArgEdges))) (Graph.inn g' node)) - calc = (\e -> - if (fst3 e == fst3 edge) - then e - else calc (head (Graph.inn g' (fst3 e)))) - in calc initEdge - w' = Map.insert node workingEdge - - storedArgs = if (atArgReuse > 1 || atArg + 1 < upTo) - then filter (< upTo) usedArgs - else delete atArg (filter (< upTo) usedArgs) - dictAddList = map (\x -> (index!!(x-1), (node,x))) storedArgs - d' = foldl' (\x (y,z) -> Map.insert y z x) d dictAddList - - stackArgs = atArg:(filter (>= upTo) usedArgs) - stackAddList = map (\x -> (node,x)) stackArgs - s' = stackArgs ++ s - - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) g edgesToRemove - g' = graphAddList (defPart:(refPart ++ removePart)) edgesRemoved - - in (g', s', d', w')) - - - store = (\(g,s,d,w) inList -> - let s' = tail s - (node, arg) = head s -- the thing on the stack that shouldnt be there - workEdge = Map.lookup node w - (reqNode, reqArg) = head inList -- what we want on the stack instead - - index = head (next 1 g) - edgemap = Map.toList (Map.lookup node usemap) -- map of the edges leading into the node - edgesOfArg = filter (\(x,y) -> (snd . thd3 $ x) == arg) edgemap -- edges using the arg we want to get rid of - - removeEdge = maximumBy useSort edgesOfArg - refEdgeList = delete removeEdge edgesOfArg - - defPart = genPart [index, "def"] True - refPart = genPart [index, "ref"] False - removePart = genPart [index, "remove" False - popPart = genPart ["pop"] True - - in consume (g', s', d', w') inList - - in consume (gr,stack,dict,workmap) expectedInput) - - - h = (\gr st di ma edge -> - let node = snd3 edge - (gr',st',di',ma') = f gr st di ma node - in process gr' st' di' ma' edge) - - f = (\gr st di ma no -> - let args = reverse [1..(nodeOutput gr no)] - func = (\(g,s,d,m) a -> - let edge = filter (\x -> fst . thd3 $ x == a) (Graph.out g no) - in if (edge == []) - then (g,s,d,m) - else h gr st di ma (head edge) - in foldl' func (gr,st,di,ma) args - - stack = [] - dictionary = Map.empty - workmap = Map.empty - - (graph',stack',dictionary',workmap') = - foldl' (\(g,s,d,m) n -> f g s d m n) (graph, stack, dictionary, workmap) nodeList - - in graph' - - - - \ No newline at end of file -- cgit