Add containers types.

Containers are syntactic sugar. They are also completely untested.

9 files changed, 671 insertions, 75 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 4ef3f43..25c4210 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -67,6 +67,28 @@ abstractSyntax ctx (First {arg}) = do
 abstractSyntax ctx (Second {arg}) = do
   arg <- abstractSyntaxBounds ctx arg
   pure (Second {arg})
+abstractSyntax ctx (Container {input, output, shapeSort, positionSort}) = do
+  input <- abstractSyntaxBounds ctx input
+  output <- abstractSyntaxBounds ctx output
+  pure (Container {input, output, shapeSort, positionSort})
+abstractSyntax ctx (MkContainer {shape, position, next}) = do
+  shape <- abstractSyntaxBounds ctx shape
+  position <- abstractSyntaxBounds ctx position
+  next <- abstractSyntaxBounds ctx next
+  pure (MkContainer {shape, position, next})
+abstractSyntax ctx (Shape {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Shape {arg})
+abstractSyntax ctx (Position {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Position {arg})
+abstractSyntax ctx (Next {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Next {arg})
+abstractSyntax ctx (Sem {pred, arg}) = do
+  pred <- abstractLambda ctx pred
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Sem {pred, arg})
 abstractSyntax ctx Bool = pure Bool
 abstractSyntax ctx True = pure True
 abstractSyntax ctx False = pure False
diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
index 07060e6..1fc6454 100644
--- a/src/Obs/Logging.idr
+++ b/src/Obs/Logging.idr
@@ -43,8 +43,8 @@ record Message (ann : Type) where
   bounds : Maybe Bounds
   tags : List String
 
-pretty : Message ann -> Doc ann
-pretty msg =
+prettyMsg : Message ann -> Doc ann
+prettyMsg msg =
   let leader =
     hsep $
       [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
@@ -107,7 +107,7 @@ discard (End v) = Just v
 export
 logToTerminal : Level -> Logging AnsiStyle a -> IO a
 logToTerminal lvl (Cont msg l) = do
-  () <- if msg.lvl <= lvl then putDoc (pretty msg) else pure ()
+  () <- if msg.lvl <= lvl then putDoc (prettyMsg msg) else pure ()
   logToTerminal lvl l
 logToTerminal lvl Abort = exitFailure
 logToTerminal lvl (End v) = pure v
@@ -167,3 +167,19 @@ Loggable ann (Doc ann) where
 export
 Pretty x => Loggable ann x where
   log lvl msg = log lvl $ pretty {ann = ann} msg
+
+-- Loggings ----------------------------------------------------------------------
+
+export
+mismatch : (expected, got : Doc ann) -> Logging ann a
+mismatch lhs rhs = fatal $
+  hang 2 (pretty "expected" <+> line <+> lhs) <+> comma <+> line <+>
+  hang 2 (pretty "got" <+> line <+> align rhs)
+
+export
+typeMismatch : Doc ann -> Doc ann -> Logging ann a
+typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs
+
+export
+universeMismatch : Doc ann -> Doc ann -> Logging ann a
+universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 0b9d2b6..b4b9f94 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -2,6 +2,7 @@ module Obs.NormalForm
 
 import Data.List.Elem
 
+import Obs.Logging
 import Obs.Pretty
 import Obs.Substitution
 import Obs.Universe
@@ -265,3 +266,11 @@ PointedRename Relevance (\r => Maybe String) NormalForm where
   point {s = Irrelevant} _ _ = Irrel
   point {s = Relevant} var i =
     Ntrl (Var {var = maybe "" id var, i})
+
+-- Useful Constructors ---------------------------------------------------------
+
+public export
+record ContainerTy (ctx : List Relevance) where
+  constructor MkContainerTy
+  inputSort, shapeSort, positionSort, outputSort : Universe
+  input, output : TypeNormalForm ctx
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index 2ea6296..e36e57c 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -1,6 +1,7 @@
 module Obs.NormalForm.Normalise
 
 import Data.Bool
+import Data.List
 import Data.Nat
 
 import Decidable.Equality
@@ -57,6 +58,14 @@ map1 : {s' : _} ->
 map1 t u = subst' u (add (LogNormalForm' ann) (Left $ pure t) (Right . There))
 
 export
+MkLambda : {rel, domainRel : _} ->
+  (var : Maybe String) ->
+  (body : NormalForm rel (domainRel :: ctx)) ->
+  NormalForm (function domainRel rel) ctx
+MkLambda {rel = Irrelevant} var body = Irrel
+MkLambda {rel = Relevant} var body = Cnstr $ Lambda {var, body, domainRel}
+
+export
 doApp : {domainRel : _} ->
   (fun : NormalForm (function domainRel codomainRel) ctx) ->
   (arg : NormalForm domainRel ctx) ->
@@ -72,6 +81,17 @@ doApp (Cnstr t) arg = inScope "wrong constructor for apply" $ fatal t
 doApp Irrel arg = pure Irrel
 
 export
+MkPair : {indexRel, elementRel : Relevance}
+  -> (first : NormalForm indexRel ctx)
+  -> (second : NormalForm elementRel ctx)
+  -> NormalForm (pair indexRel elementRel) ctx
+MkPair {indexRel = Irrelevant, elementRel = Irrelevant, first, second} = Irrel
+MkPair {indexRel = Irrelevant, elementRel = Relevant, first, second} =
+  Cnstr $ Pair {indexRel = Irrelevant, elementRel = Relevant, prf = Relevant, first, second}
+MkPair {indexRel = Relevant, elementRel, first, second} =
+  Cnstr $ Pair {indexRel = Relevant, elementRel, prf = Relevant, first, second}
+
+export
 doFst : (firstRel, secondRel : _) ->
   (arg : NormalForm (pair firstRel secondRel) ctx) ->
   LogNormalForm ann firstRel ctx
@@ -97,6 +117,193 @@ doSnd firstRel Relevant arg =
   Cnstr t => inScope "wrong constructor for snd" $ fatal t
 
 export
+doContainer : ContainerTy ctx -> TypeNormalForm ctx
+doContainer container =
+  Cnstr $ Pi
+    { domainSort = container.inputSort
+    , codomainSort =
+        max (succ container.shapeSort)
+            (container.shapeSort ~>
+             max (succ container.positionSort) (container.positionSort ~> container.outputSort))
+    , domain = MkDecl Nothing container.input
+    , codomain = Cnstr $ Sigma
+      { indexSort = succ container.shapeSort
+      , elementSort = container.shapeSort ~>
+                      max (succ container.positionSort)
+                          (container.positionSort ~> container.outputSort)
+      , index = MkDecl (Just "Shape") (cast container.shapeSort)
+      , element = Cnstr $ Pi
+        { domainSort = container.shapeSort
+        , codomainSort = max (succ container.positionSort)
+                             (container.positionSort ~> container.outputSort)
+        , domain = MkDecl Nothing (Ntrl $ Var "Shape" Here)
+        , codomain = Cnstr $ Sigma
+          { indexSort = succ container.positionSort
+          , elementSort = container.positionSort ~> container.outputSort
+          , index = MkDecl (Just "Position") (cast container.positionSort)
+          , element = Cnstr $ Pi
+            { domainSort = container.positionSort
+            , codomainSort = container.outputSort
+            , domain = MkDecl Nothing (Ntrl $ Var "Position" Here)
+            , codomain = weaken [_, _, _, _, _] container.output
+            }
+          }
+        }
+      }
+    }
+
+export
+MkContainer : (inputRel, shapeRel : Relevance) ->
+  {outputRel : Relevance} ->
+  (shape : TypeNormalForm ctx) ->
+  (position : TypeNormalForm ctx) ->
+  (next : NormalForm outputRel ctx) ->
+  LogNormalForm ann Relevant ctx
+MkContainer {inputRel, shapeRel, outputRel, shape, position, next} = do
+  shape <- doApp (Sorted.weaken [inputRel] shape) (point Nothing Here)
+  position <- doApp (weaken [shapeRel, inputRel] position) (point Nothing (There Here))
+  position <- doApp position (point Nothing Here)
+  next <- doApp (weaken [shapeRel, inputRel] next) (point Nothing (There Here))
+  next <- doApp next (point Nothing Here)
+  pure $ MkLambda
+    { var = Nothing
+    , body = MkPair
+      { first = shape
+      , second = MkLambda
+        { var = Nothing
+        , body = MkPair
+          { first = position
+          , second = next
+          }
+        }
+      }
+    }
+
+export
+doShape : (inputRel : Relevance) ->
+  (arg : NormalForm Relevant ctx) ->
+  LogNormalForm ann Relevant ctx
+doShape inputRel arg =
+  let inputIndex : NormalForm inputRel (inputRel :: ctx)
+      inputIndex = point Nothing Here
+  in do
+  inputIndexed <- doApp (weaken [_] arg) inputIndex
+  body <- doFst Relevant Relevant inputIndexed
+
+  pure $ MkLambda {var = Nothing, body}
+
+export
+doPosition : (inputRel, shapeRel, outputRel : Relevance) ->
+  (arg : NormalForm Relevant ctx) ->
+  LogNormalForm ann Relevant ctx
+doPosition {inputRel, shapeRel, outputRel, arg} =
+  let inputIndex : NormalForm inputRel (inputRel :: ctx)
+      inputIndex = point Nothing Here
+  in
+  let shapeIndex : NormalForm shapeRel (shapeRel :: inputRel :: ctx)
+      shapeIndex = point Nothing Here
+  in do
+  inputIndexed <- doApp (weaken [_] arg) inputIndex
+
+  positionNextPair <- doSnd Relevant Relevant inputIndexed
+  let positionNextPair = weaken [_] positionNextPair
+
+  shapeIndexed <- doApp positionNextPair shapeIndex
+  body <- doFst Relevant outputRel shapeIndexed
+
+  pure $ MkLambda
+    { var = Nothing
+    , body = MkLambda {var = Nothing, body}
+    }
+
+export
+doNext : (inputRel, shapeRel, outputRel : Relevance) ->
+  (arg : NormalForm Relevant ctx) ->
+  LogNormalForm ann outputRel ctx
+doNext {inputRel, shapeRel, outputRel, arg} =
+  let inputIndex : NormalForm inputRel (inputRel :: ctx)
+      inputIndex = point Nothing Here
+  in
+  let shapeIndex : NormalForm shapeRel (shapeRel :: inputRel :: ctx)
+      shapeIndex = point Nothing Here
+  in do
+  inputIndexed <- doApp (weaken [_] arg) inputIndex
+
+  positionNextPair <- doSnd Relevant Relevant inputIndexed
+  let positionNextPair = weaken [_] positionNextPair
+
+  shapeIndexed <- doApp positionNextPair shapeIndex
+  body <- doSnd Relevant outputRel shapeIndexed
+
+  pure $ MkLambda
+    { var = Nothing
+    , body = MkLambda {var = Nothing, body}
+    }
+
+export
+doSem : (container : ContainerTy ctx) ->
+  (predSort : Universe) ->
+  (pred : TypeNormalForm (relevance container.outputSort :: ctx)) ->
+  (arg : NormalForm Relevant ctx) ->
+  LogNormalForm ann Relevant ctx
+doSem {container, predSort, pred, arg} = do
+  let inputVar = Nothing
+  let shapeVar = Nothing
+  let positionVar = Nothing
+
+  let inputDomain = MkDecl inputVar container.input
+
+  shape <- doShape {inputRel = relevance container.inputSort, arg}
+  let shape = Sorted.weaken [_] shape
+
+  shapeType <- doApp shape (point inputVar Here)
+  let shapeIndex = MkDecl shapeVar shapeType
+
+  position <- doPosition
+    { inputRel = relevance container.inputSort
+    , shapeRel = relevance container.shapeSort
+    , outputRel = relevance container.outputSort
+    , arg
+    }
+  let position = Sorted.weaken [_,_] position
+
+  positionType <- doApp position (point inputVar (There Here))
+  positionType <- doApp positionType (point shapeVar Here)
+  let positionDomain = MkDecl positionVar positionType
+
+  next <- doNext
+    { inputRel = relevance container.inputSort
+    , shapeRel = relevance container.shapeSort
+    , outputRel = relevance container.outputSort
+    , arg
+    }
+  let next = Sorted.weaken [_,_,_] next
+
+  next <- doApp next (point inputVar (There (There Here)))
+  next <- doApp next (point shapeVar (There Here))
+  next <- doApp next (point positionVar Here)
+
+  let f = add (LogNormalForm' ann) (Left $ pure next) (Right . There . There . There)
+  codomain <- subst' pred f
+
+  pure $ Cnstr $ Pi
+    { domainSort = container.inputSort
+    , codomainSort = max container.shapeSort (container.positionSort ~> predSort)
+    , domain = inputDomain
+    , codomain = Cnstr $ Sigma
+      { indexSort = container.shapeSort
+      , elementSort = container.positionSort ~> predSort
+      , index = shapeIndex
+      , element = Cnstr $ Pi
+        { domainSort = container.positionSort
+        , codomainSort = predSort
+        , domain = positionDomain
+        , codomain
+        }
+      }
+    }
+
+export
 doIf : {rel : _} ->
   (discriminant : NormalForm Relevant ctx) ->
   (true, false : NormalForm rel ctx) ->
@@ -574,3 +781,125 @@ subst' Irrel f = pure Irrel
 export
 subst : NormalForm ~|> Hom (LogNormalForm ann) (LogNormalForm ann)
 subst t f = subst' t (Left . f)
+
+export
+strengthen : (ctx' : List Relevance) ->
+  Map ctx' (LogNormalForm' ann) ctx ->
+  Map (ctx' ++ ctx) (LogNormalForm' ann) ctx
+strengthen [] f = Right
+strengthen (rel :: ctx) f = add (LogNormalForm' ann) (f Here) (strengthen ctx (f . There))
+
+-- Container Utilities ---------------------------------------------------------
+
+public export
+containerSort : (container : ContainerTy ctx) -> Universe
+containerSort container =
+  container.inputSort ~>
+  max (succ container.shapeSort)
+      (container.shapeSort ~>
+       max (succ container.positionSort) (container.positionSort ~> container.outputSort))
+
+export
+matchContainer : (type : TypeNormalForm ctx) -> Logging ann (ContainerTy ctx)
+matchContainer type@(Cnstr (Pi
+  { domainSort = inputSort
+  , codomainSort = inputCodomainSort
+  , domain = MkDecl _ input
+  , codomain = Cnstr (Sigma
+    { indexSort = succShapeSort@(Set _)
+    , elementSort = shapeElementSort
+    , index = MkDecl _ (Cnstr (Universe shapeSort))
+    , element = Cnstr (Pi
+      { domainSort = shapeSort'
+      , codomainSort = shapeCodomainSort
+      , domain = MkDecl _ (Ntrl (Var _ Here))
+      , codomain = Cnstr (Sigma
+        { indexSort = succPositionSort@(Set _)
+        , elementSort = positionElementSort
+        , index = MkDecl _ (Cnstr (Universe positionSort))
+        , element = Cnstr (Pi
+          { domainSort = positionSort'
+          , codomainSort = outputSort
+          , domain = MkDecl _ (Ntrl (Var _ Here))
+          , codomain = output'
+          })
+        })
+      })
+    })
+  })) = do
+  let Yes Refl = decEq
+                   ( inputCodomainSort
+                   , succShapeSort
+                   , shapeElementSort
+                   , shapeSort'
+                   , shapeCodomainSort
+                   , succPositionSort
+                   , positionElementSort
+                   , positionSort')
+                   ( max (succ shapeSort)
+                         (shapeSort ~> max (succ positionSort) (positionSort ~> outputSort))
+                   , succ shapeSort
+                   , shapeSort ~> max (succ positionSort) (positionSort ~> outputSort)
+                   , shapeSort
+                   , max (succ positionSort) (positionSort ~> outputSort)
+                   , succ positionSort
+                   , positionSort ~> outputSort
+                   , positionSort)
+    | No _ => typeMismatch (pretty "container") (pretty type)
+
+  output <- subst' output' $
+    strengthen [_, _, _, _, _] $
+    const $ Left $ typeMismatch (pretty "container") (pretty type)
+  pure (MkContainerTy {inputSort, shapeSort, positionSort, outputSort, input, output})
+matchContainer type = typeMismatch (pretty "container") (pretty type)
+
+export
+containerShapeType : ContainerTy ctx -> TypeNormalForm ctx
+containerShapeType container =
+  Cnstr $ Pi
+    { domainSort = container.inputSort
+    , codomainSort = succ container.shapeSort
+    , domain = MkDecl Nothing container.input
+    , codomain = cast container.shapeSort
+    }
+
+export
+containerPositionType : (container : ContainerTy ctx) ->
+  (shape : TypeNormalForm (relevance container.inputSort :: ctx)) ->
+  TypeNormalForm ctx
+containerPositionType container shape =
+  Cnstr $ Pi
+    { domainSort = container.inputSort
+    , codomainSort = container.shapeSort ~> succ container.positionSort
+    , domain = MkDecl Nothing container.input
+    , codomain = Cnstr $ Pi
+      { domainSort = container.shapeSort
+      , codomainSort = succ container.positionSort
+      , domain = MkDecl Nothing shape
+      , codomain = cast container.positionSort
+      }
+    }
+
+export
+containerNextType : (container : ContainerTy ctx) ->
+  (shape : TypeNormalForm (relevance container.inputSort :: ctx)) ->
+  (position :
+    TypeNormalForm (relevance container.shapeSort :: relevance container.inputSort :: ctx)) ->
+  TypeNormalForm ctx
+containerNextType container shape position =
+  Cnstr $ Pi
+    { domainSort = container.inputSort
+    , codomainSort = container.shapeSort ~> container.positionSort ~> container.outputSort
+    , domain = MkDecl Nothing container.input
+    , codomain = Cnstr $ Pi
+      { domainSort = container.shapeSort
+      , codomainSort = container.positionSort ~> container.outputSort
+      , domain = MkDecl Nothing shape
+      , codomain = Cnstr $ Pi
+        { domainSort = container.positionSort
+        , codomainSort = container.outputSort
+        , domain = MkDecl Nothing position
+        , codomain = weaken [_, _, _] container.output
+        }
+      }
+    }
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)) |]
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 74e15c2..868e761 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -38,6 +38,15 @@ data Syntax : Type where
   Pair : (first, second : WithBounds Syntax) -> Syntax
   First : (arg : WithBounds Syntax) -> Syntax
   Second : (arg : WithBounds Syntax) -> Syntax
+  -- Containers
+  Container : (input, output : WithBounds Syntax) ->
+    (shapeSort, positionSort : WithBounds Universe) ->
+    Syntax
+  MkContainer : (shape, position, next : WithBounds Syntax) -> Syntax
+  Shape : (arg : WithBounds Syntax) -> Syntax
+  Position : (arg : WithBounds Syntax) -> Syntax
+  Next : (arg : WithBounds Syntax) -> Syntax
+  Sem : (pred : LambdaForm) -> (arg : WithBounds Syntax) -> Syntax
   -- Booleans
   Bool : Syntax
   True : Syntax
@@ -86,6 +95,24 @@ prettyPrec d (Pair {first, second}) =
   prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
 prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
+prettyPrec d (Container {input, output, shapeSort, positionSort}) =
+  prettyApp d (pretty "Container") $
+  [ prettyPrecBounds App input
+  , prettyPrecBounds App output
+  , prettyPrec App shapeSort.val
+  , prettyPrec App positionSort.val
+  ]
+prettyPrec d (MkContainer {shape, position, next}) =
+  prettyApp d (pretty "MkContainer") $
+  [ prettyPrecBounds App shape
+  , prettyPrecBounds App position
+  , prettyPrecBounds App next
+  ]
+prettyPrec d (Shape {arg}) = prettyApp d (pretty "Shape") [prettyPrecBounds App arg]
+prettyPrec d (Position {arg}) = prettyApp d (pretty "Position") [prettyPrecBounds App arg]
+prettyPrec d (Next {arg}) = prettyApp d (pretty "nextIndex") [prettyPrecBounds App arg]
+prettyPrec d (Sem {pred, arg}) =
+  prettyApp d (pretty "extension") [prettyPrecLambda App pred, prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 8dad72c..5126d99 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -44,6 +44,15 @@ data Term : Nat -> Type where
   Pair : (first, second : WithBounds (Term n)) -> Term n
   First : (arg : WithBounds (Term n)) -> Term n
   Second : (arg : WithBounds (Term n)) -> Term n
+  -- Containers
+  Container : (input, output : WithBounds (Term n)) ->
+    (shapeSort, positionSort : WithBounds Universe) ->
+    Term n
+  MkContainer : (shape, position, next : WithBounds (Term n)) -> Term n
+  Shape : (arg : WithBounds (Term n)) -> Term n
+  Position : (arg : WithBounds (Term n)) -> Term n
+  Next : (arg : WithBounds (Term n)) -> Term n
+  Sem : (pred : LambdaForm n) -> (arg : WithBounds (Term n)) -> Term n
   -- Booleans
   Bool : Term n
   True : Term n
@@ -99,6 +108,24 @@ prettyPrec d (Pair {first, second}) =
   prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
 prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
+prettyPrec d (Container {input, output, shapeSort, positionSort}) =
+  prettyApp d (pretty "Container") $
+  [ prettyPrecBounds App input
+  , prettyPrecBounds App output
+  , prettyPrec App shapeSort.val
+  , prettyPrec App positionSort.val
+  ]
+prettyPrec d (MkContainer {shape, position, next}) =
+  prettyApp d (pretty "MkContainer") $
+  [ prettyPrecBounds App shape
+  , prettyPrecBounds App position
+  , prettyPrecBounds App next
+  ]
+prettyPrec d (Shape {arg}) = prettyApp d (pretty "Shape") [prettyPrecBounds App arg]
+prettyPrec d (Position {arg}) = prettyApp d (pretty "Position") [prettyPrecBounds App arg]
+prettyPrec d (Next {arg}) = prettyApp d (pretty "nextIndex") [prettyPrecBounds App arg]
+prettyPrec d (Sem {pred, arg}) =
+  prettyApp d (pretty "extension") [prettyPrecLambda App pred, prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index c3dcfbf..8369fe0 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -23,30 +23,8 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default total
 
--- Loggings ----------------------------------------------------------------------
-
-mismatch : (expected, got : Doc ann) -> Logging ann a
-mismatch lhs rhs = fatal $
-  hang 2 (pretty "expected" <+> line <+> lhs) <+> comma <+> line <+>
-  hang 2 (pretty "got" <+> line <+> align rhs)
-
-typeMismatch : Doc ann -> Doc ann -> Logging ann a
-typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs
-
-universeMismatch : Doc ann -> Doc ann -> Logging ann a
-universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs
-
 -- Utilities -------------------------------------------------------------------
 
-MkPair : (indexRel, elementRel : Relevance)
-  -> (first : NormalForm indexRel ctx)
-  -> (second : NormalForm elementRel ctx)
-  -> NormalForm (pair indexRel elementRel) ctx
-MkPair Irrelevant Irrelevant first second = Irrel
-MkPair Irrelevant Relevant first second =
-  Cnstr $ Pair {indexRel = Irrelevant, elementRel = Relevant, prf = Relevant, first, second}
-MkPair Relevant elementRel first second =
-  Cnstr $ Pair {indexRel = Relevant, elementRel, prf = Relevant, first, second}
 
 -- Checking and Inference ------------------------------------------------------
 
@@ -102,15 +80,14 @@ check' ctx sort
 
   let Yes Refl = decEq sort (domainSort ~> codomainSort)
     | No _ => fatal "internal universe mismatch"
+  rewrite functionRelevance domainSort codomainSort
 
   let bodyCtx = ctx ::< MkFreeVar domainSort domain.type var.val
 
   trace $ pretty {ann} "checking body has type" <++> pretty codomainSort
   body <- check bodyCtx codomainSort codomain body
 
-  pure $ case codomainSort of
-    Prop => Irrel
-    Set _ => Cnstr (Lambda {domainRel = _, var = Just var.val, body})
+  pure $ MkLambda {var = Just var.val, body}
 
 check' ctx sort type (Lambda {body}) = typeMismatch (pretty "function") (pretty type)
 
@@ -130,10 +107,58 @@ check' ctx sort
   trace $ pretty {ann} "checking second has type" <++> pretty element
   second <- check ctx elementSort element second
 
-  pure $ MkPair {indexRel = _, elementRel = _, first, second}
+  pure $ MkPair {first, second}
 
 check' ctx sort type (Pair {first, second}) = typeMismatch (pretty "pair type") (pretty type)
 
+check' ctx sort type (MkContainer {shape, position, next}) = do
+  container <- matchContainer type
+
+  let Yes Refl = decEq sort $
+        container.inputSort ~>
+        max (succ container.shapeSort)
+            (container.shapeSort ~>
+             max (succ container.positionSort) (container.positionSort ~> container.outputSort))
+    | No _ => fatal "internal universe mismatch"
+
+  info "encountered container constructor"
+
+  let shapeType = containerShapeType container
+  trace $ pretty {ann} "checking shape has type" <++> pretty shapeType
+  shape <- check ctx (container.inputSort ~> succ container.shapeSort) shapeType shape
+
+  shapeInstance <- doApp (weaken [relevance container.inputSort] shape) (point Nothing Here)
+
+  let positionType = containerPositionType container shapeInstance
+  trace $ pretty {ann} "checking position has type" <++> pretty positionType
+  position <- check
+    { tyCtx = ctx
+    , sort = container.inputSort ~> container.shapeSort ~> succ container.positionSort
+    , type = positionType
+    , term = position
+    }
+
+  let positionInstance = weaken [relevance container.shapeSort, relevance container.inputSort] position
+  positionInstance <- doApp positionInstance (point Nothing (There Here))
+  positionInstance <- doApp positionInstance (point Nothing Here)
+
+  let nextType = containerNextType container shapeInstance positionInstance
+  trace $ pretty {ann} "checking next has type" <++> pretty nextType
+  next <- check
+    { tyCtx = ctx
+    , sort = container.inputSort ~> container.shapeSort ~> container.positionSort ~> container.outputSort
+    , type = nextType
+    , term = next
+    }
+
+  MkContainer
+    { inputRel = relevance container.inputSort
+    , shapeRel = relevance container.shapeSort
+    , shape
+    , position
+    , next
+    }
+
 check' ctx sort type (Absurd {contradiction}) = do
   info "encountered absurd"
 
@@ -281,6 +306,133 @@ infer' ctx (Second {arg}) = do
 
     pure (elementSort ** (returnType, returnValue))
 
+infer' ctx (Container {input, output, shapeSort, positionSort}) = do
+  info "encountered container"
+
+  (inputSort, input) <- inferType ctx input
+  trace $ pretty {ann} "input type is" <++> pretty input
+
+  (outputSort, output) <- inferType ctx output
+  trace $ pretty {ann} "output type is" <++> pretty output
+
+  let shapeSort = shapeSort.val
+  let positionSort = positionSort.val
+
+  let containerSort = foldr1 max
+        [ inputSort ~> succ shapeSort
+        , inputSort ~> shapeSort ~> succ positionSort
+        , inputSort ~> shapeSort ~> positionSort ~> outputSort
+        ]
+  let container = MkContainerTy {inputSort, shapeSort, positionSort, outputSort, input, output}
+  let container = doContainer container
+
+  pure (succ containerSort ** (cast containerSort, container))
+
+infer' ctx (MkContainer {shape, position, next}) = fatal "cannot infer type of container"
+
+infer' ctx (Shape {arg}) = do
+  info "encountered Shape"
+
+  (sort ** (type, arg)) <- infer ctx arg
+  trace $ pretty {ann} "argument type is" <++> pretty type
+
+  container <- matchContainer type
+
+  let Yes Refl = decEq sort (containerSort container)
+    | No _ => fatal "internal universe mismatch"
+
+  let shapeType = containerShapeType container
+  shape <- doShape {inputRel = relevance container.inputSort, arg}
+
+  pure ((container.inputSort ~> succ container.shapeSort) ** (shapeType, shape))
+
+infer' ctx (Position {arg}) = do
+  info "encountered Position"
+
+  (sort ** (type, arg)) <- infer ctx arg
+  trace $ pretty {ann} "argument type is" <++> pretty type
+
+  container <- matchContainer type
+
+  let Yes Refl = decEq sort (containerSort container)
+    | No _ => fatal "internal universe mismatch"
+
+  shape <- doShape {inputRel = relevance container.inputSort, arg}
+  shape <- doApp (weaken [_] shape) (point Nothing Here)
+
+  let positionType = containerPositionType container shape
+  position <- doPosition
+    { inputRel = relevance container.inputSort
+    , shapeRel = relevance container.shapeSort
+    , outputRel = relevance container.outputSort
+    , arg
+    }
+
+  pure ((container.inputSort ~> container.shapeSort ~> succ container.positionSort) **
+        (positionType, position))
+
+infer' ctx (Next {arg}) =
+  let eq : (a, b, c, d : Universe) -> relevance (a ~> b ~> c ~> d) = relevance d
+      eq a b c d =
+        rewrite sym $ functionRelevance c d in
+        rewrite sym $ functionRelevance b (c ~> d) in
+        rewrite sym $ functionRelevance a (b ~> c ~> d) in
+        Refl
+  in do
+  info "encountered nextIndex"
+
+  (sort ** (type, arg)) <- infer ctx arg
+  trace $ pretty {ann} "argument type is" <++> pretty type
+
+  container <- matchContainer type
+
+  let Yes Refl = decEq sort (containerSort container)
+    | No _ => fatal "internal universe mismatch"
+
+  shape <- doShape {inputRel = relevance container.inputSort, arg}
+  shape <- doApp (weaken [_] shape) (point Nothing Here)
+
+  position <- doPosition
+    { inputRel = relevance container.inputSort
+    , shapeRel = relevance container.shapeSort
+    , outputRel = relevance container.outputSort
+    , arg
+    }
+  position <- doApp (weaken [_, _] position) (point Nothing (There Here))
+  position <- doApp position (point Nothing Here)
+
+  let nextType = containerNextType container shape position
+  nextIndex <- doNext
+    { inputRel = relevance container.inputSort
+    , shapeRel = relevance container.shapeSort
+    , outputRel = relevance container.outputSort
+    , arg
+    }
+
+  let next' = rewrite eq container.inputSort container.shapeSort container.positionSort container.outputSort in nextIndex
+
+  pure ((container.inputSort ~> container.shapeSort ~> container.positionSort ~> container.outputSort) **
+        (nextType, next'))
+
+infer' ctx (Sem {pred = MkLambda var pred, arg}) = do
+  info "encountered extension"
+
+  (sort ** (type, arg)) <- infer ctx arg
+  trace $ pretty {ann} "argument type is" <++> pretty type
+
+  container <- matchContainer type
+
+  let Yes Refl = decEq sort (containerSort container)
+    | No _ => fatal "internal universe mismatch"
+
+  let predCtx = ctx ::< MkFreeVar container.outputSort container.output var.val
+  (predSort, pred) <- inferType predCtx pred
+
+  let semSort = container.inputSort ~> max container.shapeSort (container.positionSort ~> predSort)
+  semType <- doSem container predSort pred arg
+
+  pure (succ semSort ** (cast semSort, semType))
+
 infer' ctx Bool = do
     info "encountered bool"
     pure (Set 1 ** (cast (Set 0), Cnstr Bool))
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 93812c1..28a3c18 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -88,8 +88,8 @@ convertCnstr
 
   pure (convertIndex && convertElement)
 convertCnstr
-  left@(Pair {indexRel, elementRel, prf = _, first, second})
-  right@(Pair
+  (Pair {indexRel, elementRel, prf = _, first, second})
+  (Pair
     { indexRel = indexRel'
     , elementRel = elementRel'
     , prf = _