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

CHANGELOG+1−1

compare with master

unifiedsplit

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

2--------------

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

4 --testpkg command-line option

5−

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

6

7New in 0.9.13:

8--------------

libs/base/Providers.idr−9

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

11 ||| @ msg the error message

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

13

14− ||| Postulate the goal type

15− Postulate : Provider a

16−

17-- instances

14-- instances

18instance Functor Provider where

15instance Functor Provider where

19 map f (Provide a) = Provide (f a)

16 map f (Provide a) = Provide (f a)

20 map f (Error err) = Error err

17 map f (Error err) = Error err

21− map f Postulate = Postulate

22

18

23instance Applicative Provider where

19instance Applicative Provider where

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

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

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

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

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

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

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

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

29− Postulate <$> _ = Postulate

30 pure = Provide

23 pure = Provide

31

24

32−-- is this correct for Postulate?

33instance Monad Provider where

25instance Monad Provider where

34 (Provide x) >>= f = f x

26 (Provide x) >>= f = f x

35 (Error err) >>= _ = Error err

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

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

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

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

110

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

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

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

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

280 [] -> throwError (NoSuchVariable ty)

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

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

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

283 [ns] -> ns ++ [n]

284 _ -> [n]

src/Idris/AbsSyntaxTree.hs+6−5

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

493type DataOpts = [DataOpt]

494

495-- | Type provider - what to provide

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

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

497− | ProvPostulate -- ^ only allow postulates

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

498− | ProvAny -- ^ either is ok

499− deriving (Show, Eq)

498+ deriving (Show, Eq, Functor)

499+

500+type ProvideWhat = ProvideWhat' PTerm

500

501

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

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

502-- datatypes and typeclasses.

503-- datatypes and typeclasses.

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

530 | PSyntax FC Syntax -- ^ Syntax definition

531 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

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

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

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

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

536 deriving Functor

537 deriving Functor

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

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

709

710

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

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

714 where

715 cantResolve :: Elab' aux a

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

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

719 Int -> -- most problems

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

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

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

722 Elab' aux a

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

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

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

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

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

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

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

12 mapDefCtxt,

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

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

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

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

869 map fst ns

870

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

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

872−lookupTy n ctxt

872+lookupTyName n ctxt = do

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

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

874− case tfst def of

874+ ty <- case tfst def of

875 (Function ty _) -> return ty

876 (TyDecl _ ty) -> return ty

877 (Operator ty _ _) -> return ty

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

879+ return (name, ty)

880+

881+

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

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

879

884

880isConName :: Name -> Context -> Bool

885isConName :: Name -> Context -> Bool

881isConName n ctxt = isTConName n ctxt || isDConName n ctxt

886isConName n ctxt = isTConName n ctxt || isDConName n ctxt

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

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

133 | NoTypeDecl Name

134 | NotInjective t t t

135 | CantResolve t

136− | CantResolveAlts [String]

136+ | CantResolveAlts [Name]

137 | IncompleteTerm t

138 | UniverseError

139 | ProgramLineComment

src/Idris/DeepSeq.hs+5−7

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

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

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

158 rnf (PDirective x1) = ()

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

159+ rnf (PProvider x1 x2 x3 x4)

160− = rnf x1 `seq`

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

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

162 rnf (PTransform x1 x2 x3 x4)

161 rnf (PTransform x1 x2 x3 x4)

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

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

164

163

165−instance NFData ProvideWhat where

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

166− rnf ProvAny = ()

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

167− rnf ProvTerm = ()

168− rnf ProvPostulate = ()

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

169

167

170instance NFData PunInfo where

168instance NFData PunInfo where

171 rnf x = x `seq` ()

169 rnf x = x `seq` ()

src/Idris/Delaborate.hs+26−2

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

1{-# 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

3

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

5-- purposes.

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

9import Idris.AbsSyntax

10import Idris.Core.TT

11import Idris.Core.Evaluate

12+import Idris.Docstrings (overview, renderDocstring)

12import Idris.ErrReverse

13import Idris.ErrReverse

13

14

14import Data.List (intersperse)

15import Data.List (intersperse)

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

195 pprintTerm i (delab i y)

196 pprintTerm i (delab i y)

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

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

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

198pprintErr' 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)))

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

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

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

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

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

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

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

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

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

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

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

260

261

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+

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

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

262showSc i [] = empty

286showSc i [] = empty

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

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

src/Idris/ElabDecls.hs+15−13

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

681

682

683-- | Elaborate a type provider

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

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

685−elabProvider info syn fc what n ty tm

685+elabProvider info syn fc what n

686 = do i <- getIState

687 -- Ensure that the experimental extension is enabled

688 unless (TypeProviders `elem` idris_language_extensions i) $

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

692 ctxt <- getContext

693

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

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

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

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

697+ ProvTerm ty p -> elabVal toplevel False ty

698+ ProvPostulate _ -> elabVal toplevel False PType

696 unless (isTType typ) $

699 unless (isTType typ) $

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

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

698

701

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

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

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

704+ ProvTerm _ tm -> elabVal toplevel False tm

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

705+ ProvPostulate tm -> elabVal toplevel False tm

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

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

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

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

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

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

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

715

720

716 case provided of

721 case provided of

717 Provide tm

722 Provide tm

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

723+ | ProvTerm ty _ <- what ->

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

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

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

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

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

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

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

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

727 do -- Add the postulate

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

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

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

730 | otherwise ->

732 | otherwise ->

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

733 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

2042 [c] -> return c

2044 [c] -> return c

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

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

2044 cs -> tclift $ tfail $ At fc

2046 cs -> tclift $ tfail $ At fc

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

2047+ (CantResolveAlts (map fst cs))

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

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

2047 let iname = mkiname n ps expn

2049 let iname = mkiname n ps expn

2048 let emptyclass = null (class_methods ci)

2050 let emptyclass = null (class_methods ci)

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

2408 addIBC (IBCDSL n)

2410 addIBC (IBCDSL n)

2409elabDecl' what info (PDirective i)

2411elabDecl' what info (PDirective i)

2410 | what /= EDefns = i

2412 | what /= EDefns = i

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

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

2412 | what /= EDefns

2414 | what /= EDefns

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

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

2414− elabProvider info syn fc provWhat n tp tm

2416+ elabProvider info syn fc provWhat n

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

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

2416 = elabTransform info fc safety old new

2418 = elabTransform info fc safety old new

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

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

src/Idris/ElabTerm.hs+8−8

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

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

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

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

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

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

275− showHd (PRef _ n) = show n

275+ showHd (PRef _ n) = n

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

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

277− showHd x = show x

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

278 elab' ina (PAlternative False as)

279 = trySeq as

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

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

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

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

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

994− show fn')) fnimps

994+ fn')) fnimps

995 tryAll tacs

996 when autoSolve solveAll

997 where envArgs n = do e <- get_env

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

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

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

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

1010− show fn')) fnimps

1010+ fn')) fnimps

1011 tryAll tacs

1012 when autoSolve solveAll

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

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

1609 ]

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

1611reflectErr (CantResolveAlts ss) =

1612− raw_apply (Var $ reflErrName "CantResolve")

1612+ raw_apply (Var $ reflErrName "CantResolveAlts")

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

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

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

1615reflectErr UniverseError = Var $ reflErrName "UniverseError"

1616reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

src/Idris/Erasure.hs+1−1

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

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

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

111 [] -> Left (NoSuchVariable n)

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

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

113 where

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

115

src/Idris/Interactive.hs+4−4

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

162 mn <- case lookupNames n ctxt of

163 [x] -> return x

164 [] -> return n

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

165+ ns -> ierror (CantResolveAlts ns)

166 i <- getIState

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

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

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

242 let isProv = checkProv tyline (show n)

243

244 ctxt <- getContext

245− mty <- case lookupTy n ctxt of

245+ mty <- case lookupTyName n ctxt of

246− [t] -> return t

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

247 [] -> ierror (NoSuchVariable n)

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

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

249 i <- getIState

250

251 if (not isProv) then do

src/Idris/Output.hs−32

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

83 RawOutput -> consoleDisplayAnnotated h d

84 IdeSlave n -> ideSlaveReturnAnnotated n h d

85

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−

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

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

119ideSlaveReturnWithStatus status n h out = do

87ideSlaveReturnWithStatus status n h out = do

120 ist <- getIState

88 ist <- getIState

src/Idris/Parser.hs+14−13

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

1034 case lookupCtxtName n (idris_implicits i) of

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

1036 [] -> throwError (NoSuchVariable n)

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

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

1038

1039pLangExt :: IdrisParser LanguageExt

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

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

1061 -}

1062provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1064− what <- provideWhat

1064+ provideTerm <|> providePostulate

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]

1070 <?> "type provider"

1065 <?> "type provider"

1071− where provideWhat :: IdrisParser ProvideWhat

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

1072− provideWhat = option ProvAny

1067+ fc <- getFC

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

1068+ reserved "with"

1074− pure ProvTerm)

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

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

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

1071+ providePostulate = do reserved "postulate"

1076− <?> "provider variety")

1072+ n <- fnName

1073+ fc <- getFC

1074+ reserved "with"

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

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

1077+

1077{- | Parses a transform

1078{- | Parses a transform

1078

1079

1079@

1080@

src/Idris/Providers.hs+1−7

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

11

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

13providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm

14+providerTy fc tm

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

16

17ioret = sUN "prim_io_return"

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

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

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

21

20

22data Provided a = Provide a

21data Provided a = Provide a

23− | Postulate

24 deriving (Show, Eq, Functor)

22 deriving (Show, Eq, Functor)

25

23

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

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

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

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

36 , pioret == ioret && nm == prmod

34 , pioret == ioret && nm == prmod

37 = return . Provide $ res

35 = return . Provide $ res

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

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

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

41− = return Postulate

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

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

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

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

44

38

src/Idris/REPL.hs+2−2

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

512 n <- case lookupNames n' ctxt of

513 [x] -> return x

514 [] -> return n'

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

515+ ns -> ierror (CantResolveAlts ns)

516 return n

517

518removeProof :: Name -> Idris ()

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

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

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

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

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

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

799 prover (lit fn) n

800 -- recheck totality

801 i <- getIState

test/ffi005/Postulate.idr+3−3

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

4

5%language TypeProviders

6

7−bad : IO (Provider _|_)

7+bad : IO (Provider Type)

8−bad = pure Postulate

8+bad = return $ pure _|_

9

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

10+%provide postulate oops with bad

11

12main : IO ()

13main = 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 @@

1oops

2−oops

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

test/ffi005/run−7

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

3idris $@ Postulate.idr -o postulate

4./postulate

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