From ff4c5f15f354aa8da7bb5868d913dbbef23832a3 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 16:36:09 +0000
Subject: Add dependent products.

---
 src/Obs/Parser.idr | 95 +++++++++++++++++++++++++++++++++---------------------
 1 file changed, 58 insertions(+), 37 deletions(-)

(limited to 'src/Obs/Parser.idr')

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 67446bf..c9705fb 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -36,25 +36,31 @@ data ObsTokenKind
   | OTPOpen
   | OTPClose
   -- Definition characters
+  | OTBackslash
+  | OTThinArrow
+  | OTFatArrow
   | OTEqual
   | OTColon
 
 Eq ObsTokenKind where
   OTNewline == OTNewline = True
-  OTIgnore  == OTIgnore  = True
-  OTIdent   == OTIdent   = True
-  OTProp    == OTProp    = True
-  OTSet     == OTSet     = True
-  OTNat     == OTNat     = True
-  OTUnit    == OTUnit    = True
-  OTPoint   == OTPoint   = True
-  OTVoid    == OTVoid    = True
-  OTAbsurd  == OTAbsurd  = True
-  OTPOpen   == OTPOpen   = True
-  OTPClose  == OTPClose  = True
-  OTEqual   == OTEqual   = True
-  OTColon   == OTColon   = True
-  _         == _         = False
+  OTIgnore == OTIgnore = True
+  OTIdent == OTIdent = True
+  OTProp == OTProp = True
+  OTSet == OTSet = True
+  OTNat == OTNat = True
+  OTUnit == OTUnit = True
+  OTPoint == OTPoint = True
+  OTVoid == OTVoid = True
+  OTAbsurd == OTAbsurd = True
+  OTPOpen == OTPOpen = True
+  OTPClose == OTPClose = True
+  OTBackslash == OTBackslash = True
+  OTThinArrow == OTThinArrow = True
+  OTFatArrow == OTFatArrow = True
+  OTEqual == OTEqual = True
+  OTColon == OTColon = True
+  _ == _ = False
 
 TokenKind ObsTokenKind where
   TokType OTIdent = String
@@ -62,19 +68,22 @@ TokenKind ObsTokenKind where
   TokType _     = ()
 
   tokValue OTNewline s = ()
-  tokValue OTIgnore  s = ()
-  tokValue OTIdent   s = s
-  tokValue OTProp    s = ()
-  tokValue OTSet     s = ()
-  tokValue OTNat     s = stringToNatOrZ s
-  tokValue OTUnit    s = ()
-  tokValue OTPoint   s = ()
-  tokValue OTVoid    s = ()
-  tokValue OTAbsurd  s = ()
-  tokValue OTPOpen   s = ()
-  tokValue OTPClose  s = ()
-  tokValue OTEqual   s = ()
-  tokValue OTColon   s = ()
+  tokValue OTIgnore s = ()
+  tokValue OTIdent s = s
+  tokValue OTProp s = ()
+  tokValue OTSet s = ()
+  tokValue OTNat s = stringToNatOrZ s
+  tokValue OTUnit s = ()
+  tokValue OTPoint s = ()
+  tokValue OTVoid s = ()
+  tokValue OTAbsurd s = ()
+  tokValue OTPOpen s = ()
+  tokValue OTPClose s = ()
+  tokValue OTBackslash s = ()
+  tokValue OTThinArrow s = ()
+  tokValue OTFatArrow s = ()
+  tokValue OTEqual s = ()
+  tokValue OTColon s = ()
 
 ObsToken : Type
 ObsToken = Token ObsTokenKind
@@ -105,6 +114,9 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
   , (exact "*", OTPoint)
   , (exact "(", OTPOpen)
   , (exact ")", OTPClose)
+  , (exact "=>", OTFatArrow)
+  , (exact "->", OTThinArrow)
+  , (exact "\\", OTBackslash)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
   ]
@@ -121,9 +133,7 @@ ident : Grammar state ObsToken True (WithBounds String)
 ident = bounds $ match OTIdent
 
 var : Grammar state ObsToken True Syntax
-var = do
-  id <- ident <* commit
-  pure (Var id.bounds id.val)
+var = [| Var (ident <* commit) |]
 
 prop : Grammar state ObsToken True Syntax
 prop = do
@@ -161,6 +171,11 @@ set = do
   i <- [| mergeBounds (bounds $ match OTSet) (bounds $ map Set $ option 0 $ match OTNat) |] <* commit
   pure (Sort i.bounds i.val)
 
+lambda : Grammar state ObsToken True (Syntax -> Syntax)
+lambda = do
+  name <- bounds $ match OTBackslash *> commit *> ident <* match OTFatArrow
+  pure (Lambda name.bounds name.val)
+
 botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
 botElim = do
   absurd <- bounds $ match OTAbsurd <* commit
@@ -168,21 +183,27 @@ botElim = do
 
 -- NOTE: these functions are all total.
 partial
+pi : Grammar state ObsToken True (Syntax -> Syntax)
+partial
 term : Grammar state ObsToken True Syntax
-
 partial
 precGteApp : Grammar state ObsToken True Syntax
-
+partial
+exp' : Grammar state ObsToken True Syntax
 partial
 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)
-
-partial
-decl : Grammar state ObsToken True (WithBounds String, Syntax)
-decl = [| MkPair ident (commit *> match OTColon *> exp) |]
+exp' = precGteApp <|> (botElim <*> term <*> term)
+exp = (pi <*> exp) <|> (lambda <*> exp) <|> (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
+decl = [| MkPair ident (match OTColon *> commit *> exp) |]
 
 partial
 def : Grammar state ObsToken True (WithBounds String, Syntax)
-- 
cgit v1.2.3