From 3649c9965e787c9cb0dc1cedc4400cdec4c5b8a2 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 26 Mar 2023 03:50:28 +0100
Subject: Add type checking.

Currently, there is Set in Set. Next step is to add universe levels.
---
 src/CC/Term/Parse.idr | 155 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 132 insertions(+), 23 deletions(-)

(limited to 'src/CC/Term/Parse.idr')

diff --git a/src/CC/Term/Parse.idr b/src/CC/Term/Parse.idr
index 3615956..5c8956a 100644
--- a/src/CC/Term/Parse.idr
+++ b/src/CC/Term/Parse.idr
@@ -4,40 +4,65 @@ import CC.Name
 import CC.Term
 import CC.Term.Raw
 
+import Data.Bool
 import Data.List
 
 import Text.Lexer
 import Text.Parser
 
+%hide Text.Parser.match
+
+-- Utilities -------------------------------------------------------------------
+
+expandBindList : Functor f => (f (Maybe Name), RawTerm) -> f RawBinding
+expandBindList (xs, t) = map (`Of` t) xs
+
 -- Tokens ----------------------------------------------------------------------
 
 data CCTokenKind
   = TIgnore
+  -- Variables
   | TIdent
-  -- Keywords
+  -- Let Syntax
   | TLet
-  -- Symbols
+  | TDef
+  | TSemi
+  -- Universes
+  | TSet
+  -- Abstraction
+  | TThinArrow
   | TLambda
-  | TPOpen
-  | TPClose
   | TComma
   | TFatArrow
-  | TDef
-  | TSemi
+  -- Symbols
+  | TUnderscore
+  | TColon
+  | TPOpen
+  | TPClose
 
 %name CCTokenKind k
 
 Eq CCTokenKind where
   TIgnore == TIgnore = True
+
   TIdent == TIdent = True
+
   TLet == TLet = True
+  TDef == TDef = True
+  TSemi == TSemi = True
+
+  TSet == TSet = True
+
+  TThinArrow == TThinArrow = True
   TLambda == TLambda = True
-  TPOpen == TPOpen = True
-  TPClose == TPClose = True
   TComma == TComma = True
   TFatArrow == TFatArrow = True
-  TDef == TDef = True
-  TSemi == TSemi = True
+
+  TUnderscore == TUnderscore = True
+  TColon == TColon = True
+  TPOpen == TPOpen = True
+  TPClose == TPClose = True
+
   _ == _ = False
 
 TokenKind CCTokenKind where
@@ -45,15 +70,45 @@ TokenKind CCTokenKind where
   TokType _ = ()
 
   tokValue TIgnore s = ()
+
   tokValue TIdent s = s
+
   tokValue TLet s = ()
+  tokValue TDef s = ()
+  tokValue TSemi s = ()
+
+  tokValue TSet s = ()
+
+  tokValue TThinArrow s = ()
   tokValue TLambda s = ()
-  tokValue TPOpen s = ()
-  tokValue TPClose s = ()
   tokValue TComma s = ()
   tokValue TFatArrow s = ()
-  tokValue TDef s = ()
-  tokValue TSemi s = ()
+
+  tokValue TUnderscore s = ()
+  tokValue TColon s = ()
+  tokValue TPOpen s = ()
+  tokValue TPClose s = ()
+
+Interpolation CCTokenKind where
+  interpolate TIgnore = "whitespace"
+
+  interpolate TIdent = "identifier"
+
+  interpolate TLet = #""let""#
+  interpolate TDef = #""=""#
+  interpolate TSemi = #"";""#
+
+  interpolate TSet = #""Set""#
+
+  interpolate TThinArrow = #""->""#
+  interpolate TLambda = #""\""#
+  interpolate TComma = #"",""#
+  interpolate TFatArrow = #""=>""#
+
+  interpolate TUnderscore = #""_""#
+  interpolate TColon = #"":""#
+  interpolate TPOpen = #""(""#
+  interpolate TPClose = #"")""#
 
 export
 CCToken : Type
@@ -68,47 +123,92 @@ identifier : Lexer
 identifier = alpha <+> many alphaNum
 
 keywords : List (String, CCTokenKind)
-keywords = [("let", TLet)]
+keywords = [("let", TLet), ("Set", TSet)]
 
 tokenMap : TokenMap CCToken
 tokenMap =
+  -- Ignored
   toTokenMap (map (, TIgnore) ignored) ++
+  -- Identifiers
   [(identifier, \s =>
     case lookup s keywords of
       Just kind => Tok kind s
       Nothing => Tok TIdent s)
   ] ++ toTokenMap [
+    -- Abstraction
+    (exact "->", TThinArrow),
     (exact "\\", TLambda),
     (exact "\x03BB", TLambda),
-    (exact "(", TPOpen),
-    (exact ")", TPClose),
     (exact ",", TComma),
     (exact "=>", TFatArrow),
+    -- Symbols
+    (exact "_", TUnderscore),
+    (exact ":", TColon),
+    (exact "(", TPOpen),
+    (exact ")", TPClose),
+    -- Let syntax (has to be after fat arrow)
     (exact "=", TDef),
     (exact ";", TSemi)
   ]
 
 -- Parser ----------------------------------------------------------------------
 
+match : (kind : CCTokenKind) -> Grammar state CCToken True (TokType kind)
+match k = terminal "expected \{k}" $
+  \t => if t.kind == k then Just $ tokValue k t.text else Nothing
+
 %tcinline
 parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty
-parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t)
+parens p = match TPOpen >> p >>= (\t => match TPClose *> pure t)
 
 parseIdent : Grammar state CCToken True Name
 parseIdent = MkName <$> (bounds $ match TIdent)
 
+parseBinder : Grammar state CCToken True (Maybe Name)
+parseBinder = either Just (const Nothing) <$> (parseIdent <||> match TUnderscore)
+
+%tcinline
+withBounds : Grammar state CCToken True RawTerm -> Grammar state CCToken True RawTerm
+withBounds p = Bounded <$> bounds p
+
+parseBindList : Grammar state CCToken True (List1 (Maybe Name))
+parseBindList = sepBy1 (match TComma) parseBinder
+
+parseAnnot : (commit : Bool) -> Grammar state CCToken True RawTerm
+parseMaybeAnnot : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm)
+parseAnnotArgs : (commit : Bool) -> Grammar state CCToken True (List1 (Maybe Name), RawTerm)
+parseOptArrow : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm)
+
 parseTerm : Grammar state CCToken True RawTerm
+parsePi : Grammar state CCToken True RawTerm
 parseLambda : Grammar state CCToken True RawTerm
 parseLet : Grammar state CCToken True RawTerm
+parseChain : Grammar state CCToken True RawTerm
 parseSpine : Grammar state CCToken True RawTerm
 parseAtom : Grammar state CCToken True RawTerm
 
-parseTerm = parseLambda <|> parseLet <|> parseSpine
+parseAnnot False = match TColon >> parseTerm
+parseAnnot True = match TColon >> commit >> parseTerm
+
+parseMaybeAnnot b = Just <$> parseAnnot b <|> pure Nothing
+
+parseAnnotArgs b = [| MkPair parseBindList (parseAnnot b) |]
+
+parseOptArrow False = Just <$> (match TThinArrow >> parseTerm) <|> pure Nothing
+parseOptArrow True = Just <$> (match TThinArrow >> commit >> parseTerm) <|> pure Nothing
+
+parseTerm = withBounds (parsePi <|> parseLambda <|> parseLet <|> parseChain)
+
+parsePi = do
+  dom <- parens (parseAnnotArgs False)
+  match TThinArrow
+  cod <- parseTerm
+  pure $ foldr1By Pi (flip Pi cod) $ expandBindList dom
 
 parseLambda = do
   match TLambda
   commit
-  names <- sepBy1 (match TComma >> commit) parseIdent
+  names <- parseBindList
   commit
   match TFatArrow
   commit
@@ -120,19 +220,28 @@ parseLet = do
   commit
   n <- parseIdent
   commit
+  ty <- parseMaybeAnnot True
   match TDef
   commit
   t <- parseTerm
   match TSemi
   commit
   u <- parseTerm
-  pure $ Let n t u
+  pure $ Let n ty t u
+
+parseChain = do
+  spine <- parseSpine
+  maybeCod <- parseOptArrow True
+  pure $ case maybeCod of
+    Just cod => Pi (Nothing `Of` spine) cod
+    Nothing => spine
 
 parseSpine = foldl1 App <$> some parseAtom
 
 parseAtom =
-  (Var <$> parseIdent <* commit) <|>
-  (parens parseTerm)
+  withBounds (Var <$> parseIdent <* commit) <|>
+  withBounds (Set <$ match TSet <* commit) <|>
+  parens parseTerm
 
 parseSrc : Grammar state CCToken True RawTerm
 parseSrc = parseTerm <* eof
-- 
cgit v1.2.3