From 02cb45707da07d5e6faca92158d10a6e454a6bac Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Thu, 22 Dec 2022 00:02:23 +0000 Subject: Add Container types. --- src/Obs/Abstract.idr | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'src/Obs/Abstract.idr') 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 -- cgit v1.2.3