git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commit4bebb7240bd089fae45bccd0d3a26e428c3412b4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Jun 2013, 17:24 (13 years ago) parentd8580168dedc4b
13 files changed+277−672
compare with master
unifiedsplit
contribs/tool-support/completion/idris.bash+31 rts/idris_bitstring.h+4−4 src/Core/Execute.hs+16−475 src/IRTS/CodegenCommon.hs−7 src/Idris/AbsSyntax.hs+5 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabDecls.hs+39 src/Idris/IBC.hs+3−2 src/Idris/Primitives.hs+148−172 src/Idris/Providers.hs−1 src/Idris/REPL.hs+28−4 src/Main.hs+2 src/Util/System.hs−7
contribs/tool-support/completion/idris.bashnew file+31
@@ -0,0 +1,31 @@
1+_idris() {
2+ local cur prev words opts LIBRARIES TARGETS
3+ _init_completion || return
4+
5+ opts=$(_parse_help "$1")
6+ LIBRARIES="effects"
7+ TARGETS="C Java bytecode javascript node"
8+
9+ case "${prev}" in
10+ -o)
11+ _filedir
12+ ;;
13+ -i|--ibcsubdir)
14+ _filedir -d
15+ ;;
16+ -p)
17+ COMPREPLY=( $(compgen -W "${LIBRARIES}" -- ${cur}))
18+ ;;
19+ --target)
20+ COMPREPLY=( $(compgen -W "${TARGETS}" -- ${cur}))
21+ ;;
22+ esac
23+
24+ if [[ $cur == -* ]]; then
25+ COMPREPLY=($(compgen -W "${opts}" -- ${cur}))
26+ return
27+ fi
28+
29+ _filedir '@(idr)'
30+} &&
31+complete -o default -F _idris idris
rts/idris_bitstring.h+4−4
@@ -32,7 +32,7 @@ VAL idris_b8Compl(VM *vm, VAL a);
3232VAL idris_b8And(VM *vm, VAL a, VAL b);
3333VAL idris_b8Or(VM *vm, VAL a, VAL b);
3434VAL idris_b8Neg(VM *vm, VAL a);
35−VAL idris_b8XOr(VM *vm, VAL a, VAL b);
35+VAL idris_b8Xor(VM *vm, VAL a, VAL b);
3636VAL idris_b8Shl(VM *vm, VAL a, VAL b);
3737VAL idris_b8LShr(VM *vm, VAL a, VAL b);
3838VAL idris_b8AShr(VM *vm, VAL a, VAL b);
@@ -64,7 +64,7 @@ VAL idris_b16Compl(VM *vm, VAL a);
6464VAL idris_b16And(VM *vm, VAL a, VAL b);
6565VAL idris_b16Or(VM *vm, VAL a, VAL b);
6666VAL idris_b16Neg(VM *vm, VAL a);
67−VAL idris_b16XOr(VM *vm, VAL a, VAL b);
67+VAL idris_b16Xor(VM *vm, VAL a, VAL b);
6868VAL idris_b16Shl(VM *vm, VAL a, VAL b);
6969VAL idris_b16LShr(VM *vm, VAL a, VAL b);
7070VAL idris_b16AShr(VM *vm, VAL a, VAL b);
@@ -91,7 +91,7 @@ VAL idris_b32Compl(VM *vm, VAL a);
9191VAL idris_b32And(VM *vm, VAL a, VAL b);
9292VAL idris_b32Or(VM *vm, VAL a, VAL b);
9393VAL idris_b32Neg(VM *vm, VAL a);
94−VAL idris_b32XOr(VM *vm, VAL a, VAL b);
94+VAL idris_b32Xor(VM *vm, VAL a, VAL b);
9595VAL idris_b32Shl(VM *vm, VAL a, VAL b);
9696VAL idris_b32LShr(VM *vm, VAL a, VAL b);
9797VAL idris_b32AShr(VM *vm, VAL a, VAL b);
@@ -117,7 +117,7 @@ VAL idris_b64Compl(VM *vm, VAL a);
117117VAL idris_b64And(VM *vm, VAL a, VAL b);
118118VAL idris_b64Or(VM *vm, VAL a, VAL b);
119119VAL idris_b64Neg(VM *vm, VAL a);
120−VAL idris_b64XOr(VM *vm, VAL a, VAL b);
120+VAL idris_b64Xor(VM *vm, VAL a, VAL b);
121121VAL idris_b64Shl(VM *vm, VAL a, VAL b);
122122VAL idris_b64LShr(VM *vm, VAL a, VAL b);
123123VAL idris_b64AShr(VM *vm, VAL a, VAL b);
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/IRTS/CodegenCommon.hs−7
@@ -1,5 +1,3 @@
1−{-# LANGUAGE CPP #-}
2−
31module IRTS.CodegenCommon where
42
53import Core.TT
@@ -14,9 +12,4 @@ data OutputType = Raw | Object | Executable deriving (Eq, Show)
1412environment :: String -> IO (Maybe String)
1513environment x = Control.Exception.catch (do e <- getEnv x
1614 return (Just e))
17−#if MIN_VERSION_base(4,0,0)
1815 (\y-> do return (y::SomeException); return Nothing)
19−#endif
20−#if !MIN_VERSION_base(4,0,0)
21− (\_-> return Nothing)
22−#endif
src/Idris/AbsSyntax.hs+5
@@ -340,6 +340,11 @@ setQuiet q = do i <- getIState
340340 let opt' = opts { opt_quiet = q }
341341 putIState $ i { idris_options = opt' }
342342
343+getQuiet :: Idris Bool
344+getQuiet = do i <- getIState
345+ let opts = idris_options i
346+ return (opt_quiet opts)
347+
343348setTarget :: Target -> Idris ()
344349setTarget t = do i <- getIState
345350 let opts = idris_options i
src/Idris/AbsSyntaxTree.hs+1
@@ -253,6 +253,7 @@ data Opt = Filename String
253253 | UseTarget Target
254254 | OutputTy OutputType
255255 | Extension LanguageExt
256+ | InterpretScript String
256257 deriving (Show, Eq)
257258
258259-- Parsed declarations
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/IBC.hs+3−2
@@ -134,11 +134,12 @@ process :: IBCFile -> FilePath -> Idris ()
134134process i fn
135135 | ver i /= ibcVersion = do iLOG "ibc out of date"
136136 fail "Incorrect ibc version"
137− | otherwise =
137+ | otherwise =
138138 do srcok <- liftIO $ doesFileExist (sourcefile i)
139139 when srcok $ liftIO $ timestampOlder (sourcefile i) fn
140140 v <- verbose
141− when (v && srcok) $ iputStrLn $ "Skipping " ++ sourcefile i
141+ quiet <- getQuiet
142+ when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
142143 pImports (ibc_imports i)
143144 pImps (ibc_implicits i)
144145 pFixes (ibc_fixes i)
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
src/Idris/REPL.hs+28−4
@@ -605,6 +605,8 @@ parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
605605parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
606606parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
607607parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)
608+parseArgs ["--exec"] = InterpretScript "Main.main" : []
609+parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
608610parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)
609611parseArgs (n:ns) = Filename n : (parseArgs ns)
610612
@@ -640,11 +642,16 @@ idrisMain opts =
640642 let tgt = case opt getTarget opts of
641643 [] -> ViaC
642644 xs -> last xs
645+ script <- case opt getExecScript opts of
646+ [] -> return Nothing
647+ x:y:xs -> do iputStrLn "More than one interpreter expression found."
648+ liftIO $ exitWith (ExitFailure 1)
649+ [expr] -> return (Just expr)
643650 when (DefaultTotal `elem` opts) $ do i <- getIState
644651 putIState (i { default_total = True })
645652 mapM_ addLangExt (opt getLanguageExt opts)
646653 setREPL runrepl
647− setQuiet quiet
654+ setQuiet (quiet || isJust script)
648655 setIdeSlave idesl
649656 setVerbose runrepl
650657 setCmdLine opts
@@ -670,16 +677,19 @@ idrisMain opts =
670677 elabPrims
671678 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
672679 return ()
673− when (runrepl && not quiet && not idesl) $ iputStrLn banner
680+ when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
674681 ist <- getIState
675682 mods <- mapM loadModule inputs
676683 ok <- noErrors
677684 when ok $ case output of
678685 [] -> return ()
679− (o:_) -> process "" (Compile tgt o)
686+ (o:_) -> process "" (Compile tgt o)
680687 when ok $ case newoutput of
681688 [] -> return ()
682− (o:_) -> process "" (NewCompile o)
689+ (o:_) -> process "" (NewCompile o)
690+ case script of
691+ Nothing -> return ()
692+ Just expr -> execScript expr
683693 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
684694 when (idesl) $ ideslaveStart ist inputs
685695 ok <- noErrors
@@ -696,6 +706,16 @@ idrisMain opts =
696706 addPkgDir p = do ddir <- liftIO $ getDataDir
697707 addImportDir (ddir </> p)
698708
709+execScript :: String -> Idris ()
710+execScript expr = do i <- getIState
711+ case parseExpr i expr of
712+ Left err -> do iputStrLn $ show err
713+ liftIO $ exitWith (ExitFailure 1)
714+ Right term -> do ctxt <- getContext
715+ (tm, _) <- elabVal toplevel False term
716+ res <- execute tm
717+ liftIO $ exitWith ExitSuccess
718+
699719getFile :: Opt -> Maybe String
700720getFile (Filename str) = Just str
701721getFile _ = Nothing
@@ -741,6 +761,10 @@ getTarget :: Opt -> Maybe Target
741761getTarget (UseTarget x) = Just x
742762getTarget _ = Nothing
743763
764+getExecScript :: Opt -> Maybe String
765+getExecScript (InterpretScript expr) = Just expr
766+getExecScript _ = Nothing
767+
744768getOutputTy :: Opt -> Maybe OutputType
745769getOutputTy (OutputTy t) = Just t
746770getOutputTy _ = Nothing
src/Main.hs+2
@@ -91,6 +91,8 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++
9191 "\t--log [level] Type debugging log level\n" ++
9292 "\t-S Do no further compilation of code generator output\n" ++
9393 "\t-c Compile to object files rather than an executable\n" ++
94+ "\t--exec [expr] Execute the expression expr in the interpreter, defaulting to\n" ++
95+ "\t Main.main if none provided, and exit.\n" ++
9496 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in s-expressions)\n" ++
9597 "\t--libdir Show library install directory and exit\n" ++
9698 "\t--link Show C library directories and exit (for C linking)\n" ++
src/Util/System.hs−7
@@ -15,22 +15,15 @@ import System.FilePath ((</>), addTrailingPathSeparator, normalise)
1515import System.Environment
1616import System.IO
1717import System.IO.Error
18−#if MIN_VERSION_base(4,0,0)
1918import Control.Exception as CE
20−#endif
2119
2220import Paths_idris
2321
24−#if MIN_VERSION_base(4,0,0)
2522catchIO :: IO a -> (IOError -> IO a) -> IO a
2623catchIO = CE.catch
2724
2825throwIO :: IOError -> IO a
2926throwIO = CE.throw
30−#else
31−catchIO = catch
32−throwIO = throw
33−#endif
3427
3528
3629