6554c7d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Towards primitives in new VM

6554c7dEdwin Brady14 years ago

src/Core/TT.hs+3−1

compare with master

unifiedsplit

@@ -236,7 +236,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

236

237data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

239− | PtrType | Forgot

239+ | PtrType | VoidType | Forgot

240 deriving Eq

241{-!

242deriving instance Binary Const

@@ -257,6 +257,7 @@ instance Pretty Const where

257 pretty ChType = text "Char"

258 pretty StrType = text "String"

259 pretty PtrType = text "Ptr"

260+ pretty VoidType = text "Void"

260 pretty Forgot = text "Forgot"

261 pretty Forgot = text "Forgot"

261

262

262data Raw = Var Name

263data Raw = Var Name

@@ -605,6 +606,7 @@ instance Show Const where

605 show ChType = "Char"

606 show ChType = "Char"

606 show StrType = "String"

607 show StrType = "String"

607 show PtrType = "Ptr"

608 show PtrType = "Ptr"

609+ show VoidType = "Void"

608

610

609showEnv env t = showEnv' env t False

611showEnv env t = showEnv' env t False

610showEnvDbg env t = showEnv' env t True

612showEnvDbg env t = showEnv' env t True

src/Idris/AbsSyntax.hs+3−1

@@ -7,6 +7,7 @@ import Core.TT

7import Core.Evaluate

8import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10+import RTS.SC

11import Paths_idris

12import Paths_idris

@@ -66,6 +67,7 @@ data IState = IState { tt_ctxt :: Context,

66 syntax_keywords :: [String],

67 syntax_keywords :: [String],

67 imported :: [FilePath],

68 imported :: [FilePath],

68 idris_prims :: [(Name, ([E.Name], E.Term))],

69 idris_prims :: [(Name, ([E.Name], E.Term))],

70+ idris_scprims :: [(Name, ([CType], CType, SPrim))],

69 idris_objs :: [FilePath],

71 idris_objs :: [FilePath],

70 idris_libs :: [String],

72 idris_libs :: [String],

71 idris_hdrs :: [String],

73 idris_hdrs :: [String],

@@ -105,7 +107,7 @@ data IBCWrite = IBCFix FixDecl

105idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

107idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

106 emptyContext emptyContext emptyContext emptyContext

108 emptyContext emptyContext emptyContext emptyContext

107 emptyContext emptyContext emptyContext

109 emptyContext emptyContext emptyContext

108− [] "" defaultOpts 6 [] [] [] [] [] [] [] []

110+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

109 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

111 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

110

112

111-- The monad for the main REPL - reading and processing files and updating

113-- The monad for the main REPL - reading and processing files and updating

src/Idris/Primitives.hs+79−66

@@ -6,6 +6,8 @@ import Idris.ElabDecls

6import Idris.ElabTerm

7import Idris.AbsSyntax

9+import RTS.SC

10+

9import Core.TT

11import Core.TT

10import Core.Evaluate

12import Core.Evaluate

@@ -17,6 +19,7 @@ data Prim = Prim { p_name :: Name,

17 p_arity :: Int,

19 p_arity :: Int,

18 p_def :: [Value] -> Maybe Value,

20 p_def :: [Value] -> Maybe Value,

19 p_epic :: ([E.Name], E.Term),

21 p_epic :: ([E.Name], E.Term),

22+ p_sc :: ([CType], CType, SPrim),

20 p_total :: Totality

23 p_total :: Totality

21 }

24 }

@@ -79,137 +82,146 @@ partial = Partial NotCovering

79primitives =

82primitives =

80 -- operators

83 -- operators

81 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

84 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

82− (eOp E.plus_) total,

85+ (eOp E.plus_) ([sInt, sInt], sInt, AddI) total,

83 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))

86 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))

84− (eOp E.minus_) total,

87+ (eOp E.minus_)

88+ ([sInt, sInt], sInt, SubI) total,

85 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))

89 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))

86− (eOp E.times_) total,

90+ (eOp E.times_) ([sInt, sInt], sInt, MulI) total,

87 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))

91 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))

88− (eOp E.divide_) partial,

92+ (eOp E.divide_) ([sInt, sInt], sInt, DivI) partial,

89 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))

93 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))

90− (eOp E.eq_) total,

94+ (eOp E.eq_) ([sInt, sInt], sInt, EqI) total,

91 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))

95 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))

92− (eOp E.lt_) total,

96+ (eOp E.lt_) ([sInt, sInt], sInt, LtI) total,

93 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))

97 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))

94− (eOp E.lte_) total,

98+ (eOp E.lte_) ([sInt, sInt], sInt, LteI) total,

95 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))

99 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))

96− (eOp E.gt_) total,

100+ (eOp E.gt_) ([sInt, sInt], sInt, GtI) total,

97 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))

101 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))

98− (eOp E.gte_) total,

102+ (eOp E.gte_) ([sInt, sInt], sInt, GteI) total,

99 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

103 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

100− (eOp E.eq_) total,

104+ (eOp E.eq_) ([sChar, sChar], sInt, EqC) total,

101 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

105 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

102− (eOp E.lt_) total,

106+ (eOp E.lt_) ([sChar, sChar], sInt, LtC) total,

103 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))

107 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))

104− (eOp E.lte_) total,

108+ (eOp E.lte_) ([sChar, sChar], sInt, LteC) total,

105 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))

109 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))

106− (eOp E.gt_) total,

110+ (eOp E.gt_) ([sChar, sChar], sInt, GtC) total,

107 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

111 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

108− (eOp E.gte_) total,

112+ (eOp E.gte_) ([sChar, sChar], sInt, GteC) total,

109 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

113 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

110− (eOpFn tyBigInt tyBigInt "addBig") total,

114+ (eOpFn tyBigInt tyBigInt "addBig")

115+ ([sBigInt, sBigInt], sBigInt, AddBI) total,

111 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

116 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

112− (eOpFn tyBigInt tyBigInt "subBig") total,

117+ (eOpFn tyBigInt tyBigInt "subBig") ([sBigInt, sBigInt], sBigInt, SubBI) total,

113 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))

118 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))

114− (eOpFn tyBigInt tyBigInt "mulBig") total,

119+ (eOpFn tyBigInt tyBigInt "mulBig") ([sBigInt, sBigInt], sBigInt, MulBI) total,

115 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))

120 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))

116− (eOpFn tyBigInt tyBigInt "divBig") partial,

121+ (eOpFn tyBigInt tyBigInt "divBig") ([sBigInt, sBigInt], sBigInt,DivBI) partial,

117 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))

122 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))

118− (eOpFn tyBigInt tyInt "eqBig") total,

123+ (eOpFn tyBigInt tyInt "eqBig") ([sBigInt, sBigInt], sInt, EqBI) total,

119 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))

124 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))

120− (eOpFn tyBigInt tyInt "ltBig") total,

125+ (eOpFn tyBigInt tyInt "ltBig") ([sBigInt, sBigInt], sInt, LtBI) total,

121 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))

126 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))

122− (eOpFn tyBigInt tyInt "leBig") total,

127+ (eOpFn tyBigInt tyInt "leBig") ([sBigInt, sBigInt], sInt, LteBI) total,

123 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))

128 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))

124− (eOpFn tyBigInt tyInt "gtBig") total,

129+ (eOpFn tyBigInt tyInt "gtBig") ([sBigInt, sBigInt], sInt, GtBI) total,

125 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))

130 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))

126− (eOpFn tyBigInt tyInt "geBig") total,

131+ (eOpFn tyBigInt tyInt "geBig") ([sBigInt, sBigInt], sInt, GteBI) total,

127 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

132 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

128− (eOp E.plusF_) total,

133+ (eOp E.plusF_) ([sFloat, sFloat], sFloat, AddF) total,

129 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

134 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

130− (eOp E.minusF_) total,

135+ (eOp E.minusF_) ([sFloat, sFloat], sFloat, SubF) total,

131 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))

136 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))

132− (eOp E.timesF_) total,

137+ (eOp E.timesF_) ([sFloat, sFloat], sFloat, MulF) total,

133 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))

138 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))

134− (eOp E.divideF_) total,

139+ (eOp E.divideF_) ([sFloat, sFloat], sFloat, DivF) total,

135 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))

140 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))

136− (eOp E.eqF_) total,

141+ (eOp E.eqF_) ([sFloat, sFloat], sInt, EqF) total,

137 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))

142 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))

138− (eOp E.ltF_) total,

143+ (eOp E.ltF_) ([sFloat, sFloat], sInt, LtF) total,

139 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))

144 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))

140− (eOp E.lteF_) total,

145+ (eOp E.lteF_) ([sFloat, sFloat], sInt, LteF) total,

141 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))

146 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))

142− (eOp E.gtF_) total,

147+ (eOp E.gtF_) ([sFloat, sFloat], sInt, GtF) total,

143 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))

148 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))

144− (eOp E.gteF_) total,

149+ (eOp E.gteF_) ([sFloat, sFloat], sInt, GteF) total,

145 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

150 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

146− ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y") total,

151+ ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")

152+ ([sString, sString], sString, ConcatS) total,

147 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))

153 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))

148− ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")) total,

154+ ([E.name "x", E.name "y"], strEq (fun "x") (fun "y"))

155+ ([sString, sString], sInt, EqS) total,

149 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

156 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

150− ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")) total,

157+ ([E.name "x", E.name "y"], strLt (fun "x") (fun "y"))

158+ ([sString, sString], sInt, LtS) total,

151 -- Conversions

159 -- Conversions

152 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

160 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

153− ([E.name "x"], strToInt (fun "x")) total,

161+ ([E.name "x"], strToInt (fun "x")) ([sString], sInt, StoI) total,

154 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

162 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

155− ([E.name "x"], intToStr (fun "x")) total,

163+ ([E.name "x"], intToStr (fun "x")) ([sInt], sString, ItoS) total,

156 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

164 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

157− ([E.name "x"], charToInt (fun "x")) total,

165+ ([E.name "x"], charToInt (fun "x")) ([sChar], sInt, CtoI) total,

158 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

166 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

159− ([E.name "x"], intToChar (fun "x")) total,

167+ ([E.name "x"], intToChar (fun "x")) ([sInt], sChar, ItoC) total,

160 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

168 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

161− ([E.name "x"], intToBigInt (fun "x")) total,

169+ ([E.name "x"], intToBigInt (fun "x")) ([sInt], sBigInt, ItoBI) total,

162 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)

170 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)

163− ([E.name "x"], bigIntToInt (fun "x")) total,

171+ ([E.name "x"], bigIntToInt (fun "x")) ([sBigInt], sInt, BItoI) total,

164 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

172 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

165− ([E.name "x"], strToBigInt (fun "x")) total,

173+ ([E.name "x"], strToBigInt (fun "x")) ([sString], sBigInt, StoBI) total,

166 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

174 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

167− ([E.name "x"], bigIntToStr (fun "x")) total,

175+ ([E.name "x"], bigIntToStr (fun "x")) ([sBigInt], sString, BItoS) total,

168 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

176 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

169− ([E.name "x"], strToFloat (fun "x")) total,

177+ ([E.name "x"], strToFloat (fun "x")) ([sString], sFloat, StoF) total,

170 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

178 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

171− ([E.name "x"], floatToStr (fun "x")) total,

179+ ([E.name "x"], floatToStr (fun "x")) ([sFloat], sString, FtoS) total,

172 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)

180 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)

173− ([E.name "x"], intToFloat (fun "x")) total,

181+ ([E.name "x"], intToFloat (fun "x")) ([sInt], sFloat, ItoF) total,

174 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

182 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

175− ([E.name "x"], floatToInt (fun "x")) total,

183+ ([E.name "x"], floatToInt (fun "x")) ([sFloat], sInt, FtoI) total,

176

184

177 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

185 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

178− ([E.name "x"], floatExp (fun "x")) total,

186+ ([E.name "x"], floatExp (fun "x")) ([sFloat], sFloat, ExpF) total,

179 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

187 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

180− ([E.name "x"], floatLog (fun "x")) total,

188+ ([E.name "x"], floatLog (fun "x")) ([sFloat], sFloat, LogF) total,

181 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)

189 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)

182− ([E.name "x"], floatSin (fun "x")) total,

190+ ([E.name "x"], floatSin (fun "x")) ([sFloat], sFloat, SinF) total,

183 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)

191 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)

184− ([E.name "x"], floatCos (fun "x")) total,

192+ ([E.name "x"], floatCos (fun "x")) ([sFloat], sFloat, CosF) total,

185 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)

193 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)

186− ([E.name "x"], floatTan (fun "x")) total,

194+ ([E.name "x"], floatTan (fun "x")) ([sFloat], sFloat, TanF) total,

187 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)

195 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)

188− ([E.name "x"], floatASin (fun "x")) total,

196+ ([E.name "x"], floatASin (fun "x")) ([sFloat], sFloat, ASinF) total,

189 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)

197 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)

190− ([E.name "x"], floatACos (fun "x")) total,

198+ ([E.name "x"], floatACos (fun "x")) ([sFloat], sFloat, ACosF) total,

191 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)

199 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)

192− ([E.name "x"], floatATan (fun "x")) total,

200+ ([E.name "x"], floatATan (fun "x")) ([sFloat], sFloat, ATanF) total,

193 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)

201 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)

194− ([E.name "x"], floatSqrt (fun "x")) total,

202+ ([E.name "x"], floatSqrt (fun "x")) ([sFloat], sFloat, SqrtF) total,

195 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)

203 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)

196− ([E.name "x"], floatFloor (fun "x")) total,

204+ ([E.name "x"], floatFloor (fun "x")) ([sFloat], sFloat, FloorF) total,

197 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)

205 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)

198− ([E.name "x"], floatCeil (fun "x")) total,

206+ ([E.name "x"], floatCeil (fun "x")) ([sFloat], sFloat, CeilF) total,

199

207

200 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

208 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

201− ([E.name "x"], strHead (fun "x")) partial,

209+ ([E.name "x"], strHead (fun "x")) ([sString], sChar, HeadS) partial,

202 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

210 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

203− ([E.name "x"], strTail (fun "x")) partial,

211+ ([E.name "x"], strTail (fun "x")) ([sString], sString, TailS) partial,

204 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

212 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

205− ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")) total,

213+ ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs"))

214+ ([sChar, sString], sString, ConsS) total,

206 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

215 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

207− ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")) partial,

216+ ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i"))

217+ ([sString, sInt], sChar, IndexS) partial,

208 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

218 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

209− ([E.name "x"], strRev (fun "x")) total,

219+ ([E.name "x"], strRev (fun "x"))

220+ ([sString], sString, RevS) total,

210

221

211 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

222 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

212− ([E.name "a", E.name "b", E.name "x"], fun "x") total -- ahem

223+ ([E.name "a", E.name "b", E.name "x"], fun "x")

224+ ([Nothing], Nothing, BelieveMe) total -- ahem

213 ]

225 ]

214

226

215p_believeMe [_,_,x] = Just x

227p_believeMe [_,_,x] = Just x

@@ -311,11 +323,12 @@ p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

311p_strRev _ = Nothing

323p_strRev _ = Nothing

312

324

313elabPrim :: Prim -> Idris ()

325elabPrim :: Prim -> Idris ()

314−elabPrim (Prim n ty i def epic tot)

326+elabPrim (Prim n ty i def epic sc tot)

315 = do updateContext (addOperator n ty i def)

327 = do updateContext (addOperator n ty i def)

316 setTotality n tot

328 setTotality n tot

317 i <- getIState

329 i <- getIState

318− putIState i { idris_prims = (n, epic) : idris_prims i }

330+ putIState i { idris_prims = (n, epic) : idris_prims i,

331+ idris_scprims = (n, sc) : idris_scprims i }

319

332

320elabPrims :: Idris ()

333elabPrims :: Idris ()

321elabPrims = do mapM_ (elabDecl toplevel)

334elabPrims = do mapM_ (elabDecl toplevel)

src/Idris/REPL.hs+2−2

@@ -199,9 +199,9 @@ process fn (DebugInfo n)

199 let d = lookupDef Nothing n (tt_ctxt i)

200 when (not (null d)) $ liftIO $

201 do print (head d)

202− print (sclift (n, head d))

202+ print (toSC i (n, head d))

203 putStrLn (showSep "\n"

204− (map show (bcdefs (sclift (n, head d)))))

204+ (map show (bcdefs (toSC i (n, head d)))))

205process fn (Info n) = do i <- get

206 case lookupCtxt Nothing n (idris_classes i) of

207 [c] -> classInfo c

src/RTS/BCParser.hs+1−1

@@ -87,7 +87,7 @@ pInstruction =

87 bc <- many1 pInstruction

88 return (fromInteger t, bc))

90−pValue :: BParser Value

90+pValue :: BParser SValue

91pValue = try (do x <- integer; lchar 'L'; return (VBigInt x))

92 <|> try (do x <- integer; return (VInt (fromInteger x)))

93 <|> try (do x <- float; return (VFloat x))

src/RTS/Bytecode.hs+25−8

@@ -1,17 +1,21 @@

1module RTS.Bytecode where

3import Core.TT

4+import Core.CaseTree

5+import Core.Evaluate

7+import Idris.AbsSyntax

4import RTS.SC

8import RTS.SC

6−data Value = VInt Int

10+data SValue = VInt Int

7− | VFloat Double

11+ | VFloat Double

8− | VString String

12+ | VString String

9− | VChar Char

13+ | VChar Char

10− | VBigInt Integer

14+ | VBigInt Integer

11− | VRef Int

15+ | VRef Int

12 deriving Show

16 deriving Show

14−data BCOp = PUSH Value

18+data BCOp = PUSH SValue

15 | SLIDE Int -- Keep top stack value, discard n below it

19 | SLIDE Int -- Keep top stack value, discard n below it

16 | DISCARD Int

20 | DISCARD Int

17 | DISCARDINT Int

21 | DISCARDINT Int

@@ -23,11 +27,12 @@ data BCOp = PUSH Value

23 | CASE [(Int, Bytecode)] (Maybe Bytecode)

27 | CASE [(Int, Bytecode)] (Maybe Bytecode)

24 | INTCASE [(Int, Bytecode)] (Maybe Bytecode)

28 | INTCASE [(Int, Bytecode)] (Maybe Bytecode)

25 -- case looks at top stack item, discards immediately,

29 -- case looks at top stack item, discards immediately,

26− -- places constructor args on stack, last to first

30+ -- places constructor args on stack, last to first (first at ref 0)

27 | SPLIT -- get arguments from constructor form

31 | SPLIT -- get arguments from constructor form

28 | CALL Name Int -- name, number of arguments to take

32 | CALL Name Int -- name, number of arguments to take

29 | CALLVAR Int Int -- stack ref, number of arguments to take

33 | CALLVAR Int Int -- stack ref, number of arguments to take

30 | FOREIGNCALL String CType [CType] -- TT constants for types

34 | FOREIGNCALL String CType [CType] -- TT constants for types

35+ | PRIMOP SPrim [Int] -- apply to list of stack references

31 | ERROR String

36 | ERROR String

32 | DUMP

37 | DUMP

33 deriving Show

38 deriving Show

@@ -37,6 +42,14 @@ type Bytecode = [BCOp]

37data BCProg = BCProg [(Name, Bytecode)]

42data BCProg = BCProg [(Name, Bytecode)]

38 deriving Show

43 deriving Show

45+toSC :: IState -> (Name, Def) -> [(Name, SCDef)]

46+toSC i (n, d) = case lookup n (idris_scprims i) of

47+ Nothing -> sclift (n, d)

48+ Just (args, rt, op) ->

49+ let anames = zipWith mkA args [0..] in

50+ [(n, SCDef anames (SPrimOp op (map (SRef . fst) anames)))]

51+ where mkA t i = (MN i "primArg", t)

52+

40bcdefs :: [(Name, SCDef)] -> [(Name, Bytecode)]

53bcdefs :: [(Name, SCDef)] -> [(Name, Bytecode)]

41bcdefs = map (\ (n, s) -> (n, bc [] s))

54bcdefs = map (\ (n, s) -> (n, bc [] s))

@@ -111,3 +124,7 @@ instance BC SCExp where

111 addLocs [] l = l

124 addLocs [] l = l

112 addLocs (n : ns) locs = addLocs ns ((n, 0) : offset locs)

125 addLocs (n : ns) locs = addLocs ns ((n, 0) : offset locs)

113

126

127+ bc locs (SPrimOp p args)

128+ = bc' locs (reverse args)

129+ where bc' locs [] = [PRIMOP p [0..length args-1]]

130+ bc' locs (x : xs) = bc locs x ++ bc' (offset locs) xs

src/RTS/SC.hs+74−6

@@ -1,3 +1,5 @@

1+{-# LANGUAGE PatternGuards #-}

1module RTS.SC where

3module RTS.SC where

3import Core.TT

5import Core.TT

@@ -22,6 +24,27 @@ data SCExp = SRef Name

22 | SConst Const

24 | SConst Const

23 | SError String

25 | SError String

24 | SCase Name [SAlt]

26 | SCase Name [SAlt]

27+ | SPrimOp SPrim [SCExp]

28+ deriving Show

29+

30+data SPrim = AddI | SubI | MulI | DivI

31+ | EqI | LtI | LteI | GtI | GteI

32+ | EqC | LtC | LteC | GtC | GteC

33+ | AddBI | SubBI | MulBI | DivBI

35+ | AddF | SubF | MulF | DivF

36+ | EqF | LtF | LteF | GtF | GteF

37+ | ConcatS | EqS | LtS

38+ | StoI | ItoS

39+ | CtoI | ItoC

40+ | ItoBI | BItoI

41+ | StoBI | BItoS

42+ | StoF | FtoS

43+ | ItoF | FtoI

47+ | BelieveMe

25 deriving Show

48 deriving Show

27data SAlt = SConCase Tag [Name] SCExp

50data SAlt = SConCase Tag [Name] SCExp

@@ -29,6 +52,14 @@ data SAlt = SConCase Tag [Name] SCExp

29 | SDefaultCase SCExp

52 | SDefaultCase SCExp

30 deriving Show

53 deriving Show

55+sInt, sFloat, sChar, sString, sPtr, sBigInt :: CType

56+sInt = Just IType

57+sFloat = Just FlType

58+sChar = Just ChType

59+sString = Just StrType

60+sPtr = Just PtrType

61+sBigInt = Just BIType

62+

32type SCState = ([(Name, SCDef)], Name)

63type SCState = ([(Name, SCDef)], Name)

34sclift :: (Name, Def) -> [(Name, SCDef)]

65sclift :: (Name, Def) -> [(Name, SCDef)]

@@ -71,12 +102,15 @@ instance Lift (TT Name) SCExp where

71 sc env (V i) = return $ SRef (env!!i)

102 sc env (V i) = return $ SRef (env!!i)

72 sc env fn@(App _ _)

103 sc env fn@(App _ _)

73 = do let (f, args) = unApply fn

104 = do let (f, args) = unApply fn

105+ prim <- sPrim env f args

106+ case prim of

107+ Just t -> return t

74− args' <- mapM (sc env) args

108+ Nothing -> do args' <- mapM (sc env) args

75− case f of

109+ case f of

76− (P (DCon t a) _ _) -> return $ SCon t args'

110+ (P (DCon t a) _ _) -> return $ SCon t args'

77− (P (TCon t a) _ _) -> return $ SCon t args'

111+ (P (TCon t a) _ _) -> return $ SCon t args'

78− _ -> do f' <- sc env f

112+ _ -> do f' <- sc env f

79− return $ SApp f' args'

113+ return $ SApp f' args'

80 sc env (Constant c) = return $ SConst c

114 sc env (Constant c) = return $ SConst c

81 sc env (Bind n (Let _ v) e) = do v' <- sc env v

115 sc env (Bind n (Let _ v) e) = do v' <- sc env v

82 e' <- sc (n : env) e

116 e' <- sc (n : env) e

@@ -106,3 +140,37 @@ instance Lift CaseAlt SAlt where

106 sc env (DefaultCase e) = do e' <- sc env e

140 sc env (DefaultCase e) = do e' <- sc env e

107 return (SDefaultCase e')

141 return (SDefaultCase e')

108

142

143+-- Deal with primitives: mkForeign, -- lazy, prim__IO, io_bind, malloc, trace_malloc

144+

145+sPrim :: [Name] -> TT Name -> [TT Name] -> State SCState (Maybe SCExp)

146+sPrim env (P _ (UN "mkForeign") _) args = do x <- doForeign env args

147+ return (Just x)

148+sPrim env f args = return Nothing

149+

150+doForeign env (_ : fgn : args)

151+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

152+ = let tys = getFTypes fgnArgTys

153+ rty = mkEty' ret in

154+ do args' <- mapM (sc env) args

155+ -- wrap it in a prim__IO

156+ -- return $ con_ 0 @@ impossible @@

157+ return $ SFCall fgnName rty (zip args' tys)

158+ | otherwise = fail "Badly formed foreign function call"

159+

160+getFTypes :: TT Name -> [CType]

161+getFTypes tm = case unApply tm of

162+ (nil, []) -> []

163+ (cons, [ty, xs]) ->

164+ let rest = getFTypes xs in

165+ mkEty' ty : rest

166+

167+mkEty' (P _ (UN ty) _) = mkEty ty

168+mkEty' _ = Nothing

169+

170+mkEty "FInt" = Just IType

171+mkEty "FFloat" = Just FlType

172+mkEty "FChar" = Just ChType

173+mkEty "FString" = Just StrType

174+mkEty "FPtr" = Just PtrType

175+mkEty "FUnit" = Just VoidType

176+