1579621 · Idris-dev · git.iko.soy

src/Core/Execute.hs+2

compare with master

unifiedsplit

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

7 , intTyToConst

8 , FType(..))

9

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

11+

10import Core.TT

12import Core.TT

11import Core.Evaluate

13import Core.Evaluate

12import Core.CaseTree

14import Core.CaseTree

src/Idris/ElabDecls.hs+22

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

12import Idris.Coverage

13import Idris.DataOpts

14import Idris.Providers

15+import Idris.Primitives

15import Paths_idris

16import Paths_idris

16

17

17import Core.TT

18import Core.TT

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

210 | otherwise = count n ts

211 | otherwise = count n ts

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

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

212

213

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+

213-- | Elaborate a type provider

235-- | Elaborate a type provider

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

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

215elabProvider info syn fc n ty tm

237elabProvider info syn fc n ty tm

src/Idris/Primitives.hs+2−20

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

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

2

3−module Idris.Primitives(elabPrims) where

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

4

5−import Idris.ElabDecls

6−import Idris.ElabTerm

7import Idris.AbsSyntax

5import Idris.AbsSyntax

8

6

9import IRTS.Lang

7import IRTS.Lang

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

458p_cantreduce :: a -> Maybe b

456p_cantreduce :: a -> Maybe b

459p_cantreduce _ = Nothing

457p_cantreduce _ = Nothing

460

458

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

459+

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

478

460