diff options
Diffstat (limited to 'src/Library/Command.hs')
| -rw-r--r-- | src/Library/Command.hs | 406 |
1 files changed, 203 insertions, 203 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)
+
+
|