Add containers types.

Containers are syntactic sugar. They are also completely untested.

1 files changed, 22 insertions, 0 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