Reorganising source code

1 files changed, 0 insertions, 203 deletions

diff --git a/Library/Command.hs b/Library/Command.hs
deleted file mode 100644
index 47f0537..0000000
--- a/Library/Command.hs
+++ /dev/null
@@ -1,203 +0,0 @@
-module Library.Command (
-	name,
-	number,
-	absTerm,
-	absThm,
-	appTerm,
-	appThm,
-	assume,
-	axiom,
-	betaConv,
-	constant,
-	constTerm,
-	deductAntisym,
-	defineConst,
-	defineTypeOp,
-	eqMp,
-	opType,
-	refl,
-	subst,
-	thm,
-	typeOp,
-	var,
-	varTerm,
-	varType
-    ) where
-
--- deliberately not included:
--- cons, nil, def, ref, remove, pop
-
--- all functions here deal exclusively with arguments
--- and results from/to the stack
-
-import Control.Monad
-import Data.List
-import Data.Maybe
-import qualified Data.Set as Set
-import qualified Data.Map as Map
-import Library.TypeVar
-import Library.Term
-import Library.Theorem
-import Library.Object
-import Library.Parse
-
-
-name :: String -> Maybe Name
-name str =
-	do guard (isName str)
-	   let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str
-	   return (Name (init wordlist) (last wordlist))
-
-
-number :: String -> Maybe Number
-number num =
-	do guard (isNumber num)
-	   return (read num)
-
-
-absTerm :: Term -> Var -> Term
-absTerm term var =
-	TAbs (TVar var) term
-
-
-absThm :: Theorem -> Var -> Maybe Theorem
-absThm thm var =
-	do guard (not (Set.member (TVar var) (thmHyp thm)))
-	   return (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm))
-	   	                                      (TAbs (TVar var) (getrhs . thmCon $ thm))))
-
-
-appTerm :: Term -> Term -> Term
-appTerm term1 term2 =
-	TApp term2 term1
-
-
-appThm :: Theorem -> Theorem -> Theorem
-appThm thm1 thm2 =
-	Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
-	        (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1))
-                      (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1)))
-
-
-assume :: Term -> Maybe Theorem
-assume term =
-	do guard (typeOf term == typeBool)
-	   return (Theorem (Set.singleton term) term)
-
-
-axiom :: Term -> [Term] -> Maybe Theorem
-axiom term termlist =
-	do guard (all ((== typeBool) . typeOf) termlist)
-	   return (Theorem (Set.fromList termlist) term)
-
-
-betaConv :: Term -> Theorem
-betaConv term =
-	Theorem (Set.empty)
-            (mkEquals term
-                      (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)])
-                                  (tAbsTerm . tAppLeft $ term)))
-
-
-constant :: Name -> Const
-constant name =
-	Const name
-
-
-constTerm :: Type -> Const -> Term
-constTerm ty c =
-	TConst c ty
-
-
-deductAntisym :: Theorem -> Theorem -> Theorem
-deductAntisym x y =
-	Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y))
-                       (Set.delete (thmCon $ y) (thmHyp $ x)))
-            (mkEquals (thmCon $ y) (thmCon $ x))
-
-
-defineConst :: Term -> Name -> Maybe (Theorem, Const)
-defineConst term name =
-	do guard ((freeVars term == Set.empty) && (typeVarsInTerm term == typeVarsInType (typeOf term)))
-	   let constant = Const name
-	       constTerm = TConst constant (typeOf term)
-	       theorem = Theorem Set.empty (mkEquals constTerm term)
-	   return (theorem, constant)
-
-
-defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp)
-defineTypeOp thm namelist r a n =
-	do guard ((typeVarsInTerm . tAppLeft . thmCon $ thm) == (Set.fromList . map (TypeVar) $ namelist) &&
-		      (length namelist) == (length . nub $ namelist))
-	   let rep = Const r
-	       abst = Const a
-	       op = TypeOp n
-	       rtype = typeOf . tAppRight . thmCon $ thm
-	       atype = AType (map (TypeVar) namelist) op
-	       r' = TVar (Var (Name [] "r'") rtype)
-	       a' = TVar (Var (Name [] "a'") atype)
-	       reptype = typeFunc atype rtype
-	       abstype = typeFunc rtype atype
-	       repTerm = TConst rep reptype
-	       absTerm = TConst abst abstype
-	       rthm = Theorem Set.empty
-	                      (mkEquals (TApp (tAppLeft . thmCon $ thm) r')
-	                      	        (mkEquals (TApp repTerm (TApp absTerm r')) r'))
-	       athm = Theorem Set.empty
-	                      (mkEquals (TApp absTerm (TApp repTerm a')) a')
-	   return (rthm, athm, rep, abst, op)
-
-
-eqMp :: Theorem -> Theorem -> Maybe Theorem
-eqMp thm1 thm2 =
-	do guard (thmCon thm1 == (getlhs . thmCon $ thm2))
-	   return (Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
-	   	               (getrhs . thmCon $ thm2))
-
-
-opType :: [Type] -> TypeOp -> Type
-opType typelist tyOp =
-	AType typelist tyOp
-
-
-refl :: Term -> Theorem
-refl term =
-	Theorem Set.empty (mkEquals term term)
-
-
-subst :: Theorem -> [Object] -> Maybe Theorem
-subst thm list =
-	do s <- makeSubst list
-	   return (Theorem (Set.map (substitute s) (thmHyp thm))
-                       (substitute s (thmCon thm)))
-
-
-thm :: Term -> [Term] -> Theorem -> Maybe Theorem
-thm term termlist oldthm =
-	do guard ((term == thmCon oldthm) && (Set.fromList termlist == thmHyp oldthm))
-	   return (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist))
-	   	               (alphaConvert (thmCon oldthm) term))
-
-
-typeOp :: Name -> TypeOp
-typeOp name =
-	TypeOp name
-
-
-var :: Type -> Name -> Maybe Var
-var ty name =
-    do guard ((nameSpace name) == [])
-       return (Var name ty)
-
-
-varTerm :: Var -> Term
-varTerm var =
-	TVar var
-
-
-varType :: Name -> Maybe Type
-varType name =
-    do guard ((nameSpace name) == [])
-       return (TypeVar name)
-
-