Add more program structure to raw syntax.

3 files changed, 132 insertions, 141 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index a9ef411..f91be66 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -21,73 +21,73 @@ 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))
 
-abstractSyntax ctx (Var var) = do
+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 a b) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds (bind ctx var.val) b
+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)
-abstractSyntax ctx (Lambda var t) = do
-  t <- abstractSyntaxBounds (bind ctx var.val) t
+abstractSyntax ctx (Lambda {var, body}) = do
+  t <- abstractSyntaxBounds (bind ctx var.val) body
   pure (Lambda var t)
-abstractSyntax ctx (App t u) = do
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
+abstractSyntax ctx (App {fun, arg}) = do
+  t <- abstractSyntaxBounds ctx fun
+  u <- abstractSyntaxBounds ctx arg
   pure (App t u)
-abstractSyntax ctx (Sigma var a b) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds (bind ctx var.val) b
+abstractSyntax ctx (Sigma {var, index, element}) = do
+  a <- abstractSyntaxBounds ctx index
+  b <- abstractSyntaxBounds (bind ctx var.val) element
   pure (Sigma var a b)
-abstractSyntax ctx (Pair t u) = do
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
+abstractSyntax ctx (Pair {first, second}) = do
+  t <- abstractSyntaxBounds ctx first
+  u <- abstractSyntaxBounds ctx second
   pure (Pair t u)
-abstractSyntax ctx (Fst t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (First {arg}) = do
+  t <- abstractSyntaxBounds ctx arg
   pure (Fst t)
-abstractSyntax ctx (Snd t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Second {arg}) = do
+  t <- abstractSyntaxBounds ctx arg
   pure (Snd t)
 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
-  f <- abstractSyntaxBounds ctx f
-  g <- abstractSyntaxBounds ctx g
+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)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
-abstractSyntax ctx (Absurd t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Absurd {contradiction}) = do
+  t <- abstractSyntaxBounds ctx contradiction
   pure (Absurd t)
-abstractSyntax ctx (Equal t u) = do
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
+abstractSyntax ctx (Equal {left, right}) = do
+  t <- abstractSyntaxBounds ctx left
+  u <- abstractSyntaxBounds ctx right
   pure (Equal t u)
-abstractSyntax ctx (Refl t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (Refl {value}) = do
+  t <- abstractSyntaxBounds ctx value
   pure (Refl t)
-abstractSyntax ctx (Transp a t u t' e) = do
-  a <- abstractSyntaxBounds ctx a
-  t <- abstractSyntaxBounds ctx t
-  u <- abstractSyntaxBounds ctx u
-  t' <- abstractSyntaxBounds ctx t'
-  e <- abstractSyntaxBounds ctx e
+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)
-abstractSyntax ctx (Cast a b e t) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds ctx b
-  e <- abstractSyntaxBounds ctx e
-  t <- abstractSyntaxBounds ctx t
+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)
-abstractSyntax ctx (CastId t) = do
-  t <- abstractSyntaxBounds ctx t
+abstractSyntax ctx (CastId {value}) = do
+  t <- abstractSyntaxBounds ctx value
   pure (CastId t)
 
 abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index f92a0e2..8eea42c 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -266,8 +266,8 @@ termForms =
 
 headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax)))
 headForms =
-  [ (OTFst, (0 ** uncurry 1 Fst))
-  , (OTSnd, (0 ** uncurry 1 Snd))
+  [ (OTFst, (0 ** uncurry 1 First))
+  , (OTSnd, (0 ** uncurry 1 Second))
   , (OTAbsurd, (0 ** uncurry 1 Absurd))
   , (OTRefl, (0 ** uncurry 1 Refl))
   , (OTTransp, (4 ** (uncurry 5 Transp)))
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 32e86c0..a8a468c 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -12,35 +12,37 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var : String -> Syntax
+  Var : (var : String) -> Syntax
   -- Universes
-  Universe : Universe -> Syntax
+  Universe : (s : Universe) -> Syntax
   -- Dependent Products
-  Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Lambda : WithBounds String -> WithBounds Syntax -> Syntax
-  App : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Pi : (var : WithBounds String) -> (domain, codomain : WithBounds Syntax) -> Syntax
+  Lambda : (var : WithBounds String) -> (body : WithBounds Syntax) -> Syntax
+  App : (fun, arg : WithBounds Syntax) -> Syntax
   -- Dependent Sums
-  Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Fst : WithBounds Syntax -> Syntax
-  Snd : WithBounds Syntax -> Syntax
+  Sigma : (var : WithBounds String) -> (index, element : WithBounds Syntax) -> Syntax
+  Pair : (first, second : WithBounds Syntax) -> Syntax
+  First : (arg : WithBounds Syntax) -> Syntax
+  Second : (arg : WithBounds Syntax) -> Syntax
   -- Booleans
   Bool : Syntax
   True : Syntax
   False : Syntax
-  If : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  If : (var : WithBounds String) ->
+    (returnType, discriminant, true, false : WithBounds Syntax) ->
+    Syntax
   -- True
   Top : Syntax
   Point : Syntax
   -- False
   Bottom : Syntax
-  Absurd : WithBounds Syntax -> Syntax
+  Absurd : (contradiction : WithBounds Syntax) -> Syntax
   -- Equality
-  Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Refl : WithBounds Syntax -> Syntax
-  Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  CastId : WithBounds Syntax -> Syntax
+  Equal : (left, right : WithBounds Syntax) -> Syntax
+  Refl : (value : WithBounds Syntax) -> Syntax
+  Transp : (indexedType, oldIndex, value, newIndex, equality : WithBounds Syntax) -> Syntax
+  Cast : (oldType, newType, equality, value : WithBounds Syntax) -> Syntax
+  CastId : (value : WithBounds Syntax) -> Syntax
 
 public export
 record Definition where
@@ -51,102 +53,91 @@ record Definition where
 
 -- Pretty Print ----------------------------------------------------------------
 
-prettyPrec : Prec -> Syntax -> Doc ann
-prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
+prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
+prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
 
-prettyPrec d (Var var) = pretty var
-prettyPrec d (Universe s) = prettyPrec d s
-prettyPrec d (Pi var a b) =
-  parenthesise (d > Open) $
-  group $
-  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
-  pretty "->" <+> line <+>
-  align (prettyPrecBounds Open b)
-prettyPrec d (Lambda var t) =
+prettyDeclForm : (prec : Prec) ->
+  (name : String) ->
+  (ty : Doc ann) ->
+  (sep : String) ->
+  (tail : Doc ann) ->
+  Doc ann
+prettyDeclForm d name ty sep tail =
   parenthesise (d > Open) $
   group $
-  backslash <+> pretty var.val <++>
-  pretty "=>" <+> line <+>
-  align (prettyPrecBounds Open t)
-prettyPrec d (App t u) =
-  parenthesise (d >= App) $
-  group $
-  vsep [prettyPrecBounds Open t, prettyPrecBounds App u]
-prettyPrec d (Sigma var a b) =
+  vsep $
+  [prettyDecl name ty <++> pretty sep, align tail]
+
+prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
+prettyLambda d name body =
   parenthesise (d >= App) $
   group $
-  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
-  pretty "**" <+> line <+>
-  align (prettyPrecBounds Open b)
-prettyPrec d (Pair t u) =
+  backslash <+> pretty name <++> pretty "=>" <+> line <+> align body
+
+prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann
+prettyApp d head tail = parenthesise (d >= App) $ group $ vsep (align head :: map (hang 2) tail)
+
+prettyPrec : Prec -> Syntax -> Doc ann
+prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
+
+prettyPrec d (Var {var}) = pretty var
+prettyPrec d (Universe {s}) = prettyPrec d s
+prettyPrec d (Pi {var, domain, codomain}) =
+  prettyDeclForm d var.val (prettyPrecBounds Open domain) "->" (prettyPrecBounds Open codomain)
+prettyPrec d (Lambda {var, body}) = prettyLambda d var.val (prettyPrecBounds Open body)
+prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg]
+prettyPrec d (Sigma {var, index, element}) =
+  prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
+prettyPrec d (Pair {first, second}) =
   angles $
   group $
-  neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral
-prettyPrec d (Fst t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "fst", prettyPrecBounds App t]
-prettyPrec d (Snd t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "snd", prettyPrecBounds App t]
+  neutral <++>
+  align (prettyPrecBounds Open first) <+>
+  comma <+>
+  line <+>
+  align (prettyPrecBounds Open second) <++>
+  neutral
+prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
+prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
-prettyPrec d (If var a t f g) =
-  parenthesise (d >= App) $
-  group $
-  vsep $
-  [ pretty "if"
-  , parens $
-    group $
-    backslash <+> pretty var.val <++>
-    pretty "=>" <+> line <+>
-    align (prettyPrecBounds Open a)
-  , prettyPrecBounds App t
-  , prettyPrecBounds App f
-  , prettyPrecBounds App g
+prettyPrec d (If {var, returnType, discriminant, true, false}) =
+  prettyApp d (pretty "if") $
+  [ prettyLambda App var.val (prettyPrecBounds Open returnType)
+  , prettyPrecBounds App discriminant
+  , prettyPrecBounds App true
+  , prettyPrecBounds App false
   ]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-prettyPrec d (Absurd t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "absurd", prettyPrecBounds App t]
-prettyPrec d (Equal t u) =
+prettyPrec d (Absurd {contradiction}) =
+  prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction]
+prettyPrec d (Equal {left, right}) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u
-prettyPrec d (Refl t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "refl", prettyPrecBounds App t]
-prettyPrec d (Transp a t u t' e) =
-  parenthesise (d >= App) $
-  group $
-  vsep $
-  [ pretty "transp"
-  , prettyPrecBounds App a
-  , prettyPrecBounds App t
-  , prettyPrecBounds App u
-  , prettyPrecBounds App t'
-  , prettyPrecBounds App e
+  align (prettyPrecBounds Equal left) <++>
+  pretty "~" <+>
+  line <+>
+  align (prettyPrecBounds Equal right)
+prettyPrec d (Refl {value}) = prettyApp d (pretty "refl") [prettyPrecBounds App value]
+prettyPrec d (Transp {indexedType, oldIndex, value, newIndex, equality}) =
+  prettyApp d (pretty "transp") $
+  [ prettyPrecBounds App indexedType
+  , prettyPrecBounds App oldIndex
+  , prettyPrecBounds App value
+  , prettyPrecBounds App newIndex
+  , prettyPrecBounds App equality
   ]
-prettyPrec d (Cast a b e t) =
-  parenthesise (d >= App) $
-  group $
-  vsep $
-  [ pretty "cast"
-  , prettyPrecBounds App a
-  , prettyPrecBounds App b
-  , prettyPrecBounds App e
-  , prettyPrecBounds App t
+prettyPrec d (Cast {oldType, newType, equality, value}) =
+  prettyApp d (pretty "cast") $
+  [ prettyPrecBounds App oldType
+  , prettyPrecBounds App newType
+  , prettyPrecBounds App equality
+  , prettyPrecBounds App value
   ]
-prettyPrec d (CastId t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "castRefl", prettyPrecBounds App t]
+prettyPrec d (CastId {value}) = prettyApp d (pretty "castRefl") [prettyPrecBounds App value]
 
 prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val