Add dependent sums.

1 files changed, 62 insertions, 13 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index f9daa62..efe7857 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -22,18 +22,24 @@ data ObsTokenKind
   | OTProp
   | OTSet
   | OTNat
+  | OTFst
+  | OTSnd
+  | OTPoint
   | OTVoid
   | OTAbsurd
   -- Special symbols
   | OTUnit
-  | OTPoint
   -- Grouping symbols
   | OTPOpen
   | OTPClose
+  | OTAOpen
+  | OTAClose
   -- Definition characters
   | OTBackslash
   | OTThinArrow
   | OTFatArrow
+  | OTProduct
+  | OTComma
   | OTEqual
   | OTColon
 
@@ -44,15 +50,21 @@ Eq ObsTokenKind where
   OTProp == OTProp = True
   OTSet == OTSet = True
   OTNat == OTNat = True
-  OTUnit == OTUnit = True
+  OTFst == OTFst = True
+  OTSnd == OTSnd = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
+  OTUnit == OTUnit = True
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
+  OTAOpen == OTAOpen = True
+  OTAClose == OTAClose = True
   OTBackslash == OTBackslash = True
   OTThinArrow == OTThinArrow = True
   OTFatArrow == OTFatArrow = True
+  OTProduct == OTProduct = True
+  OTComma == OTComma = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
   _ == _ = False
@@ -68,15 +80,21 @@ TokenKind ObsTokenKind where
   tokValue OTProp s = ()
   tokValue OTSet s = ()
   tokValue OTNat s = stringToNatOrZ s
-  tokValue OTUnit s = ()
+  tokValue OTFst s = ()
+  tokValue OTSnd s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
+  tokValue OTUnit s = ()
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
+  tokValue OTAOpen s = ()
+  tokValue OTAClose s = ()
   tokValue OTBackslash s = ()
   tokValue OTThinArrow s = ()
   tokValue OTFatArrow s = ()
+  tokValue OTProduct s = ()
+  tokValue OTComma s = ()
   tokValue OTEqual s = ()
   tokValue OTColon s = ()
 
@@ -94,6 +112,9 @@ keywords : List (String, ObsTokenKind)
 keywords =
   [ ("Set", OTSet)
   , ("Prop", OTProp)
+  , ("fst", OTFst)
+  , ("snd", OTSnd)
+  , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
   ]
@@ -106,12 +127,15 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
           Nothing => Tok OTIdent s)
   ] ++ toTokenMap
   [ (digits, OTNat)
-  , (exact "*", OTPoint)
   , (exact "(", OTPOpen)
   , (exact ")", OTPClose)
+  , (exact "<", OTAOpen)
+  , (exact ">", OTAClose)
   , (exact "=>", OTFatArrow)
   , (exact "->", OTThinArrow)
   , (exact "\\", OTBackslash)
+  , (exact "**", OTProduct)
+  , (exact ",", OTComma)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
   ]
@@ -171,6 +195,16 @@ lambda = do
   name <- bounds $ match OTBackslash *> commit *> ident <* match OTFatArrow
   pure (Lambda name.bounds name.val)
 
+projFst : Grammar state ObsToken True (Syntax -> Syntax)
+projFst = do
+  fst <- bounds $ match OTFst <* commit
+  pure (Fst fst.bounds)
+
+projSnd : Grammar state ObsToken True (Syntax -> Syntax)
+projSnd = do
+  snd <- bounds $ match OTSnd <* commit
+  pure (Snd snd.bounds)
+
 botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
 botElim = do
   absurd <- bounds $ match OTAbsurd <* commit
@@ -178,7 +212,11 @@ botElim = do
 
 -- NOTE: these functions are all total.
 partial
-pi : Grammar state ObsToken True (Syntax -> Syntax)
+pi : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
+partial
+sigma : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
+partial
+pair : Grammar state ObsToken True Syntax -> Grammar state ObsToken True Syntax -> Grammar state ObsToken True Syntax
 partial
 term : Grammar state ObsToken True Syntax
 partial
@@ -190,14 +228,25 @@ exp : Grammar state ObsToken True Syntax
 partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)
 
-pi = do
-  decl <- bounds $ parens decl <* match OTThinArrow <* commit
-  pure (uncurry (Pi decl.bounds) decl.val)
-
-term = atomic <|> parens exp
-precGteApp = atomicNoSet <|> set <|> parens exp
-exp' = precGteApp <|> (botElim <*> term <*> term)
-exp = (pi <*> exp) <|> (lambda <*> exp) <|> (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
+pi decl = do
+  _ <- match OTThinArrow <* commit
+  Parser.Core.pure (uncurry (Pi decl.bounds) decl.val)
+
+sigma decl = do
+  _ <- match OTProduct <* commit
+  Parser.Core.pure (uncurry (Sigma decl.bounds) decl.val)
+
+pair fst snd = do
+  pair <- bounds $ [| MkPair (match OTAOpen *> fst <* match OTComma) (snd <* match OTAClose) |]
+  pure (uncurry (Pair pair.bounds) pair.val)
+
+term = atomic <|> pair exp exp <|> parens exp
+precGteApp = atomicNoSet <|> set <|> pair exp exp <|> parens exp
+exp' = precGteApp <|> (projFst <*> term) <|> (projSnd <*> term) <|> (botElim <*> term <*> term)
+exp =
+  (bounds (parens decl) >>= (\decl => (pi decl <|> sigma decl) <*> exp)) <|>
+  (lambda <*> exp) <|>
+  (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
 decl = [| MkPair ident (match OTColon *> commit *> exp) |]
 
 partial