Add Container types.

9 files changed, 424 insertions, 7 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 03367dc..48709c1 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -68,6 +68,30 @@ abstractSyntax ctx (Case t s b f g) = do
   f <- abstractSyntaxBounds ctx f
   g <- abstractSyntaxBounds ctx g
   pure (Case t s b f g)
+abstractSyntax ctx (Container a s s') = do
+  a <- abstractSyntaxBounds ctx a
+  s <- abstractSyntaxBounds ctx s
+  s' <- abstractSyntaxBounds ctx s'
+  pure (Container a s s')
+abstractSyntax ctx (MkContainer t p f) = do
+  t <- abstractSyntaxBounds ctx t
+  p <- abstractSyntaxBounds ctx p
+  f <- abstractSyntaxBounds ctx f
+  pure (MkContainer t p f)
+abstractSyntax ctx (Tag t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Tag t)
+abstractSyntax ctx (Position t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Position t)
+abstractSyntax ctx (Next t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Next t)
+abstractSyntax ctx (Sem s a t) = do
+  s <- abstractSyntaxBounds ctx s
+  a <- abstractSyntaxBounds ctx a
+  t <- abstractSyntaxBounds ctx t
+  pure (Sem s a t)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 71b554c..cf5bb61 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -26,6 +26,8 @@ data Constructor : Nat -> Type where
   Sum    : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n
   Left   : NormalForm n -> Constructor n
   Right  : NormalForm n -> Constructor n
+  Container : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
+  MkContainer : NormalForm n -> NormalForm n -> NormalForm n -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
@@ -36,6 +38,9 @@ data Neutral : Nat -> Type where
   Fst    : Neutral n -> Neutral n
   Snd    : Neutral n -> Neutral n
   Case   : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
+  Tag    : Neutral n -> Neutral n
+  Position : Neutral n -> Neutral n
+  Next   : Neutral n -> Neutral n
   Absurd : Neutral n
   Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
   EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
@@ -79,6 +84,8 @@ eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
 eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
 eqCnstr (Left t) (Left t') = eqWhnf t t'
 eqCnstr (Right t) (Right t') = eqWhnf t t'
+eqCnstr (Container s a s' s'') (Container l a' l' l'') = s == l && eqWhnf a a' && s' == l' && s'' == l''
+eqCnstr (MkContainer t p f) (MkContainer t' p' f') = eqWhnf t t' && eqWhnf p p' && eqWhnf f f'
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
@@ -88,6 +95,9 @@ eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
 eqNtrl (Fst t) (Fst t') = eqNtrl t t'
 eqNtrl (Snd t) (Snd t') = eqNtrl t t'
 eqNtrl (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g'
+eqNtrl (Tag t) (Tag t') = eqNtrl t t'
+eqNtrl (Position t) (Position t') = eqNtrl t t'
+eqNtrl (Next t) (Next t') = eqNtrl t t'
 eqNtrl Absurd Absurd = True
 eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
 eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
@@ -164,6 +174,18 @@ prettyPrecCnstr d (Right t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "Right", prettyPrecWhnf App t]
+prettyPrecCnstr d (Container s a s' s'') =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Container", prettyPrecWhnf App a, prettyPrec App s', prettyPrec App s'']
+prettyPrecCnstr d (MkContainer t p f) =
+  parenthesise (d >= User 0) $
+  group $
+  fillSep
+    [ prettyPrecWhnf (User 0) t <++> pretty "<|"
+    , prettyPrecWhnf (User 0) p <++> pretty "/"
+    , prettyPrecWhnf (User 0) f
+    ]
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -184,6 +206,18 @@ prettyPrecNtrl d (Case t f g) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g]
+prettyPrecNtrl d (Tag t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "tag", prettyPrecNtrl App t]
+prettyPrecNtrl d (Position t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "position", prettyPrecNtrl App t]
+prettyPrecNtrl d (Next t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "next", prettyPrecNtrl App t]
 prettyPrecNtrl d Absurd = pretty "absurd"
 prettyPrecNtrl d (Equal _ t u) =
   parenthesise (d >= Equal) $
@@ -258,6 +292,8 @@ renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
 renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f)
 renameCnstr (Left t) f = Left (renameWhnf t f)
 renameCnstr (Right t) f = Right (renameWhnf t f)
+renameCnstr (Container s a s' s'') f = Container s (renameWhnf a f) s' s''
+renameCnstr (MkContainer t p u) f = MkContainer (renameWhnf t f) (renameWhnf p f) (renameWhnf u f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
@@ -266,6 +302,9 @@ renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
 renameNtrl (Fst t) f = Fst (renameNtrl t f)
 renameNtrl (Snd t) f = Snd (renameNtrl t f)
 renameNtrl (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf t' f)
+renameNtrl (Tag t) f = Tag (renameNtrl t f)
+renameNtrl (Position t) f = Position (renameNtrl t f)
+renameNtrl (Next t) f = Next (renameNtrl t f)
 renameNtrl Absurd f = Absurd
 renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
 renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index 919067e..b50b520 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -7,7 +7,7 @@ import Obs.NormalForm
 import Obs.Sort
 import Obs.Substitution
 
--- Substitution ----------------------------------------------------------------
+-- Utilities -------------------------------------------------------------------
 
 mergeName : String -> String -> String
 mergeName "" s' = s'
@@ -22,6 +22,38 @@ wkn (var :: vars) f =
     (pure $ Ntrl $ Var var FZ)
     (\i => pure $ rename !(wkn vars f i) FS)
 
+export
+expandContainerTy : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
+expandContainerTy s a s' s'' =
+  let tagTy : Constructor n
+      tagTy = Pi s (suc s') "i" a (cast s')
+  in
+  let posTy : Constructor (S n)
+      posTy =
+        Pi s (s' ~> suc s'') "i"
+          (weaken 1 a)
+          (Cnstr $ Pi s' (suc s'') "t"
+            (Ntrl $ App (Var "tag" 1) (Ntrl $ Var "i" 0))
+            (cast s''))
+  in
+  let nextTy : Constructor (2 + n)
+      nextTy =
+        Pi s (s' ~> suc s'' ~> s) "i"
+          (weaken 2 a)
+          (Cnstr $ Pi s' (suc s'' ~> s) "t"
+            (Ntrl $ App (Var "tag" 2) (Ntrl $ Var "i" 0))
+            (Cnstr $ Pi (suc s'') s "p"
+              (Ntrl $ App (App (Var "pos" 2) (Ntrl $ Var "i" 1)) (Ntrl $ Var "p" 0))
+              (weaken 5 a)))
+  in
+  Sigma (s ~> suc s') (lub (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s)) "tag"
+    (Cnstr tagTy) $
+  Cnstr $ Sigma (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s) "pos"
+    (Cnstr posTy)
+    (Cnstr nextTy)
+
+-- Substitution ----------------------------------------------------------------
+
 partial
 substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
 partial
@@ -39,6 +71,12 @@ doSnd      : NormalForm n -> Logging ann (NormalForm n)
 partial export
 doCase     : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 partial export
+doTag      : NormalForm n -> Logging ann (NormalForm n)
+partial export
+doPosition : NormalForm n -> Logging ann (NormalForm n)
+partial export
+doNext     : NormalForm n -> Logging ann (NormalForm n)
+partial export
 doEqual    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 partial
 doEqualL   : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
@@ -52,6 +90,10 @@ partial
 doCastR    : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 partial
 doCastU    : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
+partial export
+expandContainer : NormalForm n -> Logging ann (Constructor n)
+partial export
+contractContainer : NormalForm n -> Logging ann (Constructor n)
 
 substCnstr (Sort s) f = pure $ Sort s
 substCnstr (Pi s s' var a b) f = do
@@ -79,6 +121,14 @@ substCnstr (Left t) f = do
 substCnstr (Right t) f = do
   t <- subst t f
   pure (Right t)
+substCnstr (Container s a s' s'') f = do
+  a <- subst a f
+  pure (Container s a s' s'')
+substCnstr (MkContainer t p u) f = do
+  t <- subst t f
+  p <- subst p f
+  u <- subst u f
+  pure (MkContainer t p u)
 substCnstr Top f = pure $ Top
 substCnstr Bottom  f = pure $ Bottom
 
@@ -101,6 +151,15 @@ substNtrl (Case t u t') f = do
   u <- subst u f
   t' <- subst t' f
   doCase t u t'
+substNtrl (Tag t) f = do
+  t <- substNtrl t f
+  doTag t
+substNtrl (Position t) f = do
+  t <- substNtrl t f
+  doPosition t
+substNtrl (Next t) f = do
+  t <- substNtrl t f
+  doNext t
 substNtrl Absurd f = pure $ Ntrl Absurd
 substNtrl (Equal a t u) f = do
   a <- substNtrl a f
@@ -162,6 +221,21 @@ doCase (Cnstr (Left t)) f g = doApp f t
 doCase (Cnstr (Right t)) f g = doApp g t
 doCase (Cnstr t) f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal t
 
+doTag (Ntrl t) = pure $ Ntrl (Tag t)
+doTag Irrel = pure $ Irrel
+doTag (Cnstr (MkContainer t p f)) = pure t
+doTag (Cnstr t) = inScope "bug" $ inScope "wrong constructor in tag" $ fatal t
+
+doPosition (Ntrl t) = pure $ Ntrl (Position t)
+doPosition Irrel = pure $ Irrel
+doPosition (Cnstr (MkContainer t p f)) = pure p
+doPosition (Cnstr t) = inScope "bug" $ inScope "wrong constructor in position" $ fatal t
+
+doNext (Ntrl t) = pure $ Ntrl (Next t)
+doNext Irrel = pure $ Irrel
+doNext (Cnstr (MkContainer t p f)) = pure f
+doNext (Cnstr t) = inScope "bug" $ inScope "wrong constructor in next" $ fatal t
+
 doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u)
 doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel"
 doEqual (Cnstr (Sort Prop)) t u =
@@ -201,8 +275,14 @@ doEqual (Cnstr (Sum s s' a b)) t u = do
   fBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" ll)) (Cnstr (Lambda "y" lr))
   gBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" rl)) (Cnstr (Lambda "y" rr))
   doCase t (Cnstr (Lambda "x" fBody)) (Cnstr (Lambda "x" gBody))
+doEqual (Cnstr (Container s a s' s'')) t u = do
+  let containerTy = expandContainerTy s a s' s''
+  t <- expandContainer t
+  u <- expandContainer u
+  doEqual (Cnstr containerTy) (Cnstr t) (Cnstr u)
 doEqual (Cnstr Top) t u = pure $ Cnstr Top
 doEqual (Cnstr Bottom) t u = pure $ Cnstr Top
+doEqual (Cnstr a) t u = inScope "bug" $ inScope "wrong type under equal" $ fatal a
 
 doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u)
 doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel"
@@ -229,12 +309,15 @@ doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l')
     b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
     eqRhs <- doEqual (cast s') b b'
     pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == s' && l == l') of
+doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == l && s' == l') of
   False => pure $ Cnstr Bottom
   True => do
     eqLhs <- doEqual (cast s) a a'
     eqRhs <- doEqual (cast s) b b'
     pure $ Cnstr (Sigma Prop Prop "" eqLhs (weaken 1 eqRhs))
+doEqualU i (Container s a s' s'') (Container l a' l' l'') = case (s == l && s' == l' && s'' == l'') of
+  False => pure $ Cnstr Bottom
+  True => doEqual (cast s) a a'
 doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far
 
 doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t)
@@ -267,6 +350,51 @@ doCastU (Sum s s' a b) (Sum l l' a' b') t = do
   castL <- doCastL (weaken 1 a) (weaken 1 a') x
   castR <- doCastL (weaken 1 b) (weaken 1 b') x
   doCase t (Cnstr (Lambda "x" (Cnstr (Left castL)))) (Cnstr (Lambda "x" (Cnstr (Right castR))))
+doCastU (Container s a s' s'') (Container l b l' l'') t = do
+  t <- expandContainer t
+  let a = expandContainerTy s a s' s''
+  let b = expandContainerTy l b l' l''
+  t <- doCastU a b (Cnstr t)
+  t <- contractContainer t
+  pure $ Cnstr t
 doCastU Top Top t = pure Irrel
 doCastU Bottom Bottom t = pure Irrel
 doCastU a b t = pure $ Ntrl (CastU a b t)
+
+expandContainer t = do
+  tag <- doTag t
+  pos <- doPosition t
+  next <- doNext t
+  pure $ Pair tag (Cnstr $ Pair pos next)
+
+contractContainer t = do
+  tag <- doFst t
+  t <- doSnd t
+  pos <- doFst t
+  next <- doSnd t
+  pure $ MkContainer tag pos next
+
+-- More utilities --------------------------------------------------------------
+
+export
+tagTy : Sort -> NormalForm n -> Sort -> Constructor n
+tagTy s a s' = Pi s (suc s') "i" a (cast s')
+
+export
+positionTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> Logging ann (Constructor n)
+positionTy s a s' tag s'' = do
+  let i = Var "i" 0
+  tagI <- doApp (weaken 1 tag) (Ntrl i)
+  pure $ Pi s (s' ~> suc s'') "i" a (Cnstr $ Pi s' (suc s'') "t" tagI (cast s''))
+
+export
+nextTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> NormalForm n -> Logging ann (Constructor n)
+nextTy s a s' tag s'' pos = do
+  let i = Var "i" 0
+  tagI <- doApp (weaken 1 tag) (Ntrl i)
+  let t = Var "t" 0
+  posI <- doApp (weaken 1 pos) (Ntrl i)
+  posIT <- doApp (weaken 1 posI) (Ntrl t)
+  pure $ Pi s (s' ~> s'' ~> s) "i" a $
+  Cnstr $ Pi s' (s'' ~> s) "t" tagI $
+  Cnstr $ Pi s'' s "p" posIT (weaken 3 a)
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
 
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
index bbd6975..f76453a 100644
--- a/src/Obs/Sort.idr
+++ b/src/Obs/Sort.idr
@@ -35,7 +35,7 @@ Pretty Sort where
 
 -- Operations ------------------------------------------------------------------
 
-infix 5 ~>
+infixr 5 ~>
 
 public export
 suc : Sort -> Sort
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 9f64c38..d21569a 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -28,6 +28,13 @@ data Syntax : Type where
   Left   : WithBounds Syntax -> Syntax
   Right  : WithBounds Syntax -> Syntax
   Case   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  -- Containers
+  Container : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  MkContainer : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Tag : WithBounds Syntax -> Syntax
+  Position : WithBounds Syntax -> Syntax
+  Next : WithBounds Syntax -> Syntax
+  Sem : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- True
   Top    : Syntax
   Point  : Syntax
@@ -105,6 +112,34 @@ prettyPrec d (Case t s b f g) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
+prettyPrec d (Container a s s') =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s']
+prettyPrec d (MkContainer t p f) =
+  parenthesise (d >= User 0) $
+  group $
+  fillSep
+    [ prettyPrecBounds (User 0) t <++> pretty "<|"
+    , prettyPrecBounds (User 0) p <++> pretty "/"
+    , prettyPrecBounds (User 0) f
+    ]
+prettyPrec d (Tag t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "tag", prettyPrecBounds App t]
+prettyPrec d (Position t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "position", prettyPrecBounds App t]
+prettyPrec d (Next t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "next", prettyPrecBounds App t]
+prettyPrec d (Sem s a t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index be3721f..10f2129 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -29,6 +29,13 @@ data Term : Nat -> Type where
   Left   : WithBounds (Term n) -> Term n
   Right  : WithBounds (Term n) -> Term n
   Case   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  -- Containers
+  Container : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  MkContainer : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Tag : WithBounds (Term n) -> Term n
+  Position : WithBounds (Term n) -> Term n
+  Next : WithBounds (Term n) -> Term n
+  Sem : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- True
   Top    : Term n
   Point  : Term n
@@ -111,6 +118,34 @@ prettyPrec d (Case t s b f g) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
+prettyPrec d (Container a s s') =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s']
+prettyPrec d (MkContainer t p f) =
+  parenthesise (d >= User 0) $
+  group $
+  fillSep
+    [ prettyPrecBounds (User 0) t <++> pretty "<|"
+    , prettyPrecBounds (User 0) p <++> pretty "/"
+    , prettyPrecBounds (User 0) f
+    ]
+prettyPrec d (Tag t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "tag", prettyPrecBounds App t]
+prettyPrec d (Position t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "position", prettyPrecBounds App t]
+prettyPrec d (Next t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "next", prettyPrecBounds App t]
+prettyPrec d (Sem s a t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index b327397..f814f93 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -78,6 +78,8 @@ infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Norma
 partial
 inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a}
   -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort)
+partial
+inferSort : TyContext m n -> WithBounds (Term n) -> Logging ann Sort
 
 check ctx tm ty s = case (tm.val, ty) of
   (Lambda _ t, Cnstr (Pi s s' var a b)) => do
@@ -115,6 +117,22 @@ check ctx tm ty s = case (tm.val, ty) of
     inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
     pure (Cnstr $ Right t)
   (Right _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
+  (MkContainer t p f, Cnstr (Container s a s' s'')) => do
+    inScope "check" $ trace $ map (\_ => "checking container constructor") tm
+    let tagTy = tagTy s a s'
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking tag for type" <++> pretty tagTy) tm
+    t <- check ctx t (Cnstr tagTy) (s ~> suc s')
+    inScope "check" $ trace $ map (\_ => "tag is well typed") tm
+    positionTy <- positionTy s a s' t s''
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking position for type" <++> pretty positionTy) tm
+    p <- check ctx p (Cnstr positionTy) (s ~> s' ~> suc s'')
+    inScope "check" $ trace $ map (\_ => "position is well typed") tm
+    nextTy <- nextTy s a s' t s'' p
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking next for type" <++> pretty nextTy) tm
+    f <- check ctx f (Cnstr nextTy) (s ~> s' ~> s'' ~> s)
+    inScope "check" $ trace $ map (\_ => "next is well typed") tm
+    pure (Cnstr $ MkContainer t p f)
+  (MkContainer t p f, ty) => typeMismatch tm.bounds (pretty "container") (pretty ty)
   (_, _) => do
     inScope "check" $ trace $ map (\_ => "checking has fallen through") tm
     (v, a, s') <- infer ctx tm
@@ -193,8 +211,7 @@ infer ctx tm = case tm.val of
     (t, ty@(Cnstr (Sum s s' a b)), s'') <- infer ctx t
       | (_, ty, _) => inScope "wrong type to case" $ fatal (map (\_ => ty) tm)
     inScope "infer" $ trace $ map (\_ => pretty {ann} "sum has type" <++> pretty ty) tm
-    (Cnstr (Sort l), _) <- inferType ctx l
-      | (s, _) => typeMismatch l.bounds (pretty "sort") (pretty s)
+    l <- inferSort ctx l
     inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
     let ty' = Cnstr (Pi s'' (suc l) "x" ty (cast l))
     inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty ty') tm
@@ -214,6 +231,72 @@ infer ctx tm = case tm.val of
     out <- doApp out t
     inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty out) tm
     pure (res, out, l)
+  (Container a s' s'') => do
+    inScope "infer" $ trace $ map (\_ => "encountered container") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "index has type" <++> pretty a) tm
+    s' <- inferSort ctx s'
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "tag has sort" <++> pretty s') tm
+    s'' <- inferSort ctx s''
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "position has sort" <++> pretty s'') tm
+    pure (Cnstr (Container s a s' s''), cast (lub s (suc $ lub s' s'')), suc (lub s (suc $ lub s' s'')))
+  (MkContainer _ _ _) => inScope "cannot infer type" $ fatal tm
+  (Tag t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered tag") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
+    tag <- doTag t
+    let out = tagTy s a s'
+    pure (tag, Cnstr out, s ~> suc s')
+  (Position t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered position") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
+    tag <- doTag t
+    pos <- doPosition t
+    out <- positionTy s a s' tag s''
+    pure (pos, Cnstr out, s ~> s' ~> suc s'')
+  (Next t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered next") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
+    tag <- doTag t
+    pos <- doPosition t
+    next <- doNext t
+    out <- nextTy s a s' tag s'' pos
+    pure (next, Cnstr out, s ~> s' ~> s'' ~> s)
+  (Sem l b t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered sem") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "interpretting a container" <++> pretty ty) tm
+    l <- inferSort ctx l
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
+    let outTy = Cnstr (Pi s (suc l) "i" a (cast l))
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty outTy) tm
+    b <- check ctx b outTy (s ~> suc l)
+    inScope "infer" $ trace $ map (\_ => "output is well typed") tm
+    tag <- doTag t
+    pos <- doPosition t
+    next <- doNext t
+    let i = Ntrl (Var "i" 0)
+    tag <- doApp (weaken 1 tag) i
+    pos <- doApp (weaken 1 pos) i
+    next <- doApp (weaken 1 next) i
+    let t = Ntrl (Var "t" 0)
+    pos <- doApp (weaken 1 pos) t
+    next <- doApp (weaken 1 next) t
+    let p = Ntrl (Var "p" 0)
+    next <- doApp (weaken 1 next) p
+    out <- doApp (weaken 3 b) next
+    let out = Cnstr $ Lambda "i" $
+              Cnstr $ Sigma s' (s'' ~> l) "t" tag $
+              Cnstr $ Pi s'' l "p" pos out
+    let ty = Cnstr $ Pi s (suc (lub s' (s'' ~> l))) "i" a (cast (lub s' (s'' ~> l)))
+    pure (out, ty, suc (s ~> suc (lub s' (s'' ~> l))))
   Top => pure $ (Cnstr Top, cast Prop, Set 0)
   Point => pure $ (Irrel, Cnstr Top, Prop)
   Bottom  => pure $ (Cnstr Bottom, cast Prop, Set 0)
@@ -292,6 +375,11 @@ inferType ctx a = do
     | (_, ty, _) => tag a.bounds (pretty "sort") (pretty ty)
   pure (a, s)
 
+inferSort ctx a = do
+  (Cnstr (Sort s), _, _) <- infer ctx a
+    | (t, _, _) => inScope "infer" $ typeMismatch a.bounds (pretty "sort") (pretty t)
+  pure s
+
 -- Checking Definitions and Blocks ---------------------------------------------
 
 partial
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 20198c5..37bdf67 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -42,6 +42,11 @@ convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
   convert t2 u2 b s'
 -- In type Sum (manually expanding definition of doCase)
 convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b
+-- In type Container
+convert t u (Cnstr (Container s a s' s'')) (Set l) = do
+  t <- expandContainer t
+  u <- expandContainer u
+  convert (Cnstr t) (Cnstr u) (Cnstr (expandContainerTy s a s' s'')) (Set l)
 -- Default
 convert t u a s =
   inScope "invalid conversion" $ fatal $
@@ -57,6 +62,9 @@ convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) =
 convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) =
   pure $
   s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr (Container s a s' s'')) (Cnstr (Container l a' l' l'')) =
+  pure $
+  s == l && s' == l' && s'' == l'' && !(convertSet a a')
 convertSet (Cnstr Top) (Cnstr Top) = pure True
 convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True
 convertSet (Ntrl t) u = pure (Ntrl t == u)