a805f47 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added constants and some primitive operations

a805f47Edwin Brady15 years ago

miniidris.cabal+1−1

compare with master

unifiedsplit

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

25 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

26 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

27− Idris.Delaborate

27+ Idris.Delaborate, Idris.Primitives

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

30 containers, process, transformers

prims.minew file+46

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

1+data Bool = False | True;

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

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

5+infixl 7 <<, >>;

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

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

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]

14 | UnmatchedCase String -- error message

15 deriving Show

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

18−

19data CaseAlt = ConCase Name Int [Name] SC

17data CaseAlt = ConCase Name Int [Name] SC

20 | ConstCase Const SC

18 | ConstCase Const SC

21 | DefaultCase SC

19 | DefaultCase SC

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

54 else return (PV n)

52 else return (PV n)

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

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

56 toPat' f (a' : args)

54 toPat' f (a' : args)

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

57 toPat' _ _ = return PAny

56 toPat' _ _ = return PAny

59data Partition = Cons [Clause]

58data Partition = Cons [Clause]

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

64isVarPat _ = False

63isVarPat _ = False

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

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

67−-- constants too

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

68isConPat _ = False

67isConPat _ = False

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

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

src/Core/CoreParser.hs+10−2

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

14type TokenParser a = PTok.TokenParser a

16idrisDef = haskellDef {

17+ opStart = iOpStart,

18+ opLetter = iOpLetter,

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

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

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

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

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

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

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

20 "where", "forall", "syntax",

23 "where", "forall", "syntax",

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

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

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

22 }

26 }

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

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

30+ <|> letter

31+

24lexer :: TokenParser a

32lexer :: TokenParser a

25lexer = PTok.makeTokenParser idrisDef

33lexer = PTok.makeTokenParser idrisDef

src/Core/Evaluate.hs+37−19

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

4module Core.Evaluate(normalise,

5 Fun(..), Def(..), Context,

6− addToCtxt, addConstant, addDatatype, addCasedef,

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

7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

8− Value) where

8+ Value(..)) where

10import Debug.Trace

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

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

20 | VApp Value Value

21 | VSet Int

22+ | VConstant Const

22 | VTmp Int

23 | VTmp Int

24instance Show Value where

25instance Show Value where

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

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

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

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

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

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

57 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

58 Just (CaseOp _ [] tree) ->

59 Just (CaseOp _ [] tree) ->

59 case evCase env [] [] tree of

60 case evCase env [] [] tree of

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

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

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

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

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

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

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

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

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

74+ ev env (Constant c) = VConstant c

73 ev env (Set i) = VSet i

75 ev env (Set i) = VSet i

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

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

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

81 = case evCase env ns args tree of

83 = case evCase env ns args tree of

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

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

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

85 (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

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

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

85 apply env f [] = f

93 apply env f [] = f

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

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

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

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

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

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

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

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

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

111−-- chooseAlt v _ alts amap

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

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

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

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

113 chooseAlt _ _ _ _ = Nothing

122 chooseAlt _ _ _ _ = Nothing

114

123

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

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

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

125 findDefault (DefaultCase sc : xs) = Just sc

134 findDefault (DefaultCase sc : xs) = Just sc

126 findDefault (_ : xs) = findDefault xs

135 findDefault (_ : xs) = findDefault xs

127

136

137+ findConst c [] = Nothing

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

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

140+

128 getValArgs tm = getValArgs' tm []

141 getValArgs tm = getValArgs' tm []

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

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

130 getValArgs' f as = (f, as)

143 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)))

136 where quoteB t = fmap (quote i) t

149 where quoteB t = fmap (quote i) t

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

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

138quote i (VSet u) = Set u

151quote i (VSet u) = Set u

152+quote i (VConstant c) = Constant c

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

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

140

154

141

155

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

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

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

158

172

159data Def = Function Fun

173data Def = Function Fun

160− | Constant NameType Type Value

174+ | TyDecl NameType Type Value

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

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

162 | CaseOp Type [Name] SC

176 | CaseOp Type [Name] SC

163

177

164instance Show Def where

178instance Show Def where

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

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

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

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

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

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

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

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

169

183

170-------

184-------

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

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

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

176 tm (eval ctxt [] tm))) ctxt

190 tm (eval ctxt [] tm))) ctxt

177

191

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

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

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

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

180

194

181addDatatype :: Datatype Name -> Context -> Context

195addDatatype :: Datatype Name -> Context -> Context

182addDatatype (Data n ty cons) ctxt

196addDatatype (Data n ty cons) ctxt

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

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

184 addCons 0 cons (addDef n

198 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)

186 where

200 where

187 addCons tag [] ctxt = ctxt

201 addCons tag [] ctxt = ctxt

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

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

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

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

190 addCons (tag+1) cons (addDef n

204 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)

192

206

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

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

194addCasedef n (CaseDef args sc) ty ctxt

208addCasedef n (CaseDef args sc) ty ctxt

195 = addDef n (CaseOp ty args sc) ctxt

209 = addDef n (CaseOp ty args sc) ctxt

196

210

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+

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

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

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

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

199 case def of

217 case def of

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

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

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

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

202− (Operator ty _) -> return ty

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

203 (CaseOp ty _ _) -> return ty

221 (CaseOp ty _ _) -> return ty

204

222

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

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

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

207 = do def <- lookupCtxt n ctxt

225 = do def <- lookupCtxt n ctxt

208 case def of

226 case def of

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

227 (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)

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

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

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

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

213

231

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

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

215lookupDef n ctxt = lookupCtxt n ctxt

233lookupDef n ctxt = lookupCtxt n ctxt

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

219 = do def <- lookupCtxt n ctxt

237 = do def <- lookupCtxt n ctxt

220 case def of

238 case def of

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

239 (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)

223

241

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

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

225lookupTyEnv n env = li n 0 env where

243lookupTyEnv n env = li n 0 env where

src/Core/TT.hs+20−1

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

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

97toAlist = Map.toList

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

101+ deriving Eq

102

100data Raw = Var Name

103data Raw = Var Name

101 | RBind Name (Binder Raw) Raw

104 | RBind Name (Binder Raw) Raw

102 | RApp Raw Raw

105 | RApp Raw Raw

103 | RSet Int

106 | RSet Int

107+ | RConstant Const

104 deriving Show

108 deriving Show

105

109

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

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

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

144 | V Int

148 | V Int

145 | Bind n (Binder (TT n)) (TT n)

149 | Bind n (Binder (TT n)) (TT n)

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

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

151+ | Constant Const

147 | Set Int

152 | Set Int

148 deriving Functor

153 deriving Functor

149

154

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

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

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

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

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

162 (==) (Set x) (Set y) = x == y

167 (==) (Set x) (Set y) = x == y

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

163 (==) _ _ = False

169 (==) _ _ = False

164

170

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

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

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

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

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

247 (fe (n:env) sc)

253 (fe (n:env) sc)

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

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

255+ fe env (Constant c)

256+ = RConstant c

249 fe env (Set i) = RSet i

257 fe env (Set i) = RSet i

250

258

251type Term = TT Name

259type Term = TT Name

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

261

269

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

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

263 show t = showEnv [] t

271 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+

265showEnv env t = showEnv' env t False

283showEnv env t = showEnv' env t False

266showEnvDbg env t = showEnv' env t True

284showEnvDbg env t = showEnv' env t True

267

285

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

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

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

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

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

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

295 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

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

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

279

298

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

299 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)

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

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

50check 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

51check ctxt env (RBind n b sc)

57check ctxt env (RBind n b sc)

52 = do b' <- checkBinder b

58 = do b' <- checkBinder b

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

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

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

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

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

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

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

135 isSet ctxt [] tt'

141 isSet ctxt [] tt'

136− checkProgram (addConstant n t' ctxt) xs

142+ checkProgram (addTyDecl n t' ctxt) xs

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

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

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

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

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

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

src/Idris/AbsSyntax.hs+4

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

76data Fixity = Infixl { prec :: Int }

77 | Infixr { prec :: Int }

78 | InfixN { prec :: Int }

79+ | PrefixN { prec :: Int }

79 deriving Eq

80 deriving Eq

81instance Show Fixity where

82instance Show Fixity where

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

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

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

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

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

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

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

86data FixDecl = Fix Fixity String

88data FixDecl = Fix Fixity String

87 deriving (Show, Eq)

89 deriving (Show, Eq)

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

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

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

122 | PHidden PTerm -- irrelevant or hidden pattern

124 | PHidden PTerm -- irrelevant or hidden pattern

123 | PSet

125 | PSet

126+ | PConstant Const

124 | Placeholder

127 | Placeholder

125

128

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

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

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

180 ++ concatMap seArg args

183 ++ concatMap seArg args

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

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

182 se p PSet = "Set"

185 se p PSet = "Set"

186+ se p (PConstant c) = show c

183 se p Placeholder = "_"

187 se p Placeholder = "_"

184

188

185 seArg arg = " " ++ se 0 arg

189 seArg arg = " " ++ se 0 arg

src/Idris/Delaborate.hs+1

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

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

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

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

22+ de env (Constant i) = PConstant i

22 de env (Set i) = PSet

23 de env (Set i) = PSet

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

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

src/Idris/ElabDecls.hs+8−4

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

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

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

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

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

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

24elabData :: PData -> Idris ()

25elabData (PDatadecl n t dcons)

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

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

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

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

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

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

31 cons <- mapM elabCon dcons

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

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

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

62elabVal tm

63 = do ctxt <- getContext

64+ logLvl 10 (show tm)

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

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

65 (build True (infTerm tm))

66 (build True (infTerm tm))

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

66 let vtm = getInferTerm tm'

68 let vtm = getInferTerm tm'

67 iLOG (show vtm)

69 iLOG (show vtm)

68 tclift $ recheck ctxt [] vtm

70 tclift $ recheck ctxt [] vtm

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

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

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

134 [] -> return ()

136 [] -> return ()

135

137

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

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

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

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

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

138 elab' (PRef n) | pattern

141 elab' (PRef n) | pattern

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

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

140 (patvar n)

143 (patvar n)

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

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

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

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

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

162 solve

165 solve

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

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

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

164

168

165 elabArgs [] _ = return ()

169 elabArgs [] _ = return ()

src/Idris/Parser.hs+20−2

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

32reserved = PTok.reserved lexer

33operator = PTok.operator lexer

34reservedOp= PTok.reservedOp lexer

35+integer = PTok.integer lexer

36+float = PTok.float lexer

37+strlit = PTok.stringLiteral lexer

38+chlit = PTok.charLiteral lexer

35lchar = lexeme.char

39lchar = lexeme.char

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

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

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

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

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

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

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

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

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

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

112

117

113--------- Expressions ---------

118--------- Expressions ---------

114

119

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

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

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

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

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

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

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

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

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

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

135

141

136pHSimpleExpr syn

142pHSimpleExpr syn

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

177bindList b [] sc = sc

183bindList b [] sc = sc

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

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

179

185

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+

180table fixes

194table fixes

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

181− = toTable (reverse fixes) ++

196+ ++ toTable (reverse fixes) ++

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

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

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

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

184

199

185toTable fs = map (map toBin)

200toTable fs = map (map toBin)

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

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

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

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

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

204+ toBin (Fix f op) = binary op

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

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

189 assoc (Infixl _) = AssocLeft

206 assoc (Infixl _) = AssocLeft

190 assoc (Infixr _) = AssocRight

207 assoc (Infixr _) = AssocRight

191 assoc (InfixN _) = AssocNone

208 assoc (InfixN _) = AssocNone

192

209

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

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

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

194

212

195--------- Data declarations ---------

213--------- Data declarations ---------

196

214

src/Idris/Primitives.hsnew file+41

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

1+module Idris.Primitives(elabPrims) where

3+import Idris.ElabDecls

4+import Idris.AbsSyntax

6+import Core.TT

7+import Core.Evaluate

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

19import Idris.Parser

20import Idris.REPL

21import Idris.ElabDecls

22+import Idris.Primitives

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

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

24-- on with the REPL.

25-- on with the REPL.

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

36runIdris opts =

37runIdris opts =

37 do let inputs = opt getFile opts

38 do let inputs = opt getFile opts

38 mapM_ makeOption opts

39 mapM_ makeOption opts

40+ elabPrims

39 mapM_ loadModule inputs

41 mapM_ loadModule inputs

40 repl

42 repl

41 where

43 where

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

49 i <- get

51 i <- get

50 iLOG (show (idris_infixes i))

52 iLOG (show (idris_infixes i))

51 -- Now add all the declarations to the context

53 -- Now add all the declarations to the context

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

53 mapM_ elabDecl ds

54 mapM_ elabDecl ds

54 return ()

55 return ()