affd239 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add type annotations to Primitives.hs to aid in understanding

affd239David Christiansen13 years ago

src/Idris/Primitives.hs+45−6

compare with master

unifiedsplit

@@ -22,16 +22,20 @@ data Prim = Prim { p_name :: Name,

22 p_total :: Totality

23 }

25+ty :: [Const] -> Const -> Type

25ty [] x = Constant x

26ty [] x = Constant x

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

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

29+believeTy :: Type

28believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))

30believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))

29 (Bind (UN "b") (Pi (TType (UVar (-2))))

31 (Bind (UN "b") (Pi (TType (UVar (-2))))

30 (Bind (UN "x") (Pi (V 1)) (V 1)))

32 (Bind (UN "x") (Pi (V 1)) (V 1)))

34+total, partial :: Totality

32total = Total []

35total = Total []

33−partial = Partial NotCovering

36+partial = Partial NotCovering

38+primitives :: [Prim]

35primitives =

39primitives =

36 -- operators

40 -- operators

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

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

@@ -138,7 +142,7 @@ primitives =

138 (1, LFloatStr) total,

142 (1, LFloatStr) total,

139

143

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

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

141− (1, LFExp) total,

145+ (1, LFExp) total,

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

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

143 (1, LFLog) total,

147 (1, LFLog) total,

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

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

@@ -181,6 +185,7 @@ primitives =

181 (3, LNoOp) partial -- ahem

185 (3, LNoOp) partial -- ahem

182 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]

186 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]

183

187

188+intOps :: IntTy -> [Prim]

184intOps ity =

189intOps ity =

185 [ iCmp ity "lt" (bCmp ity (<)) LLt total

190 [ iCmp ity "lt" (bCmp ity (<)) LLt total

186 , iCmp ity "lte" (bCmp ity (<=)) LLe total

191 , iCmp ity "lte" (bCmp ity (<=)) LLe total

@@ -216,50 +221,67 @@ intTyName ITNative = "Int"

216intTyName ITBig = "BigInt"

221intTyName ITBig = "BigInt"

217intTyName sized = "B" ++ show (intTyWidth sized)

222intTyName sized = "B" ++ show (intTyWidth sized)

218

223

224+iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Value] -> Maybe Value) -> (IntTy -> PrimFn) -> Totality -> Prim

219iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality

225iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality

220iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality

226iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality

221iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality

227iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality

228+

229+iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Value] -> Maybe Value) -> (IntTy -> IntTy -> PrimFn) -> Prim

222iCoerce from to op impl irop =

230iCoerce from to op impl irop =

223 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

231 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

224 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total

232 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total

225

233

234+p_believeMe :: [a] -> Maybe a

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

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

227p_believeMe _ = Nothing

236p_believeMe _ = Nothing

228

237

238+iUn :: (Int -> Int) -> [Value] -> Maybe Value

229iUn op [VConstant (I x)] = Just $ VConstant (I (op x))

239iUn op [VConstant (I x)] = Just $ VConstant (I (op x))

230iUn _ _ = Nothing

240iUn _ _ = Nothing

231

241

242+iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value

232iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

243iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

233iBin _ _ = Nothing

244iBin _ _ = Nothing

234

245

246+bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value

235bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))

247bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))

236bBin _ _ = Nothing

248bBin _ _ = Nothing

237

249

250+bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value

238bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))

251bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))

239bBini _ _ = Nothing

252bBini _ _ = Nothing

240

253

254+biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value

241biBin op = iBin (\x y -> if (op x y) then 1 else 0)

255biBin op = iBin (\x y -> if (op x y) then 1 else 0)

256+

257+bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value

242bbBin op = bBini (\x y -> if (op x y) then 1 else 0)

258bbBin op = bBini (\x y -> if (op x y) then 1 else 0)

243

259

260+fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value

244fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))

261fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))

245fBin _ _ = Nothing

262fBin _ _ = Nothing

246

263

264+bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value

247bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in

265bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in

248 Just $ VConstant (I i)

266 Just $ VConstant (I i)

249bfBin _ _ = Nothing

267bfBin _ _ = Nothing

250

268

269+bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value

251bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in

270bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in

252 Just $ VConstant (I i)

271 Just $ VConstant (I i)

253bcBin _ _ = Nothing

272bcBin _ _ = Nothing

254

273

274+bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value

255−bsBin op [VConstant (Str x), VConstant (Str y)]

275+bsBin op [VConstant (Str x), VConstant (Str y)]

256 = let i = (if op x y then 1 else 0) in

276 = let i = (if op x y then 1 else 0) in

257 Just $ VConstant (I i)

277 Just $ VConstant (I i)

258bsBin _ _ = Nothing

278bsBin _ _ = Nothing

259

279

280+sBin :: (String -> String -> String) -> [Value] -> Maybe Value

260sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

281sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

261sBin _ _ = Nothing

282sBin _ _ = Nothing

262

283

284+bsrem :: IntTy -> [Value] -> Maybe Value

263bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]

285bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]

264 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))

286 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))

265bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]

287bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]

@@ -271,6 +293,7 @@ bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]

271bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))

293bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))

272bsrem _ _ = Nothing

294bsrem _ _ = Nothing

273

295

296+bsdiv :: IntTy -> [Value] -> Maybe Value

274bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]

297bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]

275 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))

298 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))

276bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]

299bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]

@@ -282,6 +305,7 @@ bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]

282bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))

305bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))

283bsdiv _ _ = Nothing

306bsdiv _ _ = Nothing

284

307

308+bashr :: IntTy -> [Value] -> Maybe Value

285bashr IT8 [VConstant (B8 x), VConstant (B8 y)]

309bashr IT8 [VConstant (B8 x), VConstant (B8 y)]

286 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))

310 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))

287bashr IT16 [VConstant (B16 x), VConstant (B16 y)]

311bashr IT16 [VConstant (B16 x), VConstant (B16 y)]

@@ -320,6 +344,7 @@ bCmp ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (if (op

320bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

344bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

321bCmp _ _ _ = Nothing

345bCmp _ _ _ = Nothing

322

346

347+toInt :: Integral a => IntTy -> a -> Value

323toInt IT8 x = VConstant (B8 (fromIntegral x))

348toInt IT8 x = VConstant (B8 (fromIntegral x))

324toInt IT16 x = VConstant (B16 (fromIntegral x))

349toInt IT16 x = VConstant (B16 (fromIntegral x))

325toInt IT32 x = VConstant (B32 (fromIntegral x))

350toInt IT32 x = VConstant (B32 (fromIntegral x))

@@ -327,6 +352,7 @@ toInt IT64 x = VConstant (B64 (fromIntegral x))

327toInt ITBig x = VConstant (BI (fromIntegral x))

352toInt ITBig x = VConstant (BI (fromIntegral x))

328toInt ITNative x = VConstant (I (fromIntegral x))

353toInt ITNative x = VConstant (I (fromIntegral x))

329

354

355+intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value

330intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x

356intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x

331intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x

357intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x

332intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x

358intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x

@@ -335,12 +361,14 @@ intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x

335intToInt ITNative out [VConstant (I x)] = Just $ toInt out x

361intToInt ITNative out [VConstant (I x)] = Just $ toInt out x

336intToInt _ _ _ = Nothing

362intToInt _ _ _ = Nothing

337

363

364+zext :: IntTy -> IntTy -> [Value] -> Maybe Value

338zext from ITBig val = intToInt from ITBig val

365zext from ITBig val = intToInt from ITBig val

339zext ITBig _ _ = Nothing

366zext ITBig _ _ = Nothing

340zext from to val

367zext from to val

341 | intTyWidth from < intTyWidth to = intToInt from to val

368 | intTyWidth from < intTyWidth to = intToInt from to val

342zext _ _ _ = Nothing

369zext _ _ _ = Nothing

343

370

371+sext :: IntTy -> IntTy -> [Value] -> Maybe Value

344sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)

372sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)

345sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)

373sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)

346sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)

374sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)

@@ -348,6 +376,7 @@ sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)

348sext ITBig _ _ = Nothing

376sext ITBig _ _ = Nothing

349sext from to val = intToInt from to val

377sext from to val = intToInt from to val

350

378

379+trunc :: IntTy -> IntTy -> [Value] -> Maybe Value

351trunc ITBig to val = intToInt ITBig to val

380trunc ITBig to val = intToInt ITBig to val

352trunc _ ITBig _ = Nothing

381trunc _ ITBig _ = Nothing

353trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

382trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

@@ -362,25 +391,31 @@ getInt [VConstant (I x)] = Just . toInteger $ x

362getInt [VConstant (BI x)] = Just x

391getInt [VConstant (BI x)] = Just x

363getInt _ = Nothing

392getInt _ = Nothing

364

393

394+intToStr :: [Value] -> Maybe Value

365intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))

395intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))

366intToStr _ = Nothing

396intToStr _ = Nothing

367

397

398+strToInt :: IntTy -> [Value] -> Maybe Value

368strToInt ity [VConstant (Str x)] = case reads x of

399strToInt ity [VConstant (Str x)] = case reads x of

369 [(n,"")] -> Just $ toInt ity (n :: Integer)

400 [(n,"")] -> Just $ toInt ity (n :: Integer)

370 _ -> Just $ VConstant (I 0)

401 _ -> Just $ VConstant (I 0)

371strToInt _ _ = Nothing

402strToInt _ _ = Nothing

372

403

404+intToFloat :: [Value] -> Maybe Value

373intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))

405intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))

374intToFloat _ = Nothing

406intToFloat _ = Nothing

375

407

408+floatToInt :: IntTy -> [Value] -> Maybe Value

376floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)

409floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)

377floatToInt _ _ = Nothing

410floatToInt _ _ = Nothing

378

411

412+c_intToChar :: [Value] -> Maybe Value

379c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

413c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

380c_intToChar _ = Nothing

414c_intToChar _ = Nothing

381c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

415c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

382c_charToInt _ = Nothing

416c_charToInt _ = Nothing

383

417

418+c_floatToStr :: [Value] -> Maybe Value

384c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

419c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

385c_floatToStr _ = Nothing

420c_floatToStr _ = Nothing

386c_strToFloat [VConstant (Str x)] = case reads x of

421c_strToFloat [VConstant (Str x)] = case reads x of

@@ -388,9 +423,11 @@ c_strToFloat [VConstant (Str x)] = case reads x of

388 _ -> Just $ VConstant (Fl 0)

423 _ -> Just $ VConstant (Fl 0)

389c_strToFloat _ = Nothing

424c_strToFloat _ = Nothing

390

425

426+p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value

391p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

427p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

392p_fPrim f _ = Nothing

428p_fPrim f _ = Nothing

393

429

430+p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Value] -> Maybe Value

394p_floatExp = p_fPrim exp

431p_floatExp = p_fPrim exp

395p_floatLog = p_fPrim log

432p_floatLog = p_fPrim log

396p_floatSin = p_fPrim sin

433p_floatSin = p_fPrim sin

@@ -403,13 +440,14 @@ p_floatSqrt = p_fPrim sqrt

403p_floatFloor = p_fPrim (fromInteger . floor)

440p_floatFloor = p_fPrim (fromInteger . floor)

404p_floatCeil = p_fPrim (fromInteger . ceiling)

441p_floatCeil = p_fPrim (fromInteger . ceiling)

405

442

443+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value

406p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

444p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

407p_strLen _ = Nothing

445p_strLen _ = Nothing

408p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

446p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

409p_strHead _ = Nothing

447p_strHead _ = Nothing

410p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

448p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

411p_strTail _ = Nothing

449p_strTail _ = Nothing

412−p_strIndex [VConstant (Str xs), VConstant (I i)]

450+p_strIndex [VConstant (Str xs), VConstant (I i)]

413 | i < length xs = Just $ VConstant (Ch (xs!!i))

451 | i < length xs = Just $ VConstant (Ch (xs!!i))

414p_strIndex _ = Nothing

452p_strIndex _ = Nothing

415p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))

453p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))

@@ -417,17 +455,18 @@ p_strCons _ = Nothing

417p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

455p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

418p_strRev _ = Nothing

456p_strRev _ = Nothing

419

457

458+p_cantreduce :: a -> Maybe b

420p_cantreduce _ = Nothing

459p_cantreduce _ = Nothing

421

460

422elabPrim :: Prim -> Idris ()

461elabPrim :: Prim -> Idris ()

423−elabPrim (Prim n ty i def sc tot)

462+elabPrim (Prim n ty i def sc tot)

424 = do updateContext (addOperator n ty i def)

463 = do updateContext (addOperator n ty i def)

425 setTotality n tot

464 setTotality n tot

426 i <- getIState

465 i <- getIState

427 putIState i { idris_scprims = (n, sc) : idris_scprims i }

466 putIState i { idris_scprims = (n, sc) : idris_scprims i }

428

467

429elabPrims :: Idris ()

468elabPrims :: Idris ()

430−elabPrims = do mapM_ (elabDecl EAll toplevel)

469+elabPrims = do mapM_ (elabDecl EAll toplevel)

431 (map (PData "" defaultSyntax (FC "builtin" 0) False)

470 (map (PData "" defaultSyntax (FC "builtin" 0) False)

432 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

471 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

433 mapM_ elabPrim primitives

472 mapM_ elabPrim primitives