summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Concat.hs6
-rw-r--r--Delete.hs6
-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.hs10
-rw-r--r--MeaningSubst.hs10
-rw-r--r--ProofGraphMain.hs4
-rw-r--r--SemanticMain.hs4
-rw-r--r--Syntactic.hs2
-rw-r--r--Test.hs8
-rw-r--r--WriteProofMain.hs6
-rw-r--r--makefile42
23 files changed, 106 insertions, 80 deletions
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/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 )
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/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
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/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
+
+