0875310 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

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

9* Lots of performance patches for generated JavaScript

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

11 or show the type of expressions

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

12

13

13New in 0.9.11:

14New in 0.9.11:

14--------------

15--------------

src/Idris/AbsSyntaxTree.hs+7−1

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

443

444type DataOpts = [DataOpt]

445

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+

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

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

447-- datatypes and typeclasses.

453-- datatypes and typeclasses.

448data PDecl' t

454data PDecl' t

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

474 | PSyntax FC Syntax -- ^ Syntax definition

480 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

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

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

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

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

480 deriving Functor

486 deriving Functor

src/Idris/DeepSeq.hs+7−2

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

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

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

118 rnf (PDirective x1) = ()

119− rnf (PProvider x1 x2 x3 x4 x5)

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

120 = 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` ()

122 rnf (PTransform x1 x2 x3 x4)

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

124

125+instance NFData ProvideWhat where

126+ rnf ProvAny = ()

127+ rnf ProvTerm = ()

128+ rnf ProvPostulate = ()

129+

125instance NFData PunInfo where

130instance NFData PunInfo where

126 rnf x = x `seq` ()

131 rnf x = x `seq` ()

127

132

src/Idris/ElabDecls.hs+19−13

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

626

627

628-- | Elaborate a type provider

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

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

630−elabProvider info syn fc n ty tm

630+elabProvider info syn fc what n ty tm

631 = do i <- getIState

632 -- Ensure that the experimental extension is enabled

633 unless (TypeProviders `elem` idris_language_extensions i) $

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

659 provided <- getProvided fc rhs'

660

661 case provided of

662− Provide tm ->

662+ Provide tm

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

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

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

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

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

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

666+ 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+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

668+ | otherwise ->

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

667− Postulate ->

670+ Postulate

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

668− do -- Add the postulate

672+ do -- Add the postulate

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

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

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

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

675+ | otherwise ->

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

671

677

672 where isTType :: TT Name -> Bool

678 where isTType :: TT Name -> Bool

673 isTType (TType _) = True

679 isTType (TType _) = True

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

2228 addIBC (IBCDSL n)

2234 addIBC (IBCDSL n)

2229elabDecl' what info (PDirective i)

2235elabDecl' what info (PDirective i)

2230 | what /= EDefns = i

2236 | what /= EDefns = i

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

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

2232 | what /= EDefns

2238 | what /= EDefns

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

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

2234− elabProvider info syn fc n tp tm

2240+ elabProvider info syn fc provWhat n tp tm

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

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

2236 = elabTransform info fc safety old new

2242 = elabTransform info fc safety old new

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

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

src/Idris/Parser.hs+10−3

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

1039{- | Parses a type provider

1040

1041@

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

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

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

1043@

1044@

1044 -}

1045 -}

1045provider :: SyntaxInfo -> IdrisParser [PDecl]

1046provider :: SyntaxInfo -> IdrisParser [PDecl]

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

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

1048+ what <- provideWhat

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

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

1048 fc <- getFC

1050 fc <- getFC

1049 reserved "with"

1051 reserved "with"

1050 e <- expr syn

1052 e <- expr syn

1051− return [PProvider syn fc n t e]

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

1052 <?> "type provider"

1054 <?> "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")

1054{- | Parses a transform

1061{- | Parses a transform

1055

1062

1056@

1063@

test/ffi005/Postulate.idr+3−4

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

1−module Postulate

1+module Main

2

3import Providers

4

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

9

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

11

12−namespace Main

13− main : IO ()

12+main : IO ()

14− main = putStrLn "oops"

13+main = putStrLn "oops"

15

14

test/ffi005/Postulate2.idrnew file+13

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

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.idrnew file+13

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

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 +1,3 @@

1oops

2+oops

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

test/ffi005/run+8

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

1#!/usr/bin/env bash

2+

2idris $@ Postulate.idr -o postulate

3idris $@ Postulate.idr -o postulate

3./postulate

4./postulate

4rm -f postulate *.ibc

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