From 06bd13433cb5e7edcff551454107c9d4e4d88f8f Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 5 Jan 2023 17:06:33 +0000
Subject: Add more program structure to normal forms.

---
 src/Obs/Abstract.idr | 46 +++++++++++++++++++++++++++++++---------------
 1 file changed, 31 insertions(+), 15 deletions(-)

(limited to 'src/Obs/Abstract.idr')

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 039f60e..4ef3f43 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -18,29 +18,45 @@ Context n = List (String, Fin n)
 bind : Context n -> String -> Context (S n)
 bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 
-abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))
 
+abstractDecl : Context n -> DeclForm -> Logging ann (DeclForm n)
+abstractDecl ctx (MkDecl var type) = do
+  type <- abstractSyntaxBounds ctx type
+  pure (MkDecl var type)
+
+abstractLambda : Context n -> LambdaForm -> Logging ann (LambdaForm n)
+abstractLambda ctx (MkLambda var body) = do
+  body <- abstractSyntaxBounds (bind ctx var.val) body
+  pure (MkLambda var body)
+
+abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntax ctx (Var {var}) = do
   let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
   pure (Var {var, i})
 abstractSyntax ctx (Universe {s}) = pure (Universe {s})
-abstractSyntax ctx (Pi {var, domain, codomain}) = do
-  domain <- abstractSyntaxBounds ctx domain
-  codomain <- abstractSyntaxBounds (bind ctx var.val) codomain
-  pure (Pi {var, domain, codomain})
-abstractSyntax ctx (Lambda {var, body}) = do
-  body <- abstractSyntaxBounds (bind ctx var.val) body
-  pure (Lambda {var, body})
+abstractSyntax ctx (Pi {domain, codomain}) = do
+  domain <- abstractDecl ctx domain
+
+  let ctx = bind ctx domain.var.val
+  codomain <- abstractSyntaxBounds ctx codomain
+
+  pure (Pi {domain, codomain})
+abstractSyntax ctx (Lambda {body}) = do
+  body <- abstractLambda ctx body
+  pure (Lambda {body})
 abstractSyntax ctx (App {fun, arg}) = do
   fun <- abstractSyntaxBounds ctx fun
   arg <- abstractSyntaxBounds ctx arg
   pure (App {fun, arg})
-abstractSyntax ctx (Sigma {var, index, element}) = do
-  index <- abstractSyntaxBounds ctx index
-  element <- abstractSyntaxBounds (bind ctx var.val) element
-  pure (Sigma {var, index, element})
+abstractSyntax ctx (Sigma {index, element}) = do
+  index <- abstractDecl ctx index
+
+  let ctx = bind ctx index.var.val
+  element <- abstractSyntaxBounds ctx element
+
+  pure (Sigma {index, element})
 abstractSyntax ctx (Pair {first, second}) = do
   first <- abstractSyntaxBounds ctx first
   second <- abstractSyntaxBounds ctx second
@@ -54,12 +70,12 @@ abstractSyntax ctx (Second {arg}) = do
 abstractSyntax ctx Bool = pure Bool
 abstractSyntax ctx True = pure True
 abstractSyntax ctx False = pure False
-abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
-  returnType <- abstractSyntaxBounds (bind ctx var.val) returnType
+abstractSyntax ctx (If {returnType, discriminant, true, false}) = do
+  returnType <- abstractLambda ctx returnType
   discriminant <- abstractSyntaxBounds ctx discriminant
   true <- abstractSyntaxBounds ctx true
   false <- abstractSyntaxBounds ctx false
-  pure (If {var, returnType, discriminant, true, false})
+  pure (If {returnType, discriminant, true, false})
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
-- 
cgit v1.2.3