Index normal forms with relevance.

- Remove container types.
- Replace sum types with booleans.
- Remove type annotation from absurd.
- Add original type as argument to cast.
- Make if (was case) take a lambda for the return type.

1 files changed, 14 insertions, 46 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 48709c1..b32af2d 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -51,54 +51,21 @@ 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
+abstractSyntax ctx Bool = pure Bool
+abstractSyntax ctx True = pure True
+abstractSyntax ctx False = pure False
+abstractSyntax ctx (If var a t f g) = do
+  a <- abstractSyntaxBounds (bind ctx var.val) a
   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 (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)
+  pure (If var a t f g)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
-abstractSyntax ctx (Absurd a t) = do
-  a <- abstractSyntaxBounds ctx a
+abstractSyntax ctx (Absurd t) = do
   t <- abstractSyntaxBounds ctx t
-  pure (Absurd a t)
+  pure (Absurd t)
 abstractSyntax ctx (Equal t u) = do
   t <- abstractSyntaxBounds ctx t
   u <- abstractSyntaxBounds ctx u
@@ -106,18 +73,19 @@ abstractSyntax ctx (Equal t u) = do
 abstractSyntax ctx (Refl t) = do
   t <- abstractSyntaxBounds ctx t
   pure (Refl t)
-abstractSyntax ctx (Transp t b u t' e) = do
+abstractSyntax ctx (Transp a t u t' e) = do
+  a <- abstractSyntaxBounds ctx a
   t <- abstractSyntaxBounds ctx t
-  b <- abstractSyntaxBounds ctx b
   u <- abstractSyntaxBounds ctx u
   t' <- abstractSyntaxBounds ctx t'
   e <- abstractSyntaxBounds ctx e
-  pure (Transp t b u t' e)
-abstractSyntax ctx (Cast b e t) = do
+  pure (Transp a t u t' e)
+abstractSyntax ctx (Cast a b e t) = do
+  a <- abstractSyntaxBounds ctx a
   b <- abstractSyntaxBounds ctx b
   e <- abstractSyntaxBounds ctx e
   t <- abstractSyntaxBounds ctx t
-  pure (Cast b e t)
+  pure (Cast a b e t)
 abstractSyntax ctx (CastId t) = do
   t <- abstractSyntaxBounds ctx t
   pure (CastId t)