Add containers types.

Containers are syntactic sugar. They are also completely untested.

1 files changed, 58 insertions, 44 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index bd4139c..d0a9fb8 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -35,6 +35,11 @@ data ObsTokenKind
   -- Head Forms
   | OTFst
   | OTSnd
+  | OTMkContainer
+  | OTShape
+  | OTPosition
+  | OTNextIndex
+  | OTExtension
   | OTAbsurd
   | OTRefl
   | OTTransp
@@ -45,6 +50,8 @@ data ObsTokenKind
   -- Decl Forms
   | OTThinArrow
   | OTProduct
+  -- Special Forms
+  | OTContainer
   -- Lambda Form
   | OTBackslash
   | OTFatArrow
@@ -78,6 +85,11 @@ Eq ObsTokenKind where
 
   OTFst == OTFst = True
   OTSnd == OTSnd = True
+  OTMkContainer == OTMkContainer = True
+  OTShape == OTShape = True
+  OTPosition == OTPosition = True
+  OTNextIndex == OTNextIndex = True
+  OTExtension == OTExtension = True
   OTAbsurd == OTAbsurd = True
   OTRefl == OTRefl = True
   OTTransp == OTTransp = True
@@ -89,6 +101,8 @@ Eq ObsTokenKind where
   OTThinArrow == OTThinArrow = True
   OTProduct == OTProduct = True
 
+  OTContainer == OTContainer = True
+
   OTBackslash == OTBackslash = True
   OTFatArrow == OTFatArrow = True
 
@@ -123,6 +137,11 @@ Show ObsTokenKind where
 
   show OTFst = "fst"
   show OTSnd = "snd"
+  show OTMkContainer = "MkContainer"
+  show OTShape = "Shape"
+  show OTPosition = "Position"
+  show OTNextIndex = "nextIndex"
+  show OTExtension = "extension"
   show OTAbsurd = "absurd"
   show OTRefl = "refl"
   show OTTransp = "transp"
@@ -134,6 +153,8 @@ Show ObsTokenKind where
   show OTThinArrow = "->"
   show OTProduct = "**"
 
+  show OTContainer = "Container"
+
   show OTBackslash = "\\"
   show OTFatArrow = "=>"
 
@@ -170,6 +191,11 @@ TokenKind ObsTokenKind where
 
   tokValue OTFst s = ()
   tokValue OTSnd s = ()
+  tokValue OTMkContainer s = ()
+  tokValue OTShape s = ()
+  tokValue OTPosition s = ()
+  tokValue OTNextIndex s = ()
+  tokValue OTExtension s = ()
   tokValue OTAbsurd s = ()
   tokValue OTRefl s = ()
   tokValue OTTransp s = ()
@@ -181,6 +207,8 @@ TokenKind ObsTokenKind where
   tokValue OTThinArrow s = ()
   tokValue OTProduct s = ()
 
+  tokValue OTContainer s = ()
+
   tokValue OTBackslash s = ()
   tokValue OTFatArrow s = ()
 
@@ -198,47 +226,10 @@ ObsToken : Type
 ObsToken = Token ObsTokenKind
 
 Show ObsToken where
-  show (Tok OTNewlines s) = "\\n"
-  show (Tok OTSpaces s) = " "
-
   show (Tok OTIdent s) = s
-
-  show (Tok OTProp s) = "Prop"
-  show (Tok OTSet s) = "Set"
   show (Tok OTNat s) = s
 
-  show (Tok OTBool s) = "Bool"
-  show (Tok OTTrue s) = "True"
-  show (Tok OTFalse s) = "False"
-  show (Tok OTUnit s) = "()"
-  show (Tok OTPoint s) = "tt"
-  show (Tok OTVoid s) = "Void"
-
-  show (Tok OTFst s) = "fst"
-  show (Tok OTSnd s) = "snd"
-  show (Tok OTAbsurd s) = "absurd"
-  show (Tok OTRefl s) = "refl"
-  show (Tok OTTransp s) = "transp"
-  show (Tok OTCast s) = "cast"
-  show (Tok OTCastRefl s) = "castRefl"
-
-  show (Tok OTIf s) = "if"
-
-  show (Tok OTThinArrow s) = "->"
-  show (Tok OTProduct s) = "**"
-
-  show (Tok OTBackslash s) = "\\"
-  show (Tok OTFatArrow s) = "=>"
-
-  show (Tok OTPOpen s) = "("
-  show (Tok OTPClose s) = ")"
-  show (Tok OTAOpen s) = "<"
-  show (Tok OTAClose s) = ">"
-
-  show (Tok OTComma s) = ","
-  show (Tok OTTilde s) = "~"
-  show (Tok OTEqual s) = "="
-  show (Tok OTColon s) = ":"
+  show (Tok kind s) = show kind
 
 identifier : Lexer
 identifier = alpha <+> many alphaNum
@@ -256,6 +247,11 @@ keywords =
 
   , ("fst", OTFst)
   , ("snd", OTSnd)
+  , ("MkContainer", OTMkContainer)
+  , ("Shape", OTShape)
+  , ("Position", OTPosition)
+  , ("nextIndex", OTNextIndex)
+  , ("extension", OTExtension)
   , ("absurd", OTAbsurd)
   , ("refl", OTRefl)
   , ("transp", OTTransp)
@@ -263,6 +259,8 @@ keywords =
   , ("castRefl", OTCastRefl)
 
   , ("if", OTIf)
+
+  , ("Container", OTContainer)
   ]
 
 obsTokenMap : TokenMap ObsToken
@@ -313,6 +311,10 @@ headForms : List (ObsTokenKind, (n ** op (WithBounds Syntax) Syntax (S n)))
 headForms =
   [ (OTFst, (0 ** First))
   , (OTSnd, (0 ** Second))
+  , (OTMkContainer, (2 ** MkContainer))
+  , (OTShape, (0 ** Shape))
+  , (OTPosition, (0 ** Position))
+  , (OTNextIndex, (0 ** Next))
   , (OTAbsurd, (0 ** Absurd))
   , (OTRefl, (0 ** Refl))
   , (OTTransp, (4 ** Transp))
@@ -321,7 +323,7 @@ headForms =
   ]
 
 headLambdaForms : List (ObsTokenKind, (n ** (LambdaForm -> op (WithBounds Syntax) Syntax n)))
-headLambdaForms = [(OTIf, (3 ** If))]
+headLambdaForms = [(OTExtension, (1 ** Sem)), (OTIf, (3 ** If))]
 
 declForms : List (ObsTokenKind, (n ** op DeclForm (WithBounds Syntax -> Syntax) (S n)))
 declForms =
@@ -363,14 +365,18 @@ universe = bounds $
   map (const Prop) (match' OTProp <* commit) <|>
   map Set (match' OTSet *> commit *> option 0 (match' OTNat <* commit))
 
+termUniverse : Grammar state ObsToken True (WithBounds Universe)
+termUniverse = noArgUniverse <|> parens universe
+
 decl : Lazy (Grammar state ObsToken True (WithBounds Syntax)) ->
   Grammar state ObsToken True DeclForm
 decl p = [| MkDecl (ident <* whitespace <* match' OTColon <* whitespace) p |]
 
-pair : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (a, a)
-pair p =
+pair : Lazy (Grammar state ObsToken True (WithBounds Syntax)) ->
+  Grammar state ObsToken True (WithBounds Syntax)
+pair p = bounds $
   match' OTAOpen *> commit *>
-  [| MkPair
+  [| Pair
       (optional whitespace *> p <* optional whitespace <* match' OTComma <* commit)
       (optional whitespace *> p <* optional whitespace) |]
   <* match' OTAClose <* commit
@@ -397,7 +403,7 @@ exp : Grammar state ObsToken True (WithBounds Syntax)
 noUniversesTerm =
   parens exp <|>
   var <|>
-  bounds (map (uncurry Pair) (pair exp)) <|>
+  pair exp <|>
   bounds (choiceMap (\(k, s) => map (const s) (match' k)) termForms)
 
 term = noUniversesTerm <|> map (map Universe) noArgUniverse
@@ -415,7 +421,15 @@ head =
     (choiceMap
       (\(hd, (n ** f)) => match' hd *> commit *>
         pure (uncurry (S n) f) <*> count (S n) (whitespace *> term))
-      headForms)
+      headForms) <|>
+  bounds
+    (match OTContainer *> commit *>
+      [| Container
+          (whitespace *> term)
+          (whitespace *> term)
+          (whitespace *> termUniverse)
+          (whitespace *> termUniverse)
+      |])
 
 spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
   [| MkPair head (many (whitespace *> term)) |]