Introduce names in contexts.

Introduce rows for n-ary sums and products.

Remove union types.

1 files changed, 46 insertions, 47 deletions

diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index e353e50..71028ba 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,24 +1,10 @@
 module Inky.Term.Pretty
 
-import Data.Fin
-import Data.Fin.Extra
-import Data.List
-import Data.String
+import Inky.Context
 import Inky.Term
 import Inky.Type.Pretty
 import Text.PrettyPrint.Prettyprinter
 
-asTmChar : Fin 9 -> Char
-asTmChar = index' ['x', 'y', 'z', 'a', 'b', 'c', 'd', 'e', 'f']
-
-export
-termName : Nat -> String
-termName n with (divMod n 9)
-  termName _ | Fraction _ 9 q r Refl =
-    strSnoc
-      (if q == 0 then "" else assert_total (termName $ pred q))
-      (asTmChar r)
-
 appPrec, prjPrec, expandPrec, annotPrec,
   letPrec, absPrec, injPrec, tupPrec, casePrec, contractPrec, foldPrec : Prec
 appPrec = App
@@ -27,29 +13,40 @@ expandPrec = PrefixMinus
 annotPrec = Equal
 letPrec = Open
 absPrec = Open
-injPrec = User 8
-tupPrec = User 2
+injPrec = App
+tupPrec = Open
 casePrec = Open
 contractPrec = PrefixMinus
 foldPrec = Open
 
 export
-prettySynth : {ty, tm : Nat} -> SynthTerm ty tm -> Prec -> Doc ann
-prettyCheck : {ty, tm : Nat} -> CheckTerm ty tm -> Prec -> Doc ann
-prettyAllCheck : {ty, tm : Nat} -> List (CheckTerm ty tm) -> Prec -> List (Doc ann)
-prettyAll1Check : {ty, tm : Nat} -> List1 (CheckTerm ty tm) -> Prec -> List (Doc ann)
+prettySynth :
+  {tyCtx, tmCtx : Context ()} ->
+  SynthTerm tyCtx tmCtx -> Prec -> Doc ann
+prettyCheck :
+  {tyCtx, tmCtx : Context ()} ->
+  CheckTerm tyCtx tmCtx -> Prec -> Doc ann
+prettyAllCheck :
+  {tyCtx, tmCtx : Context ()} ->
+  List (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann)
+prettyCheckCtx :
+  {tyCtx, tmCtx : Context ()} ->
+  Context (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann)
+prettyCheckCtxBinding :
+  {tyCtx, tmCtx : Context ()} ->
+  Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann)
 
-prettySynth (Var i) d = pretty (termName $ finToNat i)
+prettySynth (Var i) d = pretty (unVal $ nameOf i)
 prettySynth (Lit k) d = pretty k
 prettySynth (Suc t) d =
   parenthesise (d >= appPrec) $ group $ align $ hang 2 $
     "suc" <+> line <+> prettyCheck t appPrec
 prettySynth (App e ts) d =
   parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-    concatWith (\x, y => x <+> line <+> y) (prettySynth e appPrec :: prettyAll1Check ts appPrec)
-prettySynth (Prj e k) d =
+    concatWith (surround line) (prettySynth e appPrec :: prettyAllCheck ts appPrec)
+prettySynth (Prj e x) d =
   parenthesise (d > prjPrec) $ group $ align $ hang 2 $
-    prettySynth e prjPrec <+> "[" <+> line' <+> pretty k <+> line' <+> "]"
+    prettySynth e prjPrec <+> "." <+> pretty x
 prettySynth (Expand e) d =
   "!" <+>
   (parenthesise (d > expandPrec) $ group $ align $ hang 2 $
@@ -58,54 +55,56 @@ prettySynth (Annot t a) d =
   parenthesise (d > annotPrec) $ group $ align $ hang 2 $
     prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
 
-prettyCheck (Let e t) d =
+prettyCheck (Let x e t) d =
   parenthesise (d > letPrec) $ group $ align $ hang 2 $
     "let" <++>
     (group $ align $ hang 2 $
-      pretty (termName tm) <++> "=" <+> line <+> prettySynth e letPrec
+      pretty x <++> "=" <+> line <+> prettySynth e letPrec
     ) <++>
     "in" <+> line <+>
     prettyCheck t letPrec
-prettyCheck (Abs k t) d =
+prettyCheck (Abs bound t) d =
   parenthesise (d > absPrec) $ group $ align $ hang 2 $
-    "\\" <+> concatWith (\x, y => x <+> "," <++> y) (bindings tm (S k)) <++> "=>" <+> line <+>
+    "\\" <+> concatWith (surround ",") (bindings bound <>> []) <++> "=>" <+> line <+>
     prettyCheck t absPrec
   where
-  bindings : Nat -> Nat -> List (Doc ann)
-  bindings tm 0 = []
-  bindings tm (S k) = pretty (termName tm) :: bindings (S tm) k
+  bindings : Context () -> SnocList (Doc ann)
+  bindings [<] = [<]
+  bindings (bound :< (x :- ())) = bindings bound :< pretty x
 prettyCheck (Inj k t) d =
   parenthesise (d > injPrec) $ group $ align $ hang 2 $
     "<" <+> line' <+> pretty k <+> line' <+> ">" <+> prettyCheck t injPrec
-prettyCheck (Tup []) d = pretty "()"
-prettyCheck (Tup [t]) d =
-  parens $ group $ align $ hang 2 $
-    prettyCheck t tupPrec <+> line <+> ","
 prettyCheck (Tup ts) d =
-  parenthesise (d > tupPrec) $ group $ align $ hang 2 $
-    concatWith (\x, y => x <+> "," <++> line <+> y) (prettyAllCheck ts tupPrec)
+  parens $ group $ align $ hang 2 $
+    concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec)
 prettyCheck (Case e ts) d =
   parenthesise (d > casePrec) $ group $ align $ hang 2 $
     "case" <++> prettySynth e casePrec <++> "of" <+> line <+>
     (braces $ align $ hang 2 $
-      concatWith (\x, y => x <+> hardline <+> y) $
-      map (\x =>
-        parens $ group $ align $ hang 2 $
-          "\\" <+> pretty (termName tm) <++> "=>" <+> line <+> x) $
-      prettyAllCheck ts casePrec
-    )
+      concatWith (surround hardline) $
+      map parens $
+      prettyCheckCtxBinding ts casePrec)
 prettyCheck (Contract t) d =
   "~" <+>
   (parenthesise (d > contractPrec) $ group $ align $ hang 2 $
     prettyCheck t contractPrec)
-prettyCheck (Fold e t) d =
+prettyCheck (Fold e x t) d =
   parenthesise (d > foldPrec) $ group $ align $ hang 2 $
     "fold" <++> prettySynth e foldPrec <++> "by" <+> line <+>
     (parens $ group $ align $ hang 2 $
-      "\\" <+> pretty (termName tm) <++> "=>" <+> line <+> prettyCheck t foldPrec)
+      "\\" <+> pretty x <++> "=>" <+> line <+> prettyCheck t foldPrec)
 prettyCheck (Embed e) d = prettySynth e d
 
 prettyAllCheck [] d = []
 prettyAllCheck (t :: ts) d = prettyCheck t d :: prettyAllCheck ts d
 
-prettyAll1Check (t ::: ts) d = prettyCheck t d :: prettyAllCheck ts d
+prettyCheckCtx [<] d = []
+prettyCheckCtx (ts :< (x :- t)) d =
+  (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyCheck t d) ::
+  prettyCheckCtx ts d
+
+prettyCheckCtxBinding [<] d = []
+prettyCheckCtxBinding (ts :< (x :- (y ** t))) d =
+  (group $ align $ hang 2 $
+    "\\" <+> pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) ::
+  prettyCheckCtxBinding ts d