summaryrefslogtreecommitdiff
path: root/Library
diff options
context:
space:
mode:
Diffstat (limited to 'Library')
-rw-r--r--Library/Command.hs203
-rw-r--r--Library/Cost.hs29
-rw-r--r--Library/Generator.hs82
-rw-r--r--Library/GraphPart.hs161
-rw-r--r--Library/Object.hs128
-rw-r--r--Library/Parse.hs75
-rw-r--r--Library/ProofGraph.hs159
-rw-r--r--Library/Semantic.hs360
-rw-r--r--Library/Stack.hs50
-rw-r--r--Library/Term.hs193
-rw-r--r--Library/TermNet.hs214
-rw-r--r--Library/Theorem.hs19
-rw-r--r--Library/TypeVar.hs99
-rw-r--r--Library/Usage.hs80
-rw-r--r--Library/WriteProof.hs211
-rw-r--r--Library/alternate_multi_command.hs315
16 files changed, 0 insertions, 2378 deletions
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
generated by cgit (git 2.30.0) at 2024-12-23 05:01:19 +0000