879769a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Execute type providers while typechecking

879769aDavid Christiansen14 years ago

lib/Providers.idr+1−1

compare with master

unifiedsplit

@@ -3,6 +3,6 @@ module Providers

3public

4data Provider a = Provide (IO a) | Error (IO String)

6−abstract partial

6+partial public

7unProv : Provider a -> a

8unProv (Provide x) = unsafePerformIO x

src/Core/Execute.hs+9−8

@@ -24,17 +24,20 @@ import Foreign.Marshal.Alloc (free)

24-- IO was performed.

25step :: TT Name -> Idris (Maybe (TT Name))

26step tm = step' (unApply tm)

27− where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = return $ Just arg

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

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

29 step' _ = return Nothing

31-- | Perform side effects until no more can be performed, then return the

32-- resulting term (possibly the argument).

33execute :: TT Name -> Idris (TT Name)

34+execute tm = case unApply tm of

35+ (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg

36+ _ -> return tm

34−execute tm = do stepped <- step tm

37+ where execute' tm = do stepped <- step tm

35− case stepped of

38+ case stepped of

36− Nothing -> return tm

39+ Nothing -> return tm

37− Just tm' -> execute tm'

40+ Just tm' -> execute' tm'

@@ -46,8 +49,7 @@ call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))

46call (FFun name argTypes retType) args = do fn <- findForeign name

49call (FFun name argTypes retType) args = do fn <- findForeign name

47 case fn of

50 case fn of

48 Nothing -> return Nothing

51 Nothing -> return Nothing

49− Just f -> do res <- call' f args retType

52+ Just f -> return . Just =<< call' f args retType

50− return . Just $ res

51 where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)

53 where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)

52 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)

54 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)

53 return (Constant (I (fromIntegral res)))

55 return (Constant (I (fromIntegral res)))

@@ -65,7 +67,6 @@ call (FFun name argTypes retType) args = do fn <- findForeign name

65 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)

67 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)

66 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level

68 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level

68−

69 prepArgs = map prepArg

70 prepArgs = map prepArg

70 prepArg (Constant (I i)) = argCInt (fromIntegral i)

71 prepArg (Constant (I i)) = argCInt (fromIntegral i)

71 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)

72 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)

src/Idris/ElabDecls.hs+8−4

@@ -17,6 +17,7 @@ import Paths_idris

17import Core.TT

18import Core.Elaborate hiding (Tactic(..))

19import Core.Evaluate

20+import Core.Execute

20import Core.Typecheck

21import Core.Typecheck

21import Core.CaseTree

22import Core.CaseTree

@@ -191,18 +192,21 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

191elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

192elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

192elabProvider info syn fc n ty tm

193elabProvider info syn fc n ty tm

193 = do let expected = providerTy fc ty

194 = do let expected = providerTy fc ty

195+ let using = unProv fc tm

194 logLvl 1 $ "** Providing " ++

196 logLvl 1 $ "** Providing " ++

195 show n ++ " : " ++ show expected ++

197 show n ++ " : " ++ show expected ++

196− " as " ++ show tm

198+ " as " ++ show using

197 i <- getIState

199 i <- getIState

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

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

199 ctxt <- getContext

201 ctxt <- getContext

200 let e'' = normaliseAll ctxt [] e'

202 let e'' = normaliseAll ctxt [] e'

203+ logLvl 1 $ "Term is " ++ show e''

201 let et' = normaliseAll ctxt [] et

204 let et' = normaliseAll ctxt [] et

202 elabType info syn "" fc [] n ty

205 elabType info syn "" fc [] n ty

206+ rhs <- execute e''

203− elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (unProv fc tm) []]

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

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

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

205− logLvl 1 $ "** Evaluated: " ++ show e'' ++ " :as: " ++ show et'

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

206

210

207elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

211elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

208 PTerm -> String -> Name -> PTerm -> Idris ()

212 PTerm -> String -> Name -> PTerm -> Idris ()

src/Idris/Providers.hs+2−1

@@ -5,9 +5,10 @@ import Core.Evaluate

5import Idris.AbsSyntax

6import Idris.AbsSyntaxTree

8−

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

9providerTy :: FC -> PTerm -> PTerm

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

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

12unProv :: FC -> PTerm -> PTerm

13unProv :: FC -> PTerm -> PTerm

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

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