quote names in Show

lib/Quox/Name.idr

@@ -31,7 +31,7 @@ baseStr (UN x)   = x
 baseStr (MN x i) = "\{x}#\{show i}"
 baseStr Unused   = "_"
 
-export Show BaseName where show = baseStr
+export Show BaseName where show = show . baseStr
 export FromString BaseName where fromString = UN
 
 
@@ -82,7 +82,8 @@ fromPBaseName = MakeName [<] . UN
 
 export
 Show PName where
-  show (MakePName mods base) = concat $ intersperse "." $ toList $ mods :< base
+  show (MakePName mods base) =
+    show $ concat $ intersperse "." $ toList $ mods :< base
 
 export Show Name where show = show . toPName
 

lib/Quox/Parser/Parser.idr

@@ -89,7 +89,8 @@ terminalMatch what l r = terminalMatchN_ what [(l, r)]
 ||| tag without leading `'`
 export
 bareTag : Grammar True TagVal
-bareTag = terminalMatchN "bare tag" [(`(Name t), `(show t)), (`(Str s), `(s))]
+bareTag = terminalMatchN "bare tag"
+  [(`(Name t), `(toDotsP t)), (`(Str s), `(s))]
 
 ||| tag with leading quote
 export

pack.toml

@@ -1,4 +1,4 @@
-collection = "nightly-230505"
+collection = "nightly-230522"
 
 [custom.all.tap]
 type = "git"

quox-nat.agda

@@ -1,78 +0,0 @@
-open import Axiom.Extensionality.Propositional
-
-module _ (ext : ∀ {a b} → Extensionality a b) where
-
-open import Prelude hiding (zero; suc)
-open import Data.W renaming (induction to induction′)
-open import Data.Container
-open import Data.Container.Relation.Unary.All ; open □
-
-variable
-  𝓀 ℓ : Level
-  A B : Set 𝓀
-  P Q : A → Set ℓ
-  C : Container 𝓀 ℓ
-
-
-data Tag : Set where `zero `suc : Tag
-
-Body : Tag → Set
-Body t = case t of λ {`zero → ⊥ ; `suc → ⊤}
-
-Repr : Container lzero lzero
-Repr = Tag ▷ Body
-
-Nat : Set
-Nat = W Repr
-
-Nat′ : Set
-Nat′ = ⟦ Repr ⟧ Nat
-
-zero : Nat
-zero = sup (`zero , λ ())
-
-suc : Nat → Nat
-suc n = sup (`suc , const n)
-
-induction : 
-  (P : W C → Set ℓ) →
-  (IH : (t : ⟦ C ⟧ (W C)) → □ C P t → P (sup t)) →
-  (w : W C) → P w
-induction P IH = induction′ P (λ {t} → IH t)
-
-
-elim : (P : Nat → Set ℓ) →
-       (Z : P zero) →
-       (S : ∀ n → P n → P (suc n)) →
-       (n : Nat) → P n
-elim P Z S = induction _ λ (tag , body) →
-  body |>
-  (case tag
-   return (λ t → (n′ : Body t → Nat) →
-                  □ Repr P (t , n′) →
-                  P (sup (t , n′)))
-   of λ where
-     `zero → λ n′ _  → ≡.subst (λ n′ → P (sup (`zero , n′))) (ext λ ()) Z
-     `suc  → λ n′ IH → S (n′ tt) (IH .proof tt))
-
-pred : Nat → Nat
-pred = induction _ λ n@(tag , body) _ →
-  body |>
-  (case tag
-   return (λ t → (Body t → Nat) → Nat)
-   of λ where
-     `zero _ → zero
-     `suc  n → n tt)
-
-Subterms : (A : Set 𝓀) (P : A → Set ℓ) → Set _
-Subterms A P = Σ[ x ∈ A ] (P x → W (A ▷ P))
-
-subterms : W (A ▷ P) → Subterms A P
-subterms = induction _ λ t IH → t
-
-natSub : Nat → List Nat
-natSub n =
-  case subterms n of λ where
-    (`zero , body) → []
-    (`suc  , body) → [ body tt ]
-  where open List