382542a · Idris-dev · git.iko.soy

libs/effects/Effects.idr+1

compare with master

unifiedsplit

@@ -152,6 +152,7 @@ data Eff : (x : Type)

152 Eff t [x] xs' -> -- [x] (\v => xs) ->

153 Eff t [l ::: x] (\v => map (l :::) (xs' v))

154

155+%no_implicit

155(>>=) : Eff a xs xs' ->

156(>>=) : Eff a xs xs' ->

156 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

157 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

157(>>=) = ebind

158(>>=) = ebind

src/Idris/AbsSyntaxTree.hs+1

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

476 | Dictionary -- type class dictionary, eval only when

477 -- a function argument, and further evaluation resutls

478 | Implicit -- implicit coercion

479+ | NoImplicit -- do not apply implicit coercions

479 | CExport String -- export, with a C name

480 | CExport String -- export, with a C name

480 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

481 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

481 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

482 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

src/Idris/ElabTerm.hs+14

@@ -855,9 +855,23 @@ elab ist info emode opts fn tm

855 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

856 [pexp t])

857

858+

859+ -- Don't put implicit coercions around applications which are marked

860+ -- as '%noImplicit', or around case blocks, otherwise we get exponential

861+ -- blowup especially where there are errors deep in large expressions.

862+ notImplicitable (PApp _ f _) = notImplicitable f

863+ -- TMP HACK no coercing on bind (make this configurable)

864+ notImplicitable (PRef _ n)

865+ | [opts] <- lookupCtxt n (idris_flags ist)

866+ = NoImplicit `elem` opts

867+ notImplicitable (PAlternative True as) = any notImplicitable as

858 -- case is tricky enough without implicit coercions! If they are needed,

868 -- case is tricky enough without implicit coercions! If they are needed,

859 -- they can go in the branches separately.

869 -- they can go in the branches separately.

870+ notImplicitable (PCase _ _ _) = True

871+ notImplicitable _ = False

872+

860 insertCoerce ina t@(PCase _ _ _) = return t

873 insertCoerce ina t@(PCase _ _ _) = return t

874+ insertCoerce ina t | notImplicitable t = return t

861 insertCoerce ina t =

875 insertCoerce ina t =

862 do ty <- goal

876 do ty <- goal

863 -- Check for possible coercions to get to the goal

877 -- Check for possible coercions to get to the goal

src/Idris/IBC.hs+3

@@ -274,6 +274,7 @@ process i fn

274 pDefs (symbols i) (ibc_defs i)

275 pPatdefs (ibc_patdefs i)

276 pAccess (ibc_access i)

277+ pFlags (ibc_flags i)

277 pTotal (ibc_total i)

278 pTotal (ibc_total i)

278 pTotCheckErr (ibc_totcheckfail i)

279 pTotCheckErr (ibc_totcheckfail i)

279 pCG (ibc_cg i)

280 pCG (ibc_cg i)

@@ -943,6 +944,7 @@ instance Binary FnOpt where

943 ErrorHandler -> putWord8 9

944 ErrorHandler -> putWord8 9

944 ErrorReverse -> putWord8 10

945 ErrorReverse -> putWord8 10

945 CoveringFn -> putWord8 11

946 CoveringFn -> putWord8 11

947+ NoImplicit -> putWord8 12

946 get

948 get

947 = do i <- getWord8

949 = do i <- getWord8

948 case i of

950 case i of

@@ -959,6 +961,7 @@ instance Binary FnOpt where

959 9 -> return ErrorHandler

961 9 -> return ErrorHandler

960 10 -> return ErrorReverse

962 10 -> return ErrorReverse

961 11 -> return CoveringFn

963 11 -> return CoveringFn

964+ 12 -> return NoImplicit

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

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

963

966

964instance Binary Fixity where

967instance Binary Fixity where

src/Idris/Parser.hs+3

@@ -376,6 +376,7 @@ fnDecl' syn = checkFixity $

376FnOpts ::= 'total'

377 | 'partial'

378 | 'implicit'

379+ | '%' 'no_implicit'

379 | '%' 'assert_total'

380 | '%' 'assert_total'

380 | '%' 'error_handler'

381 | '%' 'error_handler'

381 | '%' 'reflection'

382 | '%' 'reflection'

@@ -402,6 +403,8 @@ fnOpts opts

402 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

403 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

403 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;

404 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;

404 fnOpts (CExport c : opts)

405 fnOpts (CExport c : opts)

406+ <|> do try (lchar '%' *> reserved "no_implicit");

407+ fnOpts (NoImplicit : opts)

405 <|> do try (lchar '%' *> reserved "assert_total");

408 <|> do try (lchar '%' *> reserved "assert_total");

406 fnOpts (AssertTotal : opts)

409 fnOpts (AssertTotal : opts)

407 <|> do try (lchar '%' *> reserved "error_handler");

410 <|> do try (lchar '%' *> reserved "error_handler");