_tactics avatar _tactics committed 9b55be5

Files

Comments (0)

Files changed (5)

+module Main where
+
+import Control.Monad
+import System.IO
+import System.Environment
+import STLC
+
+main = do
+    [infile, outfile] <- getArgs
+    fin <- openFile infile ReadMode
+    fout <- openFile outfile WriteMode
+    
+    input <- hGetContents fin
+    forM (lines input) $ \line -> do
+        let line' = trim line
+        let Just x = typeCheckD $ parseTerm line'
+        hPutStrLn fout $ show x
+        hPutStrLn fout "\n\n\n\n\n"
+        hFlush fout
+    
+module STLC where
+import Debug.Trace
+import Text.Parsec
+import Text.Parsec.Prim
+import Text.Parsec.String
+import Text.Parsec.Pos
+import Tokenizer
+import Data.Array.ST
+import Control.Monad.ST
+import Data.Array.IArray
+
+data Type = 
+    Base String |
+    Arr Type Type
+
+instance Eq Type where
+    Base a == Base b = a == b
+    (Arr s t) == (Arr s' t') = s == s' && t == t'
+    _ == _ = False
+    
+instance Show Type where
+    show (Base b) = b
+    show (Arr (Arr s t) u) = "(" ++ show s ++ " -> " ++ show t ++ ") -> " ++ show u
+    show (Arr (Base b) u) = b ++ " -> " ++ show u
+
+data Context = 
+    CtxEmpty |
+    Bind String Type Context
+    
+instance Show Context where
+    show CtxEmpty = ""
+    show (Bind x t CtxEmpty) = x ++ " : " ++ show t
+    show (Bind x t ctx') = x ++ " : " ++ show t ++ ", " ++ show ctx'
+    
+ctxlookup :: String -> Context -> Type
+ctxlookup s CtxEmpty = error $ s ++ " is not defined"
+ctxlookup s (Bind s' t ctx') | s == s' = t
+                             | otherwise = ctxlookup s ctx'
+
+ctxSafeLookup :: String -> Context -> Maybe Type
+ctxSafeLookup s CtxEmpty = Nothing
+ctxSafeLookup s (Bind s' t ctx') | s == s' = Just t
+                                 | otherwise = ctxSafeLookup s ctx'
+                             
+typeApp :: Type -> Type -> Type
+typeApp (Arr s t) s' | s == s' = t
+typeApp _  _ = error "Can't apply here"
+
+typeCanApp :: Type -> Type -> Maybe Type
+typeCanApp (Arr s t) s' | s == s' = Just t
+typeCanApp _  _ = Nothing
+
+data TypeDeriv = 
+    TyVar Context Term Type | -- Term is Var s and s appears in the context
+    TyLam Context Term Type TypeDeriv | -- Term is Lam s ty b and b shows b is typeable in context extended by s : ty
+    TyApp Context Term Type TypeDeriv TypeDeriv -- terms are f and x and the subderives show f and x are typeable in ctx
+
+instance Show TypeDeriv where
+    show (TyVar ctx tm ty) = show ctx ++ " |- " ++ show tm ++ " : " ++ show ty
+    show (TyLam ctx tm ty bDeriv) = 
+        let top = show bDeriv 
+            bottom = show ctx ++ " |- " ++ show tm ++ " : " ++ show ty
+            line = replicate (max (width top) (width bottom)) '-' in
+        top ++ "\n" ++ line ++ "\n" ++ bottom
+    show (TyApp ctx tm ty fDeriv xDeriv) = 
+        let top_left = show fDeriv
+            top_right = show xDeriv
+            top = asBlock top_left top_right
+            bottom = show ctx ++ " |- " ++ show tm ++ " : " ++ show ty
+            line1 = replicate (width top_left) '-' 
+            line2 = replicate (max (width top_right) (width bottom - length line1 - 1)) '-' in
+            top ++ "\n" ++ line1 ++ " " ++ line2 ++ "\n" ++ bottom
+            
+asBlock :: String -> String -> String
+asBlock left right = 
+    let lw = width left
+        lh = height left
+        rw = width right
+        rh = height right 
+        totalw = lw + rw + 1
+        totalh = max lh rh
+        
+        line :: Int -> String
+        line i = [farr ! (x, i) | x <- [0..totalw-1]]
+        
+        farr :: Array (Int, Int) Char
+        farr = runST $ do
+            arr <- newArray ((0::Int, 0::Int), (totalw, totalh)) ' ' :: ST s (STUArray s (Int, Int) Char)
+            copy left   0            (totalh - lh) arr
+            copy right (totalw - rw) (totalh - rh) arr
+            freeze arr
+        in 
+        trim $ unlines [line i | i <- [0..totalh-1]]
+    where 
+    copy :: String -> Int -> Int -> STUArray s (Int, Int) Char -> ST s ()
+    copy s w h arr = copy' s w h
+        where 
+        copy' ('\n':xs) cur_w cur_h = copy' xs w (cur_h+1)
+        copy' (x:xs) cur_w cur_h = do 
+            writeArray arr (cur_w, cur_h) x
+            copy' xs (cur_w+1) (cur_h)
+        copy' [] _ _ = return ()
+
+trim :: String -> String
+trim (x : '\n' : []) = [x]
+trim (x:y:xs) = x : trim (y : xs)
+trim [x] = [x]
+trim [] = []
+    
+height :: String -> Int
+height s = length $ lines s
+
+width :: String -> Int
+width s = maximum $ map (length . trim) $ lines s
+
+tdType :: TypeDeriv -> Type
+tdType (TyVar _ _ ty) = ty
+tdType (TyLam _ _ ty _) = ty
+tdType (TyApp _ _ ty _ _) = ty
+    
+data Term = 
+    Var String |
+    Lam String Type Term |
+    App Term Term
+
+instance Show Term where
+    show (Var s) = s
+    show (Lam s t b) = "\\" ++ s ++ " : " ++ show t ++ ". " ++ show b
+    show (App f (App g x)) = show f ++ " (" ++ show (App g x) ++ ")"
+    show (App f x@(Lam _ t b)) = show f ++ " (" ++ show x ++ ")"
+    show (App f (Var x)) = show f ++ " " ++ x
+
+typeCheckD :: Term -> Maybe TypeDeriv
+typeCheckD t = typeCheckD' t CtxEmpty
+    where 
+    typeCheckD' :: Term -> Context -> Maybe TypeDeriv
+    typeCheckD' (Var x) ctx = do
+        ty <- ctxSafeLookup x ctx
+        return $ TyVar ctx (Var x) ty
+    typeCheckD' (Lam x ty b) ctx = do 
+        deriv <- typeCheckD' b (Bind x ty ctx)
+        let bty = tdType deriv
+        return $ TyLam ctx (Lam x ty b) (Arr ty bty) deriv
+    typeCheckD' (App f x) ctx = do
+        derivF <- typeCheckD' f ctx
+        derivX <- typeCheckD' x ctx
+        let tyF = tdType derivF
+            tyX = tdType derivX
+        tyResult <- typeCanApp tyF tyX
+        return $ TyApp ctx (App f x) tyResult derivF derivX
+    
+typeCheck :: Term -> Type
+typeCheck t = typeCheck' t CtxEmpty
+    where
+    typeCheck' :: Term -> Context -> Type 
+    typeCheck' (Var x) ctx = ctxlookup x ctx
+    typeCheck' (Lam x t b) ctx = typeCheck' b (Bind x t ctx)
+    typeCheck' (App f x) ctx = 
+        let f_t = typeCheck' f ctx in
+        let x_t = typeCheck' x ctx in 
+        typeApp f_t x_t
+        
+    
+type STLCP = GenParser Token ()
+
+pTerm :: STLCP Term
+pTerm = try pLam <|> pApp
+
+pParen :: STLCP Term
+pParen = do
+    consumeToken TLP
+    t <- pTerm
+    consumeToken TRP
+    return t
+
+pApp :: STLCP Term
+pApp = do
+    ts <- many1 pBasic
+    return $ foldl1 App ts
+
+pBasic :: STLCP Term
+pBasic = try pVar <|> pParen
+    
+pType :: STLCP Type
+pType = try pTypeArrow
+        
+pTypeArrow :: STLCP Type
+pTypeArrow = do
+    parts <- sepBy1 pTypeVar (consumeToken TArr)
+    return $ foldr1 Arr parts
+
+pTypeVar :: STLCP Type
+pTypeVar = try (do
+    name <- pIdent
+    return $ Base name)
+    <|> pTypeParen
+    
+
+pTypeParen :: STLCP Type    
+pTypeParen = do
+    consumeToken TLP
+    t <- pType
+    consumeToken TRP
+    return t
+    
+pLam :: STLCP Term
+pLam = do
+    consumeToken TLam
+    name <- pIdent
+    consumeToken TColon
+    ty <- pType
+    consumeToken TDot
+    body <- pTerm
+    return $ Lam name ty body
+
+pVar :: STLCP Term
+pVar = do 
+    name <- pIdent
+    return $ Var name
+    
+pIdent :: STLCP String    
+pIdent = do
+    (TIdent name) <- tokSatisfy $ \x ->
+        case x of 
+            TIdent _  -> True
+            otherwise -> False
+    return name
+    
+consumeToken :: Token -> STLCP Token
+consumeToken t = tokSatisfy (==t)
+
+tokSatisfy :: Monad m => (Token -> Bool) -> ParsecT [Token] u m Token
+tokSatisfy test = tokenPrim show tokNextPos tokTest
+  where tokNextPos pos x xs = updatePosChar pos ' '
+        tokTest t = case test t of 
+                         True -> Just t
+                         False -> Nothing
+    
+parseTerm :: String ->  Term
+parseTerm i = 
+    let toks = tokenize i in
+    case parse pTerm "" toks of
+        Right res -> res
+        Left msg -> error $ show msg
+        
+{-# LANGUAGE NoMonomorphismRestriction #-}
+module Tokenizer where
+
+import Text.Parsec
+import Text.Parsec.String
+
+data Token = TIdent String -- Identifier
+           | TLP -- (
+           | TRP -- )
+           | TArr -- ->
+           | TLam -- \
+           | TColon -- :
+           | TDot -- .
+           | TEq -- =
+           | TKeyword String
+  deriving (Eq, Show)
+   
+type TokenParser = GenParser Char ()
+
+tTokens :: TokenParser [Token]
+tTokens = do
+  ts <- many $ do
+    many (char ' ')
+    t <-  tKeyword <|> tVar <|> tRP <|> tLP <|> tCol <|> tArr <|> tLam <|> tDot <|> tEq
+    many (char ' ')
+    return t
+  eof
+  return ts 
+  
+
+
+tVar :: TokenParser Token
+tVar = do
+  x <- letter
+  xs <- many letter
+  return $ TIdent (x :xs)
+
+tLP :: TokenParser Token
+tLP = do {char '('; return TLP}
+tRP :: TokenParser Token 
+tRP = do char ')'; return TRP
+tArr :: TokenParser Token 
+tArr = do char '-'; char '>'; return TArr
+tLam :: TokenParser Token 
+tLam = do char '\\'; return TLam
+tCol :: TokenParser Token 
+tCol = do char ':'; return TColon
+tDot = do char '.'; return TDot
+tEq = do char '='; return TEq
+
+tKeyword = do
+    keyword <- tryKeywords keywords
+    return $ TKeyword keyword
+    where 
+    tryKeywords [] = unexpected "Keyword expected"
+    tryKeywords (k : ks) = try $ string k <|> tryKeywords ks
+    
+tokenize :: String -> [Token]
+tokenize input = 
+    case parse tTokens "" input of
+        Right res -> res
+        Left msg -> error $ show msg
+
+keywords :: [String]
+keywords = [
+    "abstract",
+    "foreach",
+    "return",
+    "finite",
+    "as",
+    "if",
+    "static",
+    "assert",
+    "internal",
+    "super",
+    "infinite",
+    "break",
+    "is",
+    "switch",
+    "builtin",
+    "case",
+    "isnot",
+    "this",
+    "catch",
+    "it",
+    "throw",
+    "class",
+    "match",
+    "instance",
+    "const",
+    "native",
+    "try",
+    "continue",
+    "new",
+    "using",
+    "unsafe",
+    "null",
+    "virtual",
+    "export",
+    "do",
+    "volatile",
+    "import",
+    "deep",
+    "else",
+    "override",
+    "void",
+    "external",
+    "foreign",
+    "where",
+    "when",
+    "false",
+    "private",
+    "while",
+    "final",
+    "protected",
+    "forall",
+    "finally",
+    "public",
+    "exists",
+    "for",
+    "readonly",
+    "otherwise",
+    "datatype"
+
+    ]
+\f : B -> C. \g : A -> B . \x : A. f (g x)
+\f : (A -> R) -> R. \k : A -> R. f k
+                                            x : A, g : A -> B, f : B -> C |- g : A -> B x : A, g : A -> B, f : B -> C |- x : A
+                                            ------------------------------------------- --------------------------------------
+x : A, g : A -> B, f : B -> C |- f : B -> C x : A, g : A -> B, f : B -> C |- g x : B                                          
+------------------------------------------- ----------------------------------------------------------------------------------
+x : A, g : A -> B, f : B -> C |- f (g x) : C
+------------------------------------------------------------------------------------------------------------------------------
+g : A -> B, f : B -> C |- \x : A. f (g x) : A -> C
+------------------------------------------------------------------------------------------------------------------------------
+f : B -> C |- \g : A -> B. \x : A. f (g x) : (A -> B) -> A -> C
+------------------------------------------------------------------------------------------------------------------------------
+ |- \f : B -> C. \g : A -> B. \x : A. f (g x) : (B -> C) -> (A -> B) -> A -> C
+
+
+
+
+
+
+k : A -> R, f : (A -> R) -> R |- f : (A -> R) -> R k : A -> R, f : (A -> R) -> R |- k : A -> R
+-------------------------------------------------- -------------------------------------------
+k : A -> R, f : (A -> R) -> R |- f k : R
+----------------------------------------------------------------------------------------------
+f : (A -> R) -> R |- \k : A -> R. f k : (A -> R) -> R
+----------------------------------------------------------------------------------------------
+ |- \f : (A -> R) -> R. \k : A -> R. f k : (A -> R -> R) -> (A -> R) -> R
+
+
+
+
+
+
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.