From a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 21 Dec 2022 20:32:56 +0000
Subject: Add sum types.

---
 src/Obs/Parser.idr | 59 ++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 44 insertions(+), 15 deletions(-)

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

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 0ccba86..acb1360 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -25,6 +25,10 @@ data ObsTokenKind
   | OTNat
   | OTFst
   | OTSnd
+  | OTEither
+  | OTLeft
+  | OTRight
+  | OTCase
   | OTPoint
   | OTVoid
   | OTAbsurd
@@ -58,6 +62,10 @@ Eq ObsTokenKind where
   OTNat == OTNat = True
   OTFst == OTFst = True
   OTSnd == OTSnd = True
+  OTEither == OTEither = True
+  OTLeft == OTLeft = True
+  OTRight == OTRight = True
+  OTCase == OTCase = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
@@ -93,6 +101,10 @@ TokenKind ObsTokenKind where
   tokValue OTNat s = stringToNatOrZ s
   tokValue OTFst s = ()
   tokValue OTSnd s = ()
+  tokValue OTEither s = ()
+  tokValue OTLeft s = ()
+  tokValue OTRight s = ()
+  tokValue OTCase s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
@@ -126,6 +138,10 @@ Show ObsToken where
   show (Tok OTNat s) = s
   show (Tok OTFst s) = "fst"
   show (Tok OTSnd s) = "snd"
+  show (Tok OTEither s) = "Either"
+  show (Tok OTLeft s) = "Left"
+  show (Tok OTRight s) = "Right"
+  show (Tok OTCase s) = "case"
   show (Tok OTPoint s) = "tt"
   show (Tok OTVoid s) = "Void"
   show (Tok OTAbsurd s) = "absurd"
@@ -156,6 +172,10 @@ keywords =
   , ("Prop", OTProp)
   , ("fst", OTFst)
   , ("snd", OTSnd)
+  , ("Either", OTEither)
+  , ("Left", OTLeft)
+  , ("Right", OTRight)
+  , ("case", OTCase)
   , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
@@ -195,18 +215,26 @@ uncurry : (n : _) -> op a b n -> Vect n a -> b
 uncurry 0     f []        = f
 uncurry (S n) f (x :: xs) = uncurry n (f x) xs
 
-headForms : List (ObsTokenKind, (n ** (Vect n (WithBounds Syntax) -> Syntax)))
+termForms : List (ObsTokenKind, Syntax)
+termForms =
+  [ (OTPoint, Point)
+  , (OTVoid, Bottom)
+  , (OTUnit, Top)
+  ]
+
+headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax)))
 headForms =
-  [ (OTFst, (1 ** uncurry 1 Fst))
-  , (OTSnd, (1 ** uncurry 1 Snd))
-  , (OTPoint, (0 ** uncurry 0 Point))
-  , (OTVoid, (0 ** uncurry 0 Bottom))
-  , (OTAbsurd, (2 ** uncurry 2 Absurd))
-  , (OTRefl, (1 ** uncurry 1 Refl))
-  , (OTTransp, (5 ** uncurry 5 Transp))
-  , (OTCast, (3 ** uncurry 3 Cast))
-  , (OTCastRefl, (1 ** uncurry 1 CastId))
-  , (OTUnit, (0 ** uncurry 0 Top))
+  [ (OTFst, (0 ** uncurry 1 Fst))
+  , (OTSnd, (0 ** uncurry 1 Snd))
+  , (OTEither, (1 ** uncurry 2 Sum))
+  , (OTLeft, (0 ** uncurry 1 Left))
+  , (OTRight, (0 ** uncurry 1 Right))
+  , (OTCase, (4 ** uncurry 5 Case))
+  , (OTAbsurd, (1 ** uncurry 2 Absurd))
+  , (OTRefl, (0 ** uncurry 1 Refl))
+  , (OTTransp, (4 ** uncurry 5 Transp))
+  , (OTCast, (2 ** uncurry 3 Cast))
+  , (OTCastRefl, (0 ** uncurry 1 CastId))
   ]
 
 declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2))
@@ -265,7 +293,8 @@ exp : Grammar state ObsToken True (WithBounds Syntax)
 noSortsTerm =
   parens exp <|>
   var <|>
-  bounds (map (uncurry Pair) (pair exp))
+  bounds (map (uncurry Pair) (pair exp)) <|>
+  bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
 
 term = noSortsTerm <|> map (map Sort) noArgSort
 
@@ -274,7 +303,7 @@ head =
   map (map Sort) sort <|>
   bounds
     (choiceMap
-      (\(hd, (n ** f)) => match hd *> commit *> [| f (count n (whitespace *> term)) |])
+      (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |])
       headForms)
 
 spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
@@ -306,7 +335,7 @@ partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
-    [| MkPair (decl exp) (optional whitespace *> match OTNewlines *> def) |]
+    [| MkPair (decl exp <* commit) (optional whitespace *> match OTNewlines *> def <* commit) |]
     (\((name, ty), (name', tm)) =>
       if name.val == name'.val
         then pure (MkDefinition {name = name, ty, tm})
@@ -316,7 +345,7 @@ partial
 file : Grammar state ObsToken False (List Definition)
 file =
   optional (whitespace *> match OTNewlines) *>
-  sepEndBy (optional whitespace *> match OTNewlines) fullDef <*
+  sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) <*
   eof
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
-- 
cgit v1.2.3