0f89577 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr−2

compare with master

unifiedsplit

@@ -85,14 +85,12 @@ mutual

85 showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns

86 showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str

87 showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)

88− showPrec d NErased = "NErased"

89

88

90mutual

89mutual

91 instance Eq TTName where

90 instance Eq TTName where

92 (UN str1) == (UN str2) = str1 == str2

91 (UN str1) == (UN str2) = str1 == str2

93 (NS n ns) == (NS n' ns') = n == n' && ns == ns'

92 (NS n ns) == (NS n' ns') = n == n' && ns == ns'

94 (MN i str) == (MN i' str') = i == i' && str == str'

93 (MN i str) == (MN i' str') = i == i' && str == str'

95− NErased == NErased = True

96 (SN sn) == (SN sn') = assert_total $ sn == sn'

94 (SN sn) == (SN sn') = assert_total $ sn == sn'

97 x == y = False

95 x == y = False

98

96

libs/prelude/Language/Reflection.idr+1−5

@@ -40,9 +40,7 @@ mutual

40 MN Int String |

41 ||| Special names, to make conflicts impossible and language features

42 ||| predictable

43− SN SpecialName |

43+ SN SpecialName

44− ||| Name of something which is never used in scope

45− NErased

46 %name TTName n, n'

44 %name TTName n, n'

47

45

48 data SpecialName = WhereN Int TTName TTName

46 data SpecialName = WhereN Int TTName TTName

@@ -478,7 +476,6 @@ mutual

478 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))

476 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))

479 quote (MN x y) = `(MN ~(quote x) ~(quote y))

477 quote (MN x y) = `(MN ~(quote x) ~(quote y))

480 quote (SN sn) = `(SN ~(assert_total $ quote sn))

478 quote (SN sn) = `(SN ~(assert_total $ quote sn))

481− quote NErased = `(NErased)

482

479

483 instance Quotable SpecialName TT where

480 instance Quotable SpecialName TT where

484 quotedTy = `(SpecialName)

481 quotedTy = `(SpecialName)

@@ -499,7 +496,6 @@ mutual

499 quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))

496 quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))

500 quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))

497 quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))

501 quote (SN sn) = `(SN ~(assert_total $ quote sn))

498 quote (SN sn) = `(SN ~(assert_total $ quote sn))

502− quote NErased = `(NErased)

503

499

504 instance Quotable SpecialName Raw where

500 instance Quotable SpecialName Raw where

505 quotedTy = `(SpecialName)

501 quotedTy = `(SpecialName)

libs/pruviloj/Pruviloj/Core.idr−1

@@ -41,7 +41,6 @@ nameFrom (MN x n) =

41 then "n"

42 else n

43nameFrom (SN x) = gensym "SN"

44−nameFrom NErased = gensym "wasErased"

45

44

46||| Get the name at the head of the term, if it exists.

45||| Get the name at the head of the term, if it exists.

47headName : Raw -> Maybe TTName

46headName : Raw -> Maybe TTName

src/Idris/Core/Binary.hs+4−6

@@ -302,10 +302,9 @@ instance Binary Name where

302 MN x1 x2 -> do putWord8 2

303 put x1

304 put x2

305− NErased -> putWord8 3

306− SN x1 -> do putWord8 4

305+ SN x1 -> do putWord8 3

307 put x1

306 put x1

308− SymRef x1 -> do putWord8 5

307+ SymRef x1 -> do putWord8 4

309 put x1

308 put x1

310 get

309 get

311 = do i <- getWord8

310 = do i <- getWord8

@@ -318,10 +317,9 @@ instance Binary Name where

318 2 -> do x1 <- get

317 2 -> do x1 <- get

319 x2 <- get

318 x2 <- get

320 return (MN x1 x2)

319 return (MN x1 x2)

321− 3 -> return NErased

322− 4 -> do x1 <- get

320+ 3 -> do x1 <- get

323 return (SN x1)

321 return (SN x1)

324− 5 -> do x1 <- get

322+ 4 -> do x1 <- get

325 return (SymRef x1)

323 return (SymRef x1)

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

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

327

325

src/Idris/Core/DeepSeq.hs−1

@@ -13,7 +13,6 @@ instance NFData Name where

13 rnf (UN x1) = rnf x1 `seq` ()

14 rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

15 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

16− rnf NErased = ()

17 rnf (SN x1) = rnf x1 `seq` ()

16 rnf (SN x1) = rnf x1 `seq` ()

18 rnf (SymRef x1) = rnf x1 `seq` ()

17 rnf (SymRef x1) = rnf x1 `seq` ()

19

18

src/Idris/Core/TT.hs−5

@@ -447,7 +447,6 @@ traceWhen False _ a = a

447data Name = UN !T.Text -- ^ User-provided name

448 | NS !Name [T.Text] -- ^ Root, namespaces

449 | MN !Int !T.Text -- ^ Machine chosen names

450− | NErased -- ^ Name of something which is never used in scope

451 | SN !SpecialName -- ^ Decorated function names

450 | SN !SpecialName -- ^ Decorated function names

452 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

451 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

453 deriving (Eq, Ord, Data, Typeable)

452 deriving (Eq, Ord, Data, Typeable)

@@ -514,7 +513,6 @@ instance Pretty Name OutputAnnotation where

514 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)

513 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)

515 pretty n@(SymRef i) = annotate (AnnName n Nothing Nothing Nothing) $

514 pretty n@(SymRef i) = annotate (AnnName n Nothing Nothing Nothing) $

516 text $ "##symbol" ++ show i ++ "##"

515 text $ "##symbol" ++ show i ++ "##"

517− pretty NErased = annotate (AnnName NErased Nothing Nothing Nothing) $ text "_"

518

516

519instance Pretty [Name] OutputAnnotation where

517instance Pretty [Name] OutputAnnotation where

520 pretty = encloseSep empty empty comma . map pretty

518 pretty = encloseSep empty empty comma . map pretty

@@ -526,7 +524,6 @@ instance Show Name where

526 show (MN i s) = "{" ++ str s ++ show i ++ "}"

524 show (MN i s) = "{" ++ str s ++ show i ++ "}"

527 show (SN s) = show s

525 show (SN s) = show s

528 show (SymRef i) = "##symbol" ++ show i ++ "##"

526 show (SymRef i) = "##symbol" ++ show i ++ "##"

529− show NErased = "_"

530

527

531instance Show SpecialName where

528instance Show SpecialName where

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

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

@@ -566,7 +563,6 @@ showCG (SN s) = showCG' s

566 "_" ++ show (fst e) ++ "_" ++ show (snd e)

563 "_" ++ show (fst e) ++ "_" ++ show (snd e)

567 cgFN = concatMap (\c -> if not (isDigit c || isLetter c) then "__" else [c])

564 cgFN = concatMap (\c -> if not (isDigit c || isLetter c) then "__" else [c])

568showCG (SymRef i) = error "can't do codegen for a symbol reference"

565showCG (SymRef i) = error "can't do codegen for a symbol reference"

569−showCG NErased = "_"

570

566

571

567

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

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

1455 nextName' (MethodN n) = MethodN (nextName n)

1451 nextName' (MethodN n) = MethodN (nextName n)

1456 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)

1452 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)

1457 nextName' (MetaN parent meta) = MetaN parent (nextName meta)

1453 nextName' (MetaN parent meta) = MetaN parent (nextName meta)

1458−nextName NErased = NErased

1459nextName (SymRef i) = error "Can't generate a name from a symbol reference"

1454nextName (SymRef i) = error "Can't generate a name from a symbol reference"

1460

1455

1461type Term = TT Name

1456type Term = TT Name

src/Idris/DSL.hs+1−1

@@ -42,7 +42,7 @@ mkTTName fc n =

42 , pexp (mkList fc ns)]

43 MN i nm -> PApp fc (PRef fc [] (reflm "MN")) [ pexp (intC i)

44 , pexp (stringC nm)]

45− otherwise -> PRef fc [] $ reflm "NErased"

45+ _ -> error "Invalid name from user syntax for DSL name"

46

47expandSugar :: DSL -> PTerm -> PTerm

48expandSugar 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

443 uns <- get_usedns

444 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned

445 (h : hs) <- get_holes

446−-- trace (show (map showHd as')) $

447 ty <- goal

446 ty <- goal

448 case as' of

447 case as' of

448+ [] -> do hds <- mapM showHd as

449− [] -> lift $ tfail $ NoValidAlts (map showHd as)

449+ lift $ tfail $ NoValidAlts hds

450 [x] -> elab' ina fc x

451 -- If there's options, try now, and if that fails, postpone

452 -- to later.

453 _ -> handleError isAmbiguous

454+ (do hds <- mapM showHd as'

454− (tryAll (zip (map (elab' ina fc) as')

455+ tryAll (zip (map (elab' ina fc) as')

455− (map showHd as')))

456+ hds))

456 (do movelast h

457 (do movelast h

457 delayElab 5 $ do

458 delayElab 5 $ do

458 hs <- get_holes

459 hs <- get_holes

@@ -461,16 +462,17 @@ elab ist info emode opts fn tm

461 as'' <- doPrune as'

462 as'' <- doPrune as'

462 case as'' of

463 case as'' of

463 [x] -> elab' ina fc x

464 [x] -> elab' ina fc x

465+ _ -> do hds <- mapM showHd as''

464− _ -> tryAll (zip (map (elab' ina fc) as'')

466+ tryAll (zip (map (elab' ina fc) as'')

465− (map showHd as'')))

467+ hds))

466 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])

468 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])

467 | l == txt "Delay" = showHd (getTm arg)

469 | l == txt "Delay" = showHd (getTm arg)

468− showHd (PApp _ (PRef _ _ n) _) = n

470+ showHd (PApp _ (PRef _ _ n) _) = return n

469− showHd (PRef _ _ n) = n

471+ showHd (PRef _ _ n) = return n

470 showHd (PApp _ h _) = showHd h

472 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

472

474

473− doPrune as =

475+ doPrune as =

474 do compute

476 do compute

475 ty <- goal

477 ty <- goal

476 let (tc, _) = unApply (unDelay ty)

478 let (tc, _) = unApply (unDelay ty)

@@ -480,7 +482,6 @@ elab ist info emode opts fn tm

480 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,

482 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,

481 l == txt "Lazy'" = unDelay arg

483 l == txt "Lazy'" = unDelay arg

482 | otherwise = t

484 | otherwise = t

483−

484

485

485 isAmbiguous (CantResolveAlts _) = delayok

486 isAmbiguous (CantResolveAlts _) = delayok

486 isAmbiguous (Elaborating _ _ e) = isAmbiguous e

487 isAmbiguous (Elaborating _ _ e) = isAmbiguous e

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 122

43+ibcVersion = 123

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/Reflection.hs+3−6

@@ -270,8 +270,6 @@ reifyTTNameApp t [sn]

270 | t == reflm "MetaN" =

271 MetaN <$> reifyTTName n1 <*> reifyTTName n2

272 reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args

273−reifyTTNameApp t []

274− | t == reflm "NErased" = return NErased

275reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

273reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

276

274

277reifyTTNamespace :: Term -> ElabD [String]

275reifyTTNamespace :: Term -> ElabD [String]

@@ -679,7 +677,6 @@ reflectName (NS n ns)

679 ]

677 ]

680reflectName (MN i n)

678reflectName (MN i n)

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

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

682−reflectName NErased = Var (reflm "NErased")

683reflectName (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]

680reflectName (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]

684reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"

681reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"

685

682

@@ -963,7 +960,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "

963 Right (TextPart msg)

960 Right (TextPart msg)

964reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

961reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

965 | n == reflm "NamePart" =

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

967 Error e -> Left . InternalMsg $

964 Error e -> Left . InternalMsg $

968 "could not reify name term " ++

965 "could not reify name term " ++

969 show ttn ++

966 show ttn ++

@@ -971,7 +968,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

971 OK (n', _)-> Right $ NamePart n'

968 OK (n', _)-> Right $ NamePart n'

972reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

969reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

973 | n == reflm "TermPart" =

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

975 Error e -> Left . InternalMsg $

972 Error e -> Left . InternalMsg $

976 "could not reify reflected term " ++

973 "could not reify reflected term " ++

977 show tm ++

974 show tm ++

@@ -979,7 +976,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

979 OK (tm', _) -> Right $ TermPart tm'

976 OK (tm', _) -> Right $ TermPart tm'

980reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

977reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

981 | n == reflm "RawPart" =

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

983 Error e -> Left . InternalMsg $

980 Error e -> Left . InternalMsg $

984 "could not reify reflected raw term " ++

981 "could not reify reflected raw term " ++

985 show tm ++

982 show tm ++