summaryrefslogtreecommitdiff
path: root/Semantic.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Semantic.hs')
-rw-r--r--Semantic.hs238
1 files changed, 11 insertions, 227 deletions
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 []