Old uncommitted changes

4 files changed, 354 insertions, 354 deletions

diff --git a/src/Library/Command.hs b/src/Library/Command.hs
index 47f0537..8451d74 100644
--- a/src/Library/Command.hs
+++ b/src/Library/Command.hs
@@ -1,203 +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)
-
-
+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/src/Library/Generator.hs b/src/Library/Generator.hs
index ef9dfe2..eca4b47 100644
--- a/src/Library/Generator.hs
+++ b/src/Library/Generator.hs
@@ -1,82 +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]) ++ "\""]
-
+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/src/Library/Stack.hs b/src/Library/Stack.hs
index 99cd8e1..dd675cc 100644
--- a/src/Library/Stack.hs
+++ b/src/Library/Stack.hs
@@ -1,50 +1,50 @@
-module Library.Stack (
-	Stack,
-    empty,
-    at,
-    pop,
-    (<:>),
-    size,
-    diff
-    ) where
-
-
-import Data.List
-
-
-data Stack a = Stack [a] deriving (Eq)
-
-
-instance Show a => Show (Stack a) where
-    show (Stack x)   =   "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n"
-
-
-infixr 9 <:>
-
-
-empty :: Stack a
-empty = Stack []
-
-
-at :: Stack a -> Int -> Maybe a
-at (Stack list) index =
-    if (index < length list && index >= 0)
-    then Just (list!!index)
-    else Nothing
-
-
-pop :: Int -> Stack a -> Stack a
-pop n (Stack list) = Stack (drop n list)
-
-
-(<:>) :: a -> Stack a -> Stack a
-x <:> (Stack list) = Stack (x : list)
-
-
-size :: Stack a -> Int
-size (Stack list) = length list
-
-
-diff :: (Eq a) => Stack a -> Stack a -> Stack a
-diff (Stack one) (Stack two) = Stack (one \\ two)
-
+module Library.Stack (

+	Stack,

+    empty,

+    at,

+    pop,

+    (<:>),

+    size,

+    diff

+    ) where

+

+

+import Data.List

+

+

+data Stack a = Stack [a] deriving (Eq)

+

+

+instance Show a => Show (Stack a) where

+    show (Stack x)   =   "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n"

+

+

+infixr 9 <:>

+

+

+empty :: Stack a

+empty = Stack []

+

+

+at :: Stack a -> Int -> Maybe a

+at (Stack list) index =

+    if (index < length list && index >= 0)

+    then Just (list!!index)

+    else Nothing

+

+

+pop :: Int -> Stack a -> Stack a

+pop n (Stack list) = Stack (drop n list)

+

+

+(<:>) :: a -> Stack a -> Stack a

+x <:> (Stack list) = Stack (x : list)

+

+

+size :: Stack a -> Int

+size (Stack list) = length list

+

+

+diff :: (Eq a) => Stack a -> Stack a -> Stack a

+diff (Stack one) (Stack two) = Stack (one \\ two)

+

diff --git a/src/Library/Theorem.hs b/src/Library/Theorem.hs
index fc66cc2..a976549 100644
--- a/src/Library/Theorem.hs
+++ b/src/Library/Theorem.hs
@@ -1,19 +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)
+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)