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

src/Core/Execute.hs+1−1

compare with master

unifiedsplit

@@ -29,7 +29,7 @@ step :: TT Name -> Idris (Maybe (TT Name))

29step tm = step' (unApply tm)

30 where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped

31 step' (P _ (UN "mkForeign") _, args) = stepForeign args

32− step' (P _ (UN "prim__IO") _, [_, arg]) = step arg

32+ step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)

33 step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =

34 do line <- lift $ getLine

35 return . Just . Constant . Str $ line

src/Core/TT.hs+4

@@ -73,6 +73,7 @@ data Err = Msg String

73 | ProofSearchFail Err

74 | NoRewriting Term

75 | At FC Err

76+ | ProviderError String

76 deriving Eq

77 deriving Eq

77

78

78instance Sized Err where

79instance Sized Err where

@@ -91,6 +92,7 @@ instance Sized Err where

91 size UniverseError = 1

92 size UniverseError = 1

92 size ProgramLineComment = 1

93 size ProgramLineComment = 1

93 size (At fc err) = size fc + size err

94 size (At fc err) = size fc + size err

95+ size (ProviderError msg) = length msg

94 size _ = 1

96 size _ = 1

95

97

96score :: Err -> Int

98score :: Err -> Int

@@ -106,6 +108,7 @@ instance Show Err where

106 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

108 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

107 ++ show e ++ " in " ++ show sc ++ " " ++ show i

109 ++ show e ++ " in " ++ show sc ++ " " ++ show i

108 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

110 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

111+ show (ProviderError msg) = "Type provider error: " ++ msg

109 show _ = "Error"

112 show _ = "Error"

110

113

111instance Pretty Err where

114instance Pretty Err where

@@ -118,6 +121,7 @@ instance Pretty Err where

118 else

121 else

119 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

122 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

120 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

123 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

124+ pretty (ProviderError msg) = text msg

121 pretty _ = text "Error"

125 pretty _ = text "Error"

122

126

123data TC a = OK a

127data TC a = OK a

src/Idris/Delaborate.hs+1

@@ -118,6 +118,7 @@ pshow i (AlreadyDefined n) = show n ++ " is already defined"

118pshow i (ProofSearchFail e) = pshow i e

119pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

120pshow i (At f e) = show f ++ ":" ++ pshow i e

121+pshow i (ProviderError msg) = "Type provider error: " ++ msg

121

122

122showSc i [] = ""

123showSc i [] = ""

123showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

124showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/ElabDecls.hs+3−1

@@ -197,7 +197,7 @@ elabProvider info syn fc n ty tm

197 "\".\nYou must turn on TypeProviders extension."

198 else do let expected = providerTy fc ty

199 let using = unProv fc tm

200− logLvl 1 $ "** Providing " ++

200+ logLvl 1 $ "Providing " ++

201 show n ++ " : " ++ show expected ++

202 " as " ++ show using

203 (e', et) <- elabVal toplevel False using

@@ -207,6 +207,8 @@ elabProvider info syn fc n ty tm

207 let et' = normaliseAll ctxt [] et

208 elabType info syn "" fc [] n ty

209 rhs <- execute e''

210+ logLvl 1 $ "Normalized " ++ show n ++ "'s RHS to " ++ show rhs

211+ providerError rhs

210 elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

212 elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

211 logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et

213 logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et

212 logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'

214 logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'

src/Idris/Providers.hs+22−2

@@ -2,13 +2,33 @@ module Idris.Providers where

2

3import Core.TT

4import Core.Evaluate

5+import Core.Execute

5import Idris.AbsSyntax

6import Idris.AbsSyntax

6import Idris.AbsSyntaxTree

7import Idris.AbsSyntaxTree

8+import Idris.Error

9+

10+import Debug.Trace

7

11

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

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

9providerTy :: FC -> PTerm -> PTerm

13providerTy :: FC -> PTerm -> PTerm

10providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]

14providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]

11

15

12−-- | Wrap the RHS of a type provider definition

16+-- | Wrap the RHS of a type provider definition

13unProv :: FC -> PTerm -> PTerm

17unProv :: FC -> PTerm -> PTerm

14−unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False tm ""]

18+unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False tm ""]

19+

20+-- | Handle an error, if the type provider returned an error. Otherwise do nothing.

21+providerError :: TT Name -> Idris ()

22+providerError tm = case unApply tm of

23+ (P _ (NS (UN "unProv") ["Providers"]) _, [_, tm']) ->

24+ case unApply tm' of

25+ (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) ->

26+ do str <- execute err

27+ case (unApply str) of

28+ (Constant (Str msg), []) ->

29+ ierror . ProviderError $ msg

30+ (P _ (UN "prim__IO") _, [_, (Constant (Str msg))]) ->

31+ ierror . ProviderError $ msg

32+ _ -> fail "Error in type provider."

33+ _ -> return ()

34+ _ -> return ()

test/test023/expectednew file+1

@@ -0,0 +1 @@

1+Type provider error: Always fails

test/test023/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris --quiet test023.idr -o test023

3+rm -f test023 *.ibc

test/test023/test023.idrnew file+23

@@ -0,0 +1,23 @@

1+module Main

2+

3+-- Simple test case for trivial type providers.

4+

5+import Providers

6+

7+%language TypeProviders

8+

9+-- Provide the Unit type

10+goodProvider : Provider Type

11+goodProvider = Provide (return (the Type ()))

12+

13+%provide (Unit : Type) with goodProvider

14+

15+foo : Unit

16+foo = ()

17+

18+-- Always fail

19+badProvider : Provider Type

20+badProvider = Error (return "Always fails")

21+

22+%provide (t : Type) with badProvider

23+