git.iko.soy/Idris-dev
on master help sign in
Merge pull request #358 from david-christiansen/unite-the-primitives

Unite the primitives

commit77bf61684fca61da355d1f75dc814005fea67922 authorEdwin Brady <edwin.brady@gmail.com> dateFri 28 Jun 2013, 07:25 (13 years ago) parentb66e4a9656f219
4 files changed+203−648
compare with master
unifiedsplit
src/Core/Execute.hs+16−475 src/Idris/ElabDecls.hs+39 src/Idris/Primitives.hs+148−172 src/Idris/Providers.hs−1
src/Core/Execute.hs+16−475
@@ -7,6 +7,8 @@ import IRTS.Lang( IntTy(..)
77 , intTyToConst
88 , FType(..))
99
10+import Idris.Primitives(Prim(..), primitives)
11+
1012import Core.TT
1113import Core.Evaluate
1214import Core.CaseTree
@@ -316,490 +318,29 @@ execApp' env ctxt (EThunk i) args = do f <- force i
316318execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
317319execApp' env ctxt f args = return (mkEApp f args)
318320
319−
321+-- | Look up primitive operations in the global table and transform them into ExecVal functions
320322getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
321−getOp (UN "prim__addB16") [EConstant (B16 i1), EConstant (B16 i2)] =
322− primRes B16 (i1 + i2)
323−getOp (UN "prim__addB32") [EConstant (B32 i1), EConstant (B32 i2)] =
324− primRes B32 (i1 + i2)
325−getOp (UN "prim__addB64") [EConstant (B64 i1), EConstant (B64 i2)] =
326− primRes B64 (i1 + i2)
327−getOp (UN "prim__addB8") [EConstant (B8 i1), EConstant (B8 i2)] =
328− primRes B8 (i1 + i2)
329−getOp (UN "prim__addBigInt") [EConstant (BI i1), EConstant (BI i2)] =
330− primRes BI (i1 + i2)
331−getOp (UN "prim__addFloat") [EConstant (Fl f1), EConstant (Fl f2)] =
332− primRes Fl (f1 + f2)
333−getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
334− primRes I (i1 + i2)
335−getOp (UN "prim__andB16") [EConstant (B16 i1), EConstant (B16 i2)] =
336− primRes B16 (i1 .&. i2)
337−getOp (UN "prim__andB32") [EConstant (B32 i1), EConstant (B32 i2)] =
338− primRes B32 (i1 .&. i2)
339−getOp (UN "prim__andB64") [EConstant (B64 i1), EConstant (B64 i2)] =
340− primRes B64 (i1 .&. i2)
341−getOp (UN "prim__andB8") [EConstant (B8 i1), EConstant (B8 i2)] =
342− primRes B8 (i1 .&. i2)
343−getOp (UN "prim__andBigInt") [EConstant (BI i1), EConstant (BI i2)] =
344− primRes BI (i1 .&. i2)
345−getOp (UN "prim__andInt") [EConstant (I i1), EConstant (I i2)] =
346− primRes I (i1 .&. i2)
347−getOp (UN "prim__ashrB16") [EConstant (B16 i1), EConstant (B16 i2)] =
348− primRes B16 (shiftR i1 (fromIntegral i2))
349−getOp (UN "prim__ashrB32") [EConstant (B32 i1), EConstant (B32 i2)] =
350− primRes B32 (shiftR i1 (fromIntegral i2))
351−getOp (UN "prim__ashrB64") [EConstant (B64 i1), EConstant (B64 i2)] =
352− primRes B64 (shiftR i1 (fromIntegral i2))
353−getOp (UN "prim__ashrB8") [EConstant (B8 i1), EConstant (B8 i2)] =
354− primRes B8 (shiftR i1 (fromIntegral i2))
355−getOp (UN "prim__ashrBigInt") [EConstant (BI i1), EConstant (BI i2)] =
356− primRes BI (shiftR i1 (fromIntegral i2))
357−getOp (UN "prim__ashrInt") [EConstant (I i1), EConstant (I i2)] =
358− primRes I (shiftR i1 i2)
359−getOp (UN "prim__believe_me") [_, _, arg] = Just (return arg)
360−getOp (UN "prim__charToInt") [EConstant (Ch c)] =
361− primRes I (fromEnum c)
362−getOp (UN "prim__complB16") [EConstant (B16 i)] =
363− primRes B16 (complement i)
364−getOp (UN "prim__complB32") [EConstant (B32 i)] =
365− primRes B32 (complement i)
366−getOp (UN "prim__complB64") [EConstant (B64 i)] =
367− primRes B64 (complement i)
368−getOp (UN "prim__complB8") [EConstant (B8 i)] =
369− primRes B8 (complement i)
370−getOp (UN "prim__complBigInt") [EConstant (BI i)] =
371− primRes BI (complement i)
372−getOp (UN "prim__complInt") [EConstant (I i)] =
373− primRes I (complement i)
374−getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
375− primRes Str (s1 ++ s2)
376−getOp (UN "prim__divFloat") [EConstant (Fl f1), EConstant (Fl f2)] =
377− primRes Fl (f1 / f2)
378−getOp (UN "prim__divInt") [EConstant (I i1), EConstant (I i2)] =
379− primRes I (i1 `div` i2)
380−getOp (UN "prim__eqB16") [EConstant (B16 i1), EConstant (B16 i2)] =
381− primResBool (i1 == i2)
382−getOp (UN "prim__eqB32") [EConstant (B32 i1), EConstant (B32 i2)] =
383− primResBool (i1 == i2)
384−getOp (UN "prim__eqB64") [EConstant (B64 i1), EConstant (B64 i2)] =
385− primResBool (i1 == i2)
386−getOp (UN "prim__eqB8") [EConstant (B8 i1), EConstant (B8 i2)] =
387− primResBool (i1 == i2)
388−getOp (UN "prim__eqBigInt") [EConstant (BI i1), EConstant (BI i2)] =
389− primResBool (i1 == i2)
390−getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
391− primResBool (c1 == c2)
392−getOp (UN "prim__eqFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
393− primResBool (i1 == i2)
394−getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
395− primResBool (i1 == i2)
396−getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
397− primResBool (s1 == s2)
398−getOp (UN "prim__floatACos") [EConstant (Fl f)] =
399− primRes Fl (acos f)
400−getOp (UN "prim__floatASin") [EConstant (Fl f)] =
401− primRes Fl (asin f)
402−getOp (UN "prim__floatATan") [EConstant (Fl f)] =
403− primRes Fl (atan f)
404−getOp (UN "prim__floatCeil") [EConstant (Fl f)] =
405− primRes Fl (fromIntegral (ceiling f))
406−getOp (UN "prim__floatCos") [EConstant (Fl f)] =
407− primRes Fl (cos f)
408−getOp (UN "prim__floatExp") [EConstant (Fl f)] =
409− primRes Fl (exp f)
410−getOp (UN "prim__floatFloor") [EConstant (Fl f)] =
411− primRes Fl (fromIntegral (floor f))
412−getOp (UN "prim__floatLog") [EConstant (Fl f)] =
413− primRes Fl (log f)
414−getOp (UN "prim__floatSin") [EConstant (Fl f)] =
415− primRes Fl (sin f)
416−getOp (UN "prim__floatSqrt") [EConstant (Fl f)] =
417− primRes Fl (sqrt f)
418−getOp (UN "prim__floatTan") [EConstant (Fl f)] =
419− primRes Fl (tan f)
420−getOp (UN "prim__floatToStr") [EConstant (Fl f)] =
421− primRes Str (show f)
422−getOp (UN "prim__fromFloatB16") [EConstant (Fl f)] =
423− primRes B16 (fromIntegral (fromEnum f))
424−getOp (UN "prim__fromFloatB32") [EConstant (Fl f)] =
425− primRes B32 (fromIntegral (fromEnum f))
426−getOp (UN "prim__fromFloatB64") [EConstant (Fl f)] =
427− primRes B64 (fromIntegral (fromEnum f))
428−getOp (UN "prim__fromFloatB8") [EConstant (Fl f)] =
429− primRes B8 (fromIntegral (fromEnum f))
430−getOp (UN "prim__fromFloatBigInt") [EConstant (Fl f)] =
431− primRes BI (fromIntegral (fromEnum f))
432−getOp (UN "prim__fromFloatInt") [EConstant (Fl f)] =
433− primRes I (fromEnum f)
434−getOp (UN "prim__fromStrB16") [EConstant (Str s)] =
435− primRes B16 (fromMaybe 0 $ readMay s)
436−getOp (UN "prim__fromStrB32") [EConstant (Str s)] =
437− primRes B32 (fromMaybe 0 $ readMay s)
438−getOp (UN "prim__fromStrB64") [EConstant (Str s)] =
439− primRes B64 (fromMaybe 0 $ readMay s)
440−getOp (UN "prim__fromStrB8") [EConstant (Str s)] =
441− primRes B8 (fromMaybe 0 $ readMay s)
442−getOp (UN "prim__fromStrBigInt") [EConstant (Str s)] =
443− primRes BI (fromMaybe 0 $ readMay s)
444−getOp (UN "prim__fromStrInt") [EConstant (Str s)] =
445− primRes I (fromMaybe 0 $ readMay s)
446−getOp (UN "prim__gtB16") [EConstant (B16 x), EConstant (B16 y)] =
447− primResBool (x > y)
448−getOp (UN "prim__gtB32") [EConstant (B32 x), EConstant (B32 y)] =
449− primResBool (x > y)
450−getOp (UN "prim__gtB64") [EConstant (B64 x), EConstant (B64 y)] =
451− primResBool (x > y)
452−getOp (UN "prim__gtB8") [EConstant (B8 x), EConstant (B8 y)] =
453− primResBool (x > y)
454−getOp (UN "prim__gtBigInt") [EConstant (BI x), EConstant (BI y)] =
455− primResBool (x > y)
456−getOp (UN "prim__gtChar") [EConstant (Ch x), EConstant (Ch y)] =
457− primResBool (x > y)
458−getOp (UN "prim__gtFloat") [EConstant (Fl x), EConstant (Fl y)] =
459− primResBool (x > y)
460−getOp (UN "prim__gtInt") [EConstant (I x), EConstant (I y)] =
461− primResBool (x > y)
462−getOp (UN "prim__gteB16") [EConstant (B16 x), EConstant (B16 y)] =
463− primResBool (x >= y)
464−getOp (UN "prim__gteB32") [EConstant (B32 x), EConstant (B32 y)] =
465− primResBool (x >= y)
466−getOp (UN "prim__gteB64") [EConstant (B64 x), EConstant (B64 y)] =
467− primResBool (x >= y)
468−getOp (UN "prim__gteB8") [EConstant (B8 x), EConstant (B8 y)] =
469− primResBool (x >= y)
470−getOp (UN "prim__gteBigInt") [EConstant (BI x), EConstant (BI y)] =
471− primResBool (x >= y)
472−getOp (UN "prim__gteChar") [EConstant (Ch x), EConstant (Ch y)] =
473− primResBool (x >= y)
474−getOp (UN "prim__gteFloat") [EConstant (Fl x), EConstant (Fl y)] =
475− primResBool (x >= y)
476−getOp (UN "prim__gteInt") [EConstant (I x), EConstant (I y)] =
477− primResBool (x >= y)
478−getOp (UN "prim__intToChar") [EConstant (I i)] =
479− primRes Ch (toEnum i)
480−getOp (UN "prim__intToFloat") [EConstant (I i)] =
481− primRes Fl (fromRational (toRational i))
482−getOp (UN "prim__intToStr") [EConstant (I i)] =
483− primRes Str (show i)
484−getOp (UN "prim_lenString") [EConstant (Str s)] =
485− primRes I (length s)
486−getOp (UN "prim__lshrB16") [EConstant (B16 i1), EConstant (B16 i2)] =
487− primRes B16 (shiftR i1 (fromIntegral i2))
488−getOp (UN "prim__lshrB32") [EConstant (B32 i1), EConstant (B32 i2)] =
489− primRes B32 (shiftR i1 (fromIntegral i2))
490−getOp (UN "prim__lshrB64") [EConstant (B64 i1), EConstant (B64 i2)] =
491− primRes B64 (shiftR i1 (fromIntegral i2))
492−getOp (UN "prim__lshrB8") [EConstant (B8 i1), EConstant (B8 i2)] =
493− primRes B8 (shiftR i1 (fromIntegral i2))
494−getOp (UN "prim__lshrBigInt") [EConstant (BI i1), EConstant (BI i2)] =
495− primRes BI (shiftR i1 (fromIntegral i2))
496−getOp (UN "prim__lshrInt") [EConstant (I i1), EConstant (I i2)] =
497− primRes I (shiftR i1 i2)
498−getOp (UN "prim__ltB16") [EConstant (B16 x), EConstant (B16 y)] =
499− primResBool (x < y)
500−getOp (UN "prim__ltB32") [EConstant (B32 x), EConstant (B32 y)] =
501− primResBool (x < y)
502−getOp (UN "prim__ltB64") [EConstant (B64 x), EConstant (B64 y)] =
503− primResBool (x < y)
504−getOp (UN "prim__ltB8") [EConstant (B8 x), EConstant (B8 y)] =
505− primResBool (x < y)
506−getOp (UN "prim__ltBigInt") [EConstant (BI x), EConstant (BI y)] =
507− primResBool (x < y)
508−getOp (UN "prim__ltChar") [EConstant (Ch x), EConstant (Ch y)] =
509− primResBool (x < y)
510−getOp (UN "prim__ltFloat") [EConstant (Fl x), EConstant (Fl y)] =
511− primResBool (x < y)
512−getOp (UN "prim__ltInt") [EConstant (I x), EConstant (I y)] =
513− primResBool (x < y)
514−getOp (UN "prim__lteB16") [EConstant (B16 x), EConstant (B16 y)] =
515− primResBool (x <= y)
516−getOp (UN "prim__lteB32") [EConstant (B32 x), EConstant (B32 y)] =
517− primResBool (x <= y)
518−getOp (UN "prim__lteB64") [EConstant (B64 x), EConstant (B64 y)] =
519− primResBool (x <= y)
520−getOp (UN "prim__lteB8") [EConstant (B8 x), EConstant (B8 y)] =
521− primResBool (x <= y)
522−getOp (UN "prim__lteBigInt") [EConstant (BI x), EConstant (BI y)] =
523− primResBool (x <= y)
524−getOp (UN "prim__lteChar") [EConstant (Ch x), EConstant (Ch y)] =
525− primResBool (x <= y)
526−getOp (UN "prim__lteFloat") [EConstant (Fl x), EConstant (Fl y)] =
527− primResBool (x <= y)
528−getOp (UN "prim__lteInt") [EConstant (I x), EConstant (I y)] =
529− primResBool (x <= y)
530−getOp (UN "prim__modInt") [EConstant (I i1), EConstant (I i2)] =
531− primRes I (i1 `mod` i2)
532−getOp (UN "prim__mulB16") [EConstant (B16 i1), EConstant (B16 i2)] =
533− primRes B16 (i1 * i2)
534−getOp (UN "prim__mulB32") [EConstant (B32 i1), EConstant (B32 i2)] =
535− primRes B32 (i1 * i2)
536−getOp (UN "prim__mulB64") [EConstant (B64 i1), EConstant (B64 i2)] =
537− primRes B64 (i1 * i2)
538−getOp (UN "prim__mulB8") [EConstant (B8 i1), EConstant (B8 i2)] =
539− primRes B8 (i1 * i2)
540−getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
541− primRes BI (i1 * i2)
542−getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
543− primRes Fl (i1 * i2)
544−getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
545− primRes I (i1 * i2)
546−getOp (UN "prim__orB16") [EConstant (B16 i1), EConstant (B16 i2)] =
547− primRes B16 (i1 .|. i2)
548−getOp (UN "prim__orB32") [EConstant (B32 i1), EConstant (B32 i2)] =
549− primRes B32 (i1 .|. i2)
550−getOp (UN "prim__orB64") [EConstant (B64 i1), EConstant (B64 i2)] =
551− primRes B64 (i1 .|. i2)
552−getOp (UN "prim__orB8") [EConstant (B8 i1), EConstant (B8 i2)] =
553− primRes B8 (i1 .|. i2)
554−getOp (UN "prim__orBigInt") [EConstant (BI i1), EConstant (BI i2)] =
555− primRes BI (i1 .|. i2)
556−getOp (UN "prim__orInt") [EConstant (I i1), EConstant (I i2)] =
557− primRes I (i1 .|. i2)
323+getOp (UN "prim__believe_me") [_, _, x] = Just (return x)
558324getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
559325 Just $ do line <- execIO getLine
560326 return (EConstant (Str line))
561327getOp (UN "prim__readString") [EHandle h] =
562328 Just $ do contents <- execIO $ hGetLine h
563329 return (EConstant (Str (contents ++ "\n")))
564−getOp (UN "prim__sdivB16") [EConstant (B16 i1), EConstant (B16 i2)] =
565− primRes B16 (i1 `div` i2)
566−getOp (UN "prim__sdivB32") [EConstant (B32 i1), EConstant (B32 i2)] =
567− primRes B32 (i1 `div` i2)
568−getOp (UN "prim__sdivB64") [EConstant (B64 i1), EConstant (B64 i2)] =
569− primRes B64 (i1 `div` i2)
570−getOp (UN "prim__sdivB8") [EConstant (B8 i1), EConstant (B8 i2)] =
571− primRes B8 (i1 `div` i2)
572−getOp (UN "prim__sdivBigInt") [EConstant (BI i1), EConstant (BI i2)] =
573− primRes BI (i1 `div` i2)
574−getOp (UN "prim__sdivInt") [EConstant (I i1), EConstant (I i2)] =
575− primRes I (i1 `div` i2)
576−getOp (UN "prim__sextB16_B32") [EConstant (B16 i)] =
577− primRes B32 (fromIntegral i)
578−getOp (UN "prim__sextB16_B64") [EConstant (B16 i)] =
579− primRes B64 (fromIntegral i)
580−getOp (UN "prim__sextB16_BigInt") [EConstant (B16 i)] =
581− primRes BI (fromIntegral i)
582−getOp (UN "prim__sextB16_Int") [EConstant (B16 i)] =
583− primRes I (fromIntegral i)
584−getOp (UN "prim__sextB32_B64") [EConstant (B32 i)] =
585− primRes B64 (fromIntegral i)
586−getOp (UN "prim__sextB32_BigInt") [EConstant (B32 i)] =
587− primRes BI (fromIntegral i)
588−getOp (UN "prim__sextB32_Int") [EConstant (B32 i)] =
589− primRes I (fromIntegral i)
590−getOp (UN "prim__sextB64_BigInt") [EConstant (B64 i)] =
591− primRes BI (fromIntegral i)
592−getOp (UN "prim__sextB8_B16") [EConstant (B8 i)] =
593− primRes B16 (fromIntegral i)
594−getOp (UN "prim__sextB8_B32") [EConstant (B8 i)] =
595− primRes B32 (fromIntegral i)
596−getOp (UN "prim__sextB8_B64") [EConstant (B8 i)] =
597− primRes B64 (fromIntegral i)
598−getOp (UN "prim__sextB8_BigInt") [EConstant (B8 i)] =
599− primRes BI (fromIntegral i)
600−getOp (UN "prim__sextB8_Int") [EConstant (B8 i)] =
601− primRes I (fromIntegral i)
602−getOp (UN "prim__sextInt_B16") [EConstant (I i)] =
603− primRes B16 (fromIntegral i)
604−getOp (UN "prim__sextInt_B32") [EConstant (I i)] =
605− primRes B32 (fromIntegral i)
606−getOp (UN "prim__sextInt_B64") [EConstant (I i)] =
607− primRes B64 (fromIntegral i)
608−getOp (UN "prim__sextInt_BigInt") [EConstant (I i)] =
609− primRes BI (fromIntegral i)
610−getOp (UN "prim__shlB16") [EConstant (B16 i1), EConstant (B16 i2)] =
611− primRes B16 (shiftL i1 (fromIntegral i2))
612−getOp (UN "prim__shlB32") [EConstant (B32 i1), EConstant (B32 i2)] =
613− primRes B32 (shiftL i1 (fromIntegral i2))
614−getOp (UN "prim__shlB64") [EConstant (B64 i1), EConstant (B64 i2)] =
615− primRes B64 (shiftL i1 (fromIntegral i2))
616−getOp (UN "prim__shlB8") [EConstant (B8 i1), EConstant (B8 i2)] =
617− primRes B8 (shiftL i1 (fromIntegral i2))
618−getOp (UN "prim__shlBigInt") [EConstant (BI i1), EConstant (BI i2)] =
619− primRes BI (shiftL i1 (fromIntegral i2))
620−getOp (UN "prim__shlInt") [EConstant (I i1), EConstant (I i2)] =
621− primRes I (shiftL i1 i2)
622−getOp (UN "prim__sremB16") [EConstant (B16 i1), EConstant (B16 i2)] =
623− primRes B16 (rem i1 i2)
624−getOp (UN "prim__sremB32") [EConstant (B32 i1), EConstant (B32 i2)] =
625− primRes B32 (rem i1 i2)
626−getOp (UN "prim__sremB64") [EConstant (B64 i1), EConstant (B64 i2)] =
627− primRes B64 (rem i1 i2)
628−getOp (UN "prim__sremB8") [EConstant (B8 i1), EConstant (B8 i2)] =
629− primRes B8 (rem i1 i2)
630−getOp (UN "prim__sremBigInt") [EConstant (BI i1), EConstant (BI i2)] =
631− primRes BI (rem i1 i2)
632−getOp (UN "prim__sremInt") [EConstant (I i1), EConstant (I i2)] =
633− primRes I (rem i1 i2)
634−-- No definition for prim__stdin because the IO operations special-case it instead
635−getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
636− primRes Str (c:s)
637−getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
638− primRes Ch c
639−getOp (UN "prim__strIndex") [EConstant (Str s), EConstant (I i)]
640− | i >= 0 && i < length s = primRes Ch (s !! i)
641−getOp (UN "prim__strRev") [EConstant (Str s)] =
642− primRes Str (reverse s)
643−getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
644− primRes Str s
645−getOp (UN "prim__strToFloat") [EConstant (Str s)] =
646− primRes Fl (fromMaybe 0.0 $ readMay s)
647−getOp (UN "prim__subB16") [EConstant (B16 i1), EConstant (B16 i2)] =
648− primRes B16 (i1 - i2)
649−getOp (UN "prim__subB32") [EConstant (B32 i1), EConstant (B32 i2)] =
650− primRes B32 (i1 - i2)
651−getOp (UN "prim__subB64") [EConstant (B64 i1), EConstant (B64 i2)] =
652− primRes B64 (i1 - i2)
653−getOp (UN "prim__subB8") [EConstant (B8 i1), EConstant (B8 i2)] =
654− primRes B8 (i1 - i2)
655−getOp (UN "prim__subBigInt") [EConstant (BI i1), EConstant (BI i2)] =
656− primRes BI (i1 - i2)
657−getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
658− primRes Fl (i1 - i2)
659−getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
660− primRes I (i1 - i2)
661−getOp (UN "prim__toFloatB16") [EConstant (B16 i)] =
662− primRes Fl (fromIntegral i)
663−getOp (UN "prim__toFloatB32") [EConstant (B32 i)] =
664− primRes Fl (fromIntegral i)
665−getOp (UN "prim__toFloatB64") [EConstant (B64 i)] =
666− primRes Fl (fromIntegral i)
667−getOp (UN "prim__toFloatB8") [EConstant (B8 i)] =
668− primRes Fl (fromIntegral i)
669−getOp (UN "prim__toFloatBigInt") [EConstant (BI i)] =
670− primRes Fl (fromIntegral i)
671−getOp (UN "prim__toFloatInt") [EConstant (I i)] =
672− primRes Fl (fromIntegral i)
673−getOp (UN "prim__toStrB16") [EConstant (B16 i)] =
674− primRes Str (show i)
675−getOp (UN "prim__toStrB32") [EConstant (B32 i)] =
676− primRes Str (show i)
677−getOp (UN "prim__toStrB64") [EConstant (B64 i)] =
678− primRes Str (show i)
679−getOp (UN "prim__toStrB8") [EConstant (B8 i)] =
680− primRes Str (show i)
681−getOp (UN "prim__toStrBigInt") [EConstant (BI i)] =
682− primRes Str (show i)
683−getOp (UN "prim__toStrInt") [EConstant (I i)] =
684− primRes Str (show i)
685−getOp (UN "prim__truncB16_B8") [EConstant (B16 i)] =
686− primRes B8 (fromIntegral i)
687−getOp (UN "prim__truncB16_Int") [EConstant (B16 i)] =
688− primRes I (fromIntegral i)
689−getOp (UN "prim__truncB32_B16") [EConstant (B32 i)] =
690− primRes B16 (fromIntegral i)
691−getOp (UN "prim__truncB32_B8") [EConstant (B32 i)] =
692− primRes B8 (fromIntegral i)
693−getOp (UN "prim__truncB32_Int") [EConstant (B32 i)] =
694− primRes I (fromIntegral i)
695−getOp (UN "prim__truncB64_B16") [EConstant (B64 i)] =
696− primRes B16 (fromIntegral i)
697−getOp (UN "prim__truncB64_B32") [EConstant (B64 i)] =
698− primRes B32 (fromIntegral i)
699−getOp (UN "prim__truncB64_B8") [EConstant (B64 i)] =
700− primRes B8 (fromIntegral i)
701−getOp (UN "prim__truncB64_Int") [EConstant (B64 i)] =
702− primRes I (fromIntegral i)
703−getOp (UN "prim__truncBigInt_B16") [EConstant (BI i)] =
704− primRes B16 (fromIntegral i)
705−getOp (UN "prim__truncBigInt_B32") [EConstant (BI i)] =
706− primRes B32 (fromIntegral i)
707−getOp (UN "prim__truncBigInt_B64") [EConstant (BI i)] =
708− primRes B64 (fromIntegral i)
709−getOp (UN "prim__truncBigInt_B8") [EConstant (BI i)] =
710− primRes B8 (fromIntegral i)
711−getOp (UN "prim__truncBigInt_Int") [EConstant (BI i)] =
712− primRes I (fromIntegral i)
713−getOp (UN "prim__truncInt_B16") [EConstant (I i)] =
714− primRes B16 (fromIntegral i)
715−getOp (UN "prim__truncInt_B32") [EConstant (I i)] =
716− primRes B32 (fromIntegral i)
717−getOp (UN "prim__truncInt_B64") [EConstant (I i)] =
718− primRes B64 (fromIntegral i)
719−getOp (UN "prim__truncInt_B8") [EConstant (I i)] =
720− primRes B8 (fromIntegral i)
721−getOp (UN "prim__udivB16") [EConstant (B16 i1), EConstant (B16 i2)] =
722− primRes B16 (i1 `div` i2)
723−getOp (UN "prim__udivB32") [EConstant (B32 i1), EConstant (B32 i2)] =
724− primRes B32 (i1 `div` i2)
725−getOp (UN "prim__udivB64") [EConstant (B64 i1), EConstant (B64 i2)] =
726− primRes B64 (i1 `div` i2)
727−getOp (UN "prim__udivB8") [EConstant (B8 i1), EConstant (B8 i2)] =
728− primRes B8 (i1 `div` i2)
729−getOp (UN "prim__udivBigInt") [EConstant (BI i1), EConstant (BI i2)] =
730− primRes BI (i1 `div` i2)
731−getOp (UN "prim__udivInt") [EConstant (I i1), EConstant (I i2)] =
732− primRes I (i1 `div` i2)
733−getOp (UN "prim__uremB16") [EConstant (B16 i1), EConstant (B16 i2)] =
734− primRes B16 (rem i1 i2)
735−getOp (UN "prim__uremB32") [EConstant (B32 i1), EConstant (B32 i2)] =
736− primRes B32 (rem i1 i2)
737−getOp (UN "prim__uremB64") [EConstant (B64 i1), EConstant (B64 i2)] =
738− primRes B64 (rem i1 i2)
739−getOp (UN "prim__uremB8") [EConstant (B8 i1), EConstant (B8 i2)] =
740− primRes B8 (rem i1 i2)
741−getOp (UN "prim__uremBigInt") [EConstant (BI i1), EConstant (BI i2)] =
742− primRes BI (rem i1 i2)
743−getOp (UN "prim__uremInt") [EConstant (I i1), EConstant (I i2)] =
744− primRes I (rem i1 i2)
745−-- No implementation for prim__vm because the VM isn't available in interpreted code
746−getOp (UN "prim__xorB16") [EConstant (B16 i1), EConstant (B16 i2)] =
747− primRes B16 (i1 `xor` i2)
748−getOp (UN "prim__xorB32") [EConstant (B32 i1), EConstant (B32 i2)] =
749− primRes B32 (i1 `xor` i2)
750−getOp (UN "prim__xorB64") [EConstant (B64 i1), EConstant (B64 i2)] =
751− primRes B64 (i1 `xor` i2)
752−getOp (UN "prim__xorB8") [EConstant (B8 i1), EConstant (B8 i2)] =
753− primRes B8 (i1 `xor` i2)
754−getOp (UN "prim__xorBigInt") [EConstant (BI i1), EConstant (BI i2)] =
755− primRes BI (i1 `xor` i2)
756−getOp (UN "prim__xorInt") [EConstant (I i1), EConstant (I i2)] =
757− primRes I (i1 `xor` i2)
758−getOp (UN "prim__zextB16_B32") [EConstant (B16 i)] =
759− primRes B32 (fromIntegral i)
760−getOp (UN "prim__zextB16_B64") [EConstant (B16 i)] =
761− primRes B64 (fromIntegral i)
762−getOp (UN "prim__zextB16_BigInt") [EConstant (B16 i)] =
763− primRes BI (fromIntegral i)
764−getOp (UN "prim__zextB16_Int") [EConstant (B16 i)] =
765− primRes I (fromIntegral i)
766−getOp (UN "prim__zextB32_B64") [EConstant (B32 i)] =
767− primRes B64 (fromIntegral i)
768−getOp (UN "prim__zextB32_BigInt") [EConstant (B32 i)] =
769− primRes BI (fromIntegral i)
770−getOp (UN "prim__zextB32_Int") [EConstant (B32 i)] =
771− primRes I (fromIntegral i)
772−getOp (UN "prim__zextB64_BigInt") [EConstant (B64 i)] =
773− primRes BI (fromIntegral i)
774−getOp (UN "prim__zextB8_B16") [EConstant (B8 i)] =
775− primRes B16 (fromIntegral i)
776−getOp (UN "prim__zextB8_B32") [EConstant (B8 i)] =
777− primRes B32 (fromIntegral i)
778−getOp (UN "prim__zextB8_B64") [EConstant (B8 i)] =
779− primRes B64 (fromIntegral i)
780−getOp (UN "prim__zextB8_BigInt") [EConstant (B8 i)] =
781− primRes BI (fromIntegral i)
782−getOp (UN "prim__zextB8_Int") [EConstant (B8 i)] =
783− primRes I (fromIntegral i)
784−getOp (UN "prim__zextInt_B16") [EConstant (I i)] =
785− primRes B16 (fromIntegral i)
786−getOp (UN "prim__zextInt_B32") [EConstant (I i)] =
787− primRes B32 (fromIntegral i)
788−getOp (UN "prim__zextInt_B64") [EConstant (I i)] =
789− primRes B64 (fromIntegral i)
790−getOp (UN "prim__zextInt_BigInt") [EConstant (I i)] =
791− primRes BI (fromIntegral i)
792−getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
793−
794−-- | Helper function to construct a result of a primitive
795−primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
796−primRes constr = Just . return . EConstant . constr
797−
798−-- | Helper function with boolean conversion for primitive results
799−primResBool :: Bool -> Maybe (Exec ExecVal)
800−primResBool b = primRes I (if b then 1 else 0)
330+getOp n args = getPrim n primitives >>= flip applyPrim args
331+ where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
332+ getPrim n [] = Nothing
333+ getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
334+ | otherwise = getPrim n prims
335+
336+ execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
337+ execPrim f args = EConstant <$> (mapM getConst args >>= f)
801338
339+ getConst (EConstant c) = Just c
340+ getConst _ = Nothing
802341
342+ applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
343+ applyPrim fn args = return <$> fn args
803344
804345
805346
src/Idris/ElabDecls.hs+39
@@ -12,6 +12,8 @@ import Idris.ElabTerm
1212import Idris.Coverage
1313import Idris.DataOpts
1414import Idris.Providers
15+import Idris.Primitives
16+import IRTS.Lang
1517import Paths_idris
1618
1719import Core.TT
@@ -210,6 +212,43 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
210212 | otherwise = count n ts
211213 mParam args (_ : rest) = Nothing : mParam args rest
212214
215+-- | Elaborate primitives
216+
217+elabPrims :: Idris ()
218+elabPrims = do mapM_ (elabDecl EAll toplevel)
219+ (map (PData "" defaultSyntax (FC "builtin" 0) False)
220+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
221+ mapM_ elabPrim primitives
222+ -- Special case prim__believe_me because it doesn't work on just constants
223+ elabBelieveMe
224+ where elabPrim :: Prim -> Idris ()
225+ elabPrim (Prim n ty i def sc tot)
226+ = do updateContext (addOperator n ty i (valuePrim def))
227+ setTotality n tot
228+ i <- getIState
229+ putIState i { idris_scprims = (n, sc) : idris_scprims i }
230+
231+ valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
232+ valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)
233+
234+ getConst (VConstant c) = Just c
235+ getConst _ = Nothing
236+
237+
238+ p_believeMe [_,_,x] = Just x
239+ p_believeMe _ = Nothing
240+ believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
241+ (Bind (UN "b") (Pi (TType (UVar (-2))))
242+ (Bind (UN "x") (Pi (V 1)) (V 1)))
243+ elabBelieveMe = do let prim__believe_me = (UN "prim__believe_me")
244+ updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
245+ setTotality prim__believe_me (Partial NotCovering)
246+ i <- getIState
247+ putIState i {
248+ idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
249+ }
250+
251+
213252-- | Elaborate a type provider
214253elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
215254elabProvider info syn fc n ty tm
src/Idris/Primitives.hs+148−172
@@ -1,9 +1,7 @@
11{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
22
3−module Idris.Primitives(elabPrims) where
3+module Idris.Primitives(primitives, Prim(..)) where
44
5−import Idris.ElabDecls
6−import Idris.ElabTerm
75import Idris.AbsSyntax
86
97import IRTS.Lang
@@ -17,7 +15,7 @@ import Data.Int
1715data Prim = Prim { p_name :: Name,
1816 p_type :: Type,
1917 p_arity :: Int,
20− p_def :: [Value] -> Maybe Value,
18+ p_def :: [Const] -> Maybe Const,
2119 p_lexp :: (Int, PrimFn),
2220 p_total :: Totality
2321 }
@@ -26,11 +24,6 @@ ty :: [Const] -> Const -> Type
2624ty [] x = Constant x
2725ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
2826
29−believeTy :: Type
30−believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
31− (Bind (UN "b") (Pi (TType (UVar (-2))))
32− (Bind (UN "x") (Pi (V 1)) (V 1)))
33−
3427total, partial :: Totality
3528total = Total []
3629partial = Partial NotCovering
@@ -180,9 +173,7 @@ primitives =
180173 (0, LVMPtr) total,
181174 -- Streams
182175 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
183− (0, LStdIn) partial,
184− Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
185− (3, LNoOp) partial -- ahem
176+ (0, LStdIn) partial
186177 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
187178
188179intOps :: IntTy -> [Prim]
@@ -221,213 +212,209 @@ intTyName ITNative = "Int"
221212intTyName ITBig = "BigInt"
222213intTyName sized = "B" ++ show (intTyWidth sized)
223214
224−iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Value] -> Maybe Value) -> (IntTy -> PrimFn) -> Totality -> Prim
215+iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
225216iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
226217iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
227218iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
228219
229−iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Value] -> Maybe Value) -> (IntTy -> IntTy -> PrimFn) -> Prim
220+iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim
230221iCoerce from to op impl irop =
231222 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
232223 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
233224
234−p_believeMe :: [a] -> Maybe a
235−p_believeMe [_,_,x] = Just x
236−p_believeMe _ = Nothing
237−
238−iUn :: (Int -> Int) -> [Value] -> Maybe Value
239−iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
225+iUn :: (Int -> Int) -> [Const] -> Maybe Const
226+iUn op [I x] = Just $ I (op x)
240227iUn _ _ = Nothing
241228
242−iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value
243−iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
229+iBin :: (Int -> Int -> Int) -> [Const] -> Maybe Const
230+iBin op [I x, I y] = Just $ I (op x y)
244231iBin _ _ = Nothing
245232
246−bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value
247−bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
233+bBin :: (Integer -> Integer -> Integer) -> [Const] -> Maybe Const
234+bBin op [BI x, BI y] = Just $ BI (op x y)
248235bBin _ _ = Nothing
249236
250−bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value
251−bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
237+bBini :: (Integer -> Integer -> Int) -> [Const] -> Maybe Const
238+bBini op [BI x, BI y] = Just $ I (op x y)
252239bBini _ _ = Nothing
253240
254−biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value
241+biBin :: (Int -> Int -> Bool) -> [Const] -> Maybe Const
255242biBin op = iBin (\x y -> if (op x y) then 1 else 0)
256243
257−bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value
244+bbBin :: (Integer -> Integer -> Bool) -> [Const] -> Maybe Const
258245bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
259246
260−fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value
261−fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
247+fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const
248+fBin op [Fl x, Fl y] = Just $ Fl (op x y)
262249fBin _ _ = Nothing
263250
264−bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value
265−bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
266− Just $ VConstant (I i)
251+bfBin :: (Double -> Double -> Bool) -> [Const] -> Maybe Const
252+bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
253+ Just $ I i
267254bfBin _ _ = Nothing
268255
269−bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value
270−bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
271− Just $ VConstant (I i)
256+bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
257+bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
258+ Just $ I i
272259bcBin _ _ = Nothing
273260
274−bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value
275−bsBin op [VConstant (Str x), VConstant (Str y)]
261+bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
262+bsBin op [Str x, Str y]
276263 = let i = (if op x y then 1 else 0) in
277− Just $ VConstant (I i)
264+ Just $ I i
278265bsBin _ _ = Nothing
279266
280−sBin :: (String -> String -> String) -> [Value] -> Maybe Value
281−sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
267+sBin :: (String -> String -> String) -> [Const] -> Maybe Const
268+sBin op [Str x, Str y] = Just $ Str (op x y)
282269sBin _ _ = Nothing
283270
284−bsrem :: IntTy -> [Value] -> Maybe Value
285−bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]
286− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))
287−bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]
288− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)))
289−bsrem IT32 [VConstant (B32 x), VConstant (B32 y)]
290− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)))
291−bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]
292− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)))
293−bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))
271+bsrem :: IntTy -> [Const] -> Maybe Const
272+bsrem IT8 [B8 x, B8 y]
273+ = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))
274+bsrem IT16 [B16 x, B16 y]
275+ = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))
276+bsrem IT32 [B32 x, B32 y]
277+ = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))
278+bsrem IT64 [B64 x, B64 y]
279+ = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))
280+bsrem ITNative [I x, I y] = Just $ I (x `rem` y)
294281bsrem _ _ = Nothing
295282
296−bsdiv :: IntTy -> [Value] -> Maybe Value
297−bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]
298− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))
299−bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]
300− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)))
301−bsdiv IT32 [VConstant (B32 x), VConstant (B32 y)]
302− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)))
303−bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]
304− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)))
305−bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))
283+bsdiv :: IntTy -> [Const] -> Maybe Const
284+bsdiv IT8 [B8 x, B8 y]
285+ = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
286+bsdiv IT16 [B16 x, B16 y]
287+ = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
288+bsdiv IT32 [B32 x, B32 y]
289+ = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
290+bsdiv IT64 [B64 x, B64 y]
291+ = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
292+bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
306293bsdiv _ _ = Nothing
307294
308−bashr :: IntTy -> [Value] -> Maybe Value
309−bashr IT8 [VConstant (B8 x), VConstant (B8 y)]
310− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))
311−bashr IT16 [VConstant (B16 x), VConstant (B16 y)]
312− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16)))
313−bashr IT32 [VConstant (B32 x), VConstant (B32 y)]
314− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32)))
315−bashr IT64 [VConstant (B64 x), VConstant (B64 y)]
316− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64)))
317−bashr ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `shiftR` y))
295+bashr :: IntTy -> [Const] -> Maybe Const
296+bashr IT8 [B8 x, B8 y]
297+ = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))
298+bashr IT16 [B16 x, B16 y]
299+ = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))
300+bashr IT32 [B32 x, B32 y]
301+ = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))
302+bashr IT64 [B64 x, B64 y]
303+ = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))
304+bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)
318305bashr _ _ = Nothing
319306
320−bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Value] -> Maybe Value
321−bUn IT8 op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))
322−bUn IT16 op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))
323−bUn IT32 op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))
324−bUn IT64 op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))
325−bUn ITBig op [VConstant (BI x)] = Just $ VConstant (BI (op x))
326−bUn ITNative op [VConstant (I x)] = Just $ VConstant (I (op x))
327−bUn _ _ _ = Nothing
328−
329−bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Value] -> Maybe Value
330−bitBin IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))
331−bitBin IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))
332−bitBin IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))
333−bitBin IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))
334−bitBin ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
335−bitBin ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
336−bitBin _ _ _ = Nothing
337−
338−bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Value] -> Maybe Value
339−bCmp IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
340−bCmp IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
341−bCmp IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
342−bCmp IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
343−bCmp ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
344−bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
345−bCmp _ _ _ = Nothing
346−
347−toInt :: Integral a => IntTy -> a -> Value
348−toInt IT8 x = VConstant (B8 (fromIntegral x))
349−toInt IT16 x = VConstant (B16 (fromIntegral x))
350−toInt IT32 x = VConstant (B32 (fromIntegral x))
351−toInt IT64 x = VConstant (B64 (fromIntegral x))
352−toInt ITBig x = VConstant (BI (fromIntegral x))
353−toInt ITNative x = VConstant (I (fromIntegral x))
354−
355−intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value
356−intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x
357−intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x
358−intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x
359−intToInt IT64 out [VConstant (B64 x)] = Just $ toInt out x
360−intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x
361−intToInt ITNative out [VConstant (I x)] = Just $ toInt out x
307+bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const
308+bUn IT8 op [B8 x] = Just $ B8 (op x)
309+bUn IT16 op [B16 x] = Just $ B16 (op x)
310+bUn IT32 op [B32 x] = Just $ B32 (op x)
311+bUn IT64 op [B64 x] = Just $ B64 (op x)
312+bUn ITBig op [BI x] = Just $ BI (op x)
313+bUn ITNative op [I x] = Just $ I (op x)
314+bUn _ _ _ = Nothing
315+
316+bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const
317+bitBin IT8 op [B8 x, B8 y] = Just $ B8 (op x y)
318+bitBin IT16 op [B16 x, B16 y] = Just $ B16 (op x y)
319+bitBin IT32 op [B32 x, B32 y] = Just $ B32 (op x y)
320+bitBin IT64 op [B64 x, B64 y] = Just $ B64 (op x y)
321+bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)
322+bitBin ITNative op [I x, I y] = Just $ I (op x y)
323+bitBin _ _ _ = Nothing
324+
325+bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Const] -> Maybe Const
326+bCmp IT8 op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)
327+bCmp IT16 op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)
328+bCmp IT32 op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)
329+bCmp IT64 op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)
330+bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)
331+bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)
332+bCmp _ _ _ = Nothing
333+
334+toInt :: Integral a => IntTy -> a -> Const
335+toInt IT8 x = B8 (fromIntegral x)
336+toInt IT16 x = B16 (fromIntegral x)
337+toInt IT32 x = B32 (fromIntegral x)
338+toInt IT64 x = B64 (fromIntegral x)
339+toInt ITBig x = BI (fromIntegral x)
340+toInt ITNative x = I (fromIntegral x)
341+
342+intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const
343+intToInt IT8 out [B8 x] = Just $ toInt out x
344+intToInt IT16 out [B16 x] = Just $ toInt out x
345+intToInt IT32 out [B32 x] = Just $ toInt out x
346+intToInt IT64 out [B64 x] = Just $ toInt out x
347+intToInt ITBig out [BI x] = Just $ toInt out x
348+intToInt ITNative out [I x] = Just $ toInt out x
362349intToInt _ _ _ = Nothing
363350
364−zext :: IntTy -> IntTy -> [Value] -> Maybe Value
351+zext :: IntTy -> IntTy -> [Const] -> Maybe Const
365352zext from ITBig val = intToInt from ITBig val
366353zext ITBig _ _ = Nothing
367354zext from to val
368355 | intTyWidth from < intTyWidth to = intToInt from to val
369356zext _ _ _ = Nothing
370357
371−sext :: IntTy -> IntTy -> [Value] -> Maybe Value
372−sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)
373−sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)
374−sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)
375−sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)
376−sext ITBig _ _ = Nothing
377−sext from to val = intToInt from to val
358+sext :: IntTy -> IntTy -> [Const] -> Maybe Const
359+sext IT8 out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)
360+sext IT16 out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)
361+sext IT32 out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)
362+sext IT64 out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)
363+sext ITBig _ _ = Nothing
364+sext from to val = intToInt from to val
378365
379−trunc :: IntTy -> IntTy -> [Value] -> Maybe Value
366+trunc :: IntTy -> IntTy -> [Const] -> Maybe Const
380367trunc ITBig to val = intToInt ITBig to val
381368trunc _ ITBig _ = Nothing
382369trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
383370trunc _ _ _ = Nothing
384371
385−getInt :: [Value] -> Maybe Integer
386−getInt [VConstant (B8 x)] = Just . toInteger $ x
387−getInt [VConstant (B16 x)] = Just . toInteger $ x
388−getInt [VConstant (B32 x)] = Just . toInteger $ x
389−getInt [VConstant (B64 x)] = Just . toInteger $ x
390−getInt [VConstant (I x)] = Just . toInteger $ x
391−getInt [VConstant (BI x)] = Just x
392−getInt _ = Nothing
393−
394−intToStr :: [Value] -> Maybe Value
395−intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))
372+getInt :: [Const] -> Maybe Integer
373+getInt [B8 x] = Just . toInteger $ x
374+getInt [B16 x] = Just . toInteger $ x
375+getInt [B32 x] = Just . toInteger $ x
376+getInt [B64 x] = Just . toInteger $ x
377+getInt [I x] = Just . toInteger $ x
378+getInt [BI x] = Just x
379+getInt _ = Nothing
380+
381+intToStr :: [Const] -> Maybe Const
382+intToStr val | Just i <- getInt val = Just $ Str (show i)
396383intToStr _ = Nothing
397384
398−strToInt :: IntTy -> [Value] -> Maybe Value
399−strToInt ity [VConstant (Str x)] = case reads x of
400− [(n,"")] -> Just $ toInt ity (n :: Integer)
401− _ -> Just $ VConstant (I 0)
385+strToInt :: IntTy -> [Const] -> Maybe Const
386+strToInt ity [Str x] = case reads x of
387+ [(n,"")] -> Just $ toInt ity (n :: Integer)
388+ _ -> Just $ I 0
402389strToInt _ _ = Nothing
403390
404−intToFloat :: [Value] -> Maybe Value
405−intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))
391+intToFloat :: [Const] -> Maybe Const
392+intToFloat val | Just i <- getInt val = Just $ Fl (fromIntegral i)
406393intToFloat _ = Nothing
407394
408−floatToInt :: IntTy -> [Value] -> Maybe Value
409−floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)
395+floatToInt :: IntTy -> [Const] -> Maybe Const
396+floatToInt ity [Fl x] = Just $ toInt ity (truncate x :: Integer)
410397floatToInt _ _ = Nothing
411398
412−c_intToChar :: [Value] -> Maybe Value
413−c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
399+c_intToChar, c_charToInt :: [Const] -> Maybe Const
400+c_intToChar [(I x)] = Just . Ch . toEnum $ x
414401c_intToChar _ = Nothing
415−c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
402+c_charToInt [(Ch x)] = Just . I . fromEnum $ x
416403c_charToInt _ = Nothing
417404
418−c_floatToStr :: [Value] -> Maybe Value
419−c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
405+c_floatToStr :: [Const] -> Maybe Const
406+c_floatToStr [Fl x] = Just $ Str (show x)
420407c_floatToStr _ = Nothing
421−c_strToFloat [VConstant (Str x)] = case reads x of
422− [(n,"")] -> Just $ VConstant (Fl n)
423− _ -> Just $ VConstant (Fl 0)
408+c_strToFloat [Str x] = case reads x of
409+ [(n,"")] -> Just $ Fl n
410+ _ -> Just $ Fl 0
424411c_strToFloat _ = Nothing
425412
426−p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value
427−p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
413+p_fPrim :: (Double -> Double) -> [Const] -> Maybe Const
414+p_fPrim f [Fl x] = Just $ Fl (f x)
428415p_fPrim f _ = Nothing
429416
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
417+p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Const] -> Maybe Const
431418p_floatExp = p_fPrim exp
432419p_floatLog = p_fPrim log
433420p_floatSin = p_fPrim sin
@@ -440,34 +427,23 @@ p_floatSqrt = p_fPrim sqrt
440427p_floatFloor = p_fPrim (fromInteger . floor)
441428p_floatCeil = p_fPrim (fromInteger . ceiling)
442429
443−p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value
444−p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
430+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const
431+p_strLen [Str xs] = Just $ I (length xs)
445432p_strLen _ = Nothing
446−p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
433+p_strHead [Str (x:xs)] = Just $ Ch x
447434p_strHead _ = Nothing
448−p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
435+p_strTail [Str (x:xs)] = Just $ Str xs
449436p_strTail _ = Nothing
450−p_strIndex [VConstant (Str xs), VConstant (I i)]
451− | i < length xs = Just $ VConstant (Ch (xs!!i))
437+p_strIndex [Str xs, I i]
438+ | i < length xs = Just $ Ch (xs!!i)
452439p_strIndex _ = Nothing
453−p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
440+p_strCons [Ch x, Str xs] = Just $ Str (x:xs)
454441p_strCons _ = Nothing
455−p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
442+p_strRev [Str xs] = Just $ Str (reverse xs)
456443p_strRev _ = Nothing
457444
458445p_cantreduce :: a -> Maybe b
459446p_cantreduce _ = Nothing
460447
461−elabPrim :: Prim -> Idris ()
462−elabPrim (Prim n ty i def sc tot)
463− = do updateContext (addOperator n ty i def)
464− setTotality n tot
465− i <- getIState
466− putIState i { idris_scprims = (n, sc) : idris_scprims i }
467−
468−elabPrims :: Idris ()
469−elabPrims = do mapM_ (elabDecl EAll toplevel)
470− (map (PData "" defaultSyntax (FC "builtin" 0) False)
471− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
472− mapM_ elabPrim primitives
448+
473449
src/Idris/Providers.hs−1
@@ -3,7 +3,6 @@ module Idris.Providers (providerTy, getProvided) where
33
44import Core.TT
55import Core.Evaluate
6−import Core.Execute
76import Idris.AbsSyntax
87import Idris.AbsSyntaxTree
98import Idris.Error