Add containers types.

Containers are syntactic sugar. They are also completely untested.

1 files changed, 178 insertions, 26 deletions

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))