summaryrefslogtreecommitdiff
path: root/Command.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Command.hs')
-rw-r--r--Command.hs105
1 files changed, 47 insertions, 58 deletions
diff --git a/Command.hs b/Command.hs
index e6e0e39..fcece2e 100644
--- a/Command.hs
+++ b/Command.hs
@@ -30,6 +30,7 @@ module Command (
-- 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
@@ -43,18 +44,15 @@ import Parse
name :: String -> Maybe Name
name str =
- if (not . isName $ str)
- then Nothing
- else let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str
- name = Name (init wordlist) (last wordlist)
- in Just name
+ do guard (isName str)
+ let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str
+ return (Name (init wordlist) (last wordlist))
number :: String -> Maybe Number
number num =
- if (not . isNumber $ num)
- then Nothing
- else Just (read num)
+ do guard (isNumber num)
+ return (read num)
absTerm :: Term -> Var -> Term
@@ -64,10 +62,9 @@ absTerm term var =
absThm :: Theorem -> Var -> Maybe Theorem
absThm thm var =
- if (Set.member (TVar var) (thmHyp thm))
- then Nothing
- else Just (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm))
- (TAbs (TVar var) (getrhs . thmCon $ thm))))
+ 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
@@ -84,16 +81,14 @@ appThm thm1 thm2 =
assume :: Term -> Maybe Theorem
assume term =
- if (typeOf term /= typeBool)
- then Nothing
- else Just (Theorem (Set.singleton term) term)
+ do guard (typeOf term == typeBool)
+ return (Theorem (Set.singleton term) term)
axiom :: Term -> [Term] -> Maybe Theorem
axiom term termlist =
- if (not (all ((== typeBool) . typeOf) termlist))
- then Nothing
- else Just (Theorem (Set.fromList termlist) term)
+ do guard (all ((== typeBool) . typeOf) termlist)
+ return (Theorem (Set.fromList termlist) term)
betaConv :: Term -> Theorem
@@ -123,44 +118,41 @@ deductAntisym x y =
defineConst :: Term -> Name -> Maybe (Theorem, Const)
defineConst term name =
- if (freeVars term /= Set.empty || typeVarsInTerm term /= typeVarsInType (typeOf term))
- then Nothing
- else let constant = Const name
- constTerm = TConst constant (typeOf term)
- theorem = Theorem Set.empty (mkEquals constTerm term)
- in Just (theorem, constant)
+ 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 =
- if ((typeVarsInTerm . tAppLeft . thmCon $ thm) /= (Set.fromList . map (TypeVar) $ namelist) ||
- (length namelist) /= (length . nub $ namelist))
- then Nothing
- else 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')
- in Just (rthm, athm, rep, abst, op)
+ 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 =
- if (thmCon thm1 /= (getlhs . thmCon $ thm2))
- then Nothing
- else Just (Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
- (getrhs . thmCon $ thm2))
+ do guard (thmCon thm1 == (getlhs . thmCon $ thm2))
+ return (Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+ (getrhs . thmCon $ thm2))
opType :: [Type] -> TypeOp -> Type
@@ -182,10 +174,9 @@ subst thm list =
thm :: Term -> [Term] -> Theorem -> Maybe Theorem
thm term termlist oldthm =
- if ((term /= thmCon oldthm) || (Set.fromList termlist /= thmHyp oldthm))
- then Nothing
- else Just (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist))
- (alphaConvert (thmCon oldthm) term))
+ 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
@@ -195,9 +186,8 @@ typeOp name =
var :: Type -> Name -> Maybe Var
var ty name =
- if (nameSpace name /= [])
- then Nothing
- else Just (Var name ty)
+ do guard ((nameSpace name) == [])
+ return (Var name ty)
varTerm :: Var -> Term
@@ -207,8 +197,7 @@ varTerm var =
varType :: Name -> Maybe Type
varType name =
- if (nameSpace name /= [])
- then Nothing
- else Just (TypeVar name)
+ do guard ((nameSpace name) == [])
+ return (TypeVar name)