diff options
Diffstat (limited to 'src/Obs/Abstract.idr')
| -rw-r--r-- | src/Obs/Abstract.idr | 24 |
1 files changed, 24 insertions, 0 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 |