summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--readme.txt102
-rw-r--r--src/Library/Command.hs406
-rw-r--r--src/Library/Generator.hs164
-rw-r--r--src/Library/Stack.hs100
-rw-r--r--src/Library/Theorem.hs38
-rw-r--r--src/Test/DataTypes.hs136
-rw-r--r--test/absthm.art28
-rw-r--r--test/appterm.art50
-rw-r--r--test/appthm.art54
-rw-r--r--test/assume.art16
-rw-r--r--test/axiom.art18
-rw-r--r--test/betaconv.art42
-rw-r--r--test/cons.art8
-rw-r--r--test/const.art4
-rw-r--r--test/constterm.art14
-rw-r--r--test/deductantisym.art26
-rw-r--r--test/def.art12
-rw-r--r--test/defineconst.art18
-rw-r--r--test/definetypeop.art56
-rw-r--r--test/eqmp.art74
-rw-r--r--test/name2.art2
-rw-r--r--test/nil.art2
-rw-r--r--test/number.art2
-rw-r--r--test/opType.art8
-rw-r--r--test/pop.art4
-rw-r--r--test/ref.art16
-rw-r--r--test/refl.art12
-rw-r--r--test/remove.art16
-rw-r--r--test/subst.art94
-rw-r--r--test/thm.art46
-rw-r--r--test/typeop.art4
-rw-r--r--test/var.art8
-rw-r--r--test/varterm.art10
-rw-r--r--test/vartype.art4
34 files changed, 797 insertions, 797 deletions
diff --git a/readme.txt b/readme.txt
index 9a55603..7911d67 100644
--- a/readme.txt
+++ b/readme.txt
@@ -1,51 +1,51 @@
-
-
-Semantic <input file>
-
-Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done.
-
-
-
-
-Syntactic <input file>
-
-Checks a proof trace for syntax errors.
-
-
-
-
-ProofGraph <input file>
-
-Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace.
-
-
-
-
-WriteProof <input file> > <output file>
-
-Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace.
-
-
-
-
-Delete <input file> [<num#1>, <num#2>, <num3>] > <output file>
-
-Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can
-actually know what theorems are what. Generates a simplified proof trace as output.
-
-
-
-
-Concat <input #1> <input#2> <input #2> > <output file>
-
-Joins two proof traces together, converts it to a DAG and back again, then outputs the result.
-
-
-
-
-ListThm <input file>
-
-Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you
-are deleting.
-
-
+
+
+Semantic <input file>
+
+Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done.
+
+
+
+
+Syntactic <input file>
+
+Checks a proof trace for syntax errors.
+
+
+
+
+ProofGraph <input file>
+
+Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace.
+
+
+
+
+WriteProof <input file> > <output file>
+
+Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace.
+
+
+
+
+Delete <input file> [<num#1>, <num#2>, <num3>] > <output file>
+
+Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can
+actually know what theorems are what. Generates a simplified proof trace as output.
+
+
+
+
+Concat <input #1> <input#2> <input #2> > <output file>
+
+Joins two proof traces together, converts it to a DAG and back again, then outputs the result.
+
+
+
+
+ListThm <input file>
+
+Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you
+are deleting.
+
+
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
+
+
+
diff --git a/test/absthm.art b/test/absthm.art
index 359a4cd..244f89a 100644
--- a/test/absthm.art
+++ b/test/absthm.art
@@ -1,14 +1,14 @@
-"bool"
-"bool"
-varType
-var
-#varTerm
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-refl
-absThm
+"bool"
+"bool"
+varType
+var
+#varTerm
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+refl
+absThm
diff --git a/test/appterm.art b/test/appterm.art
index 3d566c0..5e5763f 100644
--- a/test/appterm.art
+++ b/test/appterm.art
@@ -1,25 +1,25 @@
-"f"
-const
-"->"
-typeOp
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
-nil
-cons
-cons
-opType
-constTerm
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-appTerm
+"f"
+const
+"->"
+typeOp
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
+nil
+cons
+cons
+opType
+constTerm
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+appTerm
diff --git a/test/appthm.art b/test/appthm.art
index 7e54c8c..c6e0787 100644
--- a/test/appthm.art
+++ b/test/appthm.art
@@ -1,27 +1,27 @@
-"f"
-const
-"->"
-typeOp
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
-nil
-cons
-cons
-opType
-constTerm
-refl
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-refl
-appThm
+"f"
+const
+"->"
+typeOp
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
+nil
+cons
+cons
+opType
+constTerm
+refl
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+refl
+appThm
diff --git a/test/assume.art b/test/assume.art
index ef47474..2d6e097 100644
--- a/test/assume.art
+++ b/test/assume.art
@@ -1,8 +1,8 @@
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-assume
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
diff --git a/test/axiom.art b/test/axiom.art
index bcf79bf..5940bc6 100644
--- a/test/axiom.art
+++ b/test/axiom.art
@@ -1,9 +1,9 @@
-nil
-"name"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-axiom
+nil
+"name"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+axiom
diff --git a/test/betaconv.art b/test/betaconv.art
index f0d051c..a4166bd 100644
--- a/test/betaconv.art
+++ b/test/betaconv.art
@@ -1,21 +1,21 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-"c"
-const
-1
-ref
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-betaConv
+"x"
+"bool"
+typeOp
+nil
+opType
+1
+def
+var
+"c"
+const
+1
+ref
+constTerm
+absTerm
+"a"
+const
+1
+remove
+constTerm
+appTerm
+betaConv
diff --git a/test/cons.art b/test/cons.art
index b2c48b9..da46e33 100644
--- a/test/cons.art
+++ b/test/cons.art
@@ -1,4 +1,4 @@
-"bool"
-typeOp
-nil
-cons
+"bool"
+typeOp
+nil
+cons
diff --git a/test/const.art b/test/const.art
index 8a94755..bc2d1c9 100644
--- a/test/const.art
+++ b/test/const.art
@@ -1,2 +1,2 @@
-"name"
-const
+"name"
+const
diff --git a/test/constterm.art b/test/constterm.art
index ac94e2b..cacb07d 100644
--- a/test/constterm.art
+++ b/test/constterm.art
@@ -1,7 +1,7 @@
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
diff --git a/test/deductantisym.art b/test/deductantisym.art
index 80a6eea..d61b22e 100644
--- a/test/deductantisym.art
+++ b/test/deductantisym.art
@@ -1,13 +1,13 @@
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-assume
-1
-def
-1
-remove
-deductAntisym
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
+1
+def
+1
+remove
+deductAntisym
diff --git a/test/def.art b/test/def.art
index 18cad67..7595e27 100644
--- a/test/def.art
+++ b/test/def.art
@@ -1,6 +1,6 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
+"bool"
+typeOp
+nil
+opType
+1
+def
diff --git a/test/defineconst.art b/test/defineconst.art
index 739f9c9..79ab9b3 100644
--- a/test/defineconst.art
+++ b/test/defineconst.art
@@ -1,9 +1,9 @@
-"y"
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-defineConst
+"y"
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+defineConst
diff --git a/test/definetypeop.art b/test/definetypeop.art
index 706bd3e..5577613 100644
--- a/test/definetypeop.art
+++ b/test/definetypeop.art
@@ -1,28 +1,28 @@
-"n"
-"abs"
-"rep"
-"xtype"
-nil
-cons
-"x"
-"xtype"
-varType
-var
-"c"
-const
-"bool"
-typeOp
-nil
-opType
-1
-def
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-assume
-defineTypeOp
+"n"
+"abs"
+"rep"
+"xtype"
+nil
+cons
+"x"
+"xtype"
+varType
+var
+"c"
+const
+"bool"
+typeOp
+nil
+opType
+1
+def
+constTerm
+absTerm
+"a"
+const
+1
+remove
+constTerm
+appTerm
+assume
+defineTypeOp
diff --git a/test/eqmp.art b/test/eqmp.art
index b7c63c6..bafbea9 100644
--- a/test/eqmp.art
+++ b/test/eqmp.art
@@ -1,37 +1,37 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-"c"
-const
-1
-ref
-constTerm
-2
-def
-absTerm
-"a"
-const
-1
-ref
-constTerm
-3
-def
-appTerm
-refl
-"y"
-1
-remove
-var
-2
-remove
-absTerm
-3
-remove
-appTerm
-assume
-eqMp
+"x"
+"bool"
+typeOp
+nil
+opType
+1
+def
+var
+"c"
+const
+1
+ref
+constTerm
+2
+def
+absTerm
+"a"
+const
+1
+ref
+constTerm
+3
+def
+appTerm
+refl
+"y"
+1
+remove
+var
+2
+remove
+absTerm
+3
+remove
+appTerm
+assume
+eqMp
diff --git a/test/name2.art b/test/name2.art
index a439e52..f62bdc2 100644
--- a/test/name2.art
+++ b/test/name2.art
@@ -1 +1 @@
-"->"
+"->"
diff --git a/test/nil.art b/test/nil.art
index 607602c..9b021e8 100644
--- a/test/nil.art
+++ b/test/nil.art
@@ -1 +1 @@
-nil
+nil
diff --git a/test/number.art b/test/number.art
index f599e28..d434014 100644
--- a/test/number.art
+++ b/test/number.art
@@ -1 +1 @@
-10
+10
diff --git a/test/opType.art b/test/opType.art
index 237dbd6..8548457 100644
--- a/test/opType.art
+++ b/test/opType.art
@@ -1,4 +1,4 @@
-"name"
-typeOp
-nil
-opType
+"name"
+typeOp
+nil
+opType
diff --git a/test/pop.art b/test/pop.art
index e111fc2..3717446 100644
--- a/test/pop.art
+++ b/test/pop.art
@@ -1,2 +1,2 @@
-nil
-pop
+nil
+pop
diff --git a/test/ref.art b/test/ref.art
index acd59ea..2042b3e 100644
--- a/test/ref.art
+++ b/test/ref.art
@@ -1,8 +1,8 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-ref
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+ref
diff --git a/test/refl.art b/test/refl.art
index 418ac89..3e8e20e 100644
--- a/test/refl.art
+++ b/test/refl.art
@@ -1,6 +1,6 @@
-"bool"
-"bool"
-varType
-var
-varTerm
-refl
+"bool"
+"bool"
+varType
+var
+varTerm
+refl
diff --git a/test/remove.art b/test/remove.art
index 88cadad..4f82808 100644
--- a/test/remove.art
+++ b/test/remove.art
@@ -1,8 +1,8 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
diff --git a/test/subst.art b/test/subst.art
index 8fdc934..c46903e 100644
--- a/test/subst.art
+++ b/test/subst.art
@@ -1,47 +1,47 @@
-"ytype"
-"xtype"
-varType
-nil
-cons
-cons
-nil
-cons
-"y"
-"xtype"
-varType
-var
-"z"
-"xtype"
-varType
-var
-varTerm
-nil
-cons
-cons
-nil
-cons
-nil
-cons
-cons
-"y"
-"ytype"
-varType
-var
-"c"
-const
-"bool"
-typeOp
-nil
-opType
-1
-def
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-assume
-subst
+"ytype"
+"xtype"
+varType
+nil
+cons
+cons
+nil
+cons
+"y"
+"xtype"
+varType
+var
+"z"
+"xtype"
+varType
+var
+varTerm
+nil
+cons
+cons
+nil
+cons
+nil
+cons
+cons
+"y"
+"ytype"
+varType
+var
+"c"
+const
+"bool"
+typeOp
+nil
+opType
+1
+def
+constTerm
+absTerm
+"a"
+const
+1
+remove
+constTerm
+appTerm
+assume
+subst
diff --git a/test/thm.art b/test/thm.art
index 4fee8b2..4ce6a1c 100644
--- a/test/thm.art
+++ b/test/thm.art
@@ -1,23 +1,23 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-varTerm
-assume
-"y"
-1
-ref
-var
-varTerm
-nil
-cons
-"z"
-1
-remove
-var
-varTerm
-thm
+"x"
+"bool"
+typeOp
+nil
+opType
+1
+def
+var
+varTerm
+assume
+"y"
+1
+ref
+var
+varTerm
+nil
+cons
+"z"
+1
+remove
+var
+varTerm
+thm
diff --git a/test/typeop.art b/test/typeop.art
index 6b85dd7..5a6abaf 100644
--- a/test/typeop.art
+++ b/test/typeop.art
@@ -1,2 +1,2 @@
-"bool"
-typeOp
+"bool"
+typeOp
diff --git a/test/var.art b/test/var.art
index 4c915e7..6dc6a0f 100644
--- a/test/var.art
+++ b/test/var.art
@@ -1,4 +1,4 @@
-"bool"
-"bool"
-varType
-var
+"bool"
+"bool"
+varType
+var
diff --git a/test/varterm.art b/test/varterm.art
index 5bbc768..3a2b04f 100644
--- a/test/varterm.art
+++ b/test/varterm.art
@@ -1,5 +1,5 @@
-"bool"
-"bool"
-varType
-var
-varTerm
+"bool"
+"bool"
+varType
+var
+varTerm
diff --git a/test/vartype.art b/test/vartype.art
index 72e6b3c..c9a5e7a 100644
--- a/test/vartype.art
+++ b/test/vartype.art
@@ -1,2 +1,2 @@
-"bool"
-varType
+"bool"
+varType
generated by cgit (git 2.30.0) at 2024-12-22 09:14:05 +0000