Fix showTerm not displaying empty pis correctly

WhatisRT · Dec 30, 2023 · 28a4ce8 · 28a4ce8
1 parent 9d7a073
commit 28a4ce8
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/mced/Bootstrap/Stage-3/ShowTerm.mced b/mced/Bootstrap/Stage-3/ShowTerm.mced
@@ -28,6 +28,7 @@ b-let showVar (con : List String) (v : Var) : String :=
 b-let showSort (s : Sort) : String := s ?String "*" "□".
 b-let showBinder (b : Binder) : String := b ?String "λ" "Λ" "Π" "∀".
 
+b-let emptyName (n : String) : Bool := or (stringEq n "") (stringEq n "_").
 b-let isArrow (b : Binder) : Bool := b ?Bool false false true true.
 b-let showBinderArrow (b : Binder) : String := b ?String "λ is not an arrow!" "Λ is not an arrow!" "->" "=>".
 
@@ -47,7 +48,7 @@ b-let showTermWithContext (t : Term) : List String -> String := recursionTerm ?(
   (λ v : Var. λ con : List String. showVar con v)
   (λ s : Sort. λ _ : List String. showSort s)
   (λ b : Binder. λ n : String. λ _, _ : Term. λ T, t : List String -> String. λ con : List String.
-    ifthenelse ?String (and (stringEq n "_") (isArrow b))
+    ifthenelse ?String (and (isArrow b) (emptyName n))
       φ"${T con} ${showBinderArrow b} ${t (cons ?String n con)}"
       φ"${showBinder b} ${n} : ${T con}. ${t (cons ?String n con)}")
   (λ _ : Term. λ la : List App. λ t : List String -> String.

diff --git a/mced/Test/Bootstrap/ShowTerm.mced b/mced/Test/Bootstrap/ShowTerm.mced
@@ -38,6 +38,7 @@ elet showVar (con : List String) (v : Var) : String :=
 let showSort (s : Sort) : String := s ?String "*" "□".
 let showBinder (b : Binder) : String := b ?String "λ" "Λ" "Π" "∀".
 
+let emptyName       (n : String) : Bool   := or (stringEq n "") (stringEq n "_").
 let isArrow         (b : Binder) : Bool   := b ?Bool false false true true.
 let showBinderArrow (b : Binder) : String :=
   b ?String "λ is not an arrow!" "Λ is not an arrow!" "->" "=>".
@@ -58,7 +59,7 @@ elet showTermWithContext : Term -> List String -> String := recursionTerm ?_
   (λ v : Var. λ con : List String. showVar con v)
   (λ s : Sort. λ _ : List String. showSort s)
   (λ b : Binder. λ n : String. λ _, _ : Term. λ T, t : List String -> String. λ con : List String.
-    ifthenelse ?_ (and (stringEq n "_") (isArrow b))
+    ifthenelse ?_ (and (isArrow b) (emptyName n))
       φ"${T con} ${showBinderArrow b} ${t (n ∷ con)}"
       φ"${showBinder b} ${n} : ${T con}. ${t (n ∷ con)}")
   (λ _ : Term. λ la : List App. λ t : List String -> String.