From 974717f0aa46bb295d44e239594b38f63f39ceab Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 17 Sep 2024 17:09:41 +0100
Subject: Introduce names in contexts.

Introduce rows for n-ary sums and products.

Remove union types.
---
 src/Inky/Type/Pretty.idr | 70 ++++++++++++++----------------------------------
 1 file changed, 20 insertions(+), 50 deletions(-)

(limited to 'src/Inky/Type')

diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 074d86e..1f2d35b 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -1,73 +1,43 @@
 module Inky.Type.Pretty
 
-import Data.Fin
-import Data.Fin.Extra
-import Data.List
-import Data.String
+import Inky.Context
 import Inky.Type
 import Text.PrettyPrint.Prettyprinter
 
-asTyChar : Fin 6 -> Char
-asTyChar = index' ['X', 'Y', 'Z', 'A', 'B', 'C']
-
-export
-typeName : Nat -> String
-typeName n with (divMod n 6)
-  typeName _ | Fraction _ 6 q r Refl =
-    strSnoc
-      (if q == 0 then "'" else assert_total (typeName $ pred q))
-      (asTyChar r)
-
-arrowPrec, unionPrec, prodPrec, sumPrec, fixPrec : Prec
+arrowPrec, prodPrec, sumPrec, fixPrec : Prec
 arrowPrec = Open
-unionPrec = User 2
 prodPrec = Open
-sumPrec = User 1
+sumPrec = Open
 fixPrec = Open
 
 export
-prettyType : {ty : Nat} -> Ty ty -> Prec -> Doc ann
-prettyTypeAll : {ty : Nat} -> List (Ty ty) -> Prec -> List (Doc ann)
-prettyTypeAll1 : {ty : Nat} -> List1 (Ty ty) -> Prec -> List (Doc ann)
+prettyType : {ctx : Context ()} -> Ty ctx () -> Prec -> Doc ann
+prettyTypeRow : {ctx : Context ()} -> Row (Ty ctx ()) -> Prec -> List (Doc ann)
 
-prettyType (TVar i) d = pretty (typeName $ finToNat i)
+prettyType (TVar i) d = pretty (unVal $ nameOf i)
 prettyType TNat d = pretty "Nat"
 prettyType (TArrow a b) d =
   parenthesise (d > arrowPrec) $ group $ align $ hang 2 $
     let parts = stripArrow b in
-    concatWith (\x, y => x <++> "->" <+> line <+> y) (prettyType a arrowPrec :: parts)
+    concatWith (surround $ "->" <+> line) (prettyType a arrowPrec :: parts)
   where
-  stripArrow : Ty ty -> List (Doc ann)
+  stripArrow : Ty ctx () -> List (Doc ann)
   stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b
   stripArrow a = [prettyType a arrowPrec]
-prettyType (TUnion (a ::: [])) d =
-  parens $ group $ align $ hang 2 $
-    prettyType a unionPrec <++> "&"
-prettyType (TUnion as) d =
-  parenthesise (d >= unionPrec) $ group $ align $ hang 2 $
-    let parts = prettyTypeAll1 as unionPrec in
-    concatWith (\x, y => x <++> "&" <+> line <+> y) parts
-prettyType (TProd [a]) d =
-  parens $ group $ align $ hang 2 $
-    prettyType a prodPrec <++> ","
 prettyType (TProd as) d =
-  parens $ group $ align $ hang 2 $
-    let parts = prettyTypeAll as prodPrec in
-    concatWith (\x, y => x <++> "," <+> line <+> y) parts
-prettyType (TSum []) d = "(+)"
-prettyType (TSum [a]) d =
-  parens $ group $ align $ hang 2 $
-    prettyType a sumPrec <++> "+"
+  enclose "<" ">" $ group $ align $ hang 2 $
+    let parts = prettyTypeRow as prodPrec in
+    concatWith (surround $ "," <+> line) parts
 prettyType (TSum as) d =
-  parenthesise (d >= sumPrec) $ group $ align $ hang 2 $
-    let parts = prettyTypeAll as sumPrec in
-    concatWith (\x, y => x <++> "+" <+> line <+> y) parts
-prettyType (TFix a) d =
+  enclose "[" "]" $ group $ align $ hang 2 $
+    let parts = prettyTypeRow as prodPrec in
+    concatWith (surround $ "," <+> line) parts
+prettyType (TFix x a) d =
   parens $ group $ align $ hang 2 $
-    "\\" <+> pretty (typeName ty) <++> "=>" <+> line <+>
+    "\\" <+> pretty x <++> "=>" <+> line <+>
     prettyType a fixPrec
 
-prettyTypeAll [] d = []
-prettyTypeAll (a :: as) d = prettyType a d :: prettyTypeAll as d
-
-prettyTypeAll1 (a ::: as) d = prettyType a d :: prettyTypeAll as d
+prettyTypeRow [<] d = []
+prettyTypeRow (as :< (x :- a)) d =
+  (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d)
+  :: prettyTypeRow as d
-- 
cgit v1.2.3