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

git.iko.soy/Idris-dev

Merge pull request #1287 from david-christiansen/postulate-providers

Distinguish postulate providers and type providers at use site

commit69aea8d2ba9253bb5f89e88aa42ae976d9e32208 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 5 Jun 2014, 14:35 (12 years ago) parent9593ae6 e5bc47e

12 files changed+43−91

compare with master

unifiedsplit

CHANGELOG+1−1 libs/base/Providers.idr−9 src/Idris/AbsSyntaxTree.hs+6−5 src/Idris/DeepSeq.hs+5−7 src/Idris/ElabDecls.hs+14−12 src/Idris/Parser.hs+13−12 src/Idris/Providers.hs+1−7 test/ffi005/Postulate.idr+3−3 test/ffi005/Postulate2.idr−13 test/ffi005/Postulate3.idr−13 test/ffi005/expected−2 test/ffi005/run−7

CHANGELOG+1−1

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

22--------------

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

44 --testpkg command-line option

5−

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

77New in 0.9.13:

88--------------

libs/base/Providers.idr−9

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

1111 ||| @ msg the error message

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

1313

14− ||| Postulate the goal type

15− Postulate : Provider a

16−

1714-- instances

1815instance Functor Provider where

1916 map f (Provide a) = Provide (f a)

2017 map f (Error err) = Error err

21− map f Postulate = Postulate

2218

2319instance Applicative Provider where

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

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

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

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

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

29− Postulate <$> _ = Postulate

3023 pure = Provide

3124

32−-- is this correct for Postulate?

3325instance Monad Provider where

3426 (Provide x) >>= f = f x

3527 (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

493493type DataOpts = [DataOpt]

494494

495495-- | Type provider - what to provide

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

497− | ProvPostulate -- ^ only allow postulates

498− | ProvAny -- ^ either is ok

499− deriving (Show, Eq)

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

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

498+ deriving (Show, Eq, Functor)

499+

500+type ProvideWhat = ProvideWhat' PTerm

500501

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

502503-- datatypes and typeclasses.

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

530531 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

536537 deriving Functor

src/Idris/DeepSeq.hs+5−7

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

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

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

158158 rnf (PDirective x1) = ()

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

160− = rnf x1 `seq`

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

159+ rnf (PProvider x1 x2 x3 x4)

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

162161 rnf (PTransform x1 x2 x3 x4)

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

164163

165−instance NFData ProvideWhat where

166− rnf ProvAny = ()

167− rnf ProvTerm = ()

168− rnf ProvPostulate = ()

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

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

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

169167

170168instance NFData PunInfo where

171169 rnf x = x `seq` ()

src/Idris/ElabDecls.hs+14−12

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

681681

682682

683683-- | Elaborate a type provider

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

685−elabProvider info syn fc what n ty tm

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

685+elabProvider info syn fc what n

686686 = do i <- getIState

687687 -- Ensure that the experimental extension is enabled

688688 unless (TypeProviders `elem` idris_language_extensions i) $

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

692692 ctxt <- getContext

693693

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

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

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

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

697+ ProvTerm ty p -> elabVal toplevel False ty

698+ ProvPostulate _ -> elabVal toplevel False PType

696699 unless (isTType typ) $

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

698701

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

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

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

704+ ProvTerm _ tm -> elabVal toplevel False tm

705+ ProvPostulate tm -> elabVal toplevel False tm

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

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

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

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

715720

716721 case provided of

717722 Provide tm

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

723+ | ProvTerm ty _ <- what ->

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

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

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

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

727729 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)

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

730732 | otherwise ->

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

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

24082410 addIBC (IBCDSL n)

24092411elabDecl' what info (PDirective i)

24102412 | what /= EDefns = i

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

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

24122414 | what /= EDefns

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

2414− elabProvider info syn fc provWhat n tp tm

2416+ elabProvider info syn fc provWhat n

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

24162418 = elabTransform info fc safety old new

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

src/Idris/Parser.hs+13−12

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

10611061 -}

10621062provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1064− what <- provideWhat

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]

1064+ provideTerm <|> providePostulate

10701065 <?> "type provider"

1071− where provideWhat :: IdrisParser ProvideWhat

1072− provideWhat = option ProvAny

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

1074− pure ProvTerm)

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

1076− <?> "provider variety")

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

1067+ fc <- getFC

1068+ reserved "with"

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

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

1071+ providePostulate = do reserved "postulate"

1072+ n <- fnName

1073+ fc <- getFC

1074+ reserved "with"

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

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

1077+

10771078{- | Parses a transform

10781079

10791080@

src/Idris/Providers.hs+1−7

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

1111

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

1313providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm

14+providerTy fc tm

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

1616

1717ioret = sUN "prim_io_return"

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

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

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

2120

2221data Provided a = Provide a

23− | Postulate

2422 deriving (Show, Eq, Functor)

2523

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

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

3634 , pioret == ioret && nm == prmod

3735 = return . Provide $ res

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

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

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

41− = return Postulate

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

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

4438

test/ffi005/Postulate.idr+3−3

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

55%language TypeProviders

7−bad : IO (Provider _|_)

8−bad = pure Postulate

7+bad : IO (Provider Type)

8+bad = return $ pure _|_

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

10+%provide postulate oops with bad

1111

1212main : IO ()

1313main = 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 @@

11oops

2−oops

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

test/ffi005/run−7

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

33idris $@ Postulate.idr -o postulate

44./postulate

55rm -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