69aea8d · Idris-dev · git.iko.soy

CHANGELOG+1−1

compare with master

unifiedsplit

@@ -2,7 +2,7 @@ New in 0.9.14:

2--------------

3* Support for running tests for a package with the tests section of .ipkg files and the

4 --testpkg command-line option

5−

5+* Clearly distinguish between type providers and postulate providers at the use site

6

7New in 0.9.13:

8--------------

libs/base/Providers.idr−9

@@ -11,26 +11,17 @@ data Provider : (a : Type) -> Type where

11 ||| @ msg the error message

12 Error : (msg : String) -> Provider a

13

14− ||| Postulate the goal type

15− Postulate : Provider a

16−

17-- instances

14-- instances

18instance Functor Provider where

15instance Functor Provider where

19 map f (Provide a) = Provide (f a)

16 map f (Provide a) = Provide (f a)

20 map f (Error err) = Error err

17 map f (Error err) = Error err

21− map f Postulate = Postulate

22

18

23instance Applicative Provider where

19instance Applicative Provider where

24 (Provide f) <$> (Provide x) = Provide (f x)

20 (Provide f) <$> (Provide x) = Provide (f x)

25 (Provide f) <$> (Error err) = Error err

21 (Provide f) <$> (Error err) = Error err

26− (Provide f) <$> Postulate = Postulate

27 (Error err) <$> _ = Error err

22 (Error err) <$> _ = Error err

28− Postulate <$> (Error err) = Error err

29− Postulate <$> _ = Postulate

30 pure = Provide

23 pure = Provide

31

24

32−-- is this correct for Postulate?

33instance Monad Provider where

25instance Monad Provider where

34 (Provide x) >>= f = f x

26 (Provide x) >>= f = f x

35 (Error err) >>= _ = Error err

27 (Error err) >>= _ = Error err

36− Postulate >>= f = Postulate

src/Idris/AbsSyntaxTree.hs+6−5

@@ -493,10 +493,11 @@ data DataOpt = Codata -- Set if the the data-type is coinductive

493type DataOpts = [DataOpt]

494

495-- | Type provider - what to provide

496−data ProvideWhat = ProvTerm -- ^ only allow providing terms

496+data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

497− | ProvPostulate -- ^ only allow postulates

497+ | ProvPostulate t -- ^ goal type must be Type, so only term

498− | ProvAny -- ^ either is ok

499− deriving (Show, Eq)

498+ deriving (Show, Eq, Functor)

499+

500+type ProvideWhat = ProvideWhat' PTerm

500

501

501-- | Top-level declarations such as compiler directives, definitions,

502-- | Top-level declarations such as compiler directives, definitions,

502-- datatypes and typeclasses.

503-- datatypes and typeclasses.

@@ -530,7 +531,7 @@ data PDecl' t

530 | PSyntax FC Syntax -- ^ Syntax definition

531 | PSyntax FC Syntax -- ^ Syntax definition

531 | PMutual FC [PDecl' t] -- ^ Mutual block

532 | PMutual FC [PDecl' t] -- ^ Mutual block

532 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

533 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

533− | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term

534+ | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

534 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

535 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

535 -- bool is True, lhs and rhs must be convertible

536 -- bool is True, lhs and rhs must be convertible

536 deriving Functor

537 deriving Functor

src/Idris/DeepSeq.hs+5−7

@@ -156,16 +156,14 @@ instance (NFData t) => NFData (PDecl' t) where

156 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

157 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

158 rnf (PDirective x1) = ()

159− rnf (PProvider x1 x2 x3 x4 x5 x6)

159+ rnf (PProvider x1 x2 x3 x4)

160− = rnf x1 `seq`

161− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

160+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

162 rnf (PTransform x1 x2 x3 x4)

161 rnf (PTransform x1 x2 x3 x4)

163 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

162 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

164

163

165−instance NFData ProvideWhat where

164+instance NFData t => NFData (ProvideWhat' t) where

166− rnf ProvAny = ()

165+ rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

167− rnf ProvTerm = ()

168− rnf ProvPostulate = ()

166+ rnf (ProvPostulate tm) = rnf tm `seq` ()

169

167

170instance NFData PunInfo where

168instance NFData PunInfo where

171 rnf x = x `seq` ()

169 rnf x = x `seq` ()

src/Idris/ElabDecls.hs+14−12

@@ -681,8 +681,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

681

682

683-- | Elaborate a type provider

684−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()

684+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

685−elabProvider info syn fc what n ty tm

685+elabProvider info syn fc what n

686 = do i <- getIState

687 -- Ensure that the experimental extension is enabled

688 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -692,12 +692,17 @@ elabProvider info syn fc what n ty tm

692 ctxt <- getContext

693

694 -- First elaborate the expected type (and check that it's a type)

695+ -- The goal type for a postulate is always Type.

696+ (ty', typ) <- case what of

695− (ty', typ) <- elabVal toplevel False ty

697+ ProvTerm ty p -> elabVal toplevel False ty

698+ ProvPostulate _ -> elabVal toplevel False PType

696 unless (isTType typ) $

699 unless (isTType typ) $

697 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

700 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

698

701

699 -- Elaborate the provider term to TT and check that the type matches

702 -- Elaborate the provider term to TT and check that the type matches

703+ (e, et) <- case what of

704+ ProvTerm _ tm -> elabVal toplevel False tm

700− (e, et) <- elabVal toplevel False tm

705+ ProvPostulate tm -> elabVal toplevel False tm

701 unless (isProviderOf (normalise ctxt [] ty') et) $

706 unless (isProviderOf (normalise ctxt [] ty') et) $

702 ifail $ "Expected provider type IO (Provider (" ++

707 ifail $ "Expected provider type IO (Provider (" ++

703 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

708 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

@@ -715,17 +720,14 @@ elabProvider info syn fc what n ty tm

715

720

716 case provided of

721 case provided of

717 Provide tm

722 Provide tm

718− | what `elem` [ProvTerm, ProvAny] ->

723+ | ProvTerm ty _ <- what ->

719 do -- Finally add a top-level definition of the provided term

724 do -- Finally add a top-level definition of the provided term

720 elabType info syn emptyDocstring [] fc [] n ty

725 elabType info syn emptyDocstring [] fc [] n ty

721 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

726 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

722 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

727 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

723− | otherwise ->

724− ierror . Msg $ "Attempted to provide a term where a postulate was expected."

725− Postulate

726− | what `elem` [ProvPostulate, ProvAny] ->

728+ | ProvPostulate _ <- what ->

727 do -- Add the postulate

729 do -- Add the postulate

728− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty

730+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

729 logLvl 3 $ "Elaborated provided postulate " ++ show n

731 logLvl 3 $ "Elaborated provided postulate " ++ show n

730 | otherwise ->

732 | otherwise ->

731 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

733 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

@@ -2408,10 +2410,10 @@ elabDecl' _ info (PDSL n dsl)

2408 addIBC (IBCDSL n)

2410 addIBC (IBCDSL n)

2409elabDecl' what info (PDirective i)

2411elabDecl' what info (PDirective i)

2410 | what /= EDefns = i

2412 | what /= EDefns = i

2411−elabDecl' what info (PProvider syn fc provWhat n tp tm)

2413+elabDecl' what info (PProvider syn fc provWhat n)

2412 | what /= EDefns

2414 | what /= EDefns

2413 = do iLOG $ "Elaborating type provider " ++ show n

2415 = do iLOG $ "Elaborating type provider " ++ show n

2414− elabProvider info syn fc provWhat n tp tm

2416+ elabProvider info syn fc provWhat n

2415elabDecl' what info (PTransform fc safety old new)

2417elabDecl' what info (PTransform fc safety old new)

2416 = elabTransform info fc safety old new

2418 = elabTransform info fc safety old new

2417elabDecl' _ _ _ = return () -- skipped this time

2419elabDecl' _ _ _ = return () -- skipped this time

src/Idris/Parser.hs+13−12

@@ -1061,19 +1061,20 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1061 -}

1062provider :: SyntaxInfo -> IdrisParser [PDecl]

1063provider syn = do try (lchar '%' *> reserved "provide");

1064− what <- provideWhat

1064+ provideTerm <|> providePostulate

1065− lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1066− fc <- getFC

1067− reserved "with"

1068− e <- expr syn

1069− return [PProvider syn fc what n t e]

1070 <?> "type provider"

1065 <?> "type provider"

1071− where provideWhat :: IdrisParser ProvideWhat

1066+ where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1072− provideWhat = option ProvAny

1067+ fc <- getFC

1073− ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>

1068+ reserved "with"

1074− pure ProvTerm)

1069+ e <- expr syn <?> "provider expression"

1070+ return [PProvider syn fc (ProvTerm t e) n]

1075− <|> (reserved "postulate" *> pure ProvPostulate)

1071+ providePostulate = do reserved "postulate"

1076− <?> "provider variety")

1072+ n <- fnName

1073+ fc <- getFC

1074+ reserved "with"

1075+ e <- expr syn <?> "provider expression"

1076+ return [PProvider syn fc (ProvPostulate e) n]

1077+

1077{- | Parses a transform

1078{- | Parses a transform

1078

1079

1079@

1080@

src/Idris/Providers.hs+1−7

@@ -11,16 +11,14 @@ import Debug.Trace

11

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm

14+providerTy fc tm

15 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

16

17ioret = sUN "prim_io_return"

18ermod = sNS (sUN "Error") ["Providers"]

19prmod = sNS (sUN "Provide") ["Providers"]

20−posmod = sNS (sUN "Postulate") ["Providers"]

21

20

22data Provided a = Provide a

21data Provided a = Provide a

23− | Postulate

24 deriving (Show, Eq, Functor)

22 deriving (Show, Eq, Functor)

25

23

26-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

24-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

@@ -35,10 +33,6 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

35 , (P _ nm _, [_, res]) <- unApply result

33 , (P _ nm _, [_, res]) <- unApply result

36 , pioret == ioret && nm == prmod

34 , pioret == ioret && nm == prmod

37 = return . Provide $ res

35 = return . Provide $ res

38− | (P _ pioret _, [tp, result]) <- unApply tm

39− , (P _ nm _, [_]) <- unApply result

40− , pioret == ioret && nm == posmod

41− = return Postulate

42 | otherwise = ifail $ "Internal type provider error: result was not " ++

36 | otherwise = ifail $ "Internal type provider error: result was not " ++

43 "IO (Provider a), or perhaps missing normalisation."

37 "IO (Provider a), or perhaps missing normalisation."

44

38

test/ffi005/Postulate.idr+3−3

@@ -4,10 +4,10 @@ import Providers

4

5%language TypeProviders

6

7−bad : IO (Provider _|_)

7+bad : IO (Provider Type)

8−bad = pure Postulate

8+bad = return $ pure _|_

9

10−%provide (oops : _|_) with bad

10+%provide postulate oops with bad

11

12main : IO ()

13main = putStrLn "oops"

test/ffi005/Postulate2.idrdeleted−13

@@ -1,13 +0,0 @@

1−module Main

2−

3−import Providers

4−

5−%language TypeProviders

6−

7−bad : IO (Provider _|_)

8−bad = pure Postulate

9−

10−%provide postulate (oops : _|_) with bad

11−

12−main : IO ()

13−main = putStrLn "oops"

test/ffi005/Postulate3.idrdeleted−13

@@ -1,13 +0,0 @@

1−module Main

2−

3−import Providers

4−

5−%language TypeProviders

6−

7−bad : IO (Provider _|_)

8−bad = pure Postulate

9−

10−%provide term (oops : _|_) with bad

11−

12−main : IO ()

13−main = putStrLn "oops"

test/ffi005/expected−2

@@ -1,3 +1 @@

1oops

2−oops

3−Attempted to provide a postulate where a term was expected.

test/ffi005/run−7

@@ -3,10 +3,3 @@

3idris $@ Postulate.idr -o postulate

4./postulate

5rm -f postulate *.ibc

6−

7−idris $@ Postulate2.idr -o postulate

8−./postulate

9−rm -f postulate *.ibc

10−

11−idris $@ Postulate3.idr -o postulate

12−rm -f postulate *.ibc