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

git.iko.soy/Idris-dev

Execute type providers while typechecking

commit879769aefad44c46afdb269c5db28dfecb85dbbf authorDavid Christiansen <david@davidchristiansen.dk> dateMon 18 Mar 2013, 16:55 (14 years ago) parent6f7f300

4 files changed+20−14

compare with master

unifiedsplit

lib/Providers.idr+1−1 src/Core/Execute.hs+9−8 src/Idris/ElabDecls.hs+8−4 src/Idris/Providers.hs+2−1

lib/Providers.idr+1−1

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

33public

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

6−abstract partial

6+partial public

77unProv : Provider a -> a

88unProv (Provide x) = unsafePerformIO x

src/Core/Execute.hs+9−8

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

2424-- IO was performed.

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

2626step 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

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

2929 step' _ = return Nothing

3030

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

3232-- resulting term (possibly the argument).

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

34−execute tm = do stepped <- step tm

35− case stepped of

36− Nothing -> return tm

37− Just tm' -> execute tm'

34+execute tm = case unApply tm of

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

36+ _ -> return tm

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

38+ case stepped of

39+ Nothing -> return tm

40+ Just tm' -> execute' tm'

3841

3942

4043

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

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

4750 case fn of

4851 Nothing -> return Nothing

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

50− return . Just $ res

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

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

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

5355 return (Constant (I (fromIntegral res)))

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

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

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

6769

68−

6970 prepArgs = map prepArg

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

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

src/Idris/ElabDecls.hs+8−4

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

1717import Core.TT

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

1919import Core.Evaluate

20+import Core.Execute

2021import Core.Typecheck

2122import Core.CaseTree

2223

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

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

192193elabProvider info syn fc n ty tm

193194 = do let expected = providerTy fc ty

195+ let using = unProv fc tm

194196 logLvl 1 $ "** Providing " ++

195197 show n ++ " : " ++ show expected ++

196− " as " ++ show tm

198+ " as " ++ show using

197199 i <- getIState

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

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

199201 ctxt <- getContext

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

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

201204 let et' = normaliseAll ctxt [] et

202205 elabType info syn "" fc [] n ty

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

206+ rhs <- execute e''

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

204208 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'

206210

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

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

src/Idris/Providers.hs+2−1

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

55import Idris.AbsSyntax

66import Idris.AbsSyntaxTree

8−

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

99providerTy :: FC -> PTerm -> PTerm

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

1111

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

1213unProv :: FC -> PTerm -> PTerm

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