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

CHANGELOG+25−1

compare with master

unifiedsplit

@@ -19,8 +19,32 @@ Minor language changes

19----------------------

20

21* The '[static]' annotation is changed to '%static' to be consistent with the

22−other annotations.

22+ other annotations.

23+* Added '%auto_implicits' directive. The default is '%auto_implicits on'.

24+ Placing '%auto_implicits off' in a source file means that after that

25+ point, any implicit arguments must be bound, e.g.:

26+ append : {n,m,a:_} -> Vect n a -> Vect m a -> Vect (n + m) a

23

27

28+ Only names which are used explicitly in the type need to be bound, e.g.:

29+ Here : {x, xs : _} -> Elem x (x :: xs)

30+

31+ In 'Here', there is no need to bind any of the variables in the type of

32+ 'xs' (it could be e.g. List a or Vect n a; 'a' and 'n' will still be

33+ implicitly bound).

34+

35+ You can still implicitly bind with 'using':

36+

37+ using (xs : Vect _ _)

38+ data Elem : {a, n : _} -> a -> Vect n a -> Type where

39+ Here : {x : _} -> Elem x (x :: xs)

40+ There : {x, y : _} -> Elem x xs -> Elem x (y :: xs)

41+

42+ However, note that *only* names which appear in *both* the using block

43+ *and* the type being defined will be implicitly bound. The following will

44+ therefore fail because 'n' isn't implicitly bound:

45+

46+ using (xs : Vect n a)

47+ bad : Elem x xs -> Elem x (y :: xs)

24

48

25New in 0.10:

49New in 0.10:

26============

50============

idris.cabal+3

@@ -364,6 +364,9 @@ Extra-source-files:

364 test/basic016/run

365 test/basic016/*.idr

366 test/basic016/expected

367+ test/basic017/run

368+ test/basic017/*.idr

369+ test/basic017/expected

367

370

368 test/bignum001/run

371 test/bignum001/run

369 test/bignum001/*.idr

372 test/bignum001/*.idr

src/Idris/AbsSyntax.hs+28−10

@@ -774,6 +774,16 @@ logLevel :: Idris Int

774logLevel = do i <- getIState

775 return (opt_logLevel (idris_options i))

776

777+setAutoImpls :: Bool -> Idris ()

778+setAutoImpls b = do i <- getIState

779+ let opts = idris_options i

780+ let opt' = opts { opt_autoimpls = b }

781+ putIState $ i { idris_options = opt' }

782+

783+getAutoImpls :: Idris Bool

784+getAutoImpls = do i <- getIState

785+ return (opt_autoimpls (idris_options i))

786+

777setErrContext :: Bool -> Idris ()

787setErrContext :: Bool -> Idris ()

778setErrContext t = do i <- getIState

788setErrContext t = do i <- getIState

779 let opts = idris_options i

789 let opts = idris_options i

@@ -1431,7 +1441,11 @@ addUsingConstraints syn fc t

1431addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm

1441addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm

1432addUsingImpls syn n fc t

1442addUsingImpls syn n fc t

1433 = do ist <- getIState

1443 = do ist <- getIState

1444+ autoimpl <- getAutoImpls

1434− let ns = implicitNamesIn (map iname uimpls) ist t

1445+ let ns_in = implicitNamesIn (map iname uimpls) ist t

1446+ let ns = if autoimpl then ns_in

1447+ else filter (\n -> n `elem` (map iname uimpls)) ns_in

1448+

1435 let badnames = filter (\n -> not (implicitable n) &&

1449 let badnames = filter (\n -> not (implicitable n) &&

1436 n `notElem` (map iname uimpls)) ns

1450 n `notElem` (map iname uimpls)) ns

1437 when (not (null badnames)) $

1451 when (not (null badnames)) $

@@ -1517,15 +1531,19 @@ implicit info syn n ptm = implicit' info syn [] n ptm

1517implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1531implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1518implicit' info syn ignore n ptm

1532implicit' info syn ignore n ptm

1519 = do i <- getIState

1533 = do i <- getIState

1534+ auto <- getAutoImpls

1535+ if not auto

1536+ then return ptm

1537+ else do

1520− let (tm', impdata) = implicitise syn ignore i ptm

1538+ let (tm', impdata) = implicitise syn ignore i ptm

1521− defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

1539+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

1522−-- let (tm'', spos) = findStatics i tm'

1540+ -- let (tm'', spos) = findStatics i tm'

1523− putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1541+ putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1524− addIBC (IBCImp n)

1542+ addIBC (IBCImp n)

1525− logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

1543+ logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

1526−-- i <- get

1544+ -- i <- get

1527−-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1545+ -- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1528− return tm'

1546+ return tm'

1529 where

1547 where

1530 -- Detect unknown names in default arguments and throw error if found.

1548 -- Detect unknown names in default arguments and throw error if found.

1531 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1549 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

src/Idris/AbsSyntaxTree.hs+3

@@ -94,6 +94,7 @@ data IOption = IOption {

94 , opt_printdepth :: Maybe Int

95 , opt_evaltypes :: Bool -- ^ normalise types in :t

96 , opt_desugarnats :: Bool

97+ , opt_autoimpls :: Bool

97 } deriving (Show, Eq)

98 } deriving (Show, Eq)

98

99

99defaultOpts = IOption { opt_logLevel = 0

100defaultOpts = IOption { opt_logLevel = 0

@@ -121,6 +122,7 @@ defaultOpts = IOption { opt_logLevel = 0

121 , opt_printdepth = Just 5000

122 , opt_printdepth = Just 5000

122 , opt_evaltypes = True

123 , opt_evaltypes = True

123 , opt_desugarnats = False

124 , opt_desugarnats = False

125+ , opt_autoimpls = True

124 }

126 }

125

127

126data PPOption = PPOption {

128data PPOption = PPOption {

@@ -758,6 +760,7 @@ data Directive = DLib Codegen String |

758 DErrorHandlers Name FC Name FC [(Name, FC)] |

760 DErrorHandlers Name FC Name FC [(Name, FC)] |

759 DLanguage LanguageExt |

761 DLanguage LanguageExt |

760 DDeprecate Name String |

762 DDeprecate Name String |

763+ DAutoImplicits Bool |

761 DUsed FC Name Name

764 DUsed FC Name Name

762

765

763-- | A set of instructions for things that need to happen in IState

766-- | A set of instructions for things that need to happen in IState

src/Idris/DeepSeq.hs+3−1

@@ -199,7 +199,8 @@ instance NFData IOption where

199 opt_optimise

200 opt_printdepth

201 opt_evaltypes

202− opt_desugarnats) =

202+ opt_desugarnats

203+ opt_autoimpls) =

203 rnf opt_logLevel

204 rnf opt_logLevel

204 `seq` rnf opt_typecase

205 `seq` rnf opt_typecase

205 `seq` rnf opt_typeintype

206 `seq` rnf opt_typeintype

@@ -224,6 +225,7 @@ instance NFData IOption where

224 `seq` rnf opt_printdepth

225 `seq` rnf opt_printdepth

225 `seq` rnf opt_evaltypes

226 `seq` rnf opt_evaltypes

226 `seq` rnf opt_desugarnats

227 `seq` rnf opt_desugarnats

228+ `seq` rnf opt_autoimpls

227 `seq` ()

229 `seq` ()

228

230

229instance NFData LanguageExt where

231instance NFData LanguageExt where

src/Idris/Directives.hs+2

@@ -68,6 +68,8 @@ directiveAction (DDeprecate n reason)

68 = do n' <- disambiguate n

69 addDeprecated n' reason

70 addIBC (IBCDeprecate n' reason)

71+directiveAction (DAutoImplicits b)

72+ = setAutoImpls b

71directiveAction (DUsed fc fn arg) = addUsedName fc fn arg

73directiveAction (DUsed fc fn arg) = addUsedName fc fn arg

72

74

73disambiguate :: Name -> Idris Name

75disambiguate :: Name -> Idris Name

src/Idris/Elab/Term.hs+3−1

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

236 pattern = emode == ELHS

237 intransform = emode == ETransLHS

238 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS

239+ autoimpls = opt_autoimpls (idris_options ist)

239

240

240 get_delayed_elab est =

241 get_delayed_elab est =

241 let ds = delayed_elab est in

242 let ds = delayed_elab est in

@@ -614,7 +615,8 @@ elab ist info emode opts fn tm

614 [] -> False

615 [] -> False

615 _ -> True

616 _ -> True

616 bindable (NS _ _) = False

617 bindable (NS _ _) = False

618+ bindable (MN _ _) = True

617− bindable n = implicitable n

619+ bindable n = implicitable n && autoimpls

618 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

620 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

619 elab' ina fc' tm@(PRef fc hls n)

621 elab' ina fc' tm@(PRef fc hls n)

620 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

622 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

src/Idris/Parser.hs+5

@@ -1356,7 +1356,12 @@ directive syn = do try (lchar '%' *> reserved "lib")

1356 fn <- fst <$> fnName

1357 arg <- fst <$> iName []

1358 return [PDirective (DUsed fc fn arg)]

1359+ <|> do try (lchar '%' *> reserved "auto_implicits")

1360+ b <- on_off

1361+ return [PDirective (DAutoImplicits b)]

1359 <?> "directive"

1362 <?> "directive"

1363+ where on_off = do reserved "on"; return True

1364+ <|> do reserved "off"; return False

1360

1365

1361pLangExt :: IdrisParser LanguageExt

1366pLangExt :: IdrisParser LanguageExt

1362pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1367pLangExt = (reserved "TypeProviders" >> return TypeProviders)

test/basic017/basic017.idrnew file+25

@@ -0,0 +1,25 @@

1+%auto_implicits off

2+

3+data Vect : Nat -> Type -> Type where

4+ Nil : {a : _} -> Vect Z a

5+ (::) : {a, k : _} -> a -> Vect k a -> Vect (S k) a

6+

7+data Elem : {a, n : _} -> a -> Vect n a -> Type where

8+ Here : {x, xs : _} -> Elem x (x :: xs)

9+ There : {x, y, xs : _} -> Elem x xs -> Elem x (y :: xs)

10+

11+using (xs : Vect _ _)

12+ data Elem2 : {a, n : _} -> a -> Vect n a -> Type where

13+ Here2 : {x : _} -> Elem2 x (x :: xs)

14+ There2 : {x, y : _} -> Elem2 x xs -> Elem2 x (y :: xs)

15+

16+append : {n, m, a : _} -> Vect n a -> Vect m a -> Vect (n + m) a

17+append [] ys = ys

18+append (x :: xs) ys = x :: append xs ys

19+

20+%auto_implicits on

21+

22+append2 : Vect n a -> Vect m a -> Vect (n + m) a

23+append2 [] ys = ys

24+append2 (x :: xs) ys = x :: append2 xs ys

25+

test/basic017/basic017a.idrnew file+15

@@ -0,0 +1,15 @@

1+%auto_implicits off

2+

3+data Vect : Nat -> Type -> Type where

4+ Nil : {a : _} -> Vect Z a

5+ (::) : {a, k : _} -> a -> Vect k a -> Vect (S k) a

6+

7+data Elem : {a, n : _} -> a -> Vect n a -> Type where

8+ Here : {x, xs : _} -> Elem x (x :: xs)

9+ There : {x, y, xs : _} -> Elem x xs -> Elem x (y :: xs)

10+

11+append : Vect n a -> Vect m a -> Vect (n + m) a

12+append [] ys = ys

13+append (x :: xs) ys = x :: append xs ys

14+

15+

test/basic017/expectednew file+3

@@ -0,0 +1,3 @@

1+basic017a.idr:11:8:When checking type of Main.append:

2+When checking an application of Main.Vect:

3+ No such variable n

test/basic017/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic017.idr --check --nocolor

3+${IDRIS:-idris} $@ basic017a.idr --check --nocolor

4+rm -f *.ibc