2a0885e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better representation and rendering of generated names

In particular, this means that type class instances and methods, and names in where clauses, will have more readable names in error messages. Needs make relib

commit2a0885e6d40ed7b4a0c88e7923e3a1fa688af82c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 10 Sep 2013, 20:18 (13 years ago) parent43878f4

12 files changed+131−28

compare with master

unifiedsplit

CHANGELOG+1 src/Core/Elaborate.hs+1 src/Core/TT.hs+44−1 src/IRTS/CodegenC.hs+1−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Delaborate.hs+12−1 src/Idris/ElabDecls.hs+14−7 src/Idris/ElabTerm.hs+8−3 src/Idris/IBC.hs+46−12 test/reg006/expected+1−1 test/test020/expected+1−1 test/test030/expected+1−1

CHANGELOG+1

@@ -7,6 +7,7 @@ New in 0.9.10:

77 in the scope e

88* At the REPL, "it" now refers to the previous expression

99* Semantic colouring at the REPL. Turn this off with --nocolour.

10+* Some prettifying of error message

1011

1112Internal changes

1213

src/Core/Elaborate.hs+1

@@ -394,6 +394,7 @@ prepare_apply fn imps =

394394

395395 mkMN n@(MN _ _) = n

396396 mkMN n@(UN x) = MN 1000 x

397+ mkMN n@(SN s) = MN 1000 (show s)

397398 mkMN (NS n xs) = NS (mkMN n) xs

398399

399400 rebind hs (Bind n t sc)

src/Core/TT.hs+44−1

@@ -193,29 +193,64 @@ data Name = UN String -- ^ User-provided name

193193 | NS Name [String] -- ^ Root, namespaces

194194 | MN Int String -- ^ Machine chosen names

195195 | NErased -- ^ Name of somethng which is never used in scope

196+ | SN SpecialName -- ^ Decorated function names

196197 deriving (Eq, Ord)

197198{-!

198199deriving instance Binary Name

199200!-}

200201

202+data SpecialName = WhereN Int Name Name

203+ | InstanceN Name [String]

204+ | ParentN Name String

205+ | MethodN Name

206+ | CaseN Name

207+ deriving (Eq, Ord)

208+{-!

209+deriving instance Binary SpecialName

210+!-}

211+

201212instance Sized Name where

202213 size (UN n) = 1

203214 size (NS n els) = 1 + length els

204215 size (MN i n) = 1

205− size NErased = 1

216+ size _ = 1

206217

207218instance Pretty Name where

208219 pretty (UN n) = text n

209220 pretty (NS n s) = pretty n

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

222+ pretty (SN s) = text (show s)

211223

212224instance Show Name where

213225 show (UN n) = n

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

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

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

229+ show (SN s) = show s

217230 show NErased = "_"

218231

232+instance Show SpecialName where

233+ show (WhereN i p c) = show p ++ ", " ++ show c

234+ show (InstanceN cl inst) = showSep ", " inst ++ " instance of " ++ show cl

235+ show (MethodN m) = "method " ++ show m

236+ show (ParentN p c) = show p ++ "#" ++ c

237+ show (CaseN n) = "case block in " ++ show n

238+

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

240+showCG :: Name -> String

241+showCG (UN n) = n

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

243+showCG (MN _ "underscore") = "_"

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

245+showCG (SN s) = showCG' s

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

247+ showCG' (InstanceN cl inst) = '@':show cl ++ '$':show inst

248+ showCG' (MethodN m) = '!':show m

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

250+ showCG' (CaseN c) = show c ++ "_case"

251+showCG NErased = "_"

252+

253+

219254-- |Contexts allow us to map names to things. A root name maps to a collection

220255-- of things in different namespaces with that name.

221256type Ctxt a = Map.Map Name (Map.Map Name a)

@@ -223,6 +258,9 @@ emptyContext = Map.empty

223258

224259tcname (UN ('@':_)) = True

225260tcname (NS n _) = tcname n

261+tcname (SN (InstanceN _ _)) = True

262+tcname (SN (MethodN _)) = True

263+tcname (SN (ParentN _ _)) = True

226264tcname _ = False

227265

228266implicitable (NS n _) = implicitable n

@@ -761,6 +799,11 @@ nextName (UN x) = let (num', nm') = span isDigit (reverse x)

761799 where

762800 readN "" = 0

763801 readN x = read x

802+nextName (SN x) = SN (nextName' x)

803+ where

804+ nextName' (WhereN i f x) = WhereN i f (nextName x)

805+ nextName' (CaseN n) = CaseN (nextName n)

806+ nextName' (MethodN n) = MethodN (nextName n)

764807

765808type Term = TT Name

766809type Type = Term

src/IRTS/CodegenC.hs+1−1

@@ -80,7 +80,7 @@ gccDbg TRACE = "-O2"

8080gccDbg _ = "-O2"

8181

8282cname :: Name -> String

83−cname n = "_idris_" ++ concatMap cchar (show n)

83+cname n = "_idris_" ++ concatMap cchar (showCG n)

8484 where cchar x | isAlpha x || isDigit x = [x]

8585 | otherwise = "_" ++ show (fromEnum x) ++ "_"

8686

src/Idris/AbsSyntaxTree.hs+1

@@ -1061,6 +1061,7 @@ showName ist bnd impl colour n = if colour then colourise n else showbasic n

10611061 showbasic n@(UN _) = show n

10621062 showbasic (MN _ s) = s

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

1064+ showbasic (SN s) = show s

10641065 fst3 (x, _, _) = x

10651066 colourise n = let ctxt' = fmap tt_ctxt ist in

10661067 case ctxt' of

src/Idris/Delaborate.hs+12−1

@@ -154,13 +154,24 @@ pshow i (ProofSearchFail e) = pshow i e

154154pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

155155pshow i (At f e) = show f ++ ":" ++ pshow i e

156156pshow i (Elaborating s n e) = "When elaborating " ++ s ++

157− showbasic n ++ ":\n" ++ pshow i e

157+ showqual i n ++ ":\n" ++ pshow i e

158158pshow i (ProviderError msg) = "Type provider error: " ++ msg

159159

160160showSc i [] = ""

161161showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

162162 where showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)

163163

164+showqual :: IState -> Name -> String

165+showqual i n = showName (Just i) [] False False (dens n)

166+ where

167+ dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of

168+ [_] -> n -- just one thing

169+ _ -> ns

170+ dens n = n

171+

164172showbasic n@(UN _) = show n

165173showbasic (MN _ s) = s

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

175+showbasic (SN s) = show s

176+

177+

src/Idris/ElabDecls.hs+14−7

@@ -869,8 +869,13 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

869869 checkInferred fc (delab' i crhs True) rhs

870870 return $ Right (clhs, crhs)

871871 where

872− decorate (NS x ns) = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])

873− decorate x = NS (UN ('#':show x)) [show cnum, show fname]

872+ decorate (NS x ns)

873+ = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])

874+-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])

875+ decorate x

876+ = SN (WhereN cnum fname x)

877+-- = NS (SN (WhereN cnum fname x)) [show cnum]

878+-- = NS (UN ('#':show x)) [show cnum, show fname]

874879

875880 sepBlocks bs = sepBlocks' [] bs where

876881 sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)

@@ -1134,7 +1139,7 @@ elabClass info syn doc fc constraints tn ps ds

11341139 pibind [] x = x

11351140 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

11361141

1137− mdec (UN n) = UN ('!':n)

1142+ mdec (UN n) = SN (MethodN (UN n))

11381143 mdec (NS x n) = NS (mdec x) n

11391144 mdec x = x

11401145

@@ -1174,7 +1179,8 @@ elabClass info syn doc fc constraints tn ps ds

11741179

11751180 -- Generate a function for chasing a dictionary constraint

11761181 cfun cn c syn all con

1177− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)

1182+ = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)

1183+ -- SN (ParentN cn (show con))

11781184 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

11791185 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

11801186 let lhs = PApp fc (PRef fc cfn) [pconst capp]

@@ -1254,7 +1260,8 @@ elabInstance info syn fc cs n ps t expn ds

12541260 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

12551261 let constraint = PApp fc (PRef fc n) (map pexp ps)

12561262 let iname = case expn of

1257− Nothing -> UN ('@':show n ++ "$" ++ show ps)

1263+ Nothing -> SN (InstanceN n (map show ps))

1264+ -- UN ('@':show n ++ "$" ++ show ps)

12581265 Just nm -> nm

12591266 -- if the instance type matches any of the instances we have already,

12601267 -- and it's not a named instance, then it's overlapping, so report an error

@@ -1351,8 +1358,8 @@ elabInstance info syn fc cs n ps t expn ds

13511358 _ -> return ps'

13521359 getWParams (_ : ps) = getWParams ps

13531360

1354− decorate ns iname (UN n) = NS (UN ('!':n)) ns

1355− decorate ns iname (NS (UN n) s) = NS (UN ('!':n)) ns

1361+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

1362+ decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

13561363

13571364 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

13581365

src/Idris/ElabTerm.hs+8−3

@@ -349,6 +349,7 @@ elab ist info pattern tcgen fn tm

349349 elabIArg _ = return () -- already done, just a name

350350

351351 mkN n@(NS _ _) = n

352+ mkN n@(SN _) = n

352353 mkN n = case namespace info of

353354 Just xs@(_:_) -> NS n xs

354355 _ -> n

@@ -498,8 +499,10 @@ elab ist info pattern tcgen fn tm

498499 movelast tyn

499500 solve

500501 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

501− mkCaseName (UN x) = UN (x ++ "_case")

502− mkCaseName (MN i x) = MN i (x ++ "_case")

502+ mkCaseName n = SN (CaseN n)

503+-- mkCaseName (UN x) = UN (x ++ "_case")

504+-- mkCaseName (MN i x) = MN i (x ++ "_case")

505+-- mkCaseName (SN s) =

503506 mkN n@(NS _ _) = n

504507 mkN n = case namespace info of

505508 Just xs@(_:_) -> NS n xs

@@ -685,7 +688,8 @@ resolveTC depth fn ist

685688

686689 -- HACK! Rather than giving a special name, better to have some kind

687690 -- of flag in ClassInfo structure

688− chaser (UN ('@':'@':_)) = True

691+ chaser (UN ('@':'@':_)) = True -- old way

692+ chaser (SN (ParentN _ _)) = True

689693 chaser (NS n _) = chaser n

690694 chaser _ = False

691695

@@ -1208,6 +1212,7 @@ reflectName (NS n ns)

12081212reflectName (MN i n)

12091213 = reflCall "MN" [RConstant (I i), RConstant (Str n)]

12101214reflectName (NErased) = Var (reflm "NErased")

1215+reflectName n = Var (reflm "NErased") -- special name, not yet implemented

12111216

12121217reflectBinder :: Binder Term -> Raw

12131218reflectBinder (Lam t)

src/Idris/IBC.hs+46−12

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 37

26+ibcVersion = 38

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -356,21 +356,18 @@ instance Binary FC where

356356

357357instance Binary Name where

358358 put x

359− = {-# SCC "putName" #-}

360− case x of

361− UN x1 -> {-# SCC "putUN" #-}

362− do putWord8 0

363− {-# SCC "putNString" #-} put x1

364− NS x1 x2 -> {-# SCC "putNS" #-}

365− do putWord8 1

359+ = case x of

360+ UN x1 -> do putWord8 0

361+ put x1

362+ NS x1 x2 -> do putWord8 1

366363 put x1

367364 put x2

368− MN x1 x2 -> {-# SCC "putMN" #-}

369− do putWord8 2

365+ MN x1 x2 -> do putWord8 2

370366 put x1

371367 put x2

372− NErased -> {-# SCC "putNErased" #-}

373− putWord8 3

368+ NErased -> putWord8 3

369+ SN x1 -> do putWord8 4

370+ put x1

374371 get

375372 = do i <- getWord8

376373 case i of

@@ -383,8 +380,45 @@ instance Binary Name where

383380 x2 <- get

384381 return (MN x1 x2)

385382 3 -> return NErased

383+ 4 -> do x1 <- get

384+ return (SN x1)

386385 _ -> error "Corrupted binary data for Name"

387386

387+instance Binary SpecialName where

388+ put x

389+ = case x of

390+ WhereN x1 x2 x3 -> do putWord8 0

391+ put x1

392+ put x2

393+ put x3

394+ InstanceN x1 x2 -> do putWord8 1

395+ put x1

396+ put x2

397+ ParentN x1 x2 -> do putWord8 2

398+ put x1

399+ put x2

400+ MethodN x1 -> do putWord8 3

401+ put x1

402+ CaseN x1 -> do putWord8 4; put x1

403+ get

404+ = do i <- getWord8

405+ case i of

406+ 0 -> do x1 <- get

407+ x2 <- get

408+ x3 <- get

409+ return (WhereN x1 x2 x3)

410+ 1 -> do x1 <- get

411+ x2 <- get

412+ return (InstanceN x1 x2)

413+ 2 -> do x1 <- get

414+ x2 <- get

415+ return (ParentN x1 x2)

416+ 3 -> do x1 <- get

417+ return (MethodN x1)

418+ 4 -> do x1 <- get

419+ return (CaseN x1)

420+ _ -> error "Corrupted binary data for SpecialName"

421+

388422

389423instance Binary Const where

390424 put x

test/reg006/expected+1−1

@@ -1 +1 @@

1−reg006.idr:17:RBTree.lookup is possibly not total due to: RBTree.lookup_case

1+reg006.idr:17:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

test/test020/expected+1−1

@@ -1,4 +1,4 @@

1−When elaborating right hand side of Main.foo:

1+When elaborating right hand side of foo:

22test020a.idr:16:Can't unify Vect n a with List a

44Specifically:

test/test030/expected+1−1

@@ -1,4 +1,4 @@

1−test030a.idr:12:When elaborating right hand side of test030.testReflect1:

1+test030a.idr:12:When elaborating right hand side of testReflect1:

22Can't unify IsJust (Just x) with IsJust (prove (getProof x))

44Specifically: