Add Container types.

1 files changed, 62 insertions, 2 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index acb1360..7ce31c4 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -29,6 +29,11 @@ data ObsTokenKind
   | OTLeft
   | OTRight
   | OTCase
+  | OTContainer
+  | OTTag
+  | OTPosition
+  | OTNext
+  | OTSem
   | OTPoint
   | OTVoid
   | OTAbsurd
@@ -38,6 +43,7 @@ data ObsTokenKind
   | OTCastRefl
   -- Special symbols
   | OTUnit
+  | OTTriangle
   -- Grouping symbols
   | OTPOpen
   | OTPClose
@@ -45,6 +51,7 @@ data ObsTokenKind
   | OTAClose
   -- Definition characters
   | OTBackslash
+  | OTSlash
   | OTThinArrow
   | OTFatArrow
   | OTProduct
@@ -52,6 +59,7 @@ data ObsTokenKind
   | OTTilde
   | OTEqual
   | OTColon
+  | OTPipe
 
 Eq ObsTokenKind where
   OTNewlines == OTNewlines = True
@@ -66,6 +74,11 @@ Eq ObsTokenKind where
   OTLeft == OTLeft = True
   OTRight == OTRight = True
   OTCase == OTCase = True
+  OTContainer == OTContainer = True
+  OTTag == OTTag = True
+  OTPosition == OTPosition = True
+  OTNext == OTNext = True
+  OTSem == OTSem = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
@@ -74,11 +87,13 @@ Eq ObsTokenKind where
   OTCast == OTCast = True
   OTCastRefl == OTCastRefl = True
   OTUnit == OTUnit = True
+  OTTriangle == OTTriangle = True
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
   OTAOpen == OTAOpen = True
   OTAClose == OTAClose = True
   OTBackslash == OTBackslash = True
+  OTSlash == OTSlash = True
   OTThinArrow == OTThinArrow = True
   OTFatArrow == OTFatArrow = True
   OTProduct == OTProduct = True
@@ -86,6 +101,7 @@ Eq ObsTokenKind where
   OTTilde == OTTilde = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
+  OTPipe == OTPipe = True
   _ == _ = False
 
 TokenKind ObsTokenKind where
@@ -105,6 +121,11 @@ TokenKind ObsTokenKind where
   tokValue OTLeft s = ()
   tokValue OTRight s = ()
   tokValue OTCase s = ()
+  tokValue OTContainer s = ()
+  tokValue OTTag s = ()
+  tokValue OTPosition s = ()
+  tokValue OTNext s = ()
+  tokValue OTSem s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
@@ -113,11 +134,13 @@ TokenKind ObsTokenKind where
   tokValue OTCast s = ()
   tokValue OTCastRefl s = ()
   tokValue OTUnit s = ()
+  tokValue OTTriangle s = ()
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
   tokValue OTAOpen s = ()
   tokValue OTAClose s = ()
   tokValue OTBackslash s = ()
+  tokValue OTSlash s = ()
   tokValue OTThinArrow s = ()
   tokValue OTFatArrow s = ()
   tokValue OTProduct s = ()
@@ -125,6 +148,7 @@ TokenKind ObsTokenKind where
   tokValue OTTilde s = ()
   tokValue OTEqual s = ()
   tokValue OTColon s = ()
+  tokValue OTPipe s = ()
 
 ObsToken : Type
 ObsToken = Token ObsTokenKind
@@ -142,6 +166,11 @@ Show ObsToken where
   show (Tok OTLeft s) = "Left"
   show (Tok OTRight s) = "Right"
   show (Tok OTCase s) = "case"
+  show (Tok OTContainer s) = "Container"
+  show (Tok OTTag s) = "tag"
+  show (Tok OTPosition s) = "position"
+  show (Tok OTNext s) = "next"
+  show (Tok OTSem s) = "sem"
   show (Tok OTPoint s) = "tt"
   show (Tok OTVoid s) = "Void"
   show (Tok OTAbsurd s) = "absurd"
@@ -150,11 +179,13 @@ Show ObsToken where
   show (Tok OTCast s) = "cast"
   show (Tok OTCastRefl s) = "castRefl"
   show (Tok OTUnit s) = "()"
+  show (Tok OTTriangle s) = "<|"
   show (Tok OTPOpen s) = "("
   show (Tok OTPClose s) = ")"
   show (Tok OTAOpen s) = "<"
   show (Tok OTAClose s) = ">"
   show (Tok OTBackslash s) = "\\"
+  show (Tok OTSlash s) = "/"
   show (Tok OTThinArrow s) = "->"
   show (Tok OTFatArrow s) = "=>"
   show (Tok OTProduct s) = "**"
@@ -162,6 +193,7 @@ Show ObsToken where
   show (Tok OTTilde s) = "~"
   show (Tok OTEqual s) = "="
   show (Tok OTColon s) = ":"
+  show (Tok OTPipe s) = "|"
 
 identifier : Lexer
 identifier = alpha <+> many alphaNum
@@ -176,6 +208,11 @@ keywords =
   , ("Left", OTLeft)
   , ("Right", OTRight)
   , ("case", OTCase)
+  , ("Container", OTContainer)
+  , ("tag", OTTag)
+  , ("position", OTPosition)
+  , ("next", OTNext)
+  , ("sem", OTSem)
   , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
@@ -200,11 +237,13 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++
   , (exact "=>", OTFatArrow)
   , (exact "->", OTThinArrow)
   , (exact "\\", OTBackslash)
+  , (exact "/", OTSlash)
   , (exact "**", OTProduct)
   , (exact ",", OTComma)
   , (exact "~", OTTilde)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
+  , (exact "|", OTPipe)
   ]
 
 op : Type -> Type -> Nat -> Type
@@ -230,6 +269,11 @@ headForms =
   , (OTLeft, (0 ** uncurry 1 Left))
   , (OTRight, (0 ** uncurry 1 Right))
   , (OTCase, (4 ** uncurry 5 Case))
+  , (OTContainer, (2 ** uncurry 3 Container))
+  , (OTTag, (0 ** uncurry 1 Tag))
+  , (OTPosition, (0 ** uncurry 1 Position))
+  , (OTNext, (0 ** uncurry 1 Next))
+  , (OTSem, (2 ** uncurry 3 Sem))
   , (OTAbsurd, (1 ** uncurry 2 Absurd))
   , (OTRefl, (0 ** uncurry 1 Refl))
   , (OTTransp, (4 ** uncurry 5 Transp))
@@ -286,6 +330,8 @@ head : Grammar state ObsToken True (WithBounds Syntax)
 partial
 spine : Grammar state ObsToken True (WithBounds Syntax)
 partial
+container : Grammar state ObsToken True (WithBounds Syntax)
+partial
 equals : Grammar state ObsToken True (WithBounds Syntax)
 partial
 exp : Grammar state ObsToken True (WithBounds Syntax)
@@ -309,8 +355,21 @@ head =
 spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
   [| MkPair head (many (whitespace *> term)) |]
 
+container =
+  map (\bounds@(MkBounded (t, u) _ _) => case u of
+    Nothing => t
+    Just (p, f) => map (\_ => MkContainer t p f) bounds) $
+  bounds $
+  [| MkPair spine
+      (optional
+        [| MkPair
+            (whitespace *> match OTTriangle *> commit *> whitespace *> spine)
+            (whitespace *> match OTSlash *> commit *> whitespace *> spine)
+        |])
+  |]
+
 equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $
-  [| MkPair spine (optional (whitespace *> match OTTilde *> commit *> whitespace *> spine)) |]
+  [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |]
 
 exp =
   equals <|>
@@ -358,7 +417,8 @@ whitespaceIrrelevant a = case (a.val.kind) of
 mergeToks : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
 mergeToks (a :: tail@(b :: rest)) = case (a.val.kind, b.val.kind) of
   (OTSpaces, OTNat) => mergeBounds a b :: mergeToks rest
-  (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "")) (mergeBounds a b) :: mergeToks rest
+  (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "()")) (mergeBounds a b) :: mergeToks rest
+  (OTAOpen, OTPipe) => map (\_ => (Tok OTTriangle "<|")) (mergeBounds a b) :: mergeToks rest
   _ => a :: mergeToks tail
 mergeToks toks = toks