summaryrefslogtreecommitdiff
path: root/Library/Command.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Library/Command.hs')
-rw-r--r--Library/Command.hs203
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)
-
-