module 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 TypeVar import Term import Theorem import Object import 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)