0 | module Core.Primitives

  2 | import Core.TT

  3 | import Core.Value

  4 | import Libraries.Utils.String

  6 | import Data.Vect

  8 | %default covering

 10 | public export

 11 | record Prim where

 12 |   constructor MkPrim

 13 |   {arity : Nat}

 14 |   fn : PrimFn arity

 15 |   type : ClosedTerm

 16 |   totality : Totality

 18 | binOp : (Constant -> Constant -> Maybe Constant) ->

 19 |         Vect 2 (NF vars) -> Maybe (NF vars)

 20 | binOp fn [NPrimVal fc x, NPrimVal _ y]

 21 |     = map (NPrimVal fc) (fn x y)

 22 | binOp _ _ = Nothing

 24 | unaryOp : (Constant -> Maybe Constant) ->

 25 |           Vect 1 (NF vars) -> Maybe (NF vars)

 26 | unaryOp fn [NPrimVal fc x]

 27 |     = map (NPrimVal fc) (fn x)

 28 | unaryOp _ _ = Nothing

 30 | castString : Vect 1 (NF vars) -> Maybe (NF vars)

 31 | castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))

 32 | castString [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Str (show i)))

 33 | castString [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Str (show i)))

 34 | castString [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Str (show i)))

 35 | castString [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Str (show i)))

 36 | castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))

 37 | castString [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Str (show i)))

 38 | castString [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Str (show i)))

 39 | castString [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Str (show i)))

 40 | castString [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Str (show i)))

 41 | castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))

 42 | castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))

 43 | castString _ = Nothing

 45 | castInteger : Vect 1 (NF vars) -> Maybe (NF vars)

 46 | castInteger [NPrimVal fc (I i)] = Just (NPrimVal fc (BI (cast i)))

 47 | castInteger [NPrimVal fc (I8 i)] = Just (NPrimVal fc (BI (cast i)))

 48 | castInteger [NPrimVal fc (I16 i)] = Just (NPrimVal fc (BI (cast i)))

 49 | castInteger [NPrimVal fc (I32 i)] = Just (NPrimVal fc (BI (cast i)))

 50 | castInteger [NPrimVal fc (I64 i)] = Just (NPrimVal fc (BI (cast i)))

 51 | castInteger [NPrimVal fc (B8 i)] = Just (NPrimVal fc (BI (cast i)))

 52 | castInteger [NPrimVal fc (B16 i)] = Just (NPrimVal fc (BI (cast i)))

 53 | castInteger [NPrimVal fc (B32 i)] = Just (NPrimVal fc (BI (cast i)))

 54 | castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI (cast i)))

 55 | castInteger [NPrimVal fc (Ch i)] = Just (NPrimVal fc (BI (cast (cast {to=Int} i))))

 56 | castInteger [NPrimVal fc (Db i)] = Just (NPrimVal fc (BI (cast i)))

 57 | castInteger [NPrimVal fc (Str i)] = Just (NPrimVal fc (BI (cast i)))

 58 | castInteger _ = Nothing

 60 | castInt : Vect 1 (NF vars) -> Maybe (NF vars)

 61 | castInt [NPrimVal fc (I8 i)] = Just (NPrimVal fc (I (cast i)))

 62 | castInt [NPrimVal fc (I16 i)] = Just (NPrimVal fc (I (cast i)))

 63 | castInt [NPrimVal fc (I32 i)] = Just (NPrimVal fc (I (cast i)))

 64 | castInt [NPrimVal fc (I64 i)] = Just (NPrimVal fc (I (cast i)))

 65 | castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (cast i)))

 66 | castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I (cast i)))

 67 | castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I (cast i)))

 68 | castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I (cast i)))

 69 | castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (cast i)))

 70 | castInt [NPrimVal fc (Db i)] = Just (NPrimVal fc (I (cast i)))

 71 | castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))

 72 | castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))

 73 | castInt _ = Nothing

 75 | constantIntegerValue : Constant -> Maybe Integer

 76 | constantIntegerValue (I i)   = Just $ cast i

 77 | constantIntegerValue (I8 i)   = Just $ cast i

 78 | constantIntegerValue (I16 i)   = Just $ cast i

 79 | constantIntegerValue (I32 i)   = Just $ cast i

 80 | constantIntegerValue (I64 i)   = Just $ cast i

 81 | constantIntegerValue (BI i)  = Just i

 82 | constantIntegerValue (B8 i)  = Just $ cast i

 83 | constantIntegerValue (B16 i) = Just $ cast i

 84 | constantIntegerValue (B32 i) = Just $ cast i

 85 | constantIntegerValue (B64 i) = Just $ cast i

 86 | constantIntegerValue _       = Nothing

 88 | castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)

 89 | castBits8 [NPrimVal fc constant] =

 90 |     NPrimVal fc . B8 . cast <$> constantIntegerValue constant

 91 | castBits8 _ = Nothing

 93 | castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)

 94 | castBits16 [NPrimVal fc constant] =

 95 |     NPrimVal fc . B16 . cast <$> constantIntegerValue constant

 96 | castBits16 _ = Nothing

 98 | castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)

 99 | castBits32 [NPrimVal fc constant] =

100 |     NPrimVal fc . B32 . cast <$> constantIntegerValue constant

101 | castBits32 _ = Nothing

103 | castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)

104 | castBits64 [NPrimVal fc constant] =

105 |     NPrimVal fc . B64 . cast <$> constantIntegerValue constant

106 | castBits64 _ = Nothing

108 | castInt8 : Vect 1 (NF vars) -> Maybe (NF vars)

109 | castInt8 [NPrimVal fc constant] =

110 |     NPrimVal fc . I8 . cast <$> constantIntegerValue constant

111 | castInt8 _ = Nothing

113 | castInt16 : Vect 1 (NF vars) -> Maybe (NF vars)

114 | castInt16 [NPrimVal fc constant] =

115 |     NPrimVal fc . I16 . cast <$> constantIntegerValue constant

116 | castInt16 _ = Nothing

118 | castInt32 : Vect 1 (NF vars) -> Maybe (NF vars)

119 | castInt32 [NPrimVal fc constant] =

120 |     NPrimVal fc . I32 . cast <$> constantIntegerValue constant

121 | castInt32 _ = Nothing

123 | castInt64 : Vect 1 (NF vars) -> Maybe (NF vars)

124 | castInt64 [NPrimVal fc constant] =

125 |     NPrimVal fc . I64 . cast <$> constantIntegerValue constant

126 | castInt64 _ = Nothing

128 | castDouble : Vect 1 (NF vars) -> Maybe (NF vars)

129 | castDouble [NPrimVal fc (I i)] = Just (NPrimVal fc (Db (cast i)))

130 | castDouble [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Db (cast i)))

131 | castDouble [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Db (cast i)))

132 | castDouble [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Db (cast i)))

133 | castDouble [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Db (cast i)))

134 | castDouble [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Db (cast i)))

135 | castDouble [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Db (cast i)))

136 | castDouble [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Db (cast i)))

137 | castDouble [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Db (cast i)))

138 | castDouble [NPrimVal fc (BI i)] = Just (NPrimVal fc (Db (cast i)))

139 | castDouble [NPrimVal fc (Str i)] = Just (NPrimVal fc (Db (cast i)))

140 | castDouble _ = Nothing

142 | castChar : Vect 1 (NF vars) -> Maybe (NF vars)

143 | castChar [NPrimVal fc (I i)] = Just (NPrimVal fc (Ch (cast i)))

144 | castChar [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Ch (cast i)))

145 | castChar [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Ch (cast i)))

146 | castChar [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Ch (cast i)))

147 | castChar [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Ch (cast i)))

148 | castChar [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Ch (cast i)))

149 | castChar [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Ch (cast i)))

150 | castChar [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Ch (cast i)))

151 | castChar [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Ch (cast i)))

152 | castChar [NPrimVal fc (BI i)] = Just (NPrimVal fc (Ch (cast i)))

153 | castChar _ = Nothing

155 | strLength : Vect 1 (NF vars) -> Maybe (NF vars)

156 | strLength [NPrimVal fc (Str s)] = Just (NPrimVal fc (I (cast (length s))))

157 | strLength _ = Nothing

159 | strHead : Vect 1 (NF vars) -> Maybe (NF vars)

160 | strHead [NPrimVal fc (Str "")] = Nothing

161 | strHead [NPrimVal fc (Str str)]

162 |     = Just (NPrimVal fc (Ch (assert_total (prim__strHead str))))

163 | strHead _ = Nothing

165 | strTail : Vect 1 (NF vars) -> Maybe (NF vars)

166 | strTail [NPrimVal fc (Str "")] = Nothing

167 | strTail [NPrimVal fc (Str str)]

168 |     = Just (NPrimVal fc (Str (assert_total (prim__strTail str))))

169 | strTail _ = Nothing

171 | strIndex : Vect 2 (NF vars) -> Maybe (NF vars)

172 | strIndex [NPrimVal fc (Str str), NPrimVal _ (I i)]

173 |     = if i >= 0 && integerToNat (cast i) < length str

174 |          then Just (NPrimVal fc (Ch (assert_total (prim__strIndex str i))))

175 |          else Nothing

176 | strIndex _ = Nothing

178 | strCons : Vect 2 (NF vars) -> Maybe (NF vars)

179 | strCons [NPrimVal fc (Ch x), NPrimVal _ (Str y)]

180 |     = Just (NPrimVal fc (Str (strCons x y)))

181 | strCons _ = Nothing

183 | strAppend : Vect 2 (NF vars) -> Maybe (NF vars)

184 | strAppend [NPrimVal fc (Str x), NPrimVal _ (Str y)]

185 |     = Just (NPrimVal fc (Str (x ++ y)))

186 | strAppend _ = Nothing

188 | strReverse : Vect 1 (NF vars) -> Maybe (NF vars)

189 | strReverse [NPrimVal fc (Str x)]

190 |     = Just (NPrimVal fc (Str (reverse x)))

191 | strReverse _ = Nothing

193 | strSubstr : Vect 3 (NF vars) -> Maybe (NF vars)

194 | strSubstr [NPrimVal fc (I start), NPrimVal _ (I len), NPrimVal _ (Str str)]

195 |     = Just (NPrimVal fc (Str (prim__strSubstr start len str)))

196 | strSubstr _ = Nothing

199 | add : Constant -> Constant -> Maybe Constant

200 | add (BI x) (BI y) = pure $ BI (x + y)

201 | add (I x) (I y) = pure $ I (x + y)

202 | add (I8 x) (I8 y) = pure $ I8 (x + y)

203 | add (I16 x) (I16 y) = pure $ I16 (x + y)

204 | add (I32 x) (I32 y) = pure $ I32 (x + y)

205 | add (I64 x) (I64 y) = pure $ I64 (x + y)

206 | add (B8 x) (B8 y) = pure $ B8 (x + y)

207 | add (B16 x) (B16 y) = pure $ B16 (x + y)

208 | add (B32 x) (B32 y) = pure $ B32 (x + y)

209 | add (B64 x) (B64 y) = pure $ B64 (x + y)

210 | add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))

211 | add (Db x) (Db y) = pure $ Db (x + y)

212 | add _ _ = Nothing

214 | sub : Constant -> Constant -> Maybe Constant

215 | sub (BI x) (BI y) = pure $ BI (x - y)

216 | sub (I x) (I y) = pure $ I (x - y)

217 | sub (I8 x) (I8 y) = pure $ I8 (x - y)

218 | sub (I16 x) (I16 y) = pure $ I16 (x - y)

219 | sub (I32 x) (I32 y) = pure $ I32 (x - y)

220 | sub (I64 x) (I64 y) = pure $ I64 (x - y)

221 | sub (B8 x) (B8 y) = pure $ B8 (x - y)

222 | sub (B16 x) (B16 y) = pure $ B16 (x - y)

223 | sub (B32 x) (B32 y) = pure $ B32 (x - y)

224 | sub (B64 x) (B64 y) = pure $ B64 (x - y)

225 | sub (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x - cast y))

226 | sub (Db x) (Db y) = pure $ Db (x - y)

227 | sub _ _ = Nothing

229 | mul : Constant -> Constant -> Maybe Constant

230 | mul (BI x) (BI y) = pure $ BI (x * y)

231 | mul (B8 x) (B8 y) = pure $ B8 (x * y)

232 | mul (B16 x) (B16 y) = pure $ B16 (x * y)

233 | mul (B32 x) (B32 y) = pure $ B32 (x * y)

234 | mul (B64 x) (B64 y) = pure $ B64 (x * y)

235 | mul (I x) (I y) = pure $ I (x * y)

236 | mul (I8 x) (I8 y) = pure $ I8 (x * y)

237 | mul (I16 x) (I16 y) = pure $ I16 (x * y)

238 | mul (I32 x) (I32 y) = pure $ I32 (x * y)

239 | mul (I64 x) (I64 y) = pure $ I64 (x * y)

240 | mul (Db x) (Db y) = pure $ Db (x * y)

241 | mul _ _ = Nothing

243 | div : Constant -> Constant -> Maybe Constant

244 | div (BI x) (BI 0) = Nothing

245 | div (BI x) (BI y) = pure $ BI (assert_total (x `div` y))

246 | div (I x) (I 0) = Nothing

247 | div (I x) (I y) = pure $ I (assert_total (x `div` y))

248 | div (I8 x) (I8 0) = Nothing

249 | div (I8 x) (I8 y) = pure $ I8 (assert_total (x `div` y))

250 | div (I16 x) (I16 0) = Nothing

251 | div (I16 x) (I16 y) = pure $ I16 (assert_total (x `div` y))

252 | div (I32 x) (I32 0) = Nothing

253 | div (I32 x) (I32 y) = pure $ I32 (assert_total (x `div` y))

254 | div (I64 x) (I64 0) = Nothing

255 | div (I64 x) (I64 y) = pure $ I64 (assert_total (x `div` y))

256 | div (B8 x) (B8 0) = Nothing

257 | div (B8 x) (B8 y) = pure $ B8 (assert_total (x `div` y))

258 | div (B16 x) (B16 0) = Nothing

259 | div (B16 x) (B16 y) = pure $ B16 (assert_total (x `div` y))

260 | div (B32 x) (B32 0) = Nothing

261 | div (B32 x) (B32 y) = pure $ B32 (assert_total (x `div` y))

262 | div (B64 x) (B64 0) = Nothing

263 | div (B64 x) (B64 y) = pure $ B64 (assert_total (x `div` y))

264 | div (Db x) (Db y) = pure $ Db (x / y)

265 | div _ _ = Nothing

267 | mod : Constant -> Constant -> Maybe Constant

268 | mod (BI x) (BI 0) = Nothing

269 | mod (BI x) (BI y) = pure $ BI (assert_total (x `mod` y))

270 | mod (I x) (I 0) = Nothing

271 | mod (I x) (I y) = pure $ I (assert_total (x `mod` y))

272 | mod (I8 x) (I8 0) = Nothing

273 | mod (I8 x) (I8 y) = pure $ I8 (assert_total (x `mod` y))

274 | mod (I16 x) (I16 0) = Nothing

275 | mod (I16 x) (I16 y) = pure $ I16 (assert_total (x `mod` y))

276 | mod (I32 x) (I32 0) = Nothing

277 | mod (I32 x) (I32 y) = pure $ I32 (assert_total (x `mod` y))

278 | mod (I64 x) (I64 0) = Nothing

279 | mod (I64 x) (I64 y) = pure $ I64 (assert_total (x `mod` y))

280 | mod (B8 x) (B8 0) = Nothing

281 | mod (B8 x) (B8 y) = pure $ B8 (assert_total (x `mod` y))

282 | mod (B16 x) (B16 0) = Nothing

283 | mod (B16 x) (B16 y) = pure $ B16 (assert_total (x `mod` y))

284 | mod (B32 x) (B32 0) = Nothing

285 | mod (B32 x) (B32 y) = pure $ B32 (assert_total (x `mod` y))

286 | mod (B64 x) (B64 0) = Nothing

287 | mod (B64 x) (B64 y) = pure $ B64 (assert_total (x `mod` y))

288 | mod _ _ = Nothing

290 | shiftl : Constant -> Constant -> Maybe Constant

291 | shiftl (I x) (I y) = pure $ I (prim__shl_Int x y)

292 | shiftl (I8 x) (I8 y) = pure $ I8 (prim__shl_Int8 x y)

293 | shiftl (I16 x) (I16 y) = pure $ I16 (prim__shl_Int16 x y)

294 | shiftl (I32 x) (I32 y) = pure $ I32 (prim__shl_Int32 x y)

295 | shiftl (I64 x) (I64 y) = pure $ I64 (prim__shl_Int64 x y)

296 | shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)

297 | shiftl (B8 x) (B8 y) = pure $ B8 (prim__shl_Bits8 x y)

298 | shiftl (B16 x) (B16 y) = pure $ B16 (prim__shl_Bits16 x y)

299 | shiftl (B32 x) (B32 y) = pure $ B32 (prim__shl_Bits32 x y)

300 | shiftl (B64 x) (B64 y) = pure $ B64 (prim__shl_Bits64 x y)

301 | shiftl _ _ = Nothing

303 | shiftr : Constant -> Constant -> Maybe Constant

304 | shiftr (I x) (I y) = pure $ I (prim__shr_Int x y)

305 | shiftr (I8 x) (I8 y) = pure $ I8 (prim__shr_Int8 x y)

306 | shiftr (I16 x) (I16 y) = pure $ I16 (prim__shr_Int16 x y)

307 | shiftr (I32 x) (I32 y) = pure $ I32 (prim__shr_Int32 x y)

308 | shiftr (I64 x) (I64 y) = pure $ I64 (prim__shr_Int64 x y)

309 | shiftr (BI x) (BI y) = pure $ BI (prim__shr_Integer x y)

310 | shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Bits8 x y)

311 | shiftr (B16 x) (B16 y) = pure $ B16 (prim__shr_Bits16 x y)

312 | shiftr (B32 x) (B32 y) = pure $ B32 (prim__shr_Bits32 x y)

313 | shiftr (B64 x) (B64 y) = pure $ B64 (prim__shr_Bits64 x y)

314 | shiftr _ _ = Nothing

316 | band : Constant -> Constant -> Maybe Constant

317 | band (I x) (I y) = pure $ I (prim__and_Int x y)

318 | band (I8 x) (I8 y) = pure $ I8 (prim__and_Int8 x y)

319 | band (I16 x) (I16 y) = pure $ I16 (prim__and_Int16 x y)

320 | band (I32 x) (I32 y) = pure $ I32 (prim__and_Int32 x y)

321 | band (I64 x) (I64 y) = pure $ I64 (prim__and_Int64 x y)

322 | band (BI x) (BI y) = pure $ BI (prim__and_Integer x y)

323 | band (B8 x) (B8 y) = pure $ B8 (prim__and_Bits8 x y)

324 | band (B16 x) (B16 y) = pure $ B16 (prim__and_Bits16 x y)

325 | band (B32 x) (B32 y) = pure $ B32 (prim__and_Bits32 x y)

326 | band (B64 x) (B64 y) = pure $ B64 (prim__and_Bits64 x y)

327 | band _ _ = Nothing

329 | bor : Constant -> Constant -> Maybe Constant

330 | bor (I x) (I y) = pure $ I (prim__or_Int x y)

331 | bor (I8 x) (I8 y) = pure $ I8 (prim__or_Int8 x y)

332 | bor (I16 x) (I16 y) = pure $ I16 (prim__or_Int16 x y)

333 | bor (I32 x) (I32 y) = pure $ I32 (prim__or_Int32 x y)

334 | bor (I64 x) (I64 y) = pure $ I64 (prim__or_Int64 x y)

335 | bor (BI x) (BI y) = pure $ BI (prim__or_Integer x y)

336 | bor (B8 x) (B8 y) = pure $ B8 (prim__or_Bits8 x y)

337 | bor (B16 x) (B16 y) = pure $ B16 (prim__or_Bits16 x y)

338 | bor (B32 x) (B32 y) = pure $ B32 (prim__or_Bits32 x y)

339 | bor (B64 x) (B64 y) = pure $ B64 (prim__or_Bits64 x y)

340 | bor _ _ = Nothing

342 | bxor : Constant -> Constant -> Maybe Constant

343 | bxor (I x) (I y) = pure $ I (prim__xor_Int x y)

344 | bxor (B8 x) (B8 y) = pure $ B8 (prim__xor_Bits8 x y)

345 | bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Bits16 x y)

346 | bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Bits32 x y)

347 | bxor (B64 x) (B64 y) = pure $ B64 (prim__xor_Bits64 x y)

348 | bxor (I8 x) (I8 y) = pure $ I8 (prim__xor_Int8 x y)

349 | bxor (I16 x) (I16 y) = pure $ I16 (prim__xor_Int16 x y)

350 | bxor (I32 x) (I32 y) = pure $ I32 (prim__xor_Int32 x y)

351 | bxor (I64 x) (I64 y) = pure $ I64 (prim__xor_Int64 x y)

352 | bxor (BI x) (BI y) = pure $ BI (prim__xor_Integer x y)

353 | bxor _ _ = Nothing

355 | neg : Constant -> Maybe Constant

356 | neg (BI x) = pure $ BI (-x)

357 | neg (I x) = pure $ I (-x)

358 | neg (I8 x) = pure $ I8 (-x)

359 | neg (I16 x) = pure $ I16 (-x)

360 | neg (I32 x) = pure $ I32 (-x)

361 | neg (I64 x) = pure $ I64 (-x)

362 | neg (B8 x) = pure $ B8 (-x)

363 | neg (B16 x) = pure $ B16 (-x)

364 | neg (B32 x) = pure $ B32 (-x)

365 | neg (B64 x) = pure $ B64 (-x)

366 | neg (Db x) = pure $ Db (-x)

367 | neg _ = Nothing

369 | toInt : Bool -> Constant

370 | toInt True = I 1

371 | toInt False = I 0

373 | lt : Constant -> Constant -> Maybe Constant

374 | lt (I x) (I y) = pure $ toInt (x < y)

375 | lt (I8 x) (I8 y) = pure $ toInt (x < y)

376 | lt (I16 x) (I16 y) = pure $ toInt (x < y)

377 | lt (I32 x) (I32 y) = pure $ toInt (x < y)

378 | lt (I64 x) (I64 y) = pure $ toInt (x < y)

379 | lt (BI x) (BI y) = pure $ toInt (x < y)

380 | lt (B8 x) (B8 y) = pure $ toInt (x < y)

381 | lt (B16 x) (B16 y) = pure $ toInt (x < y)

382 | lt (B32 x) (B32 y) = pure $ toInt (x < y)

383 | lt (B64 x) (B64 y) = pure $ toInt (x < y)

384 | lt (Str x) (Str y) = pure $ toInt (x < y)

385 | lt (Ch x) (Ch y) = pure $ toInt (x < y)

386 | lt (Db x) (Db y) = pure $ toInt (x < y)

387 | lt _ _ = Nothing

389 | lte : Constant -> Constant -> Maybe Constant

390 | lte (I x) (I y) = pure $ toInt (x <= y)

391 | lte (I8 x) (I8 y) = pure $ toInt (x <= y)

392 | lte (I16 x) (I16 y) = pure $ toInt (x <= y)

393 | lte (I32 x) (I32 y) = pure $ toInt (x <= y)

394 | lte (I64 x) (I64 y) = pure $ toInt (x <= y)

395 | lte (BI x) (BI y) = pure $ toInt (x <= y)

396 | lte (B8 x) (B8 y) = pure $ toInt (x <= y)

397 | lte (B16 x) (B16 y) = pure $ toInt (x <= y)

398 | lte (B32 x) (B32 y) = pure $ toInt (x <= y)

399 | lte (B64 x) (B64 y) = pure $ toInt (x <= y)

400 | lte (Str x) (Str y) = pure $ toInt (x <= y)

401 | lte (Ch x) (Ch y) = pure $ toInt (x <= y)

402 | lte (Db x) (Db y) = pure $ toInt (x <= y)

403 | lte _ _ = Nothing

405 | eq : Constant -> Constant -> Maybe Constant

406 | eq (I x) (I y) = pure $ toInt (x == y)

407 | eq (I8 x) (I8 y) = pure $ toInt (x == y)

408 | eq (I16 x) (I16 y) = pure $ toInt (x == y)

409 | eq (I32 x) (I32 y) = pure $ toInt (x == y)

410 | eq (I64 x) (I64 y) = pure $ toInt (x == y)

411 | eq (BI x) (BI y) = pure $ toInt (x == y)

412 | eq (B8 x) (B8 y) = pure $ toInt (x == y)

413 | eq (B16 x) (B16 y) = pure $ toInt (x == y)

414 | eq (B32 x) (B32 y) = pure $ toInt (x == y)

415 | eq (B64 x) (B64 y) = pure $ toInt (x == y)

416 | eq (Str x) (Str y) = pure $ toInt (x == y)

417 | eq (Ch x) (Ch y) = pure $ toInt (x == y)

418 | eq (Db x) (Db y) = pure $ toInt (x == y)

419 | eq _ _ = Nothing

421 | gte : Constant -> Constant -> Maybe Constant

422 | gte (I x) (I y) = pure $ toInt (x >= y)

423 | gte (I8 x) (I8 y) = pure $ toInt (x >= y)

424 | gte (I16 x) (I16 y) = pure $ toInt (x >= y)

425 | gte (I32 x) (I32 y) = pure $ toInt (x >= y)

426 | gte (I64 x) (I64 y) = pure $ toInt (x >= y)

427 | gte (BI x) (BI y) = pure $ toInt (x >= y)

428 | gte (B8 x) (B8 y) = pure $ toInt (x >= y)

429 | gte (B16 x) (B16 y) = pure $ toInt (x >= y)

430 | gte (B32 x) (B32 y) = pure $ toInt (x >= y)

431 | gte (B64 x) (B64 y) = pure $ toInt (x >= y)

432 | gte (Str x) (Str y) = pure $ toInt (x >= y)

433 | gte (Ch x) (Ch y) = pure $ toInt (x >= y)

434 | gte (Db x) (Db y) = pure $ toInt (x >= y)

435 | gte _ _ = Nothing

437 | gt : Constant -> Constant -> Maybe Constant

438 | gt (I x) (I y) = pure $ toInt (x > y)

439 | gt (I8 x) (I8 y) = pure $ toInt (x > y)

440 | gt (I16 x) (I16 y) = pure $ toInt (x > y)

441 | gt (I32 x) (I32 y) = pure $ toInt (x > y)

442 | gt (I64 x) (I64 y) = pure $ toInt (x > y)

443 | gt (BI x) (BI y) = pure $ toInt (x > y)

444 | gt (B8 x) (B8 y) = pure $ toInt (x > y)

445 | gt (B16 x) (B16 y) = pure $ toInt (x > y)

446 | gt (B32 x) (B32 y) = pure $ toInt (x > y)

447 | gt (B64 x) (B64 y) = pure $ toInt (x > y)

448 | gt (Str x) (Str y) = pure $ toInt (x > y)

449 | gt (Ch x) (Ch y) = pure $ toInt (x > y)

450 | gt (Db x) (Db y) = pure $ toInt (x > y)

451 | gt _ _ = Nothing

453 | doubleOp : (Double -> Double) -> Vect 1 (NF vars) -> Maybe (NF vars)

454 | doubleOp f [NPrimVal fc (Db x)] = Just (NPrimVal fc (Db (f x)))

455 | doubleOp f _ = Nothing

457 | doubleExp : Vect 1 (NF vars) -> Maybe (NF vars)

458 | doubleExp = doubleOp exp

460 | doubleLog : Vect 1 (NF vars) -> Maybe (NF vars)

461 | doubleLog = doubleOp log

463 | doublePow : {vars : _ } -> Vect 2 (NF vars) -> Maybe (NF vars)

464 | doublePow = binOp pow'

465 |     where pow' : Constant -> Constant -> Maybe Constant

466 |           pow' (Db x) (Db y) = pure $ Db (pow x y)

467 |           pow' _ _ = Nothing

469 | doubleSin : Vect 1 (NF vars) -> Maybe (NF vars)

470 | doubleSin = doubleOp sin

472 | doubleCos : Vect 1 (NF vars) -> Maybe (NF vars)

473 | doubleCos = doubleOp cos

475 | doubleTan : Vect 1 (NF vars) -> Maybe (NF vars)

476 | doubleTan = doubleOp tan

478 | doubleASin : Vect 1 (NF vars) -> Maybe (NF vars)

479 | doubleASin = doubleOp asin

481 | doubleACos : Vect 1 (NF vars) -> Maybe (NF vars)

482 | doubleACos = doubleOp acos

484 | doubleATan : Vect 1 (NF vars) -> Maybe (NF vars)

485 | doubleATan = doubleOp atan

487 | doubleSqrt : Vect 1 (NF vars) -> Maybe (NF vars)

488 | doubleSqrt = doubleOp sqrt

490 | doubleFloor : Vect 1 (NF vars) -> Maybe (NF vars)

491 | doubleFloor = doubleOp floor

493 | doubleCeiling : Vect 1 (NF vars) -> Maybe (NF vars)

494 | doubleCeiling = doubleOp ceiling

497 | believeMe : Vect 3 (NF vars) -> Maybe (NF vars)

498 | believeMe [_, _, val@(NDCon {})] = Just val

499 | believeMe [_, _, val@(NTCon {})] = Just val

500 | believeMe [_, _, val@(NPrimVal {})] = Just val

501 | believeMe [_, _, NType fc u] = Just (NType fc u)

502 | believeMe [_, _, val] = Nothing

504 | primTyVal : PrimType -> ClosedTerm

505 | primTyVal = PrimVal emptyFC . PrT

507 | constTy : PrimType -> PrimType -> PrimType -> ClosedTerm

508 | constTy a b c

509 |     = let arr = fnType emptyFC in

510 |     primTyVal a `arr` (primTyVal b `arr` primTyVal c)

512 | constTy3 : PrimType -> PrimType -> PrimType -> PrimType -> ClosedTerm

513 | constTy3 a b c d

514 |     = let arr = fnType emptyFC in

515 |     primTyVal a `arr`

516 |          (primTyVal b `arr`

517 |              (primTyVal c `arr` primTyVal d))

519 | predTy : PrimType -> PrimType -> ClosedTerm

520 | predTy a b = let arr = fnType emptyFC in

521 |              primTyVal a `arr` primTyVal b

523 | arithTy : PrimType -> ClosedTerm

524 | arithTy t = constTy t t t

526 | cmpTy : PrimType -> ClosedTerm

527 | cmpTy t = constTy t t IntType

529 | doubleTy : ClosedTerm

530 | doubleTy = predTy DoubleType DoubleType

532 | pi : (x : String) -> RigCount -> PiInfo (Term xs) -> Term xs ->

533 |      Term (UN (Basic x) :: xs) -> Term xs

534 | pi x rig plic ty sc = Bind emptyFC (UN (Basic x)) (Pi emptyFC rig plic ty) sc

536 | believeMeTy : ClosedTerm

538 |     = pi "a" erased Explicit (TType emptyFC (MN "top" 0)) $

539 |       pi "b" erased Explicit (TType emptyFC (MN "top" 0)) $

540 |       pi "x" linear Explicit (Local emptyFC Nothing _ (Later First)) $

541 |       Local emptyFC Nothing _ (Later First)

543 | crashTy : ClosedTerm

545 |     = pi "a" erased Explicit (TType emptyFC (MN "top" 0)) $

546 |       pi "msg" top Explicit (PrimVal emptyFC $ PrT StringType) $

547 |       Local emptyFC Nothing _ (Later First)

549 | castTo : PrimType -> Vect 1 (NF vars) -> Maybe (NF vars)

550 | castTo IntType = castInt

551 | castTo Int8Type = castInt8

552 | castTo Int16Type = castInt16

553 | castTo Int32Type = castInt32

554 | castTo Int64Type = castInt64

555 | castTo IntegerType = castInteger

556 | castTo Bits8Type = castBits8

557 | castTo Bits16Type = castBits16

558 | castTo Bits32Type = castBits32

559 | castTo Bits64Type = castBits64

560 | castTo StringType = castString

561 | castTo CharType = castChar

562 | castTo DoubleType = castDouble

563 | castTo WorldType = const Nothing

566 | getOp : {0 arity : Nat} -> PrimFn arity ->

567 |         {vars : Scope} -> Vect arity (NF vars) -> Maybe (NF vars)

568 | getOp (Add ty) = binOp add

569 | getOp (Sub ty) = binOp sub

570 | getOp (Mul ty) = binOp mul

571 | getOp (Div ty) = binOp div

572 | getOp (Mod ty) = binOp mod

573 | getOp (Neg ty) = unaryOp neg

574 | getOp (ShiftL ty) = binOp shiftl

575 | getOp (ShiftR ty) = binOp shiftr

577 | getOp (BAnd ty) = binOp band

578 | getOp (BOr ty) = binOp bor

579 | getOp (BXOr ty) = binOp bxor

581 | getOp (LT ty) = binOp lt

582 | getOp (LTE ty) = binOp lte

583 | getOp (EQ ty) = binOp eq

584 | getOp (GTE ty) = binOp gte

585 | getOp (GT ty) = binOp gt

587 | getOp StrLength = strLength

588 | getOp StrHead = strHead

589 | getOp StrTail = strTail

590 | getOp StrIndex = strIndex

591 | getOp StrCons = strCons

592 | getOp StrAppend = strAppend

593 | getOp StrReverse = strReverse

594 | getOp StrSubstr = strSubstr

596 | getOp DoubleExp = doubleExp

597 | getOp DoubleLog = doubleLog

598 | getOp DoublePow = doublePow

599 | getOp DoubleSin = doubleSin

600 | getOp DoubleCos = doubleCos

601 | getOp DoubleTan = doubleTan

602 | getOp DoubleASin = doubleASin

603 | getOp DoubleACos = doubleACos

604 | getOp DoubleATan = doubleATan

605 | getOp DoubleSqrt = doubleSqrt

606 | getOp DoubleFloor = doubleFloor

607 | getOp DoubleCeiling = doubleCeiling

609 | getOp (Cast _ y) = castTo y

610 | getOp BelieveMe = believeMe

612 | getOp _ = const Nothing

614 | prim : String -> Name

615 | prim str = UN $ Basic $ "prim__" ++ str

618 | opName : {0 arity : Nat} -> PrimFn arity -> Name

619 | opName (Add ty) = prim $ "add_" ++ show ty

620 | opName (Sub ty) = prim $ "sub_" ++ show ty

621 | opName (Mul ty) = prim $ "mul_" ++ show ty

622 | opName (Div ty) = prim $ "div_" ++ show ty

623 | opName (Mod ty) = prim $ "mod_" ++ show ty

624 | opName (Neg ty) = prim $ "negate_" ++ show ty

625 | opName (ShiftL ty) = prim $ "shl_" ++ show ty

626 | opName (ShiftR ty) = prim $ "shr_" ++ show ty

627 | opName (BAnd ty) = prim $ "and_" ++ show ty

628 | opName (BOr ty) = prim $ "or_" ++ show ty

629 | opName (BXOr ty) = prim $ "xor_" ++ show ty

630 | opName (LT ty) = prim $ "lt_" ++ show ty

631 | opName (LTE ty) = prim $ "lte_" ++ show ty