574a82b · Idris-dev · git.iko.soy

lib/Providers.idrnew file+8

compare with master

unifiedsplit

@@ -0,0 +1,8 @@

1+module Providers

2+

3+public

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

5+

6+abstract partial

7+unProv : Provider a -> a

8+unProv (Provide x) = unsafePerformIO x

lib/base.ipkg+2

@@ -17,6 +17,8 @@ modules = Builtins, Prelude, IO, System,

17

18 Uninhabited,

19

20+ Providers,

21+

20 Language.Reflection,

22 Language.Reflection,

21

23

22 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

24 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

src/Idris/AbsSyntaxTree.hs+11−1

@@ -330,12 +330,22 @@ data PDecl' t

330 | PSyntax FC Syntax -- ^ Syntax definition

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

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

333+ | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term

333 deriving Functor

334 deriving Functor

334{-!

335{-!

335deriving instance Binary PDecl'

336deriving instance Binary PDecl'

336!-}

337!-}

337

338

339+-- | One clause of a top-level definition. Term arguments to constructors are:

340+--

341+-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)

342+--

343+-- 2. The list of patterns

344+--

345+-- 3. The right-hand side

346+--

347+-- 4. The where block (PDecl' t)

338−data PClause' t = PClause FC Name t [t] t [PDecl' t]

348+data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

339 | PWith FC Name t [t] t [PDecl' t]

349 | PWith FC Name t [t] t [PDecl' t]

340 | PClauseR FC [t] t [PDecl' t]

350 | PClauseR FC [t] t [PDecl' t]

341 | PWithR FC [t] t [PDecl' t]

351 | PWithR FC [t] t [PDecl' t]

src/Idris/ElabDecls.hs+25

@@ -11,6 +11,7 @@ import Idris.Imports

11import Idris.ElabTerm

12import Idris.Coverage

13import Idris.DataOpts

14+import Idris.Providers

14import Paths_idris

15import Paths_idris

15

16

16import Core.TT

17import Core.TT

@@ -38,6 +39,7 @@ checkDef fc ns = do ctxt <- getContext

38 mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

39 mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

39 return (n, t')) ns

40 return (n, t')) ns

40

41

42+-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

41elabType :: ElabInfo -> SyntaxInfo -> String ->

43elabType :: ElabInfo -> SyntaxInfo -> String ->

42 FC -> FnOpts -> Name -> PTerm -> Idris ()

44 FC -> FnOpts -> Name -> PTerm -> Idris ()

43elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

45elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

@@ -185,6 +187,23 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

185 = (mn, False) : updateParamsA ns args (p : all)

187 = (mn, False) : updateParamsA ns args (p : all)

186 updateParamsA ps args all = ps

188 updateParamsA ps args all = ps

187

189

190+-- | Elaborate a type provider

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

192+elabProvider info syn fc n ty tm

193+ = do let expected = providerTy fc ty

194+ logLvl 1 $ "** Providing " ++

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

196+ " as " ++ show tm

197+ i <- getIState

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

199+ ctxt <- getContext

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

201+ let et' = normaliseAll ctxt [] et

202+ elabType info syn "" fc [] n ty

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

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

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

206+

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

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

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

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

190elabRecord info syn doc fc tyn ty cdoc cn cty

209elabRecord info syn doc fc tyn ty cdoc cn cty

@@ -329,6 +348,8 @@ elabCon info syn tn codata (doc, n, t_in, fc)

329 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

348 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

330 mkLazy t = t

349 mkLazy t = t

331

350

351+-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

352+-- top-level definition.

332elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

353elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

333elabClauses info fc opts n_in cs = let n = liftname info n_in in

354elabClauses info fc opts n_in cs = let n = liftname info n_in in

334 do ctxt <- getContext

355 do ctxt <- getContext

@@ -1263,6 +1284,10 @@ elabDecl' _ info (PDSL n dsl)

1263 addIBC (IBCDSL n)

1284 addIBC (IBCDSL n)

1264elabDecl' what info (PDirective i)

1285elabDecl' what info (PDirective i)

1265 | what /= EDefns = i

1286 | what /= EDefns = i

1287+elabDecl' what info (PProvider syn fc n tp tm)

1288+ | what /= EDefns

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

1290+ elabProvider info syn fc n tp tm

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

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

1267

1292

1268elabCaseBlock info d@(PClauses f o n ps)

1293elabCaseBlock info d@(PClauses f o n ps)

src/Idris/Parser.hs+9−21

@@ -341,6 +341,7 @@ pDecl syn = do notEndBlock

341 <|> pInstance syn

342 <|> do d <- pDSL syn; return [d]

343 <|> pDirective syn

344+ <|> pProvider syn

344 <|> try (do reserved "import"; fp <- identifier

345 <|> try (do reserved "import"; fp <- identifier

345 fail "imports must be at the top of file")

346 fail "imports must be at the top of file")

346

347

@@ -1485,27 +1486,14 @@ pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

1485 putIState (i { default_total = tot }))])

1486 putIState (i { default_total = tot }))])

1486 <|> try (do lchar '%'; reserved "logging"; i <- natural;

1487 <|> try (do lchar '%'; reserved "logging"; i <- natural;

1487 return [PDirective (setLogLevel (fromInteger i))])

1488 return [PDirective (setLogLevel (fromInteger i))])

1489+

1490+pProvider :: SyntaxInfo -> IParser [PDecl]

1488− <|> try (do lchar '%'; reserved "provide";

1491+pProvider syn = do lchar '%'; reserved "provide";

1489− lchar '('; n <- pfName; t <- pTSig syn; lchar ')'

1492+ lchar '('; n <- pfName; t <- pTSig syn; lchar ')'

1490− fc <- pfc

1493+ fc <- pfc

1491− -- pack into provider

1492− let expected = providerTy fc t

1493− reserved "with"

1494+ reserved "with"

1494− e <- pExpr syn

1495+ e <- pExpr syn

1495− return [PDirective (do logLvl 1 $ "** Providing " ++

1496+ return [PProvider syn fc n t e]

1496− show n ++ " : " ++ show expected ++

1497− " as " ++ show e

1498− i <- getIState

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

1500− ctxt <- getContext

1501− ist <- get

1502− let e'' = normaliseAll ctxt [] e'

1503− let et' = normaliseAll ctxt [] et

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

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

1506−

1507−

1508− )])

1509

1497

1510pTactic :: SyntaxInfo -> IParser PTactic

1498pTactic :: SyntaxInfo -> IParser PTactic

1511pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1499pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

src/Idris/Providers.hsnew file+13

@@ -0,0 +1,13 @@

1+module Idris.Providers where

2+

3+import Core.TT

4+import Core.Evaluate

5+import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

7+

8+

9+providerTy :: FC -> PTerm -> PTerm

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

11+

12+unProv :: FC -> PTerm -> PTerm

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