8c2a516 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -641,6 +641,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

641 -- | interface dictionary, eval only when a function

642 -- argument, and further evaluation results.

643 | Dictionary

644+ | OverlappingDictionary -- ^ Interface dictionary which may overlap

644 | Implicit -- ^ implicit coercion

645 | Implicit -- ^ implicit coercion

645 | NoImplicit -- ^ do not apply implicit coercions

646 | NoImplicit -- ^ do not apply implicit coercions

646 | CExport String -- ^ export, with a C name

647 | CExport String -- ^ export, with a C name

src/Idris/Elab/Implementation.hs+6−2

@@ -93,10 +93,12 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

93 -- if the implementation type matches any of the implementations we have already,

94 -- and it's not a named implementation, then it's overlapping, so report an error

95 case expn of

96+ Nothing

97+ | OverlappingDictionary `notElem` opts ->

96− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

98+ do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

97 (map fst $ interface_implementations ci)

99 (map fst $ interface_implementations ci)

98 addImplementation intImpl True n iname

100 addImplementation intImpl True n iname

99− Just _ -> addImplementation intImpl False n iname

101+ _ -> addImplementation intImpl False n iname

100 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do

102 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do

101 -- Add the parent implementation names to the privileged set

103 -- Add the parent implementation names to the privileged set

102 oldOpen <- addOpenImpl parents

104 oldOpen <- addOpenImpl parents

@@ -255,6 +257,8 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

255

257

256 findOverlapping i dets t n

258 findOverlapping i dets t n

257 | SN (ParentN _ _) <- n = Nothing

259 | SN (ParentN _ _) <- n = Nothing

260+ | Just opts <- lookupCtxtExact n (idris_flags i),

261+ OverlappingDictionary `elem` opts = Nothing

258 | otherwise

262 | otherwise

259 = case lookupTy n (tt_ctxt i) of

263 = case lookupTy n (tt_ctxt i) of

260 [t'] -> let tret = getRetType t

264 [t'] -> let tret = getRetType t

src/Idris/IBC.hs+2

@@ -1222,6 +1222,7 @@ instance Binary FnOpt where

1222 AutoHint -> putWord8 15

1223 PEGenerated -> putWord8 16

1224 StaticFn -> putWord8 17

1225+ OverlappingDictionary -> putWord8 18

1225 get

1226 get

1226 = do i <- getWord8

1227 = do i <- getWord8

1227 case i of

1228 case i of

@@ -1245,6 +1246,7 @@ instance Binary FnOpt where

1245 15 -> return AutoHint

1246 15 -> return AutoHint

1246 16 -> return PEGenerated

1247 16 -> return PEGenerated

1247 17 -> return StaticFn

1248 17 -> return StaticFn

1249+ 18 -> return OverlappingDictionary

1248 _ -> error "Corrupted binary data for FnOpt"

1250 _ -> error "Corrupted binary data for FnOpt"

1249

1251

1250instance Binary Fixity where

1252instance Binary Fixity where

src/Idris/Parser.hs+2

@@ -691,6 +691,8 @@ fnOpt = do reservedHL "total"; return TotalFn

691 return Reflection

692 <|> do try (lchar '%' *> reserved "hint");

693 return AutoHint

694+ <|> do try (lchar '%' *> reserved "overlapping");

695+ return OverlappingDictionary

694 <|> do lchar '%'; reserved "specialise";

696 <|> do lchar '%'; reserved "specialise";

695 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

697 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

696 return $ Specialise ns

698 return $ Specialise ns