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

git.iko.soy/Idris-dev

Added %auto_implicits directive

'%auto_implicits on' means that names in types will not be automatically bound; this could be useful for blocks which include lots of proofs, for example, or anywhere you want to be explicit about where names are bound.

commit8a9ca441ee74283755fc0f0fea6e0518a4962ece authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 1 Feb 2016, 17:20 (11 years ago) parent01484e6

12 files changed+119−13

compare with master

unifiedsplit

CHANGELOG+25−1 idris.cabal+3 src/Idris/AbsSyntax.hs+28−10 src/Idris/AbsSyntaxTree.hs+3 src/Idris/DeepSeq.hs+3−1 src/Idris/Directives.hs+2 src/Idris/Elab/Term.hs+3−1 src/Idris/Parser.hs+5 test/basic017/basic017.idr+25 test/basic017/basic017a.idr+15 test/basic017/expected+3 test/basic017/run+4

CHANGELOG+25−1

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

1919----------------------

2020

2121* 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

2327

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)

2448

2549New in 0.10:

2650============

idris.cabal+3

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

364364 test/basic016/run

365365 test/basic016/*.idr

366366 test/basic016/expected

367+ test/basic017/run

368+ test/basic017/*.idr

369+ test/basic017/expected

367370

368371 test/bignum001/run

369372 test/bignum001/*.idr

src/Idris/AbsSyntax.hs+28−10

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

774774logLevel = do i <- getIState

775775 return (opt_logLevel (idris_options i))

776776

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+

777787setErrContext :: Bool -> Idris ()

778788setErrContext t = do i <- getIState

779789 let opts = idris_options i

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

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

14321442addUsingImpls syn n fc t

14331443 = do ist <- getIState

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

1444+ autoimpl <- getAutoImpls

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+

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

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

14371451 when (not (null badnames)) $

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

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

15181532implicit' info syn ignore n ptm

15191533 = do i <- getIState

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

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

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

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

1524− addIBC (IBCImp n)

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

1526−-- i <- get

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

1528− return tm'

1534+ auto <- getAutoImpls

1535+ if not auto

1536+ then return ptm

1537+ else do

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

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

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

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

1542+ addIBC (IBCImp n)

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

1544+ -- i <- get

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

1546+ return tm'

15291547 where

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

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

src/Idris/AbsSyntaxTree.hs+3

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

9494 , opt_printdepth :: Maybe Int

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

9696 , opt_desugarnats :: Bool

97+ , opt_autoimpls :: Bool

9798 } deriving (Show, Eq)

9899

99100defaultOpts = IOption { opt_logLevel = 0

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

121122 , opt_printdepth = Just 5000

122123 , opt_evaltypes = True

123124 , opt_desugarnats = False

125+ , opt_autoimpls = True

124126 }

125127

126128data PPOption = PPOption {

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

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

759761 DLanguage LanguageExt |

760762 DDeprecate Name String |

763+ DAutoImplicits Bool |

761764 DUsed FC Name Name

762765

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

199199 opt_optimise

200200 opt_printdepth

201201 opt_evaltypes

202− opt_desugarnats) =

202+ opt_desugarnats

203+ opt_autoimpls) =

203204 rnf opt_logLevel

204205 `seq` rnf opt_typecase

205206 `seq` rnf opt_typeintype

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

224225 `seq` rnf opt_printdepth

225226 `seq` rnf opt_evaltypes

226227 `seq` rnf opt_desugarnats

228+ `seq` rnf opt_autoimpls

227229 `seq` ()

228230

229231instance NFData LanguageExt where

src/Idris/Directives.hs+2

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

6868 = do n' <- disambiguate n

6969 addDeprecated n' reason

7070 addIBC (IBCDeprecate n' reason)

71+directiveAction (DAutoImplicits b)

72+ = setAutoImpls b

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

7274

7375disambiguate :: Name -> Idris Name

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

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

236236 pattern = emode == ELHS

237237 intransform = emode == ETransLHS

238238 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS

239+ autoimpls = opt_autoimpls (idris_options ist)

239240

240241 get_delayed_elab est =

241242 let ds = delayed_elab est in

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

614615 [] -> False

615616 _ -> True

616617 bindable (NS _ _) = False

617− bindable n = implicitable n

618+ bindable (MN _ _) = True

619+ bindable n = implicitable n && autoimpls

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

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

620622 | 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")

13561356 fn <- fst <$> fnName

13571357 arg <- fst <$> iName []

13581358 return [PDirective (DUsed fc fn arg)]

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

1360+ b <- on_off

1361+ return [PDirective (DAutoImplicits b)]

13591362 <?> "directive"

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

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

13601365

13611366pLangExt :: IdrisParser LanguageExt

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

test/basic017/basic017.idrnew file+25

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

1+%auto_implicits off

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

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

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

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

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

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

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

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