diff options
| -rw-r--r-- | Object.hs | 39 | ||||
| -rw-r--r-- | Semantic.hs | 238 | ||||
| -rw-r--r-- | Term.hs | 173 | ||||
| -rw-r--r-- | Theorem.hs | 19 | ||||
| -rw-r--r-- | TypeVar.hs | 65 |
5 files changed, 307 insertions, 227 deletions
diff --git a/Object.hs b/Object.hs new file mode 100644 index 0000000..640cf08 --- /dev/null +++ b/Object.hs @@ -0,0 +1,39 @@ +module Object ( + Object(..), + + List + ) where + + + +import Data.List +import TypeVar +import Term +import Theorem + + + +data Object = ObjNum { objNum :: Number } + | ObjName { objName :: Name } + | ObjList { objList :: List } + | ObjTyOp { objTyOp :: TypeOp } + | ObjType { objType :: Type } + | ObjConst { objConst :: Const } + | ObjVar { objVar :: Var } + | ObjTerm { objTerm :: Term } + | ObjThm { objThm :: Theorem } deriving (Eq) + +type List = [Object] + + + +instance Show Object where + show (ObjNum a) = show a + show (ObjName a) = show a + show (ObjList a) = show a + show (ObjTyOp a) = show a + show (ObjType a) = show a + show (ObjConst a) = show a + show (ObjVar a) = show a + show (ObjTerm a) = show a + show (ObjThm a) = show a diff --git a/Semantic.hs b/Semantic.hs index 7de8dee..d50905c 100644 --- a/Semantic.hs +++ b/Semantic.hs @@ -1,89 +1,12 @@ import Control.Monad( liftM ) import System( getArgs ) import Data.List +import TypeVar +import Term +import Theorem +import Object -data Object = ObjNum { objNum :: Number } - | ObjName { objName :: Name } - | ObjList { objList :: List } - | ObjTyOp { objTyOp :: TypeOp } - | ObjType { objType :: Type } - | ObjConst { objConst :: Const } - | ObjVar { objVar :: Var } - | ObjTerm { objTerm :: Term } - | ObjThm { objThm :: Theorem } deriving (Eq) - -type Number = Int - -data Name = Name { nameSpace :: [String] - , nameId :: String } deriving (Eq) - -type List = [Object] - -data TypeOp = TypeOp { tyOp :: Name } deriving (Eq) - -data Type = TypeVar { typeVar :: Name } - | AType { aType :: [Type] - , aTypeOp :: TypeOp } deriving (Eq) - -data Const = Const { constName :: Name } deriving (Eq) - -data Var = Var { varName :: Name - , varTy :: Type } deriving (Eq) - -data Term = TVar { tVar :: Var } - | TConst { tConst :: Const - , tConstType :: Type } - | TApp { tAppLeft :: Term - , tAppRight :: Term } - | TAbs { tAbsVar :: Term - , tAbsTerm :: Term } - -data Theorem = Theorem { thmHyp :: [Term] - , thmCon :: Term } deriving (Eq) - - -instance Show Object where - show (ObjNum a) = show a - show (ObjName a) = show a - show (ObjList a) = show a - show (ObjTyOp a) = show a - show (ObjType a) = show a - show (ObjConst a) = show a - show (ObjVar a) = show a - show (ObjTerm a) = show a - show (ObjThm a) = show a - -instance Show Name where - show a = intercalate "." (nameSpace a ++ [nameId a]) - -instance Show TypeOp where - show a = "typeOp " ++ (show $ tyOp a) - -instance Show Type where - show (TypeVar tyVar) = "typeVar " ++ (show tyVar) - show (AType list typeOp) = "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list) - -instance Show Const where - show (Const a) = show a - -instance Show Var where - show (Var a _) = show a - -instance Show Term where - show (TVar a) = show a - show (TConst a _) = show a - show (TApp (TApp eq lhs) rhs) - | isEq eq = "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")" - show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")" - show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")" - -instance Show Theorem where - show a = (show . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) - -instance Eq Term where - a == b = a `alphaEquiv` b - data Stack = Stack { stackList :: [Object] } data Dictionary = Dictionary { dictionMap :: [(Int,Object)] } @@ -104,9 +27,6 @@ instance Show Theorems where show a = "Theorems:\n" ++ intercalate "\n" (map (show) (theoremList a)) ++ "\n\n" -type Substitution = [[[Object]]] - - data ArticleLine = Comment { commentString :: String } | Command { commandFunc :: ((Stack,Dictionary,Assumptions,Theorems)->(Stack,Dictionary,Assumptions,Theorems)) } @@ -225,7 +145,7 @@ betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumpt betaConv (s,d,a,t) = let stack = stackList s op = (\x -> Theorem [] (mkEquals x - (substitute [[], [[ObjVar . tVar . tAbsVar . tAppLeft $ x, ObjTerm . tAppRight $ x]]] + (substitute ([], [(tVar . tAbsVar . tAppLeft $ x, tAppRight $ x)]) (tAbsTerm . tAppLeft $ x)))) theorem = ObjThm $ op (objTerm $ stack!!0) s' = Stack $ theorem : (tail stack) @@ -380,7 +300,12 @@ subst (s,d,a,t) = let stack = stackList s op = (\x y -> Theorem (map (substitute y) (thmHyp x)) (substitute y (thmCon x))) - theorem = ObjThm $ op (objThm $ stack!!0) ((map (map objList)) . (map objList) . objList $ stack!!1) + substitution = + (\x -> let list = (map (map objList)) . (map objList) . objList $ x + f = (\g h x -> (g . head $ x, h . last $ x)) + in f (map (f objName objType)) (map (f objVar objTerm)) list) + + theorem = ObjThm $ op (objThm $ stack!!0) (substitution $ stack!!1) s' = Stack $ theorem : (drop 2 stack) in (s',d,a,t) @@ -434,147 +359,6 @@ varType (s,d,a,t) = - -alphaEquiv :: Term -> Term -> Bool -alphaEquiv a b = - let equiv = \term1 term2 varmap lambdaDepth -> - case (term1,term2) of - (TConst a1 b1, TConst a2 b2) -> - a1 == a2 && b1 == b2 - - (TApp a1 b1, TApp a2 b2) -> - equiv a1 a2 varmap lambdaDepth && - equiv b1 b2 varmap lambdaDepth - - (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) -> - type1 == type2 && - equiv b1 b2 newmap (lambdaDepth + 1) - where newmap = (lambdaDepth + 1, ((Var name1 type1),(Var name2 type2))) : varmap - - (TVar a1, TVar a2) -> - -- the order of the pair is important - (lambdaDepth, (a1,a2)) `elem` varmap || - not ((lambdaDepth, (a1,a2)) `elem` varmap) && a1 == a2 - - (_,_) -> False - in equiv a b [] 0 - - -alphaConvert :: Term -> Term -> Term -alphaConvert (TConst a ty) (TConst _ _) = TConst a ty -alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) -alphaConvert (TVar v) (TVar _) = TVar v -alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute [[],[[ObjVar $ tVar v1, ObjTerm $ v2]]] (TAbs v1 (alphaConvert a b)) - - -alphaConvertList :: [Term] -> [Term] -> [Term] -alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b) - - -substitute :: Substitution -> Term -> Term -substitute [tymap, vmap] term = - let typesub = - (\x y -> - case y of - (TConst a ty) -> if (ty == (objType . head $ x)) - then TConst a (objType . last $ x) - else TConst a ty - (TApp a b) -> TApp (typesub x a) (typesub x b) - (TAbs v a) -> TAbs v (typesub x a) - (TVar v) -> TVar v) - varsub = - (\x y -> - case y of - (TConst a ty) -> TConst a ty - (TApp a b) -> TApp (varsub x a) (varsub x b) - (TVar v) -> if (v == (objVar . head $ x)) - then objTerm . last $ x - else TVar v - (TAbs v a) -> let safe = rename (TAbs v a) (union [(objVar . head $ x)] (containsVars (objTerm . last $ x))) - in case safe of - (TAbs m n) -> TAbs m (varsub x n)) - tydone = foldl' (\x y -> typesub y x) term tymap - vdone = foldl' (\x y -> varsub y x) tydone vmap - in vdone - - -containsVars :: Term -> [Var] -containsVars t = - let f = (\term list -> - case term of - (TConst a b) -> list - (TApp a b) -> union list ((f a list) ++ (f b list)) - (TVar a) -> union list [a] - (TAbs a b) -> union list ([tVar a] ++ (f b list))) - in f t [] - - -rename :: Term -> [Var] -> Term -rename (TAbs (TVar v) t) varlist = - let doRename = - (\x y z -> case x of - (TAbs (TVar a) b) -> if (a == y) - then TAbs (TVar z) (doRename b y z) - else TAbs (TVar a) (doRename b y z) - (TConst a b) -> TConst a b - (TApp a b) -> TApp (doRename a y z) (doRename b y z) - (TVar a) -> if (a == y) - then TVar z - else TVar a) - findSafe = - (\x y -> if (x `elem` y) - then case x of - (Var a b) -> - case a of - (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y - else x) - in if (v `elem` varlist) - then doRename (TAbs (TVar v) t) v (findSafe v varlist) - else TAbs (TVar v) t - - - - -typeOf :: Term -> Type -typeOf (TConst c ty) = ty -typeOf (TVar v) = varTy v -typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t) -typeOf (TApp f _) = - -- type of f is of the form [[a,b], "->"] - last . aType . typeOf $ f - - -mkEquals :: Term -> Term -> Term -mkEquals lhs rhs = - let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs)) - in TApp (TApp eqConst lhs) rhs - - -mkEqualsType :: Type -> Type -mkEqualsType ty = typeFunc (AType [] (TypeOp (Name [] "bool"))) (typeFunc ty ty) - - -getlhs :: Term -> Term -getlhs (TApp (TApp eq lhs) _) = - if (isEq eq) then lhs else error "Tried to get lhs from a non-eq term" - - -getrhs :: Term -> Term -getrhs (TApp (TApp eq _) rhs) = - if (isEq eq) then rhs else error "Tried to get rhs from a non-eq term" - - -isEq :: Term -> Bool -isEq (TConst (Const (Name [] "=")) _) = True -isEq _ = False - - -typeFunc :: Type -> Type -> Type -typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) - - - - doSemanticCheck :: [String] -> (Stack,Dictionary,Assumptions,Theorems) doSemanticCheck = let s = Stack [] @@ -0,0 +1,173 @@ +module Term ( + Term(..), + + alphaEquiv, + alphaConvert, + alphaConvertList, + substitute, + containsVars, + rename, + typeOf, + mkEquals, + isEq, + getlhs, + getrhs + ) where + + + +import Data.List +import TypeVar + + + +data Term = TVar { tVar :: Var } + | TConst { tConst :: Const + , tConstType :: Type } + | TApp { tAppLeft :: Term + , tAppRight :: Term } + | TAbs { tAbsVar :: Term + , tAbsTerm :: Term } + +type Substitution = ( [(Name,Type)], [(Var,Term)] ) + + +instance Show Term where + show (TVar a) = show a + show (TConst a _) = show a + show (TApp (TApp eq lhs) rhs) + | isEq eq = "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")" + show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")" + show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")" + +instance Eq Term where + a == b = a `alphaEquiv` b + + + +alphaEquiv :: Term -> Term -> Bool +alphaEquiv a b = + let equiv = \term1 term2 varmap lambdaDepth -> + case (term1,term2) of + (TConst a1 b1, TConst a2 b2) -> + a1 == a2 && b1 == b2 + + (TApp a1 b1, TApp a2 b2) -> + equiv a1 a2 varmap lambdaDepth && + equiv b1 b2 varmap lambdaDepth + + (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) -> + type1 == type2 && + equiv b1 b2 newmap (lambdaDepth + 1) + where newmap = (lambdaDepth + 1, ((Var name1 type1),(Var name2 type2))) : varmap + + (TVar a1, TVar a2) -> + -- the order of the pair is important + (lambdaDepth, (a1,a2)) `elem` varmap || + not ((lambdaDepth, (a1,a2)) `elem` varmap) && a1 == a2 + + (_,_) -> False + in equiv a b [] 0 + + +alphaConvert :: Term -> Term -> Term +alphaConvert (TConst a ty) (TConst _ _) = TConst a ty +alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2) +alphaConvert (TVar v) (TVar _) = TVar v +alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b)) + + +alphaConvertList :: [Term] -> [Term] -> [Term] +alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b) + + +substitute :: Substitution -> Term -> Term +substitute (tymap,vmap) term = + let typesub = + (\x y -> + case y of + (TConst a ty) -> if (ty == (TypeVar . fst $ x)) + then TConst a (snd x) + else TConst a ty + (TApp a b) -> TApp (typesub x a) (typesub x b) + (TAbs v a) -> TAbs v (typesub x a) + (TVar v) -> TVar v) + varsub = + (\x y -> + case y of + (TConst a ty) -> TConst a ty + (TApp a b) -> TApp (varsub x a) (varsub x b) + (TVar v) -> if (v == (fst x)) + then snd x + else TVar v + (TAbs v a) -> let safe = rename (TAbs v a) (union [fst x] (containsVars . snd $ x)) + in case safe of + (TAbs m n) -> TAbs m (varsub x n)) + tydone = foldl' (\x y -> typesub y x) term tymap + vdone = foldl' (\x y -> varsub y x) tydone vmap + in vdone + + +containsVars :: Term -> [Var] +containsVars t = + let f = (\term list -> + case term of + (TConst a b) -> list + (TApp a b) -> union list ((f a list) ++ (f b list)) + (TVar a) -> union list [a] + (TAbs a b) -> union list ([tVar a] ++ (f b list))) + in f t [] + + +rename :: Term -> [Var] -> Term +rename (TAbs (TVar v) t) varlist = + let doRename = + (\x y z -> case x of + (TAbs (TVar a) b) -> if (a == y) + then TAbs (TVar z) (doRename b y z) + else TAbs (TVar a) (doRename b y z) + (TConst a b) -> TConst a b + (TApp a b) -> TApp (doRename a y z) (doRename b y z) + (TVar a) -> if (a == y) + then TVar z + else TVar a) + findSafe = + (\x y -> if (x `elem` y) + then case x of + (Var a b) -> + case a of + (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y + else x) + in if (v `elem` varlist) + then doRename (TAbs (TVar v) t) v (findSafe v varlist) + else TAbs (TVar v) t + + +typeOf :: Term -> Type +typeOf (TConst c ty) = ty +typeOf (TVar v) = varTy v +typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t) +typeOf (TApp f _) = + -- type of f is of the form [[a,b], "->"] + last . aType . typeOf $ f + + +mkEquals :: Term -> Term -> Term +mkEquals lhs rhs = + let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs)) + in TApp (TApp eqConst lhs) rhs + + +getlhs :: Term -> Term +getlhs (TApp (TApp eq lhs) _) + | (isEq eq) = lhs + + +getrhs :: Term -> Term +getrhs (TApp (TApp eq _) rhs) + | (isEq eq) = rhs + + +isEq :: Term -> Bool +isEq (TConst (Const (Name [] "=")) _) = True +isEq _ = False diff --git a/Theorem.hs b/Theorem.hs new file mode 100644 index 0000000..c4a36c8 --- /dev/null +++ b/Theorem.hs @@ -0,0 +1,19 @@ +module Theorem ( + Theorem(..), + ) where + + + +import Data.List +import TypeVar +import Term + + + +data Theorem = Theorem { thmHyp :: [Term] + , thmCon :: Term } deriving (Eq) + + + +instance Show Theorem where + show a = (show . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a) diff --git a/TypeVar.hs b/TypeVar.hs new file mode 100644 index 0000000..2dae613 --- /dev/null +++ b/TypeVar.hs @@ -0,0 +1,65 @@ +module TypeVar ( + Number, + + Name(..), + + TypeOp(..), + + Type(..), + + Const(..), + + Var(..), + + mkEqualsType, + typeFunc + ) where + + + +import Data.List + + + +type Number = Int + +data Name = Name { nameSpace :: [String] + , nameId :: String } deriving (Eq) + +data TypeOp = TypeOp { tyOp :: Name } deriving (Eq) + +data Type = TypeVar { typeVar :: Name } + | AType { aType :: [Type] + , aTypeOp :: TypeOp } deriving (Eq) + +data Const = Const { constName :: Name } deriving (Eq) + +data Var = Var { varName :: Name + , varTy :: Type } deriving (Eq) + + + +instance Show Name where + show a = intercalate "." (nameSpace a ++ [nameId a]) + +instance Show TypeOp where + show a = "typeOp " ++ (show $ tyOp a) + +instance Show Type where + show (TypeVar tyVar) = "typeVar " ++ (show tyVar) + show (AType list typeOp) = "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list) + +instance Show Const where + show (Const a) = show a + +instance Show Var where + show (Var a _) = show a + + + +mkEqualsType :: Type -> Type +mkEqualsType ty = typeFunc (AType [] (TypeOp (Name [] "bool"))) (typeFunc ty ty) + + +typeFunc :: Type -> Type -> Type +typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) |