From a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 21 Dec 2022 20:32:56 +0000 Subject: Add sum types. --- src/Obs/Abstract.idr | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Obs/Abstract.idr') diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr index b8fca7b..03367dc 100644 --- a/src/Obs/Abstract.idr +++ b/src/Obs/Abstract.idr @@ -51,6 +51,23 @@ abstractSyntax ctx (Fst t) = do abstractSyntax ctx (Snd t) = do t <- abstractSyntaxBounds ctx t pure (Snd t) +abstractSyntax ctx (Sum a b) = do + a <- abstractSyntaxBounds ctx a + b <- abstractSyntaxBounds ctx b + pure (Sum a b) +abstractSyntax ctx (Left t) = do + t <- abstractSyntaxBounds ctx t + pure (Left t) +abstractSyntax ctx (Right t) = do + t <- abstractSyntaxBounds ctx t + pure (Right t) +abstractSyntax ctx (Case t s b f g) = do + t <- abstractSyntaxBounds ctx t + s <- abstractSyntaxBounds ctx s + b <- abstractSyntaxBounds ctx b + f <- abstractSyntaxBounds ctx f + g <- abstractSyntaxBounds ctx g + pure (Case t s b f g) abstractSyntax ctx Top = pure Top abstractSyntax ctx Point = pure Point abstractSyntax ctx Bottom = pure Bottom -- cgit v1.2.3