22fcec9 · Idris-dev · git.iko.soy

src/Core/TT.hs+6−6

compare with master

unifiedsplit

@@ -273,15 +273,15 @@ instance Show SpecialName where

273-- Show a name in a way decorated for code generation, not human reading

274showCG :: Name -> String

275showCG (UN n) = n

276−showCG (NS n s) = showSep "." (reverse s) ++ "." ++ show n

276+showCG (NS n s) = showSep "." (reverse s) ++ "." ++ showCG n

277showCG (MN _ "underscore") = "_"

278showCG (MN i s) = "{" ++ s ++ show i ++ "}"

279showCG (SN s) = showCG' s

280− where showCG' (WhereN i p c) = show p ++ ":" ++ show c ++ ":" ++ show i

280+ where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

281− showCG' (InstanceN cl inst) = '@':show cl ++ '$':showSep ":" inst

281+ showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" inst

282− showCG' (MethodN m) = '!':show m

282+ showCG' (MethodN m) = '!':showCG m

283− showCG' (ParentN p c) = show p ++ "#" ++ show c

283+ showCG' (ParentN p c) = showCG p ++ "#" ++ show c

284− showCG' (CaseN c) = show c ++ "_case"

284+ showCG' (CaseN c) = showCG c ++ "_case"

285showCG NErased = "_"

286

287

src/Idris/AbsSyntax.hs−20

@@ -1361,26 +1361,6 @@ findStatics ist tm = trace (showImp Nothing True False tm) $

1361 return (PPi p n t sc')

1362 pos ns ss t = return t

1363

1364−-- Debugging/logging stuff

1365−

1366−dumpDecls :: [PDecl] -> String

1367−dumpDecls [] = ""

1368−dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

1369−

1370−dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

1371−dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t

1372−dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

1373−dumpDecl (PData _ _ _ _ d) = showDImp True d

1374−dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

1375−dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"

1376−dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

1377−dumpDecl (PClass _ _ _ cs n ps ds)

1378− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

1379−dumpDecl (PInstance _ _ cs n _ t _ ds)

1380− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

1381−dumpDecl _ = "..."

1382−-- dumpDecl (PImport i) = "import " ++ i

1383−

1384-- for 6.12/7 compatibility

1364-- for 6.12/7 compatibility

1385data EitherErr a b = LeftErr a | RightOK b

1365data EitherErr a b = LeftErr a | RightOK b

1386

1366

src/Idris/AbsSyntaxTree.hs+17−7

@@ -869,13 +869,23 @@ instance Show PClause where

869instance Show PData where

870 show d = showDImp False d

871

872+showDecls :: Bool -> [PDecl] -> String

873+showDecls _ [] = ""

874+showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds

875+

872showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

876showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

873−showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty

877+showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t

874−showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty

875−showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

878+showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)

876−showDeclImp _ (PData _ _ _ _ d) = show d

879+showDeclImp _ (PData _ _ _ _ d) = showDImp True d

877−showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

880+showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"

878− showSep "\n" (map show ps)

881+showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"

882+showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn

883+showDeclImp i (PClass _ _ _ cs n ps ds)

884+ = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds

885+showDeclImp i (PInstance _ _ cs n _ t _ ds)

886+ = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds

887+showDeclImp _ _ = "..."

888+-- showDeclImp (PImport i) = "import " ++ i

879

889

880

890

881showCImp :: Bool -> PClause -> String

891showCImp :: Bool -> PClause -> String

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

1121 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1131 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1122 Nothing -> showbasic n

1132 Nothing -> showbasic n

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

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

1124− showbasic n@(UN _) = show n

1134+ showbasic n@(UN _) = showCG n

1125 showbasic (MN _ s) = s

1135 showbasic (MN _ s) = s

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

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

1127 showbasic (SN s) = show s

1137 showbasic (SN s) = show s

src/Idris/Parser.hs+1−1

@@ -1021,7 +1021,7 @@ loadSource h lidr f

1021 f file pos

1022 unless (null ds') $ do

1023 let ds = namespaces mname ds'

1024− logLvl 3 (dumpDecls ds)

1024+ logLvl 3 (showDecls True ds)

1025 i <- getIState

1026 logLvl 10 (show (toAlist (idris_implicits i)))

1027 logLvl 3 (show (idris_infixes i))

src/Pkg/Package.hs+1−1

@@ -68,7 +68,7 @@ installPkg pkgdesc

68 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

69

70buildMods :: [Opt] -> [Name] -> IO ()

71−buildMods opts ns = do let f = map (toPath . show) ns

71+buildMods opts ns = do let f = map (toPath . showCG) ns

72-- putStrLn $ "MODULE: " ++ show f

73 idris (map Filename f ++ opts)

74 return ()