8319e27 · 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--------------

idris.cabal+3

@@ -299,6 +299,9 @@ Extra-source-files:

299 test/ffi004/theType

300 test/ffi004/theOtherType

301 test/ffi004/expected

302+ test/ffi005/*.idr

303+ test/ffi005/run

304+ test/ffi005/expected

302

305

303 test/interactive001/run

306 test/interactive001/run

304 test/interactive001/input

307 test/interactive001/input

libs/base/Providers.idr+8−2

@@ -1,19 +1,25 @@

1module Providers

2

3public

4−data Provider a = Provide a | Error String

4+data Provider a = Provide a | Error String | Postulate

5

6-- instances

7instance Functor Provider where

8 map f (Provide a) = Provide (f a)

9 map f (Error err) = Error err

10+ map f Postulate = Postulate

10

11

11instance Applicative Provider where

12instance Applicative Provider where

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

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

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

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

15+ (Provide f) <$> Postulate = Postulate

14− (Error err) <$> _ = Error err

16+ (Error err) <$> _ = Error err

17+ Postulate <$> (Error err) = Error err

18+ Postulate <$> _ = Postulate

15 pure = Provide

19 pure = Provide

16

20

21+-- is this correct for Postulate?

17instance Monad Provider where

22instance Monad Provider where

18 (Provide x) >>= f = f x

23 (Provide x) >>= f = f x

19 (Error err) >>= _ = Error err

24 (Error err) >>= _ = Error err

25+ Postulate >>= f = Postulate

src/Idris/AbsSyntaxTree.hs+7−1

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

444

445type DataOpts = [DataOpt]

446

447+-- | Type provider - what to provide

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

449+ | ProvPostulate -- ^ only allow postulates

450+ | ProvAny -- ^ either is ok

451+ deriving (Show, Eq)

452+

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

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

448-- datatypes and typeclasses.

454-- datatypes and typeclasses.

449data PDecl' t

455data PDecl' t

@@ -475,7 +481,7 @@ data PDecl' t

475 | PSyntax FC Syntax -- ^ Syntax definition

481 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

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

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

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

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

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

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

481 deriving Functor

487 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+23−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) $

@@ -647,9 +647,6 @@ elabProvider info syn fc n ty tm

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

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

649

650− -- Create the top-level type declaration

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

652−

653 -- Execute the type provider and normalise the result

650 -- Execute the type provider and normalise the result

654 -- use 'run__provider' to convert to a primitive IO action

651 -- use 'run__provider' to convert to a primitive IO action

655

652

@@ -658,12 +655,25 @@ elabProvider info syn fc n ty tm

658 let rhs' = normalise ctxt [] rhs

655 let rhs' = normalise ctxt [] rhs

659 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

656 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

660

657

661− -- Extract the provided term from the type provider

658+ -- Extract the provided term or postulate from the type provider

662− tm <- getProvided fc rhs'

659+ provided <- getProvided fc rhs'

663−

660+

661+ case provided of

662+ Provide tm

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

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

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

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."

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."

667

677

668 where isTType :: TT Name -> Bool

678 where isTType :: TT Name -> Bool

669 isTType (TType _) = True

679 isTType (TType _) = True

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

2224 addIBC (IBCDSL n)

2234 addIBC (IBCDSL n)

2225elabDecl' what info (PDirective i)

2235elabDecl' what info (PDirective i)

2226 | what /= EDefns = i

2236 | what /= EDefns = i

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

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

2228 | what /= EDefns

2238 | what /= EDefns

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

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

2230− elabProvider info syn fc n tp tm

2240+ elabProvider info syn fc provWhat n tp tm

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

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

2232 = elabTransform info fc safety old new

2242 = elabTransform info fc safety old new

2233elabDecl' _ _ _ = 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@

src/Idris/Providers.hs+13−4

@@ -1,5 +1,5 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE PatternGuards, DeriveFunctor #-}

2−module Idris.Providers (providerTy, getProvided) where

2+module Idris.Providers (providerTy, getProvided, Provided(..)) where

3

4import Idris.Core.TT

5import Idris.Core.Evaluate

@@ -16,9 +16,14 @@ providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm ""]

16ioret = sUN "prim_io_return"

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

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

19+posmod = sNS (sUN "Postulate") ["Providers"]

20+

21+data Provided a = Provide a

22+ | Postulate

23+ deriving (Show, Eq, Functor)

19

24

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

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

21−getProvided :: FC -> TT Name -> Idris (TT Name)

26+getProvided :: FC -> TT Name -> Idris (Provided (TT Name))

22getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

27getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

23 , (P _ nm _, [_, err]) <- unApply result

28 , (P _ nm _, [_, err]) <- unApply result

24 , pioret == ioret && nm == ermod

29 , pioret == ioret && nm == ermod

@@ -28,7 +33,11 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

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

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

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

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

30 , pioret == ioret && nm == prmod

35 , pioret == ioret && nm == prmod

31− = return res

36+ = return . Provide $ res

37+ | (P _ pioret _, [tp, result]) <- unApply tm

38+ , (P _ nm _, [_]) <- unApply result

39+ , pioret == ioret && nm == posmod

40+ = return Postulate

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

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

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

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

34

43

test/ffi005/Postulate.idrnew file+14

@@ -0,0 +1,14 @@

1+module Main

2+

3+import Providers

4+

5+%language TypeProviders

6+

7+bad : IO (Provider _|_)

8+bad = pure Postulate

9+

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

11+

12+main : IO ()

13+main = putStrLn "oops"

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/expectednew file+3

@@ -0,0 +1,3 @@

1+oops

2+oops

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

test/ffi005/runnew file+12

@@ -0,0 +1,12 @@

1+#!/usr/bin/env bash

2+

3+idris $@ Postulate.idr -o postulate

4+./postulate

5+rm -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