5365977 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -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/ElabDecls.hs+13−9

@@ -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,19 @@ 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 ->

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

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) []]

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

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

667

671

668 where isTType :: TT Name -> Bool

672 where isTType :: TT Name -> Bool

669 isTType (TType _) = True

673 isTType (TType _) = True

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

@@ -0,0 +1,15 @@

1+module Postulate

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+namespace Main

13+ main : IO ()

14+ main = putStrLn "oops"

15+

test/ffi005/expectednew file+1

@@ -0,0 +1 @@

1+oops

test/ffi005/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ Postulate.idr -o postulate

3+./postulate

4+rm -f postulate *.ibc