0f49abc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added first steps in type providers

Now, type provider syntax is parsed and the providers are elaborated to top-level definitions. Next step is to cause them to be normalized before type-checking, possibly performing IO in the process.

commit0f49abc2f38012ff5ed5fa96f324b61dcee9e7e0 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 13 Mar 2013, 12:15 (14 years ago) parent6e732f9

6 files changed+68−22

compare with master

unifiedsplit

lib/Providers.idr+8 lib/base.ipkg+2 src/Idris/AbsSyntaxTree.hs+11−1 src/Idris/ElabDecls.hs+25 src/Idris/Parser.hs+9−21 src/Idris/Providers.hs+13

lib/Providers.idrnew file+8

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

1+module Providers

3+public

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

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,

1717

1818 Uninhabited,

1919

20+ Providers,

21+

2022 Language.Reflection,

2123

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

src/Idris/AbsSyntaxTree.hs+11−1

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

330330 | PSyntax FC Syntax -- ^ Syntax definition

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

332332 | 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

333334 deriving Functor

334335{-!

335336deriving instance Binary PDecl'

336337!-}

337338

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

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)

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

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

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

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

src/Idris/ElabDecls.hs+25

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

1111import Idris.ElabTerm

1212import Idris.Coverage

1313import Idris.DataOpts

14+import Idris.Providers

1415import Paths_idris

1516

1617import Core.TT

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

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

3940 return (n, t')) ns

4041

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

4143elabType :: ElabInfo -> SyntaxInfo -> String ->

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

4345elabType 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)

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

186188 updateParamsA ps args all = ps

187189

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+

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

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

190209elabRecord info syn doc fc tyn ty cdoc cn cty

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

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

330349 mkLazy t = t

331350

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

352+-- top-level definition.

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

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

334355 do ctxt <- getContext

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

12631284 addIBC (IBCDSL n)

12641285elabDecl' what info (PDirective i)

12651286 | 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

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

12671292

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

src/Idris/Parser.hs+9−21

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

341341 <|> pInstance syn

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

343343 <|> pDirective syn

344+ <|> pProvider syn

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

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

346347

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

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

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

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

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

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

1490− fc <- pfc

1491− -- pack into provider

1492− let expected = providerTy fc t

1493− reserved "with"

1494− e <- pExpr syn

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

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− )])

1489+

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

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

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

1493+ fc <- pfc

1494+ reserved "with"

1495+ e <- pExpr syn

1496+ return [PProvider syn fc n t e]

15091497

15101498pTactic :: SyntaxInfo -> IParser PTactic

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

src/Idris/Providers.hsnew file+13

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

1+module Idris.Providers where

3+import Core.TT

4+import Core.Evaluate

5+import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

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 ""]