5365977 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Postulate providers

Now, type providers don't need to return a proof - they can postulate new axioms. The intention is to connect this both to QuickCheck and to external proof oracles, such as SMT solvers.

commit53659771ae533f36f28daff0767bdca0a66e30ff authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 26 Feb 2014, 11:37 (13 years ago) parent3bc4846

7 files changed+57−15

compare with master

unifiedsplit

idris.cabal+3 libs/base/Providers.idr+8−2 src/Idris/ElabDecls.hs+13−9 src/Idris/Providers.hs+13−4 test/ffi005/Postulate.idr+15 test/ffi005/expected+1 test/ffi005/run+4

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

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

667671

668672 where isTType :: TT Name -> Bool

669673 isTType (TType _) = True

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

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

1+module Postulate

3+import Providers

5+%language TypeProviders

7+bad : IO (Provider _|_)

8+bad = pure Postulate

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