From ea3f1f7736c57747e743a5106b917d2853c62f57 Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Thu, 13 Sep 2012 02:14:04 +1000 Subject: Cleaner directory structure, addition of make clean, grouping of library modules into a single package --- Command.hs | 203 ---------------------------- Concat.hs | 6 +- Delete.hs | 6 +- Generator.hs | 82 ------------ GraphPart.hs | 186 -------------------------- Library/Command.hs | 203 ++++++++++++++++++++++++++++ Library/Generator.hs | 82 ++++++++++++ Library/GraphPart.hs | 186 ++++++++++++++++++++++++++ Library/Object.hs | 128 ++++++++++++++++++ Library/Parse.hs | 77 +++++++++++ Library/ProofGraph.hs | 116 ++++++++++++++++ Library/Semantic.hs | 358 ++++++++++++++++++++++++++++++++++++++++++++++++++ Library/Stack.hs | 39 ++++++ Library/Term.hs | 193 +++++++++++++++++++++++++++ Library/TermNet.hs | 27 ++++ Library/Theorem.hs | 19 +++ Library/TypeVar.hs | 77 +++++++++++ Library/WriteProof.hs | 241 +++++++++++++++++++++++++++++++++ ListThm.hs | 10 +- MeaningSubst.hs | 10 +- Object.hs | 128 ------------------ Parse.hs | 77 ----------- ProofGraph.hs | 116 ---------------- ProofGraphMain.hs | 4 +- Semantic.hs | 358 -------------------------------------------------- SemanticMain.hs | 4 +- Stack.hs | 39 ------ Syntactic.hs | 2 +- Term.hs | 193 --------------------------- TermNet.hs | 27 ---- Test.hs | 8 +- Theorem.hs | 19 --- TypeVar.hs | 77 ----------- WriteProof.hs | 241 --------------------------------- WriteProofMain.hs | 6 +- makefile | 42 ++++-- 36 files changed, 1808 insertions(+), 1782 deletions(-) delete mode 100644 Command.hs delete mode 100644 Generator.hs delete mode 100644 GraphPart.hs create mode 100644 Library/Command.hs create mode 100644 Library/Generator.hs create mode 100644 Library/GraphPart.hs create mode 100644 Library/Object.hs create mode 100644 Library/Parse.hs create mode 100644 Library/ProofGraph.hs create mode 100644 Library/Semantic.hs create mode 100644 Library/Stack.hs create mode 100644 Library/Term.hs create mode 100644 Library/TermNet.hs create mode 100644 Library/Theorem.hs create mode 100644 Library/TypeVar.hs create mode 100644 Library/WriteProof.hs delete mode 100644 Object.hs delete mode 100644 Parse.hs delete mode 100644 ProofGraph.hs delete mode 100644 Semantic.hs delete mode 100644 Stack.hs delete mode 100644 Term.hs delete mode 100644 TermNet.hs delete mode 100644 Theorem.hs delete mode 100644 TypeVar.hs delete mode 100644 WriteProof.hs diff --git a/Command.hs b/Command.hs deleted file mode 100644 index fcece2e..0000000 --- a/Command.hs +++ /dev/null @@ -1,203 +0,0 @@ -module 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 TypeVar -import Term -import Theorem -import Object -import 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/Concat.hs b/Concat.hs index c10301a..18d0f5d 100644 --- a/Concat.hs +++ b/Concat.hs @@ -1,8 +1,8 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import ProofGraph -import WriteProof +import Library.Parse +import Library.ProofGraph +import Library.WriteProof diff --git a/Delete.hs b/Delete.hs index 58e29cc..3b9a1c7 100644 --- a/Delete.hs +++ b/Delete.hs @@ -1,8 +1,8 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import ProofGraph -import WriteProof +import Library.Parse +import Library.ProofGraph +import Library.WriteProof import qualified Data.Graph.Inductive.Graph as Graph diff --git a/Generator.hs b/Generator.hs deleted file mode 100644 index 7377ec1..0000000 --- a/Generator.hs +++ /dev/null @@ -1,82 +0,0 @@ -module Generator ( - listGen, - substitutionGen, - termGen, - varGen, - typeGen, - typeOpGen, - constGen, - nameGen - ) where - - -import Data.List -import Term -import 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/GraphPart.hs b/GraphPart.hs deleted file mode 100644 index bea4f72..0000000 --- a/GraphPart.hs +++ /dev/null @@ -1,186 +0,0 @@ -module GraphPart ( - graphPart, - makeGraphPart, - - nodes, - edges, - inputNode, - outputNode, - inputLab, - outputLab, - - graphAdd, - graphDel, - size, - addedSize, - overlap, - join, - - checkDupe, - nodeEquals, - resolveNodeClash - ) 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 - - -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 :: Gr String (Int,Int) -> 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) - - - -graphAdd :: GraphPart -> Maybe (Node,Int) -> Maybe (Node,Int) -> Gr String (Int,Int) -> Gr String (Int,Int) -graphAdd 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 (isNothing o || isNothing (getOutput gpart)) - then inputAdded - else Graph.insEdge (fst . fromJust $ o, - fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict), - (snd . fromJust $ o, snd . fromJust . getOutput $ gpart)) inputAdded - - graph' = outputAdded - - in checkDupe graph' - - - -graphDel :: GraphPart -> Gr String (Int,Int) -> Gr String (Int,Int) -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) -> Maybe (Node,Int) -> Gr String (Int,Int) -> 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 addedSize = Graph.noNodes (graphAdd one Nothing Nothing (getGraph two)) - totalSize = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two) - in totalSize - addedSize - - - -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) - - - -checkDupe :: Gr String (Int,Int) -> Gr String (Int,Int) -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) - diff --git a/Library/Command.hs b/Library/Command.hs new file mode 100644 index 0000000..47f0537 --- /dev/null +++ b/Library/Command.hs @@ -0,0 +1,203 @@ +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/Generator.hs b/Library/Generator.hs new file mode 100644 index 0000000..ef9dfe2 --- /dev/null +++ b/Library/Generator.hs @@ -0,0 +1,82 @@ +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 new file mode 100644 index 0000000..c63c2eb --- /dev/null +++ b/Library/GraphPart.hs @@ -0,0 +1,186 @@ +module Library.GraphPart ( + graphPart, + makeGraphPart, + + nodes, + edges, + inputNode, + outputNode, + inputLab, + outputLab, + + graphAdd, + graphDel, + size, + addedSize, + overlap, + join, + + checkDupe, + nodeEquals, + resolveNodeClash + ) 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 + + +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 :: Gr String (Int,Int) -> 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) + + + +graphAdd :: GraphPart -> Maybe (Node,Int) -> Maybe (Node,Int) -> Gr String (Int,Int) -> Gr String (Int,Int) +graphAdd 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 (isNothing o || isNothing (getOutput gpart)) + then inputAdded + else Graph.insEdge (fst . fromJust $ o, + fromJust (Map.lookup (fst . fromJust . getOutput $ gpart) dict), + (snd . fromJust $ o, snd . fromJust . getOutput $ gpart)) inputAdded + + graph' = outputAdded + + in checkDupe graph' + + + +graphDel :: GraphPart -> Gr String (Int,Int) -> Gr String (Int,Int) +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) -> Maybe (Node,Int) -> Gr String (Int,Int) -> 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 addedSize = Graph.noNodes (graphAdd one Nothing Nothing (getGraph two)) + totalSize = Graph.noNodes (getGraph one) + Graph.noNodes (getGraph two) + in totalSize - addedSize + + + +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) + + + +checkDupe :: Gr String (Int,Int) -> Gr String (Int,Int) +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) + diff --git a/Library/Object.hs b/Library/Object.hs new file mode 100644 index 0000000..9fc3b94 --- /dev/null +++ b/Library/Object.hs @@ -0,0 +1,128 @@ +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 new file mode 100644 index 0000000..0e2aa25 --- /dev/null +++ b/Library/Parse.hs @@ -0,0 +1,77 @@ +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 new file mode 100644 index 0000000..f4d956f --- /dev/null +++ b/Library/ProofGraph.hs @@ -0,0 +1,116 @@ +module Library.ProofGraph ( + PGraph, + doGraphGen + ) 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( 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 ) +import Library.GraphPart( checkDupe ) + + + +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) + + + +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 new file mode 100644 index 0000000..eac00a3 --- /dev/null +++ b/Library/Semantic.hs @@ -0,0 +1,358 @@ +module Library.Semantic ( + 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 new file mode 100644 index 0000000..7292869 --- /dev/null +++ b/Library/Stack.hs @@ -0,0 +1,39 @@ +module Library.Stack ( + Stack, + empty, + at, + pop, + (<:>) + ) where + + +import Data.List + + +data Stack a = Stack [a] + + +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) diff --git a/Library/Term.hs b/Library/Term.hs new file mode 100644 index 0000000..029af7e --- /dev/null +++ b/Library/Term.hs @@ -0,0 +1,193 @@ +module Library.Term ( + Term(..), + Substitution, + + alphaEquiv, + alphaConvert, + alphaConvertList, + substitute, + boundVars, + freeVars, + rename, + typeOf, + typeVarsInTerm, + mkEquals, + isEq, + getlhs, + getrhs + ) where + + + +import Data.List +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 a) = show a + 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) -> + type1 == type2 && + 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 a1, TVar a2) -> + a1 == a2 && Map.notMember a1 varmap1 && Map.notMember a2 varmap2 || + Map.lookup a1 varmap1 == Map.lookup a2 varmap2 + + (_,_) -> False + in equiv a b Map.empty Map.empty 0 + + +alphaConvert :: Term -> Term -> Term +alphaConvert (TConst a ty) (TConst _ _) = TConst a ty +alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) +alphaConvert (TVar v) (TVar _) = 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 (tymap,vmap) term = + let typesub = + (\x y -> + case y of + (TConst a ty) -> if (ty == (TypeVar . fst $ x)) + then TConst a (snd x) + else TConst a ty + (TApp a b) -> TApp (typesub x a) (typesub x b) + (TAbs (TVar (Var n ty)) a) -> if (ty == (TypeVar . fst $ x)) + then TAbs (TVar (Var n (snd x))) (typesub x a) + else TAbs (TVar (Var n ty)) (typesub x a) + (TVar (Var n ty)) -> if (ty == (TypeVar . fst $ x)) + then TVar (Var n (snd x)) + else TVar (Var n 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 (v == (fst x)) + then snd x + else TVar v + (TAbs v a) -> let safe = rename (TAbs v a) (Set.insert (fst x) (freeVars . snd $ x)) + in case safe of + (TAbs m n) -> TAbs m (varsub x n)) + tydone = foldl' (\x y -> typesub y x) term tymap + vdone = foldl' (\x y -> varsub y x) tydone vmap + in vdone + + +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 new file mode 100644 index 0000000..4d0b107 --- /dev/null +++ b/Library/TermNet.hs @@ -0,0 +1,27 @@ +module Library.TermNet( + TermNet, + empty, + addThm + ) where + + + +import Library.ProofGraph +import Library.Object +import Library.Theorem + + + +data TermNet = Empty | Leaf Object Node | Branch String [TermNet] + + + +empty :: TermNet +empty = Empty + + + +addThm :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)]) +addThm net graph node = + + diff --git a/Library/Theorem.hs b/Library/Theorem.hs new file mode 100644 index 0000000..fc66cc2 --- /dev/null +++ b/Library/Theorem.hs @@ -0,0 +1,19 @@ +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 new file mode 100644 index 0000000..fbb06a6 --- /dev/null +++ b/Library/TypeVar.hs @@ -0,0 +1,77 @@ +module Library.TypeVar ( + Number, + + Name(..), + + TypeOp(..), + + Type(..), + + Const(..), + + Var(..), + + mkEqualsType, + typeFunc, + typeBool, + typeVarsInType + ) where + + + +import Data.List +import qualified Data.Set as Set + + + +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) = "typeVar " ++ (show tyVar) + 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 diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs new file mode 100644 index 0000000..0f4f80f --- /dev/null +++ b/Library/WriteProof.hs @@ -0,0 +1,241 @@ +module Library.WriteProof ( + write, + writeAll, + doWriteProof, + singleCommands, + + ) 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.List +import Library.Stack( Stack, at, (<:>) ) +import qualified Library.Stack as Stack +import Library.Parse( isNumber, fst3, snd3, thd3 ) + + + +output :: Gr String (Int,Int) -> Node -> Int +output graph node = + let label = fromJust (Graph.lab graph node) + in case label of + "thm" -> 0 + "pop" -> 0 + "defineConst" -> 2 + "defineTypeOp" -> 5 + x -> 1 + + + +reuse :: Gr String (Int,Int) -> Node -> Int +reuse graph node = + let labels = map snd (Graph.lpre graph node) + f = (\x y -> length (filter (\z -> fst y == fst z) x)) + reuseList = map (f labels) labels + in maximum reuseList + + + +cost :: Gr String (Int,Int) -> Node -> Int +cost graph node = + length (subGraph graph node) + + + +next :: Int -> Gr String (Int,Int) -> [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 []) + + + +subGraph :: Gr a b -> Node -> [Node] +subGraph graph node = + let sucList = nub (Graph.suc graph node) + in nub (node : (foldl' (++) [] (map (subGraph graph) sucList))) + + + +orderNodes :: Gr String (Int,Int) -> [Node] -> [Node] +orderNodes graph nodeList = nodeList +--placeholder + + + +removeOverlap :: Gr String (Int,Int) -> Node -> [Node] -> [Node] +removeOverlap graph node list = + let nubFunc = (\x y -> (getArg graph node x) == (getArg graph node y)) + in nubBy nubFunc list + + + +--rightmostEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool +--rightmostEdge graph edge = + + + + +--crossEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool + + + +--multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +--multiCommands graph nodeList = +-- let trace = (\g n cn ca ->) +-- +-- r = (\g n p -> let g' = if ((output g n) <= 1) +-- then g +-- else let (argToUseDict, (place, placeArg)) = trace g n n 1 +-- edgesToRemove = +-- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove +-- defSubGraph = +-- edgesToRef = +-- new = +-- refsToAdd = +-- done = foldl' insertSubGraph edgesRemoved refsToAdd +-- in done +-- in f g' n) +-- +-- f = (\g n -> let argList = (removeOverlap g) . reverse $ [1 .. (Graph.outdeg g n)] +-- in foldl' (\x y -> r x (getArg x n y) n) g argList) +-- +-- in foldl' f graph nodeList + + + +multiCommandsSimple :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +multiCommandsSimple graph nodeList = + let r = (\g n p -> let g' = if ((output g n) <= 1) + then g + else let ou = output g n + index = next ou g + new = Graph.newNodes (5 * ou + 2) g -- 3 for num/def/pop, 2 for num/ref, per output plus an extra num/ref + (defNew,refNew) = splitAt (3 * ou + 2) new + + edgeCheck x y = compare (snd . thd3 $ x) (snd . thd3 $ y) + + oldEdge = maximumBy edgeCheck (filter (\x -> fst3 x == p) (Graph.inn g n)) + toConvert = delete oldEdge (Graph.inn g n) + + defNodeGen = (\i j x lim -> if (x >= lim) + then [] + else [(j!!(x*3), i!!x), (j!!(x*3+1), "def"), + (j!!(x*3+2), "pop")] ++ (defNodeGen i j (x+1) lim)) + defNodes = (defNodeGen index defNew 0 ou) ++ [(defNew!!(3*ou), index!!((snd . thd3 $ oldEdge)-1)), (defNew!!(3*ou+1), "ref")] + defEdgeGen = (\x b -> let x' = [(fst b, fst . snd $ x, (1,1))] ++ (fst x) + in (x',b)) + defEdges = [(p, (fst . last $ defNodes), thd3 oldEdge), ((fst . head $ defNodes), n, (1,1))] ++ + (fst (foldl' defEdgeGen ([], head defNodes) (tail defNodes))) + defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g + + refGen = (\i lab -> [(i!!(2*(lab-1)), index!!(lab-1)), (i!!(2*(lab-1)+1), "ref")]) + refNodes = map (refGen refNew) [1 .. (ou)] + refEdges = map (\[x,y] -> (fst y, fst x,(1,1))) refNodes + refAdded = (Graph.insEdges refEdges) . (Graph.insNodes (concat refNodes)) $ defAdded + + convertEdge = (\g e -> let new = (fst3 e, fst . last $ (refNodes!!(snd . thd3 $ e)), thd3 e) + in (Graph.insEdge new) . (Graph.delLEdge e) $ g) + + done = foldl' convertEdge refAdded toConvert + in done + in f g' n) + + f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)] + in foldl' (\x y -> r x (getArg x n y) n) g argList) + + in foldl' f graph nodeList + + + +singleCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +singleCommands graph nodeList = + let r = (\g n p -> let g' = if (((output g n) /= 1) || ((Graph.indeg g n) == 1) || ((cost g n) < 3) || ((cost g n) == 3 && (Graph.indeg g n) < 3)) + then g + else let index = head (next 1 g) + new = Graph.newNodes 4 g -- 2 new nodes for def and 2 new nodes for ref + + oldEdge = head $ (filter (\x -> fst3 x == p) (Graph.inn g n)) + defNodes = [(new!!0, "def"), (new!!1, index)] + defEdges = [(p, fst (defNodes!!0), (fst . thd3 $ oldEdge, 1)), + (fst (defNodes!!0), fst (defNodes!!1), (1,1)), + (fst (defNodes!!1), n, (1,1))] + defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g + + refNodes = [(new!!2, "ref"), (new!!3, index)] + refEdge = (fst (refNodes!!0), fst (refNodes!!1), (1,1)) + refAdded = (Graph.insEdge refEdge) . (Graph.insNodes refNodes) $ defAdded + convertEdge = (\g e -> let new = (fst3 e, fst (refNodes!!0), thd3 e) + in (Graph.insEdge new) . (Graph.delLEdge e) $ g) + done = foldl' convertEdge refAdded (filter (\x -> fst3 x /= fst (defNodes!!1)) (Graph.inn refAdded n)) + in done + in f g' n) + + f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)] + in foldl' (\x y -> r x (getArg x n y) n) g argList) + + in foldl' f graph nodeList + + + +removeUnused :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +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 :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +resolve graph nodeList = + foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommandsSimple] + + + +getArg :: Gr String (Int,Int) -> Node -> Int -> Node +getArg graph node arg = + snd3 . head $ (filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node)) + + + +writeGraph :: Gr String (Int,Int) -> Node -> [String] +writeGraph graph node = + let label = fromJust (Graph.lab graph node) + argList = [1 .. (Graph.outdeg graph node)] + in foldl' (\s a -> (writeGraph graph (getArg graph node a)) ++ s) [label] argList + + + +write :: Gr String (Int,Int) -> Node -> [String] +write graph node = + writeGraph (resolve graph [node]) node + + + +writeAll :: Gr String (Int,Int) -> [Node] -> [String] +writeAll graph nodeList = + let ordered = orderNodes graph nodeList + graph' = resolve graph ordered + f = (\g n -> if (n == []) + then [] + else (writeGraph g (head n)) ++ (f g (tail n))) + in f graph' ordered + + +-- metric relates to minimum amount of work done not-on-top of the stack + + +doWriteProof :: Gr String (Int,Int) -> [String] +doWriteProof graph = + let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) + in writeAll graph initList + diff --git a/ListThm.hs b/ListThm.hs index 3b179dd..540486d 100644 --- a/ListThm.hs +++ b/ListThm.hs @@ -1,10 +1,10 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import ProofGraph -import WriteProof -import Semantic -import Stack +import Library.Parse +import Library.ProofGraph +import Library.WriteProof +import Library.Semantic +import Library.Stack import Data.Maybe import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) diff --git a/MeaningSubst.hs b/MeaningSubst.hs index f52e2e0..f1c97eb 100644 --- a/MeaningSubst.hs +++ b/MeaningSubst.hs @@ -1,10 +1,10 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import ProofGraph -import GraphPart -import TermNet( TermNet ) -import qualified TermNet as TermNet +import Library.Parse +import Library.ProofGraph +import Library.GraphPart +import Library.TermNet( TermNet ) +import qualified Library.TermNet as TermNet import qualified Data.Graph.Inductive.Graph as Graph diff --git a/Object.hs b/Object.hs deleted file mode 100644 index 0fa1736..0000000 --- a/Object.hs +++ /dev/null @@ -1,128 +0,0 @@ -module Object ( - Object(..), - objNum, - objName, - objList, - objTyOp, - objType, - objConst, - objVar, - objTerm, - objThm, - - List, - - makeSubst - ) where - - - -import Data.Maybe -import Data.List -import TypeVar -import Term -import 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/Parse.hs b/Parse.hs deleted file mode 100644 index f8e6793..0000000 --- a/Parse.hs +++ /dev/null @@ -1,77 +0,0 @@ -module 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/ProofGraph.hs b/ProofGraph.hs deleted file mode 100644 index 96e82bd..0000000 --- a/ProofGraph.hs +++ /dev/null @@ -1,116 +0,0 @@ -module ProofGraph ( - PGraph, - doGraphGen - ) 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( LNode, LEdge, (&) ) -import qualified Data.Graph.Inductive.Graph as Graph -import Data.Graph.Inductive.Tree - -import Stack( Stack, at, (<:>) ) -import qualified Stack as Stack -import Parse( isNumber, isName ) -import GraphPart( checkDupe ) - - - -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) - - - -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/ProofGraphMain.hs b/ProofGraphMain.hs index 514dbc3..292cf01 100644 --- a/ProofGraphMain.hs +++ b/ProofGraphMain.hs @@ -1,7 +1,7 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import ProofGraph +import Library.Parse +import Library.ProofGraph main = do diff --git a/Semantic.hs b/Semantic.hs deleted file mode 100644 index 2390731..0000000 --- a/Semantic.hs +++ /dev/null @@ -1,358 +0,0 @@ -module Semantic ( - 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 TypeVar -import Term -import Theorem -import Object -import Parse -import Stack( Stack, at, (<:>) ) -import qualified Stack as Stack -import qualified 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/SemanticMain.hs b/SemanticMain.hs index 74c7c3b..c07fc8c 100644 --- a/SemanticMain.hs +++ b/SemanticMain.hs @@ -1,7 +1,7 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import Semantic +import Library.Parse +import Library.Semantic diff --git a/Stack.hs b/Stack.hs deleted file mode 100644 index 2b369b7..0000000 --- a/Stack.hs +++ /dev/null @@ -1,39 +0,0 @@ -module Stack ( - Stack, - empty, - at, - pop, - (<:>) - ) where - - -import Data.List - - -data Stack a = Stack [a] - - -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) diff --git a/Syntactic.hs b/Syntactic.hs index 6ce8561..870cc35 100644 --- a/Syntactic.hs +++ b/Syntactic.hs @@ -1,6 +1,6 @@ import System.Environment( getArgs ) import Text.Printf -import Parse +import Library.Parse diff --git a/Term.hs b/Term.hs deleted file mode 100644 index 8abdeb4..0000000 --- a/Term.hs +++ /dev/null @@ -1,193 +0,0 @@ -module Term ( - Term(..), - Substitution, - - alphaEquiv, - alphaConvert, - alphaConvertList, - substitute, - boundVars, - freeVars, - rename, - typeOf, - typeVarsInTerm, - mkEquals, - isEq, - getlhs, - getrhs - ) where - - - -import Data.List -import qualified Data.Set as Set -import qualified Data.Map as Map -import 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 a) = show a - 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) -> - type1 == type2 && - 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 a1, TVar a2) -> - a1 == a2 && Map.notMember a1 varmap1 && Map.notMember a2 varmap2 || - Map.lookup a1 varmap1 == Map.lookup a2 varmap2 - - (_,_) -> False - in equiv a b Map.empty Map.empty 0 - - -alphaConvert :: Term -> Term -> Term -alphaConvert (TConst a ty) (TConst _ _) = TConst a ty -alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) -alphaConvert (TVar v) (TVar _) = 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 (tymap,vmap) term = - let typesub = - (\x y -> - case y of - (TConst a ty) -> if (ty == (TypeVar . fst $ x)) - then TConst a (snd x) - else TConst a ty - (TApp a b) -> TApp (typesub x a) (typesub x b) - (TAbs (TVar (Var n ty)) a) -> if (ty == (TypeVar . fst $ x)) - then TAbs (TVar (Var n (snd x))) (typesub x a) - else TAbs (TVar (Var n ty)) (typesub x a) - (TVar (Var n ty)) -> if (ty == (TypeVar . fst $ x)) - then TVar (Var n (snd x)) - else TVar (Var n 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 (v == (fst x)) - then snd x - else TVar v - (TAbs v a) -> let safe = rename (TAbs v a) (Set.insert (fst x) (freeVars . snd $ x)) - in case safe of - (TAbs m n) -> TAbs m (varsub x n)) - tydone = foldl' (\x y -> typesub y x) term tymap - vdone = foldl' (\x y -> varsub y x) tydone vmap - in vdone - - -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/TermNet.hs b/TermNet.hs deleted file mode 100644 index fd21008..0000000 --- a/TermNet.hs +++ /dev/null @@ -1,27 +0,0 @@ -module TermNet( - TermNet, - empty, - addThm - ) where - - - -import ProofGraph -import Object -import Theorem - - - -data TermNet = Empty | Leaf Object Node | Branch String [TermNet] - - - -empty :: TermNet -empty = Empty - - - -addThm :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)]) -addThm net graph node = - - diff --git a/Test.hs b/Test.hs index f886dce..040bb87 100644 --- a/Test.hs +++ b/Test.hs @@ -1,8 +1,8 @@ import Test.HUnit -import Command -import TypeVar -import Term -import Theorem +import Library.Command +import Library.TypeVar +import Library.Term +import LibraryTheorem import qualified Data.Set as Set diff --git a/Theorem.hs b/Theorem.hs deleted file mode 100644 index c97a399..0000000 --- a/Theorem.hs +++ /dev/null @@ -1,19 +0,0 @@ -module Theorem ( - Theorem(..), - ) where - - - -import qualified Data.Set as Set -import TypeVar -import 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/TypeVar.hs b/TypeVar.hs deleted file mode 100644 index 436cde4..0000000 --- a/TypeVar.hs +++ /dev/null @@ -1,77 +0,0 @@ -module TypeVar ( - Number, - - Name(..), - - TypeOp(..), - - Type(..), - - Const(..), - - Var(..), - - mkEqualsType, - typeFunc, - typeBool, - typeVarsInType - ) where - - - -import Data.List -import qualified Data.Set as Set - - - -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) = "typeVar " ++ (show tyVar) - 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 diff --git a/WriteProof.hs b/WriteProof.hs deleted file mode 100644 index 2397de9..0000000 --- a/WriteProof.hs +++ /dev/null @@ -1,241 +0,0 @@ -module WriteProof ( - write, - writeAll, - doWriteProof, - singleCommands, - - ) 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.List -import Stack( Stack, at, (<:>) ) -import qualified Stack as Stack -import Parse( isNumber, fst3, snd3, thd3 ) - - - -output :: Gr String (Int,Int) -> Node -> Int -output graph node = - let label = fromJust (Graph.lab graph node) - in case label of - "thm" -> 0 - "pop" -> 0 - "defineConst" -> 2 - "defineTypeOp" -> 5 - x -> 1 - - - -reuse :: Gr String (Int,Int) -> Node -> Int -reuse graph node = - let labels = map snd (Graph.lpre graph node) - f = (\x y -> length (filter (\z -> fst y == fst z) x)) - reuseList = map (f labels) labels - in maximum reuseList - - - -cost :: Gr String (Int,Int) -> Node -> Int -cost graph node = - length (subGraph graph node) - - - -next :: Int -> Gr String (Int,Int) -> [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 []) - - - -subGraph :: Gr a b -> Node -> [Node] -subGraph graph node = - let sucList = nub (Graph.suc graph node) - in nub (node : (foldl' (++) [] (map (subGraph graph) sucList))) - - - -orderNodes :: Gr String (Int,Int) -> [Node] -> [Node] -orderNodes graph nodeList = nodeList ---placeholder - - - -removeOverlap :: Gr String (Int,Int) -> Node -> [Node] -> [Node] -removeOverlap graph node list = - let nubFunc = (\x y -> (getArg graph node x) == (getArg graph node y)) - in nubBy nubFunc list - - - ---rightmostEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool ---rightmostEdge graph edge = - - - - ---crossEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool - - - ---multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) ---multiCommands graph nodeList = --- let trace = (\g n cn ca ->) --- --- r = (\g n p -> let g' = if ((output g n) <= 1) --- then g --- else let (argToUseDict, (place, placeArg)) = trace g n n 1 --- edgesToRemove = --- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove --- defSubGraph = --- edgesToRef = --- new = --- refsToAdd = --- done = foldl' insertSubGraph edgesRemoved refsToAdd --- in done --- in f g' n) --- --- f = (\g n -> let argList = (removeOverlap g) . reverse $ [1 .. (Graph.outdeg g n)] --- in foldl' (\x y -> r x (getArg x n y) n) g argList) --- --- in foldl' f graph nodeList - - - -multiCommandsSimple :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) -multiCommandsSimple graph nodeList = - let r = (\g n p -> let g' = if ((output g n) <= 1) - then g - else let ou = output g n - index = next ou g - new = Graph.newNodes (5 * ou + 2) g -- 3 for num/def/pop, 2 for num/ref, per output plus an extra num/ref - (defNew,refNew) = splitAt (3 * ou + 2) new - - edgeCheck x y = compare (snd . thd3 $ x) (snd . thd3 $ y) - - oldEdge = maximumBy edgeCheck (filter (\x -> fst3 x == p) (Graph.inn g n)) - toConvert = delete oldEdge (Graph.inn g n) - - defNodeGen = (\i j x lim -> if (x >= lim) - then [] - else [(j!!(x*3), i!!x), (j!!(x*3+1), "def"), - (j!!(x*3+2), "pop")] ++ (defNodeGen i j (x+1) lim)) - defNodes = (defNodeGen index defNew 0 ou) ++ [(defNew!!(3*ou), index!!((snd . thd3 $ oldEdge)-1)), (defNew!!(3*ou+1), "ref")] - defEdgeGen = (\x b -> let x' = [(fst b, fst . snd $ x, (1,1))] ++ (fst x) - in (x',b)) - defEdges = [(p, (fst . last $ defNodes), thd3 oldEdge), ((fst . head $ defNodes), n, (1,1))] ++ - (fst (foldl' defEdgeGen ([], head defNodes) (tail defNodes))) - defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g - - refGen = (\i lab -> [(i!!(2*(lab-1)), index!!(lab-1)), (i!!(2*(lab-1)+1), "ref")]) - refNodes = map (refGen refNew) [1 .. (ou)] - refEdges = map (\[x,y] -> (fst y, fst x,(1,1))) refNodes - refAdded = (Graph.insEdges refEdges) . (Graph.insNodes (concat refNodes)) $ defAdded - - convertEdge = (\g e -> let new = (fst3 e, fst . last $ (refNodes!!(snd . thd3 $ e)), thd3 e) - in (Graph.insEdge new) . (Graph.delLEdge e) $ g) - - done = foldl' convertEdge refAdded toConvert - in done - in f g' n) - - f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)] - in foldl' (\x y -> r x (getArg x n y) n) g argList) - - in foldl' f graph nodeList - - - -singleCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) -singleCommands graph nodeList = - let r = (\g n p -> let g' = if (((output g n) /= 1) || ((Graph.indeg g n) == 1) || ((cost g n) < 3) || ((cost g n) == 3 && (Graph.indeg g n) < 3)) - then g - else let index = head (next 1 g) - new = Graph.newNodes 4 g -- 2 new nodes for def and 2 new nodes for ref - - oldEdge = head $ (filter (\x -> fst3 x == p) (Graph.inn g n)) - defNodes = [(new!!0, "def"), (new!!1, index)] - defEdges = [(p, fst (defNodes!!0), (fst . thd3 $ oldEdge, 1)), - (fst (defNodes!!0), fst (defNodes!!1), (1,1)), - (fst (defNodes!!1), n, (1,1))] - defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g - - refNodes = [(new!!2, "ref"), (new!!3, index)] - refEdge = (fst (refNodes!!0), fst (refNodes!!1), (1,1)) - refAdded = (Graph.insEdge refEdge) . (Graph.insNodes refNodes) $ defAdded - convertEdge = (\g e -> let new = (fst3 e, fst (refNodes!!0), thd3 e) - in (Graph.insEdge new) . (Graph.delLEdge e) $ g) - done = foldl' convertEdge refAdded (filter (\x -> fst3 x /= fst (defNodes!!1)) (Graph.inn refAdded n)) - in done - in f g' n) - - f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)] - in foldl' (\x y -> r x (getArg x n y) n) g argList) - - in foldl' f graph nodeList - - - -removeUnused :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) -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 :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) -resolve graph nodeList = - foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommandsSimple] - - - -getArg :: Gr String (Int,Int) -> Node -> Int -> Node -getArg graph node arg = - snd3 . head $ (filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node)) - - - -writeGraph :: Gr String (Int,Int) -> Node -> [String] -writeGraph graph node = - let label = fromJust (Graph.lab graph node) - argList = [1 .. (Graph.outdeg graph node)] - in foldl' (\s a -> (writeGraph graph (getArg graph node a)) ++ s) [label] argList - - - -write :: Gr String (Int,Int) -> Node -> [String] -write graph node = - writeGraph (resolve graph [node]) node - - - -writeAll :: Gr String (Int,Int) -> [Node] -> [String] -writeAll graph nodeList = - let ordered = orderNodes graph nodeList - graph' = resolve graph ordered - f = (\g n -> if (n == []) - then [] - else (writeGraph g (head n)) ++ (f g (tail n))) - in f graph' ordered - - --- metric relates to minimum amount of work done not-on-top of the stack - - -doWriteProof :: Gr String (Int,Int) -> [String] -doWriteProof graph = - let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph) - in writeAll graph initList - diff --git a/WriteProofMain.hs b/WriteProofMain.hs index 0e8d9c6..2f8625e 100644 --- a/WriteProofMain.hs +++ b/WriteProofMain.hs @@ -1,8 +1,8 @@ import System.Environment( getArgs ) import Text.Printf -import Parse -import ProofGraph -import WriteProof +import Library.Parse +import Library.ProofGraph +import Library.WriteProof diff --git a/makefile b/makefile index 524e0da..07ca71a 100644 --- a/makefile +++ b/makefile @@ -1,8 +1,34 @@ -all: - ghc --make ./SemanticMain.hs -o ./Semantic - ghc --make ./ProofGraphMain.hs -o ./ProofGraph - ghc --make ./WriteProofMain.hs -o ./WriteProof - ghc --make ./Delete.hs -o ./Delete - ghc --make ./Concat.hs -o ./Concat - ghc --make ./ListThm.hs -o ./ListThm - ghc --make ./Syntactic.hs -o ./Syntactic + +OUTPUTDIR = ./bin + + + +all: semantic syntactic proofgraph writeproof delete concat listthm + +clean: + find . -name '*.hi' -delete + find . -name '*.o' -delete + + +semantic: + ghc --make ./SemanticMain.hs -o ${OUTPUTDIR}/Semantic + +syntactic: + ghc --make ./Syntactic.hs -o ${OUTPUTDIR}/Syntactic + +proofgraph: + ghc --make ./ProofGraphMain.hs -o ${OUTPUTDIR}/ProofGraph + +writeproof: + ghc --make ./WriteProofMain.hs -o ${OUTPUTDIR}/WriteProof + +delete: + ghc --make ./Delete.hs -o ${OUTPUTDIR}/Delete + +concat: + ghc --make ./Concat.hs -o ${OUTPUTDIR}/Concat + +listthm: + ghc --make ./ListThm.hs -o ${OUTPUTDIR}/ListThm + + -- cgit