e5bc47e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Distinguish postulate providers and type providers at use site

This is not backwards compatible, but as far as I know, there are no users of postulate providers who are not me. The old system allowed both the definition of the provider and the use site to be involved in the determination of what is a postulate and what is not. This is not good - users should always be in full control of this. The new implementation has two syntaxes: %provide (x : t) with p %provide postulate x with p The first is the type provider syntax we know and love. The second requires that the provider in fact return a type, which is then made into the type of the resulting postulate.

commite5bc47eec30c022946848254e30942eadb9ef764 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 5 Jun 2014, 13:49 (12 years ago) parent9593ae6

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