diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index f8ed93f..c999393 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -1,6 +1,7 @@ module Quox.Name import public Data.SnocList +import Data.List %default total @@ -18,6 +19,11 @@ brepr (UN x) = x export Eq BaseName where (==) = (==) `on` brepr export Ord BaseName where compare = compare `on` brepr +export +Show BaseName where + show (UN x) = x + + export baseStr : BaseName -> String baseStr (UN x) = x @@ -42,6 +48,11 @@ repr x = (x.mods, brepr x.base) export Eq Name where (==) = (==) `on` repr export Ord Name where compare = compare `on` repr +export +Show Name where + show (MakeName mods base) = + concat $ intersperse "." $ toList $ mods :< show base + export FromString Name where fromString x = MakeName [<] (fromString x) diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr index d5fe1c1..dffbb51 100644 --- a/lib/Quox/Syntax/Dim.idr +++ b/lib/Quox/Syntax/Dim.idr @@ -37,6 +37,11 @@ drepr (B x) = Right x export Eq (Dim n) where (==) = (==) `on` drepr export Ord (Dim n) where compare = compare `on` drepr +export +Show (Dim n) where + show (K k) = showCon App "K" $ show k + show (B i) = showCon App "B" $ show i + export PrettyHL DimConst where prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"