diff options
| -rw-r--r-- | Concat.hs | 6 | ||||
| -rw-r--r-- | Delete.hs | 6 | ||||
| -rw-r--r-- | Library/Command.hs (renamed from Command.hs) | 12 | ||||
| -rw-r--r-- | Library/Generator.hs (renamed from Generator.hs) | 6 | ||||
| -rw-r--r-- | Library/GraphPart.hs (renamed from GraphPart.hs) | 2 | ||||
| -rw-r--r-- | Library/Object.hs (renamed from Object.hs) | 8 | ||||
| -rw-r--r-- | Library/Parse.hs (renamed from Parse.hs) | 2 | ||||
| -rw-r--r-- | Library/ProofGraph.hs (renamed from ProofGraph.hs) | 10 | ||||
| -rw-r--r-- | Library/Semantic.hs (renamed from Semantic.hs) | 18 | ||||
| -rw-r--r-- | Library/Stack.hs (renamed from Stack.hs) | 2 | ||||
| -rw-r--r-- | Library/Term.hs (renamed from Term.hs) | 4 | ||||
| -rw-r--r-- | Library/TermNet.hs (renamed from TermNet.hs) | 8 | ||||
| -rw-r--r-- | Library/Theorem.hs (renamed from Theorem.hs) | 6 | ||||
| -rw-r--r-- | Library/TypeVar.hs (renamed from TypeVar.hs) | 2 | ||||
| -rw-r--r-- | Library/WriteProof.hs (renamed from WriteProof.hs) | 8 | ||||
| -rw-r--r-- | ListThm.hs | 10 | ||||
| -rw-r--r-- | MeaningSubst.hs | 10 | ||||
| -rw-r--r-- | ProofGraphMain.hs | 4 | ||||
| -rw-r--r-- | SemanticMain.hs | 4 | ||||
| -rw-r--r-- | Syntactic.hs | 2 | ||||
| -rw-r--r-- | Test.hs | 8 | ||||
| -rw-r--r-- | WriteProofMain.hs | 6 | ||||
| -rw-r--r-- | makefile | 42 |
23 files changed, 106 insertions, 80 deletions
@@ -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 @@ -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/Command.hs b/Library/Command.hs index fcece2e..47f0537 100644 --- a/Command.hs +++ b/Library/Command.hs @@ -1,4 +1,4 @@ -module Command ( +module Library.Command ( name, number, absTerm, @@ -35,11 +35,11 @@ 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 +import Library.TypeVar +import Library.Term +import Library.Theorem +import Library.Object +import Library.Parse name :: String -> Maybe Name diff --git a/Generator.hs b/Library/Generator.hs index 7377ec1..ef9dfe2 100644 --- a/Generator.hs +++ b/Library/Generator.hs @@ -1,4 +1,4 @@ -module Generator ( +module Library.Generator ( listGen, substitutionGen, termGen, @@ -11,8 +11,8 @@ module Generator ( import Data.List -import Term -import TypeVar +import Library.Term +import Library.TypeVar diff --git a/GraphPart.hs b/Library/GraphPart.hs index bea4f72..c63c2eb 100644 --- a/GraphPart.hs +++ b/Library/GraphPart.hs @@ -1,4 +1,4 @@ -module GraphPart ( +module Library.GraphPart ( graphPart, makeGraphPart, diff --git a/Object.hs b/Library/Object.hs index 0fa1736..9fc3b94 100644 --- a/Object.hs +++ b/Library/Object.hs @@ -1,4 +1,4 @@ -module Object ( +module Library.Object ( Object(..), objNum, objName, @@ -19,9 +19,9 @@ module Object ( import Data.Maybe import Data.List -import TypeVar -import Term -import Theorem +import Library.TypeVar +import Library.Term +import Library.Theorem diff --git a/Parse.hs b/Library/Parse.hs index f8e6793..0e2aa25 100644 --- a/Parse.hs +++ b/Library/Parse.hs @@ -1,4 +1,4 @@ -module Parse ( +module Library.Parse ( getLines, stripReturn, removeEscChars, diff --git a/ProofGraph.hs b/Library/ProofGraph.hs index 96e82bd..f4d956f 100644 --- a/ProofGraph.hs +++ b/Library/ProofGraph.hs @@ -1,4 +1,4 @@ -module ProofGraph ( +module Library.ProofGraph ( PGraph, doGraphGen ) where @@ -16,10 +16,10 @@ 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 ) +import Library.Stack( Stack, at, (<:>) ) +import qualified Library.Stack as Stack +import Library.Parse( isNumber, isName ) +import Library.GraphPart( checkDupe ) diff --git a/Semantic.hs b/Library/Semantic.hs index 2390731..eac00a3 100644 --- a/Semantic.hs +++ b/Library/Semantic.hs @@ -1,4 +1,4 @@ -module Semantic ( +module Library.Semantic ( eval, doSemanticCheck ) where @@ -11,14 +11,14 @@ 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 +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 diff --git a/Stack.hs b/Library/Stack.hs index 2b369b7..7292869 100644 --- a/Stack.hs +++ b/Library/Stack.hs @@ -1,4 +1,4 @@ -module Stack ( +module Library.Stack ( Stack, empty, at, diff --git a/Term.hs b/Library/Term.hs index 8abdeb4..029af7e 100644 --- a/Term.hs +++ b/Library/Term.hs @@ -1,4 +1,4 @@ -module Term ( +module Library.Term ( Term(..), Substitution, @@ -22,7 +22,7 @@ module Term ( import Data.List import qualified Data.Set as Set import qualified Data.Map as Map -import TypeVar +import Library.TypeVar diff --git a/TermNet.hs b/Library/TermNet.hs index fd21008..4d0b107 100644 --- a/TermNet.hs +++ b/Library/TermNet.hs @@ -1,4 +1,4 @@ -module TermNet( +module Library.TermNet( TermNet, empty, addThm @@ -6,9 +6,9 @@ module TermNet( -import ProofGraph -import Object -import Theorem +import Library.ProofGraph +import Library.Object +import Library.Theorem diff --git a/Theorem.hs b/Library/Theorem.hs index c97a399..fc66cc2 100644 --- a/Theorem.hs +++ b/Library/Theorem.hs @@ -1,12 +1,12 @@ -module Theorem ( +module Library.Theorem ( Theorem(..), ) where import qualified Data.Set as Set -import TypeVar -import Term +import Library.TypeVar +import Library.Term diff --git a/TypeVar.hs b/Library/TypeVar.hs index 436cde4..fbb06a6 100644 --- a/TypeVar.hs +++ b/Library/TypeVar.hs @@ -1,4 +1,4 @@ -module TypeVar ( +module Library.TypeVar ( Number, Name(..), diff --git a/WriteProof.hs b/Library/WriteProof.hs index 2397de9..0f4f80f 100644 --- a/WriteProof.hs +++ b/Library/WriteProof.hs @@ -1,4 +1,4 @@ -module WriteProof ( +module Library.WriteProof ( write, writeAll, doWriteProof, @@ -15,9 +15,9 @@ 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 ) +import Library.Stack( Stack, at, (<:>) ) +import qualified Library.Stack as Stack +import Library.Parse( isNumber, fst3, snd3, thd3 ) @@ -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/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/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/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 @@ -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/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 @@ -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 + + |