git.iko.soy/Idris-dev
on master help sign in
Remove NErased

The name constructor NErased was produced precisely two places in the source, each as a kind of failure representation rather than as a name referring to something that had been erased, like the docs stated. The vestigial constructor has been removed.

commit0f89577db795eaa8c809e8247dba025b2652dc3c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 9 Oct 2015, 12:07 (11 years ago) parentd5b66a9
10 files changed+22−39
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr−2 libs/prelude/Language/Reflection.idr+1−5 libs/pruviloj/Pruviloj/Core.idr−1 src/Idris/Core/Binary.hs+4−6 src/Idris/Core/DeepSeq.hs−1 src/Idris/Core/TT.hs−5 src/Idris/DSL.hs+1−1 src/Idris/Elab/Term.hs+12−11 src/Idris/IBC.hs+1−1 src/Idris/Reflection.hs+3−6
libs/base/Language/Reflection/Utils.idr−2
@@ -85,14 +85,12 @@ mutual
8585 showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns
8686 showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str
8787 showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)
88− showPrec d NErased = "NErased"
8988
9089mutual
9190 instance Eq TTName where
9291 (UN str1) == (UN str2) = str1 == str2
9392 (NS n ns) == (NS n' ns') = n == n' && ns == ns'
9493 (MN i str) == (MN i' str') = i == i' && str == str'
95− NErased == NErased = True
9694 (SN sn) == (SN sn') = assert_total $ sn == sn'
9795 x == y = False
9896
libs/prelude/Language/Reflection.idr+1−5
@@ -40,9 +40,7 @@ mutual
4040 MN Int String |
4141 ||| Special names, to make conflicts impossible and language features
4242 ||| predictable
43− SN SpecialName |
44− ||| Name of something which is never used in scope
45− NErased
43+ SN SpecialName
4644 %name TTName n, n'
4745
4846 data SpecialName = WhereN Int TTName TTName
@@ -478,7 +476,6 @@ mutual
478476 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
479477 quote (MN x y) = `(MN ~(quote x) ~(quote y))
480478 quote (SN sn) = `(SN ~(assert_total $ quote sn))
481− quote NErased = `(NErased)
482479
483480 instance Quotable SpecialName TT where
484481 quotedTy = `(SpecialName)
@@ -499,7 +496,6 @@ mutual
499496 quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))
500497 quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))
501498 quote (SN sn) = `(SN ~(assert_total $ quote sn))
502− quote NErased = `(NErased)
503499
504500 instance Quotable SpecialName Raw where
505501 quotedTy = `(SpecialName)
libs/pruviloj/Pruviloj/Core.idr−1
@@ -41,7 +41,6 @@ nameFrom (MN x n) =
4141 then "n"
4242 else n
4343nameFrom (SN x) = gensym "SN"
44−nameFrom NErased = gensym "wasErased"
4544
4645||| Get the name at the head of the term, if it exists.
4746headName : Raw -> Maybe TTName
src/Idris/Core/Binary.hs+4−6
@@ -302,10 +302,9 @@ instance Binary Name where
302302 MN x1 x2 -> do putWord8 2
303303 put x1
304304 put x2
305− NErased -> putWord8 3
306− SN x1 -> do putWord8 4
305+ SN x1 -> do putWord8 3
307306 put x1
308− SymRef x1 -> do putWord8 5
307+ SymRef x1 -> do putWord8 4
309308 put x1
310309 get
311310 = do i <- getWord8
@@ -318,10 +317,9 @@ instance Binary Name where
318317 2 -> do x1 <- get
319318 x2 <- get
320319 return (MN x1 x2)
321− 3 -> return NErased
322− 4 -> do x1 <- get
320+ 3 -> do x1 <- get
323321 return (SN x1)
324− 5 -> do x1 <- get
322+ 4 -> do x1 <- get
325323 return (SymRef x1)
326324 _ -> error "Corrupted binary data for Name"
327325
src/Idris/Core/DeepSeq.hs−1
@@ -13,7 +13,6 @@ instance NFData Name where
1313 rnf (UN x1) = rnf x1 `seq` ()
1414 rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
1515 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
16− rnf NErased = ()
1716 rnf (SN x1) = rnf x1 `seq` ()
1817 rnf (SymRef x1) = rnf x1 `seq` ()
1918
src/Idris/Core/TT.hs−5
@@ -447,7 +447,6 @@ traceWhen False _ a = a
447447data Name = UN !T.Text -- ^ User-provided name
448448 | NS !Name [T.Text] -- ^ Root, namespaces
449449 | MN !Int !T.Text -- ^ Machine chosen names
450− | NErased -- ^ Name of something which is never used in scope
451450 | SN !SpecialName -- ^ Decorated function names
452451 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
453452 deriving (Eq, Ord, Data, Typeable)
@@ -514,7 +513,6 @@ instance Pretty Name OutputAnnotation where
514513 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)
515514 pretty n@(SymRef i) = annotate (AnnName n Nothing Nothing Nothing) $
516515 text $ "##symbol" ++ show i ++ "##"
517− pretty NErased = annotate (AnnName NErased Nothing Nothing Nothing) $ text "_"
518516
519517instance Pretty [Name] OutputAnnotation where
520518 pretty = encloseSep empty empty comma . map pretty
@@ -526,7 +524,6 @@ instance Show Name where
526524 show (MN i s) = "{" ++ str s ++ show i ++ "}"
527525 show (SN s) = show s
528526 show (SymRef i) = "##symbol" ++ show i ++ "##"
529− show NErased = "_"
530527
531528instance Show SpecialName where
532529 show (WhereN i p c) = show p ++ ", " ++ show c
@@ -566,7 +563,6 @@ showCG (SN s) = showCG' s
566563 "_" ++ show (fst e) ++ "_" ++ show (snd e)
567564 cgFN = concatMap (\c -> if not (isDigit c || isLetter c) then "__" else [c])
568565showCG (SymRef i) = error "can't do codegen for a symbol reference"
569−showCG NErased = "_"
570566
571567
572568-- |Contexts allow us to map names to things. A root name maps to a collection
@@ -1455,7 +1451,6 @@ nextName (SN x) = SN (nextName' x)
14551451 nextName' (MethodN n) = MethodN (nextName n)
14561452 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)
14571453 nextName' (MetaN parent meta) = MetaN parent (nextName meta)
1458−nextName NErased = NErased
14591454nextName (SymRef i) = error "Can't generate a name from a symbol reference"
14601455
14611456type Term = TT Name
src/Idris/DSL.hs+1−1
@@ -42,7 +42,7 @@ mkTTName fc n =
4242 , pexp (mkList fc ns)]
4343 MN i nm -> PApp fc (PRef fc [] (reflm "MN")) [ pexp (intC i)
4444 , pexp (stringC nm)]
45− otherwise -> PRef fc [] $ reflm "NErased"
45+ _ -> error "Invalid name from user syntax for DSL name"
4646
4747expandSugar :: DSL -> PTerm -> PTerm
4848expandSugar dsl (PLam fc n nfc ty tm)
src/Idris/Elab/Term.hs+12−11
@@ -443,16 +443,17 @@ elab ist info emode opts fn tm
443443 uns <- get_usedns
444444 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
445445 (h : hs) <- get_holes
446−-- trace (show (map showHd as')) $
447446 ty <- goal
448447 case as' of
449− [] -> lift $ tfail $ NoValidAlts (map showHd as)
448+ [] -> do hds <- mapM showHd as
449+ lift $ tfail $ NoValidAlts hds
450450 [x] -> elab' ina fc x
451451 -- If there's options, try now, and if that fails, postpone
452452 -- to later.
453453 _ -> handleError isAmbiguous
454− (tryAll (zip (map (elab' ina fc) as')
455− (map showHd as')))
454+ (do hds <- mapM showHd as'
455+ tryAll (zip (map (elab' ina fc) as')
456+ hds))
456457 (do movelast h
457458 delayElab 5 $ do
458459 hs <- get_holes
@@ -461,16 +462,17 @@ elab ist info emode opts fn tm
461462 as'' <- doPrune as'
462463 case as'' of
463464 [x] -> elab' ina fc x
464− _ -> tryAll (zip (map (elab' ina fc) as'')
465− (map showHd as'')))
465+ _ -> do hds <- mapM showHd as''
466+ tryAll (zip (map (elab' ina fc) as'')
467+ hds))
466468 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
467469 | l == txt "Delay" = showHd (getTm arg)
468− showHd (PApp _ (PRef _ _ n) _) = n
469− showHd (PRef _ _ n) = n
470+ showHd (PApp _ (PRef _ _ n) _) = return n
471+ showHd (PRef _ _ n) = return n
470472 showHd (PApp _ h _) = showHd h
471− showHd x = NErased -- We probably should do something better than this here
473+ showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
472474
473− doPrune as =
475+ doPrune as =
474476 do compute
475477 ty <- goal
476478 let (tc, _) = unApply (unDelay ty)
@@ -480,7 +482,6 @@ elab ist info emode opts fn tm
480482 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
481483 l == txt "Lazy'" = unDelay arg
482484 | otherwise = t
483−
484485
485486 isAmbiguous (CantResolveAlts _) = delayok
486487 isAmbiguous (Elaborating _ _ e) = isAmbiguous e
src/Idris/IBC.hs+1−1
@@ -40,7 +40,7 @@ import System.Directory
4040import Codec.Archive.Zip
4141
4242ibcVersion :: Word16
43−ibcVersion = 122
43+ibcVersion = 123
4444
4545data IBCFile = IBCFile { ver :: Word16,
4646 sourcefile :: FilePath,
src/Idris/Reflection.hs+3−6
@@ -270,8 +270,6 @@ reifyTTNameApp t [sn]
270270 | t == reflm "MetaN" =
271271 MetaN <$> reifyTTName n1 <*> reifyTTName n2
272272 reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args
273−reifyTTNameApp t []
274− | t == reflm "NErased" = return NErased
275273reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
276274
277275reifyTTNamespace :: Term -> ElabD [String]
@@ -679,7 +677,6 @@ reflectName (NS n ns)
679677 ]
680678reflectName (MN i n)
681679 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
682−reflectName NErased = Var (reflm "NErased")
683680reflectName (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]
684681reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"
685682
@@ -963,7 +960,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "
963960 Right (TextPart msg)
964961reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
965962 | n == reflm "NamePart" =
966− case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext emptyContext Erased) of
963+ case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of
967964 Error e -> Left . InternalMsg $
968965 "could not reify name term " ++
969966 show ttn ++
@@ -971,7 +968,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
971968 OK (n', _)-> Right $ NamePart n'
972969reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
973970 | n == reflm "TermPart" =
974− case runElab initEState (reifyTT tm) (initElaborator NErased initContext emptyContext Erased) of
971+ case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of
975972 Error e -> Left . InternalMsg $
976973 "could not reify reflected term " ++
977974 show tm ++
@@ -979,7 +976,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
979976 OK (tm', _) -> Right $ TermPart tm'
980977reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
981978 | n == reflm "RawPart" =
982− case runElab initEState (reifyRaw tm) (initElaborator NErased initContext emptyContext Erased) of
979+ case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of
983980 Error e -> Left . InternalMsg $
984981 "could not reify reflected raw term " ++
985982 show tm ++