1579621 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow Execute to import primitives without cycle

The executor can now import Idris.Primitives without introducing an import cycle. This involved moving elabPrims to the ElabDecls module.

commit1579621b7ceaec01e802995a62aa0af1dfcd9012 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 27 Jun 2013, 10:51 (13 years ago) parent55ec9cb

3 files changed+26−20

compare with master

unifiedsplit

src/Core/Execute.hs+2 src/Idris/ElabDecls.hs+22 src/Idris/Primitives.hs+2−20

src/Core/Execute.hs+2

@@ -7,6 +7,8 @@ import IRTS.Lang( IntTy(..)

77 , intTyToConst

88 , FType(..))

10+import Idris.Primitives(Prim(..), primitives)

11+

1012import Core.TT

1113import Core.Evaluate

1214import Core.CaseTree

src/Idris/ElabDecls.hs+22

@@ -12,6 +12,7 @@ import Idris.ElabTerm

1212import Idris.Coverage

1313import Idris.DataOpts

1414import Idris.Providers

15+import Idris.Primitives

1516import Paths_idris

1617

1718import Core.TT

@@ -210,6 +211,27 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

210211 | otherwise = count n ts

211212 mParam args (_ : rest) = Nothing : mParam args rest

212213

214+-- | Elaborate primitives

215+

216+elabPrims :: Idris ()

217+elabPrims = do mapM_ (elabDecl EAll toplevel)

218+ (map (PData "" defaultSyntax (FC "builtin" 0) False)

219+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

220+ mapM_ elabPrim primitives

221+ where elabPrim :: Prim -> Idris ()

222+ elabPrim (Prim n ty i def sc tot)

223+ = do updateContext (addOperator n ty i (valuePrim def))

224+ setTotality n tot

225+ i <- getIState

226+ putIState i { idris_scprims = (n, sc) : idris_scprims i }

227+

228+ valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value

229+ valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)

230+

231+ getConst (VConstant c) = Just c

232+ getConst _ = Nothing

233+

234+

213235-- | Elaborate a type provider

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

215237elabProvider info syn fc n ty tm

src/Idris/Primitives.hs+2−20

@@ -1,9 +1,7 @@

11{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}

3−module Idris.Primitives(elabPrims) where

3+module Idris.Primitives(primitives, Prim(..)) where

5−import Idris.ElabDecls

6−import Idris.ElabTerm

75import Idris.AbsSyntax

97import IRTS.Lang

@@ -458,21 +456,5 @@ p_strRev _ = Nothing

458456p_cantreduce :: a -> Maybe b

459457p_cantreduce _ = Nothing

460458

461−valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value

462−valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)

463− where getConst (VConstant c) = Just c

464− getConst _ = Nothing

465−

466−elabPrim :: Prim -> Idris ()

467−elabPrim (Prim n ty i def sc tot)

468− = do updateContext (addOperator n ty i (valuePrim def))

469− setTotality n tot

470− i <- getIState

471− putIState i { idris_scprims = (n, sc) : idris_scprims i }

472−

473−elabPrims :: Idris ()

474−elabPrims = do mapM_ (elabDecl EAll toplevel)

475− (map (PData "" defaultSyntax (FC "builtin" 0) False)

476− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

477− mapM_ elabPrim primitives

459+

478460