a805f47 · Idris-dev · git.iko.soy

miniidris.cabal+1−1

@@ -24,7 +24,7 @@ Executable miniidris

2424

2525 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

2626 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

27− Idris.Delaborate

27+ Idris.Delaborate, Idris.Primitives

2828

2929 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

3030 containers, process, transformers

prims.minew file+46

@@ -0,0 +1,46 @@

1+data Bool = False | True;

2+

3+infixl 5 ==, /=, ==.;

4+infixl 6 <, <=, >, >=, <., <=., >., >=.;

5+infixl 7 <<, >>;

6+infixl 8 +,-,++,+.,-.;

7+infixl 9 *,/,*.,/.;

8+

9+(+) : Int -> Int -> Int;

10+(+) = prim__addInt;

11+

12+(-) : Int -> Int -> Int;

13+(-) = prim__subInt;

14+

15+(*) : Int -> Int -> Int;

16+(*) = prim__mulInt;

17+

18+div : Int -> Int -> Int;

19+div = prim__divInt;

20+

21+intToBool : Int -> Bool;

22+intToBool 0 = False;

23+intToBool x = True;

24+

25+boolOp : (Int -> Int -> Int) -> Int -> Int -> Bool;

26+boolOp op x y = intToBool (op x y);

27+

28+(==) : Int -> Int -> Bool;

29+(==) = boolOp prim__eqInt;

30+

31+(<) : Int -> Int -> Bool;

32+(<) = boolOp prim__ltInt;

33+

34+(<=) : Int -> Int -> Bool;

35+(<=) = boolOp prim__lteInt;

36+

37+(>) : Int -> Int -> Bool;

38+(>) = boolOp prim__gtInt;

39+

40+(>=) : Int -> Int -> Bool;

41+(>=) = boolOp prim__gteInt;

42+

43+fact : Int -> Int;

44+fact 0 = 1;

45+fact n = n * fact (n - 1);

46+

src/Core/CaseTree.hs+2−3

@@ -14,8 +14,6 @@ data SC = Case Name [CaseAlt]

1414 | UnmatchedCase String -- error message

1515 deriving Show

1616

17−type Const = Int -- TMP until constants implemented

18−

1917data CaseAlt = ConCase Name Int [Name] SC

2018 | ConstCase Const SC

2119 | DefaultCase SC

@@ -54,6 +52,7 @@ toPat tm = evalState (toPat' tm []) []

5452 else return (PV n)

5553 toPat' (App f a) args = do a' <- toPat' a []

5654 toPat' f (a' : args)

55+ toPat' (Constant c) args = return $ PConst c

5756 toPat' _ _ = return PAny

5857

5958data Partition = Cons [Clause]

@@ -64,7 +63,7 @@ isVarPat (PAny : ps , _) = True

6463isVarPat _ = False

6564

6665isConPat (PCon _ _ _ : ps, _) = True

67−-- constants too

66+isConPat (PConst _ : ps, _) = True

6867isConPat _ = False

6968

7069partition :: [Clause] -> [Partition]

src/Core/CoreParser.hs+10−2

@@ -14,13 +14,21 @@ import Debug.Trace

1414type TokenParser a = PTok.TokenParser a

1515

1616idrisDef = haskellDef {

17+ opStart = iOpStart,

18+ opLetter = iOpLetter,

1719 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],

1820 reservedNames = ["let", "in", "data", "Set", "if", "then", "else",

19− "do", "dsl", "import", "infix", "infixl", "infixr",

21+ "do", "dsl", "import",

22+ "infix", "infixl", "infixr", "prefix",

2023 "where", "forall", "syntax",

21− "using", "params", "namespace"]

24+ "using", "params", "namespace",

25+ "Int", "Float", "Char", "String", "Ptr"]

2226 }

2327

28+iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

29+iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

30+ <|> letter

31+

2432lexer :: TokenParser a

2533lexer = PTok.makeTokenParser idrisDef

2634

src/Core/Evaluate.hs+37−19

@@ -3,9 +3,9 @@

33

44module Core.Evaluate(normalise,

55 Fun(..), Def(..), Context,

6− addToCtxt, addConstant, addDatatype, addCasedef,

6+ addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

77 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

8− Value) where

8+ Value(..)) where

99

1010import Debug.Trace

1111

@@ -19,6 +19,7 @@ data Value = VP NameType Name Value

1919 | VBind Name (Binder Value) (Value -> Value)

2020 | VApp Value Value

2121 | VSet Int

22+ | VConstant Const

2223 | VTmp Int

2324

2425instance Show Value where

@@ -54,7 +55,7 @@ eval ctxt genv tm = ev [] tm where

5455 | Just (Let t v) <- lookup n genv = ev env v

5556 ev env (P Ref n ty) = case lookupDef n ctxt of

5657 Just (Function (Fun _ _ _ v)) -> v

57− Just (Constant nt ty hty) -> VP nt n hty

58+ Just (TyDecl nt ty hty) -> VP nt n hty

5859 Just (CaseOp _ [] tree) ->

5960 case evCase env [] [] tree of

6061 (Nothing, _) -> VP Ref n (ev env ty)

@@ -70,6 +71,7 @@ eval ctxt genv tm = ev [] tm where

7071 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

7172 where vbind env t = fmap (ev env) t

7273 ev env (App f a) = evApply env [ev env a] (ev env f)

74+ ev env (Constant c) = VConstant c

7375 ev env (Set i) = VSet i

7476

7577 evApply env args (VApp f a) = evApply env (a:args) f

@@ -81,6 +83,12 @@ eval ctxt genv tm = ev [] tm where

8183 = case evCase env ns args tree of

8284 (Nothing, _) -> unload env (VP Ref n ty) args

8385 (Just v, rest) -> evApply env rest v

86+ | Just (Operator _ i op) <- lookupDef n ctxt

87+ = if (i <= length args)

88+ then case op (take i args) of

89+ Nothing -> unload env (VP Ref n ty) args

90+ Just v -> evApply env (drop i args) v

91+ else unload env (VP Ref n ty) args

8492 apply env f (a:as) = unload env f (a:as)

8593 apply env f [] = f

8694

@@ -107,9 +115,10 @@ eval ctxt genv tm = ev [] tm where

107115 Maybe ([(Name, Value)], SC)

108116 chooseAlt _ (VP (DCon i a) _ _, args) alts amap

109117 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)

110− | Just sc <- findDefault alts = Just (amap, sc)

111−-- chooseAlt v _ alts amap

112−-- | Just sc <- safeDefault alts = Just (amap, sc)

118+ | Just v <- findDefault alts = Just (amap, v)

119+ chooseAlt _ (VConstant c, []) alts amap

120+ | Just v <- findConst c alts = Just (amap, v)

121+ | Just v <- findDefault alts = Just (amap, v)

113122 chooseAlt _ _ _ _ = Nothing

114123

115124 -- Replace old variable names in the map with new matches

@@ -125,6 +134,10 @@ eval ctxt genv tm = ev [] tm where

125134 findDefault (DefaultCase sc : xs) = Just sc

126135 findDefault (_ : xs) = findDefault xs

127136

137+ findConst c [] = Nothing

138+ findConst c (ConstCase c' v : xs) | c == c' = Just v

139+ findConst c (_ : xs) = findConst c xs

140+

128141 getValArgs tm = getValArgs' tm []

129142 getValArgs' (VApp f a) as = getValArgs' f (a:as)

130143 getValArgs' f as = (f, as)

@@ -136,6 +149,7 @@ quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp i)))

136149 where quoteB t = fmap (quote i) t

137150quote i (VApp f a) = App (quote i f) (quote i a)

138151quote i (VSet u) = Set u

152+quote i (VConstant c) = Constant c

139153quote i (VTmp x) = V (i - x - 1)

140154

141155

@@ -157,14 +171,14 @@ data Fun = Fun Type Value Term Value

157171 A CaseOp is a function defined by a simple case tree -}

158172

159173data Def = Function Fun

160− | Constant NameType Type Value

161− | Operator Type ([Value] -> Maybe Value)

174+ | TyDecl NameType Type Value

175+ | Operator Type Int ([Value] -> Maybe Value)

162176 | CaseOp Type [Name] SC

163177

164178instance Show Def where

165179 show (Function f) = "Function: " ++ show f

166− show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty

167− show (Operator ty _) = "Operator: " ++ show ty

180+ show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

181+ show (Operator ty _ _) = "Operator: " ++ show ty

168182 show (CaseOp ty ns sc) = "Case: " ++ show ns ++ " " ++ show sc

169183

170184-------

@@ -175,31 +189,35 @@ addToCtxt :: Name -> Term -> Type -> Context -> Context

175189addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)

176190 tm (eval ctxt [] tm))) ctxt

177191

178−addConstant :: Name -> Type -> Context -> Context

179−addConstant n ty ctxt = addDef n (Constant Ref ty (eval ctxt [] ty)) ctxt

192+addTyDecl :: Name -> Type -> Context -> Context

193+addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (eval ctxt [] ty)) ctxt

180194

181195addDatatype :: Datatype Name -> Context -> Context

182196addDatatype (Data n ty cons) ctxt

183197 = let ty' = normalise ctxt [] ty in

184198 addCons 0 cons (addDef n

185− (Constant (TCon (arity ty')) ty (eval ctxt [] ty)) ctxt)

199+ (TyDecl (TCon (arity ty')) ty (eval ctxt [] ty)) ctxt)

186200 where

187201 addCons tag [] ctxt = ctxt

188202 addCons tag ((n, ty) : cons) ctxt

189203 = let ty' = normalise ctxt [] ty in

190204 addCons (tag+1) cons (addDef n

191− (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

205+ (TyDecl (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

192206

193207addCasedef :: Name -> CaseDef -> Type -> Context -> Context

194208addCasedef n (CaseDef args sc) ty ctxt

195209 = addDef n (CaseOp ty args sc) ctxt

196210

211+addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

212+addOperator n ty a op ctxt

213+ = addDef n (Operator ty a op) ctxt

214+

197215lookupTy :: Name -> Context -> Maybe Type

198216lookupTy n ctxt = do def <- lookupCtxt n ctxt

199217 case def of

200218 (Function (Fun ty _ _ _)) -> return ty

201− (Constant _ ty _) -> return ty

202− (Operator ty _) -> return ty

219+ (TyDecl _ ty _) -> return ty

220+ (Operator ty _ _) -> return ty

203221 (CaseOp ty _ _) -> return ty

204222

205223lookupP :: Name -> Context -> Maybe Term

@@ -207,9 +225,9 @@ lookupP n ctxt

207225 = do def <- lookupCtxt n ctxt

208226 case def of

209227 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

210− (Constant nt ty hty) -> return (P nt n ty)

228+ (TyDecl nt ty hty) -> return (P nt n ty)

211229 (CaseOp ty _ _) -> return (P Ref n ty)

212− (Operator ty _) -> return (P Ref n ty)

230+ (Operator ty _ _) -> return (P Ref n ty)

213231

214232lookupDef :: Name -> Context -> Maybe Def

215233lookupDef n ctxt = lookupCtxt n ctxt

@@ -219,7 +237,7 @@ lookupVal n ctxt

219237 = do def <- lookupCtxt n ctxt

220238 case def of

221239 (Function (Fun _ _ _ htm)) -> return htm

222− (Constant nt ty hty) -> return (VP nt n hty)

240+ (TyDecl nt ty hty) -> return (VP nt n hty)

223241

224242lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

225243lookupTyEnv n env = li n 0 env where

src/Core/TT.hs+20−1

@@ -96,11 +96,15 @@ lookupCtxt = Map.lookup

9696toAlist :: Ctxt a -> [(Name, a)]

9797toAlist = Map.toList

9898

99+data Const = I Int | Fl Double | Ch Char | Str String

101+ deriving Eq

99102

100103data Raw = Var Name

101104 | RBind Name (Binder Raw) Raw

102105 | RApp Raw Raw

103106 | RSet Int

107+ | RConstant Const

104108 deriving Show

105109

106110data Binder b = Lam { binderTy :: b }

@@ -144,6 +148,7 @@ data TT n = P NameType n (TT n) -- embed type

144148 | V Int

145149 | Bind n (Binder (TT n)) (TT n)

146150 | App (TT n) (TT n) -- function, function type, arg

151+ | Constant Const

147152 | Set Int

148153 deriving Functor

149154

@@ -160,6 +165,7 @@ instance Eq n => Eq (TT n) where

160165 (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys

161166 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

162167 (==) (Set x) (Set y) = x == y

168+ (==) (Constant x) (Constant y) = x == y

163169 (==) _ _ = False

164170

165171-- A few handy operations on well typed terms:

@@ -246,6 +252,8 @@ forget tm = fe [] tm

246252 fe env (Bind n b sc) = RBind n (fmap (fe env) b)

247253 (fe (n:env) sc)

248254 fe env (App f a) = RApp (fe env f) (fe env a)

255+ fe env (Constant c)

256+ = RConstant c

249257 fe env (Set i) = RSet i

250258

251259type Term = TT Name

@@ -261,7 +269,17 @@ type WkEnv = WkEnvTT Name

261269

262270instance (Eq n, Show n) => Show (TT n) where

263271 show t = showEnv [] t

264−

272+

273+instance Show Const where

274+ show (I i) = show i

275+ show (Fl f) = show f

276+ show (Ch c) = show c

277+ show (Str s) = show s

278+ show IType = "Int"

279+ show FlType = "Float"

280+ show ChType = "Char"

281+ show StrType = "String"

282+

265283showEnv env t = showEnv' env t False

266284showEnvDbg env t = showEnv' env t True

267285

@@ -275,6 +293,7 @@ showEnv' env t dbg = se 10 env t where

275293 | noOccurrence n sc && not dbg = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc

276294 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

277295 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

296+ se p env (Constant c) = show c

278297 se p env (Set i) = "Set" ++ show i

279298

280299 sb env n (Lam t) = showb env "\\ " " => " n t

src/Core/Typecheck.hs+7−1

@@ -48,6 +48,12 @@ check ctxt env (RApp f a)

4848 normalise ctxt env (Bind x (Let aty av) t))

4949 t -> fail "Can't apply a non-function type"

5050check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))

51+check ctxt env (RConstant c) = return (Constant c, constType c)

52+ where constType (I _) = Constant IType

53+ constType (Fl _) = Constant FlType

54+ constType (Ch _) = Constant ChType

55+ constType (Str _) = Constant StrType

56+ constType _ = Set 0

5157check ctxt env (RBind n b sc)

5258 = do b' <- checkBinder b

5359 (scv, sct) <- check ctxt ((n, b'):env) sc

@@ -133,7 +139,7 @@ checkProgram ctxt [] = return ctxt

133139checkProgram ctxt ((n, RConst t) : xs)

134140 = do (t', tt') <- trace (show n) $ check ctxt [] t

135141 isSet ctxt [] tt'

136− checkProgram (addConstant n t' ctxt) xs

142+ checkProgram (addTyDecl n t' ctxt) xs

137143checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

138144 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

139145 (val', valt') <- check ctxt [] val

src/Idris/AbsSyntax.hs+4

@@ -76,12 +76,14 @@ data Command = Quit | Help | Eval PTerm

7676data Fixity = Infixl { prec :: Int }

7777 | Infixr { prec :: Int }

7878 | InfixN { prec :: Int }

79+ | PrefixN { prec :: Int }

7980 deriving Eq

8081

8182instance Show Fixity where

8283 show (Infixl i) = "infixl " ++ show i

8384 show (Infixr i) = "infixr " ++ show i

8485 show (InfixN i) = "infix " ++ show i

86+ show (PrefixN i) = "prefix " ++ show i

8587

8688data FixDecl = Fix Fixity String

8789 deriving (Show, Eq)

@@ -121,6 +123,7 @@ data PTerm = PQuote Raw

121123 | PApp PTerm [(Name, PTerm)] [PTerm]

122124 | PHidden PTerm -- irrelevant or hidden pattern

123125 | PSet

126+ | PConstant Const

124127 | Placeholder

125128

126129-- Syntactic sugar info (TODO: namespaces, parameters, modules)

@@ -180,6 +183,7 @@ showImp impl tm = se 10 tm where

180183 ++ concatMap seArg args

181184 se p (PHidden tm) = "." ++ se 0 tm

182185 se p PSet = "Set"

186+ se p (PConstant c) = show c

183187 se p Placeholder = "_"

184188

185189 seArg arg = " " ++ se 0 arg

src/Idris/Delaborate.hs+1

@@ -19,6 +19,7 @@ delab ist tm = de [] tm

1919 de env (Bind n (Let ty val) sc)

2020 = PLet n (de env ty) (de env val) (de (n:env) sc)

2121 de env (Bind n _ sc) = de (n:env) sc

22+ de env (Constant i) = PConstant i

2223 de env (Set i) = PSet

2324

2425 deFn env (App f a) args = deFn env f (a:args)

src/Idris/ElabDecls.hs+8−4

@@ -19,7 +19,7 @@ elabType n ty

1919 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)

2020 (cty, _) <- tclift $ recheck ctxt [] ty'

2121 logLvl 2 $ "---> " ++ show cty

22− updateContext (addConstant n (normalise ctxt [] cty))

22+ updateContext (addTyDecl n (normalise ctxt [] cty))

2323

2424elabData :: PData -> Idris ()

2525elabData (PDatadecl n t dcons)

@@ -27,7 +27,7 @@ elabData (PDatadecl n t dcons)

2727 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)

2828 (cty, _) <- tclift $ recheck ctxt [] t'

2929 logLvl 2 $ "---> " ++ show cty

30− updateContext (addConstant n cty) -- temporary, to check cons

30+ updateContext (addTyDecl n cty) -- temporary, to check cons

3131 cons <- mapM elabCon dcons

3232 setContext (addDatatype (Data n cty cons) ctxt)

3333

@@ -61,8 +61,10 @@ elabClauses n cs

6161elabVal :: PTerm -> Idris (Term, Type)

6262elabVal tm

6363 = do ctxt <- getContext

64+ logLvl 10 (show tm)

6465 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

6566 (build True (infTerm tm))

67+ logLvl 3 ("Value: " ++ show tm')

6668 let vtm = getInferTerm tm'

6769 iLOG (show vtm)

6870 tclift $ recheck ctxt [] vtm

@@ -133,8 +135,9 @@ elab pattern tm = do elab' tm

133135 (h: hs) -> do patvar h; mkPat

134136 [] -> return ()

135137

136− elab' PSet = do exact (RSet 0); solve

137− elab' (PQuote r) = do exact r; solve

138+ elab' PSet = do fill (RSet 0); solve

139+ elab' (PConstant c) = do fill (RConstant c); solve

140+ elab' (PQuote r) = do fill r; solve

138141 elab' (PRef n) | pattern

139142 = try (do apply (Var n) []; solve)

140143 (patvar n)

@@ -160,6 +163,7 @@ elab pattern tm = do elab' tm

160163 elab' (PApp f [] [arg])

161164 = do simple_app (elab' f) (elab' arg)

162165 solve

166+ elab' Placeholder = fail $ "Can't deal with a placeholder here"

163167 elab' x = fail $ "Not implemented " ++ show x

164168

165169 elabArgs [] _ = return ()

src/Idris/Parser.hs+20−2

@@ -32,6 +32,10 @@ identifier= PTok.identifier lexer

3232reserved = PTok.reserved lexer

3333operator = PTok.operator lexer

3434reservedOp= PTok.reservedOp lexer

35+integer = PTok.integer lexer

36+float = PTok.float lexer

37+strlit = PTok.stringLiteral lexer

38+chlit = PTok.charLiteral lexer

3539lchar = lexeme.char

3640

3741parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

@@ -109,6 +113,7 @@ fixity :: IParser (Int -> Fixity)

109113fixity = try (do reserved "infixl"; return Infixl)

110114 <|> try (do reserved "infixr"; return Infixr)

111115 <|> try (do reserved "infix"; return InfixN)

116+ <|> try (do reserved "prefix"; return PrefixN)

112117

113118--------- Expressions ---------

114119

@@ -131,6 +136,7 @@ pSimpleExpr syn =

131136 <|> try (do x <- pfName; return (PRef x))

132137 <|> try (do lchar '_'; return Placeholder)

133138 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

139+ <|> try (do c <- pConstant; return (PConstant c))

134140 <|> try (do reserved "Set"; return PSet)

135141

136142pHSimpleExpr syn

@@ -177,20 +183,32 @@ tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)

177183bindList b [] sc = sc

178184bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

179185

186+pConstant :: IParser Const

187+pConstant = do reserved "Int"; return IType

188+ <|> do reserved "Char"; return ChType

189+ <|> do reserved "Float"; return FlType

190+ <|> do reserved "String"; return StrType

191+ <|> do reserved "Ptr"; return PtrType

192+ <|> do i <- natural; return $ I (fromInteger i)

193+

180194table fixes

181− = toTable (reverse fixes) ++

195+ = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [] [PConstant (I 0), x])]]

196+ ++ toTable (reverse fixes) ++

182197 [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],

183198 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]

184199

185200toTable fs = map (map toBin)

186201 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

187− where toBin (Fix f op) = binary op

202+ where toBin (Fix (PrefixN _) op) = prefix op

203+ (\x -> PApp (PRef (UN [op])) [] [x])

204+ toBin (Fix f op) = binary op

188205 (\x y -> PApp (PRef (UN [op])) [] [x,y]) (assoc f)

189206 assoc (Infixl _) = AssocLeft

190207 assoc (Infixr _) = AssocRight

191208 assoc (InfixN _) = AssocNone

192209

193210binary name f assoc = Infix (do { reservedOp name; return f }) assoc

211+prefix name f = Prefix (do { reservedOp name; return f })

194212

195213--------- Data declarations ---------

196214

src/Idris/Primitives.hsnew file+41

@@ -0,0 +1,41 @@

1+module Idris.Primitives(elabPrims) where

2+

3+import Idris.ElabDecls

4+import Idris.AbsSyntax

5+

6+import Core.TT

7+import Core.Evaluate

8+

9+data Prim = Prim { p_name :: Name,

10+ p_type :: Type,

11+ p_arity :: Int,

12+ p_def :: [Value] -> Maybe Value

13+ }

14+

15+ty [] x = Constant x

16+ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)

17+

18+primitives =

19+ [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (vBin (+)),

20+ Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (vBin (-)),

21+ Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (vBin (*)),

22+ Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (vBin (div)),

23+ Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (bBin (==)),

24+ Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (bBin (<)),

25+ Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (bBin (<=)),

26+ Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (bBin (>)),

27+ Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (bBin (>=))

28+ ]

29+

30+vBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

31+vBin _ _ = Nothing

32+

33+bBin op = vBin (\x y -> if (op x y) then 1 else 0)

34+

35+elabPrim :: Prim -> Idris ()

36+elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)

37+

38+elabPrims :: Idris ()

39+elabPrims = do elabDecl (PData inferDecl)

40+ mapM_ elabPrim primitives

41+

src/Main.hs+2−1

@@ -19,6 +19,7 @@ import Idris.AbsSyntax

1919import Idris.Parser

2020import Idris.REPL

2121import Idris.ElabDecls

22+import Idris.Primitives

2223

2324-- Main program reads command line options, parses the main program, and gets

2425-- on with the REPL.

@@ -36,6 +37,7 @@ runIdris :: [Opt] -> Idris ()

3637runIdris opts =

3738 do let inputs = opt getFile opts

3839 mapM_ makeOption opts

40+ elabPrims

3941 mapM_ loadModule inputs

4042 repl

4143 where

@@ -49,7 +51,6 @@ loadModule f = do iLOG ("Reading " ++ show f)

4951 i <- get

5052 iLOG (show (idris_infixes i))

5153 -- Now add all the declarations to the context

52− elabDecl (PData inferDecl) -- a handy primitive

5354 mapM_ elabDecl ds

5455 return ()

5556