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

git.iko.soy/Idris-dev

Add type provider errors + test case

Type provider errors now signal a top-level error. test023 contains a trivially succeeding type provder and a trivially failing type provider.

commit9af2d93d3eb7e3ae9f907e9c9c6a2490fd504a0e authorDavid Christiansen <david@davidchristiansen.dk> dateSun 31 Mar 2013, 20:25 (14 years ago) parentf1e61da

8 files changed+58−4

compare with master

unifiedsplit

src/Core/Execute.hs+1−1 src/Core/TT.hs+4 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+3−1 src/Idris/Providers.hs+22−2 test/test023/expected+1 test/test023/run+3 test/test023/test023.idr+23

src/Core/Execute.hs+1−1

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

2929step tm = step' (unApply tm)

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

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

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

3434 do line <- lift $ getLine

3535 return . Just . Constant . Str $ line

src/Core/TT.hs+4

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

7373 | ProofSearchFail Err

7474 | NoRewriting Term

7575 | At FC Err

76+ | ProviderError String

7677 deriving Eq

7778

7879instance Sized Err where

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

9192 size UniverseError = 1

9293 size ProgramLineComment = 1

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

95+ size (ProviderError msg) = length msg

9496 size _ = 1

9597

9698score :: Err -> Int

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

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

107109 ++ show e ++ " in " ++ show sc ++ " " ++ show i

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

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

109112 show _ = "Error"

110113

111114instance Pretty Err where

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

118121 else

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

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

124+ pretty (ProviderError msg) = text msg

121125 pretty _ = text "Error"

122126

123127data TC a = OK a

src/Idris/Delaborate.hs+1

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

118118pshow i (ProofSearchFail e) = pshow i e

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

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

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

121122

122123showSc i [] = ""

123124showSc 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

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

198198 else do let expected = providerTy fc ty

199199 let using = unProv fc tm

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

200+ logLvl 1 $ "Providing " ++

201201 show n ++ " : " ++ show expected ++

202202 " as " ++ show using

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

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

207207 let et' = normaliseAll ctxt [] et

208208 elabType info syn "" fc [] n ty

209209 rhs <- execute e''

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

211+ providerError rhs

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

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

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

src/Idris/Providers.hs+22−2

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

33import Core.TT

44import Core.Evaluate

5+import Core.Execute

56import Idris.AbsSyntax

67import Idris.AbsSyntaxTree

8+import Idris.Error

10+import Debug.Trace

711

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

913providerTy :: FC -> PTerm -> PTerm

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

1115

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

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

1317unProv :: 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

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

5+import Providers

7+%language TypeProviders

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+