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

CHANGELOG+1

compare with master

unifiedsplit

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

7 in the scope e

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

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

10+* Some prettifying of error message

10

11

11Internal changes

12Internal changes

12

13

src/Core/Elaborate.hs+1

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

394

395 mkMN n@(MN _ _) = n

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

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

397 mkMN (NS n xs) = NS (mkMN n) xs

398 mkMN (NS n xs) = NS (mkMN n) xs

398

399

399 rebind hs (Bind n t sc)

400 rebind hs (Bind n t sc)

src/Core/TT.hs+44−1

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

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

194 | MN Int String -- ^ Machine chosen names

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

196+ | SN SpecialName -- ^ Decorated function names

196 deriving (Eq, Ord)

197 deriving (Eq, Ord)

197{-!

198{-!

198deriving instance Binary Name

199deriving instance Binary Name

199!-}

200!-}

200

201

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+

201instance Sized Name where

212instance Sized Name where

202 size (UN n) = 1

213 size (UN n) = 1

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

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

204 size (MN i n) = 1

215 size (MN i n) = 1

205− size NErased = 1

216+ size _ = 1

206

217

207instance Pretty Name where

218instance Pretty Name where

208 pretty (UN n) = text n

219 pretty (UN n) = text n

209 pretty (NS n s) = pretty n

220 pretty (NS n s) = pretty n

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

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

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

211

223

212instance Show Name where

224instance Show Name where

213 show (UN n) = n

225 show (UN n) = n

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

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

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

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

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

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

229+ show (SN s) = show s

217 show NErased = "_"

230 show NErased = "_"

218

231

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+

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

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

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

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

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

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

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

223

258

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

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

225tcname (NS n _) = tcname n

260tcname (NS n _) = tcname n

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

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

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

226tcname _ = False

264tcname _ = False

227

265

228implicitable (NS n _) = implicitable n

266implicitable (NS n _) = implicitable n

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

761 where

799 where

762 readN "" = 0

800 readN "" = 0

763 readN x = read x

801 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)

764

807

765type Term = TT Name

808type Term = TT Name

766type Type = Term

809type Type = Term

src/IRTS/CodegenC.hs+1−1

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

80gccDbg _ = "-O2"

81

82cname :: Name -> String

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

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

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

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

86

src/Idris/AbsSyntaxTree.hs+1

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

1061 showbasic n@(UN _) = show n

1062 showbasic (MN _ s) = s

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

1064+ showbasic (SN s) = show s

1064 fst3 (x, _, _) = x

1065 fst3 (x, _, _) = x

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

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

1066 case ctxt' of

1067 case ctxt' of

src/Idris/Delaborate.hs+12−1

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

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

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

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

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

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

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

159

160showSc i [] = ""

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

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

163

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+

164showbasic n@(UN _) = show n

172showbasic n@(UN _) = show n

165showbasic (MN _ s) = s

173showbasic (MN _ s) = s

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

174showbasic (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)

869 checkInferred fc (delab' i crhs True) rhs

870 return $ Right (clhs, crhs)

871 where

872+ decorate (NS x ns)

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

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

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]

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

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

874

879

875 sepBlocks bs = sepBlocks' [] bs where

880 sepBlocks bs = sepBlocks' [] bs where

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

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

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

1134 pibind [] x = x

1139 pibind [] x = x

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

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

1136

1141

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

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

1138 mdec (NS x n) = NS (mdec x) n

1143 mdec (NS x n) = NS (mdec x) n

1139 mdec x = x

1144 mdec x = x

1140

1145

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

1174

1179

1175 -- Generate a function for chasing a dictionary constraint

1180 -- Generate a function for chasing a dictionary constraint

1176 cfun cn c syn all con

1181 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))

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

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

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

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

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

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

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

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

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

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

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

1256 let iname = case expn of

1262 let iname = case expn of

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

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

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

1258 Just nm -> nm

1265 Just nm -> nm

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

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

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

1267 -- 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

1351 _ -> return ps'

1358 _ -> return ps'

1352 getWParams (_ : ps) = getWParams ps

1359 getWParams (_ : ps) = getWParams ps

1353

1360

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

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

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

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

1356

1363

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

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

1358

1365

src/Idris/ElabTerm.hs+8−3

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

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

350

351 mkN n@(NS _ _) = n

352+ mkN n@(SN _) = n

352 mkN n = case namespace info of

353 mkN n = case namespace info of

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

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

354 _ -> n

355 _ -> n

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

498 movelast tyn

499 movelast tyn

499 solve

500 solve

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

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

502+ mkCaseName n = SN (CaseN n)

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

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

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

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

505+-- mkCaseName (SN s) =

503 mkN n@(NS _ _) = n

506 mkN n@(NS _ _) = n

504 mkN n = case namespace info of

507 mkN n = case namespace info of

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

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

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

685

688

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

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

687 -- of flag in ClassInfo structure

690 -- of flag in ClassInfo structure

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

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

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

689 chaser (NS n _) = chaser n

693 chaser (NS n _) = chaser n

690 chaser _ = False

694 chaser _ = False

691

695

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

1208reflectName (MN i n)

1212reflectName (MN i n)

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

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

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

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

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

1211

1216

1212reflectBinder :: Binder Term -> Raw

1217reflectBinder :: Binder Term -> Raw

1213reflectBinder (Lam t)

1218reflectBinder (Lam t)

src/Idris/IBC.hs+46−12

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

23import Paths_idris

24

25ibcVersion :: Word8

26−ibcVersion = 37

26+ibcVersion = 38

27

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

356

357instance Binary Name where

358 put x

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

360− case x of

359+ = case x of

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

362− do putWord8 0

360+ UN x1 -> do putWord8 0

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

361+ put x1

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

365− do putWord8 1

362+ NS x1 x2 -> do putWord8 1

366 put x1

363 put x1

367 put x2

364 put x2

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

369− do putWord8 2

365+ MN x1 x2 -> do putWord8 2

370 put x1

366 put x1

371 put x2

367 put x2

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

373− putWord8 3

368+ NErased -> putWord8 3

369+ SN x1 -> do putWord8 4

370+ put x1

374 get

371 get

375 = do i <- getWord8

372 = do i <- getWord8

376 case i of

373 case i of

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

383 x2 <- get

380 x2 <- get

384 return (MN x1 x2)

381 return (MN x1 x2)

385 3 -> return NErased

382 3 -> return NErased

383+ 4 -> do x1 <- get

384+ return (SN x1)

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

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

387

386

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+

388

422

389instance Binary Const where

423instance Binary Const where

390 put x

424 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:

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

3

4Specifically:

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:

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

3

4Specifically: