Mercurial > hg > Members > atton > tapl
changeset 12:d5e85961789f
Wrote simplebool
author | atton |
---|---|
date | Thu, 03 Nov 2016 10:02:24 +0000 |
parents | 3a4b3f0e595b |
children | 17b9b80fa047 |
files | simplebool/SimpleBool.hs |
diffstat | 1 files changed, 66 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/simplebool/SimpleBool.hs Thu Nov 03 10:02:24 2016 +0000 @@ -0,0 +1,66 @@ +module SimpleBool where + +import Control.Applicative +import Data.Either + +type Index = Int +type ContextSize = Int +type Name = String +type Error = String +type EitherE = Either Error + +data Binding = NameBind + | VarBind Type + deriving (Show, Eq) +type Context = [(Name, Binding)] + +data Type = TyArr Type Type + | TyBool + deriving (Show, Eq) + +data Term = TmVar Index ContextSize + | TmAbs Name Type Term + | TmApp Term Term + | TmTrue + | TmFalse + | TmIf Term Term Term + deriving Show + + +index2name ctx i = "hoge" + + +addBinding :: Context -> Name-> Binding -> Context +addBinding ctx n b = (n, b) : ctx + +getBinding :: Context -> Index -> EitherE Binding +getBinding ctx i + | length ctx < i = Left "Index Error." + | otherwise = return . snd $ ctx !! i + + +getTypeFromContext :: Context -> Index -> EitherE Type +getTypeFromContext ctx i = getTypeFromBinding $ getBinding ctx i + where + getTypeFromBinding (Right (VarBind t)) = return t + getTypeFromBinding _ = Left $ "getTypeFromContext: Wrong kind of binding for variable " ++ index2name ctx i + + +typeOf :: Context -> Term -> EitherE Type +typeOf ctx (TmVar i _) = getTypeFromContext ctx i +typeOf ctx (TmAbs x ty tm2) = let ctx' = addBinding ctx x (VarBind ty) + in (typeOf ctx' tm2) >>= (\ty2 -> return $ TyArr ty ty2) +typeOf ctx (TmApp tm1 tm2) = do + ty1 <- typeOf ctx tm1 + ty2 <- typeOf ctx tm2 + case ty1 of + (TyArr ty11 ty12) -> if ty2 == ty11 then return ty12 + else Left "Parameter type mismatch." +typeOf ctx (TmTrue) = return TyBool +typeOf ctx (TmFalse) = return TyBool +typeOf ctx (TmIf tm1 tm2 tm3) + | (typeOf ctx tm1) == (Right TyBool) = do ty2 <- typeOf ctx tm2 + ty3 <- typeOf ctx tm3 + if (ty2 == ty3) then return ty2 + else Left "arms of conditional have different types" + | otherwise = Left "guard of conditional not a boolean"