0875310 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Control whether provider decls accept postulates

Extends the provider syntax to accept an optional "what" parameter, which controls if it can be satisfied with just proof terms, just postulates, or either.

commit0875310e6946d7b923c9925ee3d535aab3710dd8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 26 Feb 2014, 14:22 (13 years ago) parent5365977

10 files changed+83−23

compare with master

unifiedsplit

CHANGELOG+1 src/Idris/AbsSyntaxTree.hs+7−1 src/Idris/DeepSeq.hs+7−2 src/Idris/ElabDecls.hs+19−13 src/Idris/Parser.hs+10−3 test/ffi005/Postulate.idr+3−4 test/ffi005/Postulate2.idr+13 test/ffi005/Postulate3.idr+13 test/ffi005/expected+2 test/ffi005/run+8

CHANGELOG+1

@@ -9,6 +9,7 @@ New in 0.9.12:

99* Lots of performance patches for generated JavaScript

1010* New commands :eval (:e) and :type (:t) in the prover, which either normalise

1111 or show the type of expressions

12+* Allow type providers to return postulates in addition to terms

1213

1314New in 0.9.11:

1415--------------

src/Idris/AbsSyntaxTree.hs+7−1

@@ -443,6 +443,12 @@ data DataOpt = Codata -- Set if the the data-type is coinductive

443443

444444type DataOpts = [DataOpt]

445445

446+-- | Type provider - what to provide

447+data ProvideWhat = ProvTerm -- ^ only allow providing terms

448+ | ProvPostulate -- ^ only allow postulates

449+ | ProvAny -- ^ either is ok

450+ deriving (Show, Eq)

451+

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

447453-- datatypes and typeclasses.

448454data PDecl' t

@@ -474,7 +480,7 @@ data PDecl' t

474480 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

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

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

480486 deriving Functor

src/Idris/DeepSeq.hs+7−2

@@ -116,12 +116,17 @@ instance (NFData t) => NFData (PDecl' t) where

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

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

118118 rnf (PDirective x1) = ()

119− rnf (PProvider x1 x2 x3 x4 x5)

119+ rnf (PProvider x1 x2 x3 x4 x5 x6)

120120 = rnf x1 `seq`

121− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

121+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

122122 rnf (PTransform x1 x2 x3 x4)

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

124124

125+instance NFData ProvideWhat where

126+ rnf ProvAny = ()

127+ rnf ProvTerm = ()

128+ rnf ProvPostulate = ()

129+

125130instance NFData PunInfo where

126131 rnf x = x `seq` ()

127132

src/Idris/ElabDecls.hs+19−13

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

626626

627627

628628-- | Elaborate a type provider

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

630−elabProvider info syn fc n ty tm

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

630+elabProvider info syn fc what n ty tm

631631 = do i <- getIState

632632 -- Ensure that the experimental extension is enabled

633633 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -659,15 +659,21 @@ elabProvider info syn fc n ty tm

659659 provided <- getProvided fc rhs'

660660

661661 case provided of

662− Provide tm ->

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

664− elabType info syn "" fc [] n ty

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

666− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

667− Postulate ->

668− do -- Add the postulate

669− elabPostulate info syn "Provided postulate" fc [] n ty

670− logLvl 1 $ "Elaborated provided postulate " ++ show n

662+ Provide tm

663+ | what `elem` [ProvTerm, ProvAny] ->

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

665+ elabType info syn "" fc [] n ty

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

667+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

668+ | otherwise ->

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

670+ Postulate

671+ | what `elem` [ProvPostulate, ProvAny] ->

672+ do -- Add the postulate

673+ elabPostulate info syn "Provided postulate" fc [] n ty

674+ logLvl 1 $ "Elaborated provided postulate " ++ show n

675+ | otherwise ->

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

671677

672678 where isTType :: TT Name -> Bool

673679 isTType (TType _) = True

@@ -2228,10 +2234,10 @@ elabDecl' _ info (PDSL n dsl)

22282234 addIBC (IBCDSL n)

22292235elabDecl' what info (PDirective i)

22302236 | what /= EDefns = i

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

2237+elabDecl' what info (PProvider syn fc provWhat n tp tm)

22322238 | what /= EDefns

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

2234− elabProvider info syn fc n tp tm

2240+ elabProvider info syn fc provWhat n tp tm

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

22362242 = elabTransform info fc safety old new

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

src/Idris/Parser.hs+10−3

@@ -1039,18 +1039,25 @@ totality

10391039{- | Parses a type provider

10401040

10411041@

1042−Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

1042+Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1043+ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

10431044@

10441045 -}

10451046provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1048+ what <- provideWhat

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

10481050 fc <- getFC

10491051 reserved "with"

10501052 e <- expr syn

1051− return [PProvider syn fc n t e]

1053+ return [PProvider syn fc what n t e]

10521054 <?> "type provider"

1053−

1055+ where provideWhat :: IdrisParser ProvideWhat

1056+ provideWhat = option ProvAny

1057+ ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>

1058+ pure ProvTerm)

1059+ <|> (reserved "postulate" *> pure ProvPostulate)

1060+ <?> "provider variety")

10541061{- | Parses a transform

10551062

10561063@

test/ffi005/Postulate.idr+3−4

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

1−module Postulate

1+module Main

33import Providers

@@ -9,7 +9,6 @@ bad = pure Postulate

1010%provide (oops : _|_) with bad

1111

12−namespace Main

13− main : IO ()

14− main = putStrLn "oops"

12+main : IO ()

13+main = putStrLn "oops"

1514

test/ffi005/Postulate2.idrnew file+13

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

1+module Main

3+import Providers

5+%language TypeProviders

7+bad : IO (Provider _|_)

8+bad = pure Postulate

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

11+

12+main : IO ()

13+main = putStrLn "oops"

test/ffi005/Postulate3.idrnew file+13

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

1+module Main

3+import Providers

5+%language TypeProviders

7+bad : IO (Provider _|_)

8+bad = pure Postulate

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

11+

12+main : IO ()

13+main = putStrLn "oops"

test/ffi005/expected+2

@@ -1 +1,3 @@

11oops

2+oops

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

test/ffi005/run+8

@@ -1,4 +1,12 @@

11#!/usr/bin/env bash

23idris $@ Postulate.idr -o postulate

34./postulate

45rm -f postulate *.ibc

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