summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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
5 files changed, 422 insertions, 422 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)
+
+
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
+
+
+
generated by cgit (git 2.30.0) at 2024-12-22 18:55:56 +0000