Stuff

3 files changed, 185 insertions, 26 deletions

diff --git a/src/AST.hs b/src/AST.hs
index 42967bc..ba018f5 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -22,6 +22,8 @@ data Term
   | TIMax Term Term      -- ^ Maximum of two levels
   | TISucc Term          -- ^ Level + 1
 
+  | TAnnot (OfType Term Term)  -- ^ term : type
+
   -- Temporary stuff until we have proper inductive types:
   | TOne                   -- ^ The unit type
   | TUnit                  -- ^ The element of the unit type
@@ -31,4 +33,11 @@ data Term
   | TProj2 Term            -- ^ Second projection of a dependent pair
   deriving (Show)
 
+data Definition = Definition Name (OfType Term Term)
+  deriving (Show)
+
 type Env = Map Name Term
+
+data OfType a b = a :| b
+  deriving (Show)
+infix 1 :|
diff --git a/src/Parser.hs b/src/Parser.hs
new file mode 100644
index 0000000..7464d85
--- /dev/null
+++ b/src/Parser.hs
@@ -0,0 +1,138 @@
+module Parser (parseProgram) where
+
+import Control.Monad
+import Data.Char
+import Data.List (foldl')
+import Text.Parsec hiding (token)
+import Text.Parsec.Expr
+
+import AST
+
+
+type Parser = Parsec String ()
+
+parseProgram :: String -> String -> Either ParseError [Definition]
+parseProgram fname source = parse pProgram fname source
+
+pProgram :: Parser [Definition]
+pProgram = do
+  whitespaceTo0
+  choice
+    [eof >> return []
+    ,(:) <$> pDef <*> pProgram]
+
+-- | Assumes column 0
+pDef :: Parser Definition
+pDef = do
+  name <- pName
+  whitespace
+  token ":"
+  whitespace
+  typ <- pTerm
+  whitespaceTo0
+  name2 <- pName
+  when (name /= name2) $
+    fail $ "Definition of '" ++ name ++ "' followed by definition for '" ++ name2 ++ "'"
+  whitespace
+  token "="
+  whitespace
+  rhs <- pTerm
+  return (Definition name (rhs :| typ))
+
+pTerm :: Parser Term
+pTerm = buildExpressionParser optable pTermEAtom
+  where
+    optable =
+      [[Infix (token "->" >> return makePi) AssocRight
+       ,Infix (token "→" >> return makePi) AssocRight]
+      ,[Infix (token ":" >> return (\a b -> TAnnot (a :| b))) AssocNone]]
+
+makePi :: Term -> Term -> Term
+makePi (TAnnot (TVar x :| ty1)) ty2 = TPi x ty1 ty2
+makePi ty1 ty2 = TPi ";_" ty1 ty2
+
+pTermEAtom :: Parser Term
+pTermEAtom = pLambda <|> pApp
+
+pLambda :: Parser Term
+pLambda = do
+  token "\\" <|> token "λ"
+  whitespace
+  _ <- char '('
+  whitespace
+  x <- pName
+  whitespace
+  token ":"
+  whitespace
+  ty <- pTerm
+  whitespace
+  _ <- char ')'
+  whitespace
+  token "->"
+  rhs <- pTerm
+  return (TLam x ty rhs)
+
+pApp :: Parser Term
+pApp = do
+  e1 <- pAtom
+  args <- many (try (whitespace >> pTerm))
+  return (foldl' TApp e1 args)
+
+pAtom :: Parser Term
+pAtom = choice
+  [do _ <- char '('
+      whitespace
+      e <- pTerm
+      whitespace
+      _ <- char ')'
+      return e
+  ,TVar <$> pName]
+
+TODO TPair, TSigma ("%"). The rest are environment entries.
+
+pName :: Parser Name
+pName = do
+  name <- many1 pNameChar
+  guard (name `notElem` keywords)
+  return name
+  where
+    keywords = ["=", "->", "→", ":", "?", "\\", "λ", "∀", "..", "..."
+               ,"%"  -- for Sigma; hopefully temporary
+               ,"forall", "data", "import", "in", "let"]
+
+pNameChar :: Parser Char
+pNameChar = satisfy (\c -> not (isSpace c) && c `notElem` ".;{}()@\"")
+
+inlineWhite :: Parser ()
+inlineWhite = do
+  spaces
+  choice
+    [inlineComment
+    -- TODO: nested {- -} comments
+    ,return ()]
+
+inlineComment :: Parser ()
+inlineComment = token "--" >> manyTill anyChar newline >> return ()
+
+-- | Skips to the furthest point from here that can be reached without
+-- consuming any tokens, and without ending on column 0.
+whitespace :: Parser ()
+whitespace = do
+  inlineWhite
+  optional $
+    many newline >> (void space <|> inlineComment) >> whitespace
+
+-- | Skips as much whitespace as possible, and throws an error if that doesn't
+-- leave us on column 0.
+whitespaceTo0 :: Parser ()
+whitespaceTo0 = do
+  inlineWhite
+  choice
+    [eof
+    ,newline >> whitespaceTo0
+    ,do pos <- getPosition
+        when (sourceColumn pos /= 1) $
+          unexpected "indented code"]
+
+token :: String -> Parser ()
+token s = try $ string s >> (eof <|> void (lookAhead (satisfy (\c -> isSpace c || c `elem` ".;{}()@\""))))
diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs
index 4c05c4b..1406a67 100644
--- a/src/TypeCheck.hs
+++ b/src/TypeCheck.hs
@@ -3,22 +3,37 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DeriveFoldable #-}
-module TypeCheck where
+module TypeCheck (typeCheck, typeInfer) where
 
 import Control.Monad
-import Control.Monad.Trans.Class
-import Control.Monad.Trans.State.Strict
-import Control.Monad.Trans.Writer.CPS
-import Data.Foldable (toList)
-import Data.Map.Strict (Map)
+-- import Control.Monad.Trans.Class
+-- import Control.Monad.Trans.State.Strict
+-- import Control.Monad.Trans.Writer.CPS
+-- import Data.Foldable (toList)
+-- import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import Numeric.Natural
+-- import Numeric.Natural
 
 import AST
 
 
+typeCheck :: Env -> Term -> Term -> Either String Term
+typeCheck env typ term =
+  runTM (check env term typ)
+  -- runTM (check env term typ) >>= \case
+  --   ([], term') -> return term'
+  --   (_, _) -> error "Don't know how to solve constraints yet"
+
+typeInfer :: Env -> Term -> Either String (OfType Term Term)
+typeInfer env term =
+  runTM (infer env term)
+  -- runTM (infer env term) >>= \case
+  --   ([], jud) -> return jud
+  --   (_, _) -> error "Don't know how to solve constraints yet"
+
+
 -- | type checking monad
-newtype TM a = TM (WriterT (Bag Constr) (StateT Natural (Either String)) a)
+newtype TM a = TM ({- WriterT (Bag Constr) (StateT Natural ( -} Either String {- )) -} a)
   deriving stock (Functor)
   deriving newtype (Applicative, Monad)
 
@@ -31,28 +46,23 @@ data Constr = VarEq Name Term
             | LevelLeq Term Term
   deriving (Show)
 
-type Subst = Map Name Term
-
-runTM :: TM a -> Either String ([Constr], a)
-runTM (TM m) = do
-  (res, cs) <- evalStateT (runWriterT m) 0
-  return (toList cs, res)
+runTM :: TM a -> Either String a
+runTM (TM m) = m
+  -- (res, cs) <- evalStateT (runWriterT m) 0
+  -- return (toList cs, res)
 
-genId :: TM Natural
-genId = TM (lift (state (\i -> (i, i + 1))))
+-- genId :: TM Natural
+-- genId = TM (lift (state (\i -> (i, i + 1))))
 
-genName :: TM Name
-genName = ("." ++) . show <$> genId
+-- genName :: TM Name
+-- genName = ("." ++) . show <$> genId
 
 throw :: String -> TM a
-throw err = TM (lift (lift (Left err)))
+-- throw err = TM (lift (lift (Left err)))
+throw err = TM (Left err)
 
-emit :: Constr -> TM ()
-emit c = TM (tell (BOne c))
-
-data OfType a b = a :| b
-  deriving stock (Show)
-infix 1 :|
+-- emit :: Constr -> TM ()
+-- emit c = TM (tell (BOne c))
 
 check :: Env -> Term -> Term -> TM Term
 check env topTerm typ = case topTerm of
@@ -151,8 +161,10 @@ infer env = \case
   TSigma x a b -> do
     inferW env a >>= \case
       a' :| TSet lvlA -> do
-        inferW env b >>= \case
+        inferW (Map.insert x a' env) b >>= \case
           b' :| TSet lvlB -> do
+            when (x `freeIn` lvlB) $
+              throw $ "Variable " ++ show x ++ " escapes Sigma"
             return (TSigma x a' b' :| TSet (TIMax lvlA lvlB))
           _ :| tb -> throw $ "RHS of a Sigma not of type Set i, but: " ++ show tb
       _ :| ta -> throw $ "LHS type of a Sigma not of type Set i, but: " ++ show ta