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/NormalForm.idr | 267 +++++++++++++++++++++++++------------------------
 1 file changed, 137 insertions(+), 130 deletions(-)

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

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index d660111..0b9d2b6 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -2,6 +2,7 @@ module Obs.NormalForm
 
 import Data.List.Elem
 
+import Obs.Pretty
 import Obs.Substitution
 import Obs.Universe
 
@@ -18,28 +19,32 @@ public export
 TypeNormalForm : Unsorted.Family Relevance
 TypeNormalForm = NormalForm Relevant
 
+public export
+record DeclForm (ctx : List Relevance) where
+  constructor MkDecl
+  var : Maybe String
+  type : TypeNormalForm ctx
+
 public export
 data Constructor : Unsorted.Family Relevance where
   Universe : (s : Universe) -> Constructor ctx
-  Pi : (s, s' : Universe)
-    -> (var : String)
-    -> (a : TypeNormalForm ctx)
-    -> (b : TypeNormalForm (relevance s :: ctx))
-    -> Constructor ctx
-  Lambda : (s : Universe)
-    -> (var : String)
-    -> NormalForm Relevant (relevance s :: ctx)
-    -> Constructor ctx
-  Sigma : (s, s' : Universe)
-    -> (var : String)
-    -> (a : TypeNormalForm ctx)
-    -> (b : TypeNormalForm (relevance s :: ctx))
-    -> Constructor ctx
-  Pair : (s, s' : Universe)
-    -> (prf : IsRelevant (max s s'))
-    -> NormalForm (relevance s) ctx
-    -> NormalForm (relevance s') ctx
-    -> Constructor ctx
+  Pi : (domainSort, codomainSort : Universe) ->
+    (domain : DeclForm ctx) ->
+    (codomain : TypeNormalForm (relevance domainSort :: ctx)) ->
+    Constructor ctx
+  Lambda : (domainRel : Relevance) ->
+    (var : Maybe String) ->
+    (body : NormalForm Relevant (domainRel :: ctx)) ->
+    Constructor ctx
+  Sigma : (indexSort, elementSort : Universe) ->
+    (index : DeclForm ctx) ->
+    (element : TypeNormalForm (relevance indexSort :: ctx)) ->
+    Constructor ctx
+  Pair : (indexRel, elementRel : Relevance) ->
+    (prf : IsRelevant (pair indexRel elementRel)) ->
+    (first : NormalForm indexRel ctx) ->
+    (second : NormalForm elementRel ctx) ->
+    Constructor ctx
   Bool : Constructor ctx
   True : Constructor ctx
   False : Constructor ctx
@@ -48,26 +53,27 @@ data Constructor : Unsorted.Family Relevance where
 
 public export
 data Neutral : Unsorted.Family Relevance where
-  Var : (var : String)
-    -> (sort : Universe)
-    -> (prf : IsRelevant sort)
-    -> (i : Elem Relevant ctx)
-    -> Neutral ctx
-  App : (r : Relevance) -> Neutral ctx -> NormalForm r ctx -> Neutral ctx
-  Fst : (r : Relevance) -> Neutral ctx -> Neutral ctx
-  Snd : (r : Relevance) -> Neutral ctx -> Neutral ctx
-  If : Neutral ctx -> (f, g : NormalForm Relevant ctx) -> Neutral ctx
+  Var : (var : String) -> (i : Elem Relevant ctx) -> Neutral ctx
+  App : (argRel : Relevance) -> (fun : Neutral ctx) -> (arg : NormalForm argRel ctx) -> Neutral ctx
+  First : (secondRel : Relevance) -> (arg : Neutral ctx) -> Neutral ctx
+  Second : (firstRel : Relevance) -> (arg : Neutral ctx) -> Neutral ctx
+  If : (discriminant : Neutral ctx) -> (true, false : NormalForm Relevant ctx) -> Neutral ctx
   Absurd : Neutral ctx
-  Equal : Neutral ctx -> NormalForm Relevant ctx -> NormalForm Relevant ctx -> Neutral ctx
-  EqualL : (a : Neutral ctx) -> (b : TypeNormalForm ctx) -> Neutral ctx
-  EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx
-  EqualStuck : (a, b : Constructor ctx) -> Neutral ctx
-  CastL : (a : Neutral ctx) ->
-    (b : TypeNormalForm ctx) ->
-    NormalForm Relevant ctx ->
+  Equal : (type : Neutral ctx) -> (left, right : NormalForm Relevant ctx) -> Neutral ctx
+  EqualL : (left : Neutral ctx) -> (right : TypeNormalForm ctx) -> Neutral ctx
+  EqualR : (left : Constructor ctx) -> (right : Neutral ctx) -> Neutral ctx
+  EqualStuck : (left, right : Constructor ctx) -> Neutral ctx
+  CastL : (oldType : Neutral ctx) ->
+    (newType : TypeNormalForm ctx) ->
+    (value : NormalForm Relevant ctx) ->
+    Neutral ctx
+  CastR : (oldType : Constructor ctx) ->
+    (newType : Neutral ctx) ->
+    (value : NormalForm Relevant ctx) ->
+    Neutral ctx
+  CastStuck : (oldType, newType : Constructor ctx) ->
+    (value : NormalForm Relevant ctx) ->
     Neutral ctx
-  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm Relevant ctx -> Neutral ctx
-  CastStuck : (a, b : Constructor ctx) -> NormalForm Relevant ctx -> Neutral ctx
 
 public export
 data NormalForm : Sorted.Family Relevance where
@@ -108,34 +114,19 @@ Cast Universe (NormalForm Relevant ctx) where
 
 prettyPrec : Prec -> NormalForm b ctx -> Doc ann
 
+prettyPrecDecl : DeclForm ctx -> Doc ann
+prettyPrecDecl (MkDecl var type) = prettyDecl var (prettyPrec Open type)
+
 prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
-prettyPrecCnstr d (Universe s) = prettyPrec d s
-prettyPrecCnstr d (Pi s s' var a b) =
-  let lhs = case var of
-              "" => align (prettyPrec App a)
-              _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a))
-  in
-  parenthesise (d > Open) $
-  group $
-  lhs <++> pretty "->" <+> line <+> align (prettyPrec Open b)
-prettyPrecCnstr d (Lambda _ var t) =
-  parenthesise (d > Open) $
-  group $
-  backslash <+> pretty var <++>
-  pretty "=>" <+> line <+>
-  align (prettyPrec Open t)
-prettyPrecCnstr d (Sigma s s' var a b) =
-  let lhs = case var of
-              "" => align (prettyPrec App a)
-              _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a))
-  in
-  parenthesise (d > Open) $
-  group $
-  lhs <++> pretty "**" <+> line <+> align (prettyPrec Open b)
-prettyPrecCnstr d (Pair s s' prf t u) =
-  angles $
-  group $
-  neutral <++> prettyPrec Open t <+> comma <+> line <+> prettyPrec Open u <++> neutral
+prettyPrecCnstr d (Universe {s}) = prettyPrec d s
+prettyPrecCnstr d (Pi {domainSort, codomainSort, domain, codomain}) =
+  prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrec Open codomain)
+prettyPrecCnstr d (Lambda {domainRel, var, body}) =
+  prettyLambda d (maybe "_" id var) (prettyPrec Open body)
+prettyPrecCnstr d (Sigma {indexSort, elementSort, index, element}) =
+  prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrec Open element)
+prettyPrecCnstr d (Pair {indexRel, elementRel, prf, first, second}) =
+  prettyPair (prettyPrec Open first) (prettyPrec Open second)
 prettyPrecCnstr d Bool = pretty "Bool"
 prettyPrecCnstr d True = pretty "True"
 prettyPrecCnstr d False = pretty "False"
@@ -143,52 +134,34 @@ prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
 prettyPrecNtrl : Prec -> Neutral ctx -> Doc ann
-prettyPrecNtrl d (Var var sort prf i) = pretty "\{var}@\{show $ elemToNat i}"
-prettyPrecNtrl d (App _ t u) =
-  parenthesise (d >= App) $
-  group $
-  vsep [prettyPrecNtrl Open t, prettyPrec App u]
-prettyPrecNtrl d (Fst _ t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "fst", prettyPrecNtrl App t]
-prettyPrecNtrl d (Snd _ t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "snd", prettyPrecNtrl App t]
-prettyPrecNtrl d (If t f g) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "if", prettyPrecNtrl App t, prettyPrec App f, prettyPrec App g]
+prettyPrecNtrl d (Var {var, i}) = pretty "\{var}@\{show $ elemToNat i}"
+prettyPrecNtrl d (App {argRel, fun, arg}) =
+  prettyApp d (prettyPrecNtrl Open fun) [prettyPrec App arg]
+prettyPrecNtrl d (First {secondRel, arg}) =
+  prettyApp d (pretty "fst") [prettyPrecNtrl App arg]
+prettyPrecNtrl d (Second {firstRel, arg}) =
+  prettyApp d (pretty "snd") [prettyPrecNtrl App arg]
+prettyPrecNtrl d (If {discriminant, true, false}) =
+  prettyApp d (pretty "if") $
+  [prettyPrecNtrl App discriminant, prettyPrec App true, prettyPrec App false]
 prettyPrecNtrl d Absurd = pretty "absurd"
-prettyPrecNtrl d (Equal a t u) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrec Equal t <++> pretty "~" <+> line <+> prettyPrec Equal u
-prettyPrecNtrl d (EqualL a b) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecNtrl Equal a <++> pretty "~" <+> line <+> prettyPrec Equal b
-prettyPrecNtrl d (EqualR a b) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecNtrl Equal b
-prettyPrecNtrl d (EqualStuck a b) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecCnstr Equal b
-prettyPrecNtrl d (CastL a b t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "cast", prettyPrecNtrl App a, prettyPrec App b, prettyPrec App t]
-prettyPrecNtrl d (CastR a b t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrec App t]
-prettyPrecNtrl d (CastStuck a b t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrec App t]
+prettyPrecNtrl d (Equal {type, left, right}) =
+  prettyEqual d (prettyPrec Equal left) (prettyPrec Equal right)
+prettyPrecNtrl d (EqualL {left, right}) =
+  prettyEqual d (prettyPrecNtrl Equal left) (prettyPrec Equal right)
+prettyPrecNtrl d (EqualR {left, right}) =
+  prettyEqual d (prettyPrecCnstr Equal left) (prettyPrecNtrl Equal right)
+prettyPrecNtrl d (EqualStuck {left, right}) =
+  prettyEqual d (prettyPrecCnstr Equal left) (prettyPrecCnstr Equal right)
+prettyPrecNtrl d (CastL {oldType, newType, value}) =
+  prettyApp d (pretty "cast") $
+  [prettyPrecNtrl App oldType, prettyPrec App newType, prettyPrec App value]
+prettyPrecNtrl d (CastR {oldType, newType, value}) =
+  prettyApp d (pretty "cast") $
+  [prettyPrecCnstr App oldType, prettyPrecNtrl App newType, prettyPrec App value]
+prettyPrecNtrl d (CastStuck {oldType, newType, value}) =
+  prettyApp d (pretty "cast") $
+  [prettyPrecCnstr App oldType, prettyPrecCnstr App newType, prettyPrec App value]
 
 prettyPrec d (Ntrl t) = prettyPrecNtrl d t
 prettyPrec d (Cnstr t) = prettyPrecCnstr d t
@@ -210,13 +183,35 @@ Pretty (NormalForm b ctx) where
 
 rename : NormalForm ~|> Hom Elem NormalForm
 
+renameDecl : DeclForm ~|> Hom Elem DeclForm
+renameDecl (MkDecl var type) f = MkDecl var (rename type f)
+
 renameCnstr : Constructor ~|> Hom Elem Constructor
-renameCnstr (Universe s) f = Universe s
-renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f))
-renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f))
-renameCnstr (Sigma s s' var a b) f =
-  Sigma s s' var (rename a f) (rename b (lift [(_ ** ())] f))
-renameCnstr (Pair s s' prf t u) f = Pair s s' prf (rename t f) (rename u f)
+renameCnstr (Universe {s}) f = Universe {s}
+renameCnstr (Pi {domainSort, codomainSort, domain, codomain}) f =
+  Pi
+    { domainSort
+    , codomainSort
+    , domain = renameDecl domain f
+    , codomain = rename codomain (lift [(_ ** ())] f)
+    }
+renameCnstr (Lambda {domainRel, var, body}) f =
+  Lambda {domainRel, var, body = rename body (lift [(_ ** ())] f)}
+renameCnstr (Sigma {indexSort, elementSort, index, element}) f =
+  Sigma
+    { indexSort
+    , elementSort
+    , index = renameDecl index f
+    , element = rename element (lift [(_ ** ())] f)
+    }
+renameCnstr (Pair {indexRel, elementRel, prf, first, second}) f =
+  Pair
+    { indexRel
+    , elementRel
+    , prf
+    , first = rename first f
+    , second = rename second f
+    }
 renameCnstr Bool f = Bool
 renameCnstr True f = True
 renameCnstr False f = False
@@ -224,19 +219,30 @@ renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
 renameNtrl : Neutral ~|> Hom Elem Neutral
-renameNtrl (Var var sort prf i) f = Var var sort prf (f i)
-renameNtrl (App b t u) f = App b (renameNtrl t f) (rename u f)
-renameNtrl (Fst b t) f = Fst b (renameNtrl t f)
-renameNtrl (Snd b t) f = Snd b (renameNtrl t f)
-renameNtrl (If t u v) f = If (renameNtrl t f) (rename u f) (rename v f)
+renameNtrl (Var {var, i}) f = Var {var, i = f i}
+renameNtrl (App {argRel, fun, arg}) f = App {argRel, fun = renameNtrl fun f, arg = rename arg f}
+renameNtrl (First {secondRel, arg}) f = First {secondRel, arg = renameNtrl arg f}
+renameNtrl (Second {firstRel, arg}) f = Second {firstRel, arg = renameNtrl arg f}
+renameNtrl (If {discriminant, true, false}) f =
+  If {discriminant = renameNtrl discriminant f, true = rename true f, false = rename false f}
 renameNtrl Absurd f = Absurd
-renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (rename t f) (rename u f)
-renameNtrl (EqualL a b) f = EqualL (renameNtrl a f) (rename b f)
-renameNtrl (EqualR a b) f = EqualR (renameCnstr a f) (renameNtrl b f)
-renameNtrl (EqualStuck a b) f = EqualStuck (renameCnstr a f) (renameCnstr b f)
-renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (rename b f) (rename t f)
-renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (rename t f)
-renameNtrl (CastStuck a b t) f = CastStuck (renameCnstr a f) (renameCnstr b f) (rename t f)
+renameNtrl (Equal {type, left, right}) f =
+  Equal {type = renameNtrl type f, left = rename left f, right = rename right f}
+renameNtrl (EqualL {left, right}) f = EqualL {left = renameNtrl left f, right = rename right f}
+renameNtrl (EqualR {left, right}) f =
+  EqualR {left = renameCnstr left f, right = renameNtrl right f}
+renameNtrl (EqualStuck {left, right}) f =
+  EqualStuck {left = renameCnstr left f, right = renameCnstr right f}
+renameNtrl (CastL {oldType, newType, value}) f =
+ CastL {oldType = renameNtrl oldType f, newType = rename newType f, value = rename value f}
+renameNtrl (CastR {oldType, newType, value}) f =
+ CastR {oldType = renameCnstr oldType f, newType = renameNtrl newType f, value = rename value f}
+renameNtrl (CastStuck {oldType, newType, value}) f =
+ CastStuck
+   { oldType = renameCnstr oldType f
+   , newType = renameCnstr newType f
+   , value = rename value f
+   }
 
 rename (Ntrl t) f = Ntrl $ renameNtrl t f
 rename (Cnstr t) f = Cnstr $ renameCnstr t f
@@ -249,12 +255,13 @@ Unsorted.Rename Relevance Constructor where
 export
 Unsorted.Rename Relevance Neutral where
   rename = renameNtrl
-  
+
 export
 Sorted.Rename Relevance NormalForm where
   rename = NormalForm.rename
 
 export
-PointedRename Relevance (\r => (String, (s : Universe ** relevance s = r))) NormalForm where
+PointedRename Relevance (\r => Maybe String) NormalForm where
   point {s = Irrelevant} _ _ = Irrel
-  point {s = Relevant} (var, (s@(Set _) ** prf)) i = Ntrl (Var var s Set i)
+  point {s = Relevant} var i =
+    Ntrl (Var {var = maybe "" id var, i})
-- 
cgit v1.2.3