9c59a19 · Idris-dev · git.iko.soy

CHANGELOG+1−1

@@ -2,7 +2,7 @@ New in 0.9.14:

22--------------

33* Support for running tests for a package with the tests section of .ipkg files and the

44 --testpkg command-line option

5−

5+* Clearly distinguish between type providers and postulate providers at the use site

66

77New in 0.9.13:

88--------------

libs/base/Providers.idr−9

@@ -11,26 +11,17 @@ data Provider : (a : Type) -> Type where

1111 ||| @ msg the error message

1212 Error : (msg : String) -> Provider a

1313

14− ||| Postulate the goal type

15− Postulate : Provider a

16−

1714-- instances

1815instance Functor Provider where

1916 map f (Provide a) = Provide (f a)

2017 map f (Error err) = Error err

21− map f Postulate = Postulate

2218

2319instance Applicative Provider where

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

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

26− (Provide f) <$> Postulate = Postulate

2722 (Error err) <$> _ = Error err

28− Postulate <$> (Error err) = Error err

29− Postulate <$> _ = Postulate

3023 pure = Provide

3124

32−-- is this correct for Postulate?

3325instance Monad Provider where

3426 (Provide x) >>= f = f x

3527 (Error err) >>= _ = Error err

36− Postulate >>= f = Postulate

libs/prelude/Prelude/Algebra.idr+1−1

@@ -106,7 +106,7 @@ class AbelianGroup a => Ring a where

106106class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

107107 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

108108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

109− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

109+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)

110110

111111||| Sets equipped with two binary operations, one associative and commutative

112112||| supplied with a neutral element, and the other associative supplied with a

src/Idris/AbsSyntax.hs+1−1

@@ -278,7 +278,7 @@ addNameHint ty n

278278 ty' <- case lookupCtxtName ty (idris_implicits i) of

279279 [(tyn, _)] -> return tyn

280280 [] -> throwError (NoSuchVariable ty)

281− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))

281+ tyns -> throwError (CantResolveAlts (map fst tyns))

282282 let ns' = case lookupCtxt ty' (idris_namehints i) of

283283 [ns] -> ns ++ [n]

284284 _ -> [n]

src/Idris/AbsSyntaxTree.hs+6−5

@@ -493,10 +493,11 @@ data DataOpt = Codata -- Set if the the data-type is coinductive

493493type DataOpts = [DataOpt]

494494

495495-- | Type provider - what to provide

496−data ProvideWhat = ProvTerm -- ^ only allow providing terms

497− | ProvPostulate -- ^ only allow postulates

498− | ProvAny -- ^ either is ok

499− deriving (Show, Eq)

496+data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

497+ | ProvPostulate t -- ^ goal type must be Type, so only term

498+ deriving (Show, Eq, Functor)

499+

500+type ProvideWhat = ProvideWhat' PTerm

500501

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

502503-- datatypes and typeclasses.

@@ -530,7 +531,7 @@ data PDecl' t

530531 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

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

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

536537 deriving Functor

src/Idris/Core/Elaborate.hs+2−2

@@ -709,7 +709,7 @@ tryWhen False a b = a

709709

710710

711711-- Try a selection of tactics. Exactly one must work, all others must fail

712−tryAll :: [(Elab' aux a, String)] -> Elab' aux a

712+tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

713713tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

714714 where

715715 cantResolve :: Elab' aux a

@@ -718,7 +718,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

718718 tryAll' :: [Elab' aux a] -> -- successes

719719 Int -> -- most problems

720720 (Elab' aux a, Int) -> -- smallest failure

721− [(Elab' aux a, String)] -> -- still to try

721+ [(Elab' aux a, Name)] -> -- still to try

722722 Elab' aux a

723723 tryAll' [res] pmax _ [] = res

724724 tryAll' (_:_) pmax _ [] = cantResolve

src/Idris/Core/Evaluate.hs+10−5

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

1212 mapDefCtxt,

1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

1414 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

@@ -868,14 +868,19 @@ lookupNames n ctxt

868868 = let ns = lookupCtxtName n (definitions ctxt) in

869869 map fst ns

870870

871−lookupTy :: Name -> Context -> [Type]

872−lookupTy n ctxt

873− = do def <- lookupCtxt n (definitions ctxt)

874− case tfst def of

871+lookupTyName :: Name -> Context -> [(Name, Type)]

872+lookupTyName n ctxt = do

873+ (name, def) <- lookupCtxtName n (definitions ctxt)

874+ ty <- case tfst def of

875875 (Function ty _) -> return ty

876876 (TyDecl _ ty) -> return ty

877877 (Operator ty _ _) -> return ty

878878 (CaseOp _ ty _ _ _ _) -> return ty

879+ return (name, ty)

880+

881+

882+lookupTy :: Name -> Context -> [Type]

883+lookupTy n ctxt = map snd (lookupTyName n ctxt)

879884

880885isConName :: Name -> Context -> Bool

881886isConName n ctxt = isTConName n ctxt || isDConName n ctxt

src/Idris/Core/TT.hs+1−1

@@ -133,7 +133,7 @@ data Err' t

133133 | NoTypeDecl Name

134134 | NotInjective t t t

135135 | CantResolve t

136− | CantResolveAlts [String]

136+ | CantResolveAlts [Name]

137137 | IncompleteTerm t

138138 | UniverseError

139139 | ProgramLineComment

src/Idris/DeepSeq.hs+5−7

@@ -156,16 +156,14 @@ instance (NFData t) => NFData (PDecl' t) where

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

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

158158 rnf (PDirective x1) = ()

159− rnf (PProvider x1 x2 x3 x4 x5 x6)

160− = rnf x1 `seq`

161− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

159+ rnf (PProvider x1 x2 x3 x4)

160+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

162161 rnf (PTransform x1 x2 x3 x4)

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

164163

165−instance NFData ProvideWhat where

166− rnf ProvAny = ()

167− rnf ProvTerm = ()

168− rnf ProvPostulate = ()

164+instance NFData t => NFData (ProvideWhat' t) where

165+ rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

166+ rnf (ProvPostulate tm) = rnf tm `seq` ()

169167

170168instance NFData PunInfo where

171169 rnf x = x `seq` ()

src/Idris/Delaborate.hs+26−2

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

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where

2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintErr) where

33

44-- Convert core TT back into high level syntax, primarily for display

55-- purposes.

@@ -9,6 +9,7 @@ import Util.Pretty

99import Idris.AbsSyntax

1010import Idris.Core.TT

1111import Idris.Core.Evaluate

12+import Idris.Docstrings (overview, renderDocstring)

1213import Idris.ErrReverse

1314

1415import Data.List (intersperse)

@@ -195,7 +196,7 @@ pprintErr' i (NotInjective p x y) =

195196 pprintTerm i (delab i y)

196197pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

197198pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

198− align (cat (punctuate (comma <> space) (map text as)))

199+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

199200pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

200201pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

201202pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

@@ -258,6 +259,29 @@ annName n = annName' n (showbasic n)

258259annName' :: Name -> String -> Doc OutputAnnotation

259260annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

260261

262+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

263+fancifyAnnots ist annot@(AnnName n _ _ _) =

264+ do let ctxt = tt_ctxt ist

265+ docs = docOverview ist n

266+ ty = Just (getTy ist n)

267+ case () of

268+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

269+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

270+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

271+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

272+ _ | otherwise -> annot

273+ where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

274+ docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

275+ let o = overview (fst docs)

276+ -- TODO make width configurable

277+ out = displayS . renderPretty 1.0 50 $ renderDocstring o

278+ return (out "")

279+ getTy :: IState -> Name -> String -- fails if name not already extant!

280+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

281+ delabTy ist n

282+ in (displayS . renderPretty 1.0 50 $ theTy) ""

283+fancifyAnnots _ annot = annot

284+

261285showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

262286showSc i [] = empty

263287showSc i xs = line <> line <> text "In context:" <>

src/Idris/ElabDecls.hs+15−13

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

681681

682682

683683-- | Elaborate a type provider

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

685−elabProvider info syn fc what n ty tm

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

685+elabProvider info syn fc what n

686686 = do i <- getIState

687687 -- Ensure that the experimental extension is enabled

688688 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -692,12 +692,17 @@ elabProvider info syn fc what n ty tm

692692 ctxt <- getContext

693693

694694 -- First elaborate the expected type (and check that it's a type)

695− (ty', typ) <- elabVal toplevel False ty

695+ -- The goal type for a postulate is always Type.

696+ (ty', typ) <- case what of

697+ ProvTerm ty p -> elabVal toplevel False ty

698+ ProvPostulate _ -> elabVal toplevel False PType

696699 unless (isTType typ) $

697700 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

698701

699702 -- Elaborate the provider term to TT and check that the type matches

700− (e, et) <- elabVal toplevel False tm

703+ (e, et) <- case what of

704+ ProvTerm _ tm -> elabVal toplevel False tm

705+ ProvPostulate tm -> elabVal toplevel False tm

701706 unless (isProviderOf (normalise ctxt [] ty') et) $

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

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

@@ -715,17 +720,14 @@ elabProvider info syn fc what n ty tm

715720

716721 case provided of

717722 Provide tm

718− | what `elem` [ProvTerm, ProvAny] ->

723+ | ProvTerm ty _ <- what ->

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

720725 elabType info syn emptyDocstring [] fc [] n ty

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

722727 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

723− | otherwise ->

724− ierror . Msg $ "Attempted to provide a term where a postulate was expected."

725− Postulate

726− | what `elem` [ProvPostulate, ProvAny] ->

728+ | ProvPostulate _ <- what ->

727729 do -- Add the postulate

728− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty

730+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

729731 logLvl 3 $ "Elaborated provided postulate " ++ show n

730732 | otherwise ->

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

@@ -2042,7 +2044,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20422044 [c] -> return c

20432045 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

20442046 cs -> tclift $ tfail $ At fc

2045− (CantResolveAlts (map (show . fst) cs))

2047+ (CantResolveAlts (map fst cs))

20462048 let constraint = PApp fc (PRef fc n) (map pexp ps)

20472049 let iname = mkiname n ps expn

20482050 let emptyclass = null (class_methods ci)

@@ -2408,10 +2410,10 @@ elabDecl' _ info (PDSL n dsl)

24082410 addIBC (IBCDSL n)

24092411elabDecl' what info (PDirective i)

24102412 | what /= EDefns = i

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

2413+elabDecl' what info (PProvider syn fc provWhat n)

24122414 | what /= EDefns

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

2414− elabProvider info syn fc provWhat n tp tm

2416+ elabProvider info syn fc provWhat n

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

24162418 = elabTransform info fc safety old new

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

src/Idris/ElabTerm.hs+8−8

@@ -271,10 +271,10 @@ elab ist info pattern opts fn tm

271271 let as' = pruneByType (map fst env) tc ctxt as

272272-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

273273 tryAll (zip (map (elab' ina) as') (map showHd as'))

274− where showHd (PApp _ (PRef _ n) _) = show n

275− showHd (PRef _ n) = show n

276− showHd (PApp _ h _) = show h

277− showHd x = show x

274+ where showHd (PApp _ (PRef _ n) _) = n

275+ showHd (PRef _ n) = n

276+ showHd (PApp _ h _) = showHd h

277+ showHd x = NErased -- We probably should do something better than this here

278278 elab' ina (PAlternative False as)

279279 = trySeq as

280280 where -- if none work, take the error from the first

@@ -991,7 +991,7 @@ runTac autoSolve ist fn tac

991991 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)

992992 let tacs = map (\ (fn', imps) ->

993993 (match_apply (Var fn') (map (\x -> (x, 0)) imps),

994− show fn')) fnimps

994+ fn')) fnimps

995995 tryAll tacs

996996 when autoSolve solveAll

997997 where envArgs n = do e <- get_env

@@ -1007,7 +1007,7 @@ runTac autoSolve ist fn tac

10071007 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)

10081008 let tacs = map (\ (fn', imps) ->

10091009 (apply (Var fn') (map (\x -> (x, 0)) imps),

1010− show fn')) fnimps

1010+ fn')) fnimps

10111011 tryAll tacs

10121012 when autoSolve solveAll

10131013 where isImp (PImp _ _ _ _ _) = True

@@ -1609,8 +1609,8 @@ reflectErr (NotInjective t1 t2 t3) =

16091609 ]

16101610reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

16111611reflectErr (CantResolveAlts ss) =

1612− raw_apply (Var $ reflErrName "CantResolve")

1613− [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

1612+ raw_apply (Var $ reflErrName "CantResolveAlts")

1613+ [rawList (Var $ (sUN "String")) (map Var ss)]

16141614reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

16151615reflectErr UniverseError = Var $ reflErrName "UniverseError"

16161616reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

src/Idris/Erasure.hs+1−1

@@ -109,7 +109,7 @@ performUsageAnalysis = do

109109 getMainName ist = case lookupCtxtName n (idris_implicits ist) of

110110 [(n', _)] -> Right n'

111111 [] -> Left (NoSuchVariable n)

112− more -> Left (CantResolveAlts (map (show . fst) more))

112+ more -> Left (CantResolveAlts (map fst more))

113113 where

114114 n = sNS (sUN "main") ["Main"]

115115

src/Idris/Interactive.hs+4−4

@@ -162,7 +162,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

162162 mn <- case lookupNames n ctxt of

163163 [x] -> return x

164164 [] -> return n

165− ns -> ierror (CantResolveAlts (map show ns))

165+ ns -> ierror (CantResolveAlts ns)

166166 i <- getIState

167167 let (top, envlen, _) = case lookup mn (idris_metavars i) of

168168 Just (t, e, False) -> (t, e, False)

@@ -242,10 +242,10 @@ makeLemma h fn updatefile l n

242242 let isProv = checkProv tyline (show n)

243243

244244 ctxt <- getContext

245− mty <- case lookupTy n ctxt of

246− [t] -> return t

245+ mty <- case lookupTyName n ctxt of

246+ [(_,t)] -> return t

247247 [] -> ierror (NoSuchVariable n)

248− ns -> ierror (CantResolveAlts (map show ns))

248+ ns -> ierror (CantResolveAlts (map fst ns))

249249 i <- getIState

250250

251251 if (not isProv) then do

src/Idris/Output.hs−32

@@ -83,38 +83,6 @@ ihRenderResult h d = do ist <- getIState

8383 RawOutput -> consoleDisplayAnnotated h d

8484 IdeSlave n -> ideSlaveReturnAnnotated n h d

8585

86−makeAnnName :: IState -> Name -> Maybe OutputAnnotation

87−makeAnnName ist n

88− | isDConName n ctxt = annName DataOutput

89− | isFnName n ctxt = annName FunOutput

90− | isTConName n ctxt = annName TypeOutput

91− | isMetavarName n ist = annName MetavarOutput

92− | otherwise = Nothing

93− where ctxt = tt_ctxt ist

94− docs = docOverview ist n

95− ty = Just (getTy ist n)

96−

97− annName :: NameOutput -> Maybe OutputAnnotation

98− annName nameType = Just (AnnName n (Just nameType) docs ty)

99− docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

100− docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

101− let o = overview (fst docs)

102− -- TODO make width configurable

103− out = displayS . renderPretty 1.0 50 $ renderDocstring o

104− return (out "")

105− getTy :: IState -> Name -> String -- fails if name not already extant!

106− getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

107− delabTy ist n

108− in (displayS . renderPretty 1.0 50 $ theTy) ""

109−

110−

111−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

112−fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of

113− Just fancyAnnot -> fancyAnnot

114− Nothing -> annot

115−fancifyAnnots _ annot = annot

116−

117−

11886ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

11987ideSlaveReturnWithStatus status n h out = do

12088 ist <- getIState

src/Idris/Parser.hs+14−13

@@ -1034,7 +1034,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

10341034 case lookupCtxtName n (idris_implicits i) of

10351035 [(n', _)] -> return n'

10361036 [] -> throwError (NoSuchVariable n)

1037− more -> throwError (CantResolveAlts (map (show . fst) more))

1037+ more -> throwError (CantResolveAlts (map fst more))

10381038

10391039pLangExt :: IdrisParser LanguageExt

10401040pLangExt = (reserved "TypeProviders" >> return TypeProviders)

@@ -1061,19 +1061,20 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

10611061 -}

10621062provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1064− what <- provideWhat

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

1066− fc <- getFC

1067− reserved "with"

1068− e <- expr syn

1069− return [PProvider syn fc what n t e]

1064+ provideTerm <|> providePostulate

10701065 <?> "type provider"

1071− where provideWhat :: IdrisParser ProvideWhat

1072− provideWhat = option ProvAny

1073− ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>

1074− pure ProvTerm)

1075− <|> (reserved "postulate" *> pure ProvPostulate)

1076− <?> "provider variety")

1066+ where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1067+ fc <- getFC

1068+ reserved "with"

1069+ e <- expr syn <?> "provider expression"

1070+ return [PProvider syn fc (ProvTerm t e) n]

1071+ providePostulate = do reserved "postulate"

1072+ n <- fnName

1073+ fc <- getFC

1074+ reserved "with"

1075+ e <- expr syn <?> "provider expression"

1076+ return [PProvider syn fc (ProvPostulate e) n]

1077+

10771078{- | Parses a transform

10781079

10791080@

src/Idris/Providers.hs+1−7

@@ -11,16 +11,14 @@ import Debug.Trace

1111

1212-- | Wrap a type provider in the type of type providers

1313providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm

14+providerTy fc tm

1515 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

1616

1717ioret = sUN "prim_io_return"

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

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

20−posmod = sNS (sUN "Postulate") ["Providers"]

2120

2221data Provided a = Provide a

23− | Postulate

2422 deriving (Show, Eq, Functor)

2523

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

@@ -35,10 +33,6 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

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

3634 , pioret == ioret && nm == prmod

3735 = return . Provide $ res

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

39− , (P _ nm _, [_]) <- unApply result

40− , pioret == ioret && nm == posmod

41− = return Postulate

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

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

4438

src/Idris/REPL.hs+2−2

@@ -512,7 +512,7 @@ resolveProof n'

512512 n <- case lookupNames n' ctxt of

513513 [x] -> return x

514514 [] -> return n'

515− ns -> ierror (CantResolveAlts (map show ns))

515+ ns -> ierror (CantResolveAlts ns)

516516 return n

517517

518518removeProof :: Name -> Idris ()

@@ -795,7 +795,7 @@ process h fn (Prove n')

795795 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

796796 [(n, (_,_,False))] -> return n

797797 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

798− ns -> ierror (CantResolveAlts (map show ns))

798+ ns -> ierror (CantResolveAlts (map fst ns))

799799 prover (lit fn) n

800800 -- recheck totality

801801 i <- getIState

test/ffi005/Postulate.idr+3−3

@@ -4,10 +4,10 @@ import Providers

44

55%language TypeProviders

66

7−bad : IO (Provider _|_)

8−bad = pure Postulate

7+bad : IO (Provider Type)

8+bad = return $ pure _|_

99

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

10+%provide postulate oops with bad

1111

1212main : IO ()

1313main = putStrLn "oops"

test/ffi005/Postulate2.idrdeleted−13

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

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.idrdeleted−13

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

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

11oops

2−oops

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

test/ffi005/run−7

@@ -3,10 +3,3 @@

33idris $@ Postulate.idr -o postulate

44./postulate

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