From 5395287cc2f758d94bec8befe8956ba2dcc3940c Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Thu, 15 Dec 2016 14:28:31 +1100 Subject: Old uncommitted changes --- src/Library/Command.hs | 406 +++++++++++++++++++++++------------------------ src/Library/Generator.hs | 164 +++++++++---------- src/Library/Stack.hs | 100 ++++++------ src/Library/Theorem.hs | 38 ++--- src/Test/DataTypes.hs | 136 ++++++++-------- 5 files changed, 422 insertions(+), 422 deletions(-) (limited to 'src') 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) + + diff --git a/src/Library/Generator.hs b/src/Library/Generator.hs index ef9dfe2..eca4b47 100644 --- a/src/Library/Generator.hs +++ b/src/Library/Generator.hs @@ -1,82 +1,82 @@ -module Library.Generator ( - listGen, - substitutionGen, - termGen, - varGen, - typeGen, - typeOpGen, - constGen, - nameGen - ) where - - -import Data.List -import Library.Term -import Library.TypeVar - - - -listGen :: (a -> [String]) -> [a] -> [String] -listGen f list = - concat (map f list) ++ ["nil"] ++ replicate (length list) "cons" - - - -substitutionGen :: Substitution -> [String] -substitutionGen sub = - let varTermList = listGen varTermPair (snd sub) - nameTypeList = listGen nameTypePair (fst sub) - in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"] - - - -varTermPair :: (Var, Term) -> [String] -varTermPair (var, term) = - (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"] - - - -nameTypePair :: (Name, Type) -> [String] -nameTypePair (name, ty) = - (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"] - - - -termGen :: Term -> [String] -termGen (TVar v) = (varGen v) ++ ["varTerm"] -termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"] -termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"] -termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"] - - - -varGen :: Var -> [String] -varGen var = - (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"] - - - -typeGen :: Type -> [String] -typeGen (TypeVar v) = (nameGen v) ++ ["varType"] -typeGen (AType ty op) = - let list = listGen typeGen ty - in (typeOpGen op) ++ list ++ ["opType"] - - - -typeOpGen :: TypeOp -> [String] -typeOpGen op = - (nameGen . tyOp $ op) ++ ["typeOp"] - - - -constGen :: Const -> [String] -constGen c = - (nameGen . constName $ c) ++ ["const"] - - - -nameGen :: Name -> [String] -nameGen name = - ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""] - +module Library.Generator ( + listGen, + substitutionGen, + termGen, + varGen, + typeGen, + typeOpGen, + constGen, + nameGen + ) where + + +import Data.List +import Library.Term +import Library.TypeVar + + + +listGen :: (a -> [String]) -> [a] -> [String] +listGen f list = + concat (map f list) ++ ["nil"] ++ replicate (length list) "cons" + + + +substitutionGen :: Substitution -> [String] +substitutionGen sub = + let varTermList = listGen varTermPair (snd sub) + nameTypeList = listGen nameTypePair (fst sub) + in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"] + + + +varTermPair :: (Var, Term) -> [String] +varTermPair (var, term) = + (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"] + + + +nameTypePair :: (Name, Type) -> [String] +nameTypePair (name, ty) = + (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"] + + + +termGen :: Term -> [String] +termGen (TVar v) = (varGen v) ++ ["varTerm"] +termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"] +termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"] +termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"] + + + +varGen :: Var -> [String] +varGen var = + (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"] + + + +typeGen :: Type -> [String] +typeGen (TypeVar v) = (nameGen v) ++ ["varType"] +typeGen (AType ty op) = + let list = listGen typeGen ty + in (typeOpGen op) ++ list ++ ["opType"] + + + +typeOpGen :: TypeOp -> [String] +typeOpGen op = + (nameGen . tyOp $ op) ++ ["typeOp"] + + + +constGen :: Const -> [String] +constGen c = + (nameGen . constName $ c) ++ ["const"] + + + +nameGen :: Name -> [String] +nameGen name = + ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""] + diff --git a/src/Library/Stack.hs b/src/Library/Stack.hs index 99cd8e1..dd675cc 100644 --- a/src/Library/Stack.hs +++ b/src/Library/Stack.hs @@ -1,50 +1,50 @@ -module Library.Stack ( - Stack, - empty, - at, - pop, - (<:>), - size, - diff - ) where - - -import Data.List - - -data Stack a = Stack [a] deriving (Eq) - - -instance Show a => Show (Stack a) where - show (Stack x) = "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n" - - -infixr 9 <:> - - -empty :: Stack a -empty = Stack [] - - -at :: Stack a -> Int -> Maybe a -at (Stack list) index = - if (index < length list && index >= 0) - then Just (list!!index) - else Nothing - - -pop :: Int -> Stack a -> Stack a -pop n (Stack list) = Stack (drop n list) - - -(<:>) :: a -> Stack a -> Stack a -x <:> (Stack list) = Stack (x : list) - - -size :: Stack a -> Int -size (Stack list) = length list - - -diff :: (Eq a) => Stack a -> Stack a -> Stack a -diff (Stack one) (Stack two) = Stack (one \\ two) - +module Library.Stack ( + Stack, + empty, + at, + pop, + (<:>), + size, + diff + ) where + + +import Data.List + + +data Stack a = Stack [a] deriving (Eq) + + +instance Show a => Show (Stack a) where + show (Stack x) = "Stack:\n" ++ intercalate "\n" (map (show) x) ++ "\n\n" + + +infixr 9 <:> + + +empty :: Stack a +empty = Stack [] + + +at :: Stack a -> Int -> Maybe a +at (Stack list) index = + if (index < length list && index >= 0) + then Just (list!!index) + else Nothing + + +pop :: Int -> Stack a -> Stack a +pop n (Stack list) = Stack (drop n list) + + +(<:>) :: a -> Stack a -> Stack a +x <:> (Stack list) = Stack (x : list) + + +size :: Stack a -> Int +size (Stack list) = length list + + +diff :: (Eq a) => Stack a -> Stack a -> Stack a +diff (Stack one) (Stack two) = Stack (one \\ two) + diff --git a/src/Library/Theorem.hs b/src/Library/Theorem.hs index fc66cc2..a976549 100644 --- a/src/Library/Theorem.hs +++ b/src/Library/Theorem.hs @@ -1,19 +1,19 @@ -module Library.Theorem ( - Theorem(..), - ) where - - - -import qualified Data.Set as Set -import Library.TypeVar -import Library.Term - - - -data Theorem = Theorem { thmHyp :: Set.Set Term - , thmCon :: Term } deriving (Eq, Ord) - - - -instance Show Theorem where - show a = (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) +module Library.Theorem ( + Theorem(..), + ) where + + + +import qualified Data.Set as Set +import Library.TypeVar +import Library.Term + + + +data Theorem = Theorem { thmHyp :: Set.Set Term + , thmCon :: Term } deriving (Eq, Ord) + + + +instance Show Theorem where + show a = (show . Set.toList . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) diff --git a/src/Test/DataTypes.hs b/src/Test/DataTypes.hs index 28db135..76713fe 100644 --- a/src/Test/DataTypes.hs +++ b/src/Test/DataTypes.hs @@ -1,68 +1,68 @@ -module Test.DataTypes( - stdName, - stdType, - stdConst, - stdConstTerm, - stdTypeVarName, - altTypeVarName, - stdTypeVar, - altTypeVar, - stdVar, - stdVarTerm, - altVar, - altVarTerm, - stdAbsTerm, - stdAppTerm - ) where - - - -import Library.TypeVar -import Library.Term - - - -stdName :: String -> Name -stdName s = Name [] s - -stdType :: Type -stdType = AType [] (TypeOp (stdName "atype")) - -stdConst :: Const -stdConst = Const (stdName "const") - -stdConstTerm :: Term -stdConstTerm = TConst stdConst stdType - -stdTypeVarName :: Name -stdTypeVarName = stdName "typevar" - -altTypeVarName :: Name -altTypeVarName = stdName "alttypevar" - -stdTypeVar :: Type -stdTypeVar = TypeVar stdTypeVarName - -altTypeVar :: Type -altTypeVar = TypeVar altTypeVarName - -stdVar :: String -> Var -stdVar s = Var (stdName s) stdTypeVar - -stdVarTerm :: String -> Term -stdVarTerm s = TVar (stdVar s) - -altVar :: String -> Var -altVar s = Var (stdName s) altTypeVar - -altVarTerm :: String -> Term -altVarTerm s = TVar (altVar s) - -stdAbsTerm :: String -> Term -stdAbsTerm s = TAbs (stdVarTerm s) stdConstTerm - -stdAppTerm :: String -> Term -stdAppTerm s = TApp (stdAbsTerm s) stdConstTerm - - - +module Test.DataTypes( + stdName, + stdType, + stdConst, + stdConstTerm, + stdTypeVarName, + altTypeVarName, + stdTypeVar, + altTypeVar, + stdVar, + stdVarTerm, + altVar, + altVarTerm, + stdAbsTerm, + stdAppTerm + ) where + + + +import Library.TypeVar +import Library.Term + + + +stdName :: String -> Name +stdName s = Name [] s + +stdType :: Type +stdType = AType [] (TypeOp (stdName "atype")) + +stdConst :: Const +stdConst = Const (stdName "const") + +stdConstTerm :: Term +stdConstTerm = TConst stdConst stdType + +stdTypeVarName :: Name +stdTypeVarName = stdName "typevar" + +altTypeVarName :: Name +altTypeVarName = stdName "alttypevar" + +stdTypeVar :: Type +stdTypeVar = TypeVar stdTypeVarName + +altTypeVar :: Type +altTypeVar = TypeVar altTypeVarName + +stdVar :: String -> Var +stdVar s = Var (stdName s) stdTypeVar + +stdVarTerm :: String -> Term +stdVarTerm s = TVar (stdVar s) + +altVar :: String -> Var +altVar s = Var (stdName s) altTypeVar + +altVarTerm :: String -> Term +altVarTerm s = TVar (altVar s) + +stdAbsTerm :: String -> Term +stdAbsTerm s = TAbs (stdVarTerm s) stdConstTerm + +stdAppTerm :: String -> Term +stdAppTerm s = TApp (stdAbsTerm s) stdConstTerm + + + -- cgit