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 --- readme.txt | 102 ++++++------ 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 ++++++++-------- test/absthm.art | 28 ++-- test/appterm.art | 50 +++--- test/appthm.art | 54 +++---- test/assume.art | 16 +- test/axiom.art | 18 +-- test/betaconv.art | 42 ++--- test/cons.art | 8 +- test/const.art | 4 +- test/constterm.art | 14 +- test/deductantisym.art | 26 +-- test/def.art | 12 +- test/defineconst.art | 18 +-- test/definetypeop.art | 56 +++---- test/eqmp.art | 74 ++++----- test/name2.art | 2 +- test/nil.art | 2 +- test/number.art | 2 +- test/opType.art | 8 +- test/pop.art | 4 +- test/ref.art | 16 +- test/refl.art | 12 +- test/remove.art | 16 +- test/subst.art | 94 +++++------ test/thm.art | 46 +++--- test/typeop.art | 4 +- test/var.art | 8 +- test/varterm.art | 10 +- test/vartype.art | 4 +- 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 - -Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done. - - - - -Syntactic - -Checks a proof trace for syntax errors. - - - - -ProofGraph - -Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace. - - - - -WriteProof > - -Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace. - - - - -Delete [, , ] > - -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 > - -Joins two proof traces together, converts it to a DAG and back again, then outputs the result. - - - - -ListThm - -Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you -are deleting. - - + + +Semantic + +Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done. + + + + +Syntactic + +Checks a proof trace for syntax errors. + + + + +ProofGraph + +Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace. + + + + +WriteProof > + +Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace. + + + + +Delete [, , ] > + +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 > + +Joins two proof traces together, converts it to a DAG and back again, then outputs the result. + + + + +ListThm + +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 -- cgit