725587f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed testing failures I accidentally introduced when showing a better naming for machine generated names (so that I could better debug)

725587fAhmad Salim Al-Sibahi13 years ago

src/Core/TT.hs+2−2

@@ -253,14 +253,14 @@ instance Sized Name where

253instance Pretty Name where

254 pretty (UN n) = text n

255 pretty (NS n s) = pretty n

256− pretty (MN i s) = text "«" <+> text s <+> (text . show $ i) <+> text "»"

256+ pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace

257 pretty (SN s) = text (show s)

258

259instance Show Name where

260 show (UN n) = n

261 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

262 show (MN _ "underscore") = "_"

263− show (MN i s) = "«" ++ s ++ show i ++ "»"

263+ show (MN i s) = "{" ++ s ++ show i ++ "}"

264 show (SN s) = show s

265 show NErased = "_"

266

src/Idris/AbsSyntaxTree.hs+2−2

@@ -940,7 +940,7 @@ prettyImp impl = prettySe 10

940 prettyBasic n

941 where

942 prettyBasic n@(UN _) = pretty n

943− prettyBasic n@(MN _ _) = pretty n

943+ prettyBasic (MN _ s) = text s

944 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n

945 prettyBasic (SN sn) = text (show sn)

946 prettySe p (PLam n ty sc) =

@@ -1126,7 +1126,7 @@ showName ist bnd impl colour n = case ist of

1126 Nothing -> showbasic n

1127 where name = if impl then show n else showbasic n

1128 showbasic n@(UN _) = show n

1129− showbasic n@(MN _ _) = show n

1129+ showbasic (MN _ s) = s

1130 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

1131 showbasic (SN s) = show s

1132 fst3 (x, _, _) = x