8319e27 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Postulate providers

commit8319e27dddd153009399e4bb35234595a407678c authorEdwin Brady <edwin.brady@gmail.com> dateFri 28 Feb 2014, 11:13 (13 years ago) parentda8d396 0875310

13 files changed+127−25

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+3 libs/base/Providers.idr+8−2 src/Idris/AbsSyntaxTree.hs+7−1 src/Idris/DeepSeq.hs+7−2 src/Idris/ElabDecls.hs+23−13 src/Idris/Parser.hs+10−3 src/Idris/Providers.hs+13−4 test/ffi005/Postulate.idr+14 test/ffi005/Postulate2.idr+13 test/ffi005/Postulate3.idr+13 test/ffi005/expected+3 test/ffi005/run+12

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

idris.cabal+3

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

299299 test/ffi004/theType

300300 test/ffi004/theOtherType

301301 test/ffi004/expected

302+ test/ffi005/*.idr

303+ test/ffi005/run

304+ test/ffi005/expected

302305

303306 test/interactive001/run

304307 test/interactive001/input

libs/base/Providers.idr+8−2

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

11module Providers

33public

4−data Provider a = Provide a | Error String

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

66-- instances

77instance Functor Provider where

88 map f (Provide a) = Provide (f a)

99 map f (Error err) = Error err

10+ map f Postulate = Postulate

1011

1112instance Applicative Provider where

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

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

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

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

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

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

18+ Postulate <$> _ = Postulate

1519 pure = Provide

1620

21+-- is this correct for Postulate?

1722instance Monad Provider where

1823 (Provide x) >>= f = f x

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

444444

445445type DataOpts = [DataOpt]

446446

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+

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

448454-- datatypes and typeclasses.

449455data PDecl' t

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

475481 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

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

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

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

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

649649

650− -- Create the top-level type declaration

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

652−

653650 -- Execute the type provider and normalise the result

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

655652

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

658655 let rhs' = normalise ctxt [] rhs

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

660657

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

662− tm <- getProvided fc rhs'

663−

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

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

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

659+ provided <- getProvided fc rhs'

660+

661+ case provided of

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

667677

668678 where isTType :: TT Name -> Bool

669679 isTType (TType _) = True

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

22242234 addIBC (IBCDSL n)

22252235elabDecl' what info (PDirective i)

22262236 | what /= EDefns = i

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

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

22282238 | what /= EDefns

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

2230− elabProvider info syn fc n tp tm

2240+ elabProvider info syn fc provWhat n tp tm

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

22322242 = elabTransform info fc safety old new

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

src/Idris/Providers.hs+13−4

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

1−{-# LANGUAGE PatternGuards #-}

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

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

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

44import Idris.Core.TT

55import Idris.Core.Evaluate

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

1616ioret = sUN "prim_io_return"

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

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

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

20+

21+data Provided a = Provide a

22+ | Postulate

23+ deriving (Show, Eq, Functor)

1924

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

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

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

2429 , pioret == ioret && nm == ermod

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

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

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

3035 , 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

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

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

3443

test/ffi005/Postulate.idrnew file+14

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

1+module Main

3+import Providers

5+%language TypeProviders

7+bad : IO (Provider _|_)

8+bad = pure Postulate

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

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

3+idris $@ Postulate.idr -o postulate

4+./postulate

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