From 3950a84c00f54ab39f2a209c368cc02460eeebd7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 3 Jan 2023 13:46:38 +0000
Subject: Add more program structure to abstract terms.

Add more program structure to type inference and checking.
---
 src/Obs/Abstract.idr | 95 ++++++++++++++++++++++++++--------------------------
 1 file changed, 48 insertions(+), 47 deletions(-)

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

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index f91be66..039f60e 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -24,74 +24,75 @@ abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds
 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)
+  pure (Var {var, i})
+abstractSyntax ctx (Universe {s}) = pure (Universe {s})
 abstractSyntax ctx (Pi {var, domain, codomain}) = do
-  a <- abstractSyntaxBounds ctx domain
-  b <- abstractSyntaxBounds (bind ctx var.val) codomain
-  pure (Pi var a b)
+  domain <- abstractSyntaxBounds ctx domain
+  codomain <- abstractSyntaxBounds (bind ctx var.val) codomain
+  pure (Pi {var, domain, codomain})
 abstractSyntax ctx (Lambda {var, body}) = do
-  t <- abstractSyntaxBounds (bind ctx var.val) body
-  pure (Lambda var t)
+  body <- abstractSyntaxBounds (bind ctx var.val) body
+  pure (Lambda {var, body})
 abstractSyntax ctx (App {fun, arg}) = do
-  t <- abstractSyntaxBounds ctx fun
-  u <- abstractSyntaxBounds ctx arg
-  pure (App t u)
+  fun <- abstractSyntaxBounds ctx fun
+  arg <- abstractSyntaxBounds ctx arg
+  pure (App {fun, arg})
 abstractSyntax ctx (Sigma {var, index, element}) = do
-  a <- abstractSyntaxBounds ctx index
-  b <- abstractSyntaxBounds (bind ctx var.val) element
-  pure (Sigma var a b)
+  index <- abstractSyntaxBounds ctx index
+  element <- abstractSyntaxBounds (bind ctx var.val) element
+  pure (Sigma {var, index, element})
 abstractSyntax ctx (Pair {first, second}) = do
-  t <- abstractSyntaxBounds ctx first
-  u <- abstractSyntaxBounds ctx second
-  pure (Pair t u)
+  first <- abstractSyntaxBounds ctx first
+  second <- abstractSyntaxBounds ctx second
+  pure (Pair {first, second})
 abstractSyntax ctx (First {arg}) = do
-  t <- abstractSyntaxBounds ctx arg
-  pure (Fst t)
+  arg <- abstractSyntaxBounds ctx arg
+  pure (First {arg})
 abstractSyntax ctx (Second {arg}) = do
-  t <- abstractSyntaxBounds ctx arg
-  pure (Snd t)
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Second {arg})
 abstractSyntax ctx Bool = pure Bool
 abstractSyntax ctx True = pure True
 abstractSyntax ctx False = pure False
 abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
-  a <- abstractSyntaxBounds (bind ctx var.val) returnType
-  t <- abstractSyntaxBounds ctx discriminant
-  f <- abstractSyntaxBounds ctx true
-  g <- abstractSyntaxBounds ctx false
-  pure (If var a t f g)
+  returnType <- abstractSyntaxBounds (bind ctx var.val) returnType
+  discriminant <- abstractSyntaxBounds ctx discriminant
+  true <- abstractSyntaxBounds ctx true
+  false <- abstractSyntaxBounds ctx false
+  pure (If {var, returnType, discriminant, true, false})
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
 abstractSyntax ctx (Absurd {contradiction}) = do
-  t <- abstractSyntaxBounds ctx contradiction
-  pure (Absurd t)
+  contradiction <- abstractSyntaxBounds ctx contradiction
+  pure (Absurd {contradiction})
 abstractSyntax ctx (Equal {left, right}) = do
-  t <- abstractSyntaxBounds ctx left
-  u <- abstractSyntaxBounds ctx right
-  pure (Equal t u)
+  left <- abstractSyntaxBounds ctx left
+  right <- abstractSyntaxBounds ctx right
+  pure (Equal {left, right})
 abstractSyntax ctx (Refl {value}) = do
-  t <- abstractSyntaxBounds ctx value
-  pure (Refl t)
+  value <- abstractSyntaxBounds ctx value
+  pure (Refl {value})
 abstractSyntax ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
-  a <- abstractSyntaxBounds ctx indexedType
-  t <- abstractSyntaxBounds ctx oldIndex
-  u <- abstractSyntaxBounds ctx value
-  t' <- abstractSyntaxBounds ctx newIndex
-  e <- abstractSyntaxBounds ctx equality
-  pure (Transp a t u t' e)
+  indexedType <- abstractSyntaxBounds ctx indexedType
+  oldIndex <- abstractSyntaxBounds ctx oldIndex
+  value <- abstractSyntaxBounds ctx value
+  newIndex <- abstractSyntaxBounds ctx newIndex
+  equality <- abstractSyntaxBounds ctx equality
+  pure (Transp {indexedType, oldIndex, value, newIndex, equality})
 abstractSyntax ctx (Cast {oldType, newType, equality, value}) = do
-  a <- abstractSyntaxBounds ctx oldType
-  b <- abstractSyntaxBounds ctx newType
-  e <- abstractSyntaxBounds ctx equality
-  t <- abstractSyntaxBounds ctx value
-  pure (Cast a b e t)
+  oldType <- abstractSyntaxBounds ctx oldType
+  newType <- abstractSyntaxBounds ctx newType
+  equality <- abstractSyntaxBounds ctx equality
+  value <- abstractSyntaxBounds ctx value
+  pure (Cast {oldType, newType, equality, value})
 abstractSyntax ctx (CastId {value}) = do
-  t <- abstractSyntaxBounds ctx value
-  pure (CastId t)
+  value <- abstractSyntaxBounds ctx value
+  pure (CastId {value})
 
-abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
-  pure $ MkBounded !(abstractSyntax ctx v) irrel bnds
+abstractSyntaxBounds ctx val@(MkBounded v irrel bnds) = do
+  term <- inBounds $ (MkBounded (abstractSyntax ctx v) irrel bnds)
+  pure $ map (const term) val
 
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
-- 
cgit v1.2.3