git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
4bebb72Edwin Brady
contribs/tool-support/completion/idris.bashnew file+31
compare with master
unifiedsplit
@@ -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);
32VAL idris_b8And(VM *vm, VAL a, VAL b);
32VAL idris_b8And(VM *vm, VAL a, VAL b);
33VAL idris_b8Or(VM *vm, VAL a, VAL b);
33VAL idris_b8Or(VM *vm, VAL a, VAL b);
34VAL idris_b8Neg(VM *vm, VAL a);
34VAL 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);
36VAL idris_b8Shl(VM *vm, VAL a, VAL b);
36VAL idris_b8Shl(VM *vm, VAL a, VAL b);
37VAL idris_b8LShr(VM *vm, VAL a, VAL b);
37VAL idris_b8LShr(VM *vm, VAL a, VAL b);
38VAL idris_b8AShr(VM *vm, VAL a, VAL b);
38VAL idris_b8AShr(VM *vm, VAL a, VAL b);
@@ -64,7 +64,7 @@ VAL idris_b16Compl(VM *vm, VAL a);
64VAL idris_b16And(VM *vm, VAL a, VAL b);
64VAL idris_b16And(VM *vm, VAL a, VAL b);
65VAL idris_b16Or(VM *vm, VAL a, VAL b);
65VAL idris_b16Or(VM *vm, VAL a, VAL b);
66VAL idris_b16Neg(VM *vm, VAL a);
66VAL 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);
68VAL idris_b16Shl(VM *vm, VAL a, VAL b);
68VAL idris_b16Shl(VM *vm, VAL a, VAL b);
69VAL idris_b16LShr(VM *vm, VAL a, VAL b);
69VAL idris_b16LShr(VM *vm, VAL a, VAL b);
70VAL idris_b16AShr(VM *vm, VAL a, VAL b);
70VAL idris_b16AShr(VM *vm, VAL a, VAL b);
@@ -91,7 +91,7 @@ VAL idris_b32Compl(VM *vm, VAL a);
91VAL idris_b32And(VM *vm, VAL a, VAL b);
91VAL idris_b32And(VM *vm, VAL a, VAL b);
92VAL idris_b32Or(VM *vm, VAL a, VAL b);
92VAL idris_b32Or(VM *vm, VAL a, VAL b);
93VAL idris_b32Neg(VM *vm, VAL a);
93VAL 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);
95VAL idris_b32Shl(VM *vm, VAL a, VAL b);
95VAL idris_b32Shl(VM *vm, VAL a, VAL b);
96VAL idris_b32LShr(VM *vm, VAL a, VAL b);
96VAL idris_b32LShr(VM *vm, VAL a, VAL b);
97VAL idris_b32AShr(VM *vm, VAL a, VAL b);
97VAL idris_b32AShr(VM *vm, VAL a, VAL b);
@@ -117,7 +117,7 @@ VAL idris_b64Compl(VM *vm, VAL a);
117VAL idris_b64And(VM *vm, VAL a, VAL b);
117VAL idris_b64And(VM *vm, VAL a, VAL b);
118VAL idris_b64Or(VM *vm, VAL a, VAL b);
118VAL idris_b64Or(VM *vm, VAL a, VAL b);
119VAL idris_b64Neg(VM *vm, VAL a);
119VAL 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);
121VAL idris_b64Shl(VM *vm, VAL a, VAL b);
121VAL idris_b64Shl(VM *vm, VAL a, VAL b);
122VAL idris_b64LShr(VM *vm, VAL a, VAL b);
122VAL idris_b64LShr(VM *vm, VAL a, VAL b);
123VAL idris_b64AShr(VM *vm, VAL a, VAL b);
123VAL idris_b64AShr(VM *vm, VAL a, VAL b);
src/Core/Execute.hs+16−475
@@ -7,6 +7,8 @@ import IRTS.Lang( IntTy(..)
7 , intTyToConst
7 , intTyToConst
8 , FType(..))
8 , FType(..))
9
9
10+import Idris.Primitives(Prim(..), primitives)
11+
10import Core.TT
12import Core.TT
11import Core.Evaluate
13import Core.Evaluate
12import Core.CaseTree
14import Core.CaseTree
@@ -316,490 +318,29 @@ execApp' env ctxt (EThunk i) args = do f <- force i
316execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
318execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
317execApp' env ctxt f args = return (mkEApp f args)
319execApp' env ctxt f args = return (mkEApp f args)
318
320
319−
321+-- | Look up primitive operations in the global table and transform them into ExecVal functions
320getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
322getOp :: 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)
323+getOp (UN "prim__believe_me") [_, _, x] = Just (return x)
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)
558getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
324getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
559 Just $ do line <- execIO getLine
325 Just $ do line <- execIO getLine
560 return (EConstant (Str line))
326 return (EConstant (Str line))
561getOp (UN "prim__readString") [EHandle h] =
327getOp (UN "prim__readString") [EHandle h] =
562 Just $ do contents <- execIO $ hGetLine h
328 Just $ do contents <- execIO $ hGetLine h
563 return (EConstant (Str (contents ++ "\n")))
329 return (EConstant (Str (contents ++ "\n")))
564−getOp (UN "prim__sdivB16") [EConstant (B16 i1), EConstant (B16 i2)] =
330+getOp n args = getPrim n primitives >>= flip applyPrim args
565− primRes B16 (i1 `div` i2)
331+ where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
566−getOp (UN "prim__sdivB32") [EConstant (B32 i1), EConstant (B32 i2)] =
332+ getPrim n [] = Nothing
567− primRes B32 (i1 `div` i2)
333+ getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
568−getOp (UN "prim__sdivB64") [EConstant (B64 i1), EConstant (B64 i2)] =
334+ | otherwise = getPrim n prims
569− primRes B64 (i1 `div` i2)
335+
570−getOp (UN "prim__sdivB8") [EConstant (B8 i1), EConstant (B8 i2)] =
336+ execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
571− primRes B8 (i1 `div` i2)
337+ execPrim f args = EConstant <$> (mapM getConst args >>= f)
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)
801
338
339+ getConst (EConstant c) = Just c
340+ getConst _ = Nothing
802
341
342+ applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
343+ applyPrim fn args = return <$> fn args
803
344
804
345
805
346
src/IRTS/CodegenCommon.hs−7
@@ -1,5 +1,3 @@
1−{-# LANGUAGE CPP #-}
2−
3module IRTS.CodegenCommon where
1module IRTS.CodegenCommon where
4
2
5import Core.TT
3import Core.TT
@@ -14,9 +12,4 @@ data OutputType = Raw | Object | Executable deriving (Eq, Show)
14environment :: String -> IO (Maybe String)
12environment :: String -> IO (Maybe String)
15environment x = Control.Exception.catch (do e <- getEnv x
13environment x = Control.Exception.catch (do e <- getEnv x
16 return (Just e))
14 return (Just e))
17−#if MIN_VERSION_base(4,0,0)
18 (\y-> do return (y::SomeException); return Nothing)
15 (\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
340 let opt' = opts { opt_quiet = q }
340 let opt' = opts { opt_quiet = q }
341 putIState $ i { idris_options = opt' }
341 putIState $ i { idris_options = opt' }
342
342
343+getQuiet :: Idris Bool
344+getQuiet = do i <- getIState
345+ let opts = idris_options i
346+ return (opt_quiet opts)
347+
343setTarget :: Target -> Idris ()
348setTarget :: Target -> Idris ()
344setTarget t = do i <- getIState
349setTarget t = do i <- getIState
345 let opts = idris_options i
350 let opts = idris_options i
src/Idris/AbsSyntaxTree.hs+1
@@ -253,6 +253,7 @@ data Opt = Filename String
253 | UseTarget Target
253 | UseTarget Target
254 | OutputTy OutputType
254 | OutputTy OutputType
255 | Extension LanguageExt
255 | Extension LanguageExt
256+ | InterpretScript String
256 deriving (Show, Eq)
257 deriving (Show, Eq)
257
258
258-- Parsed declarations
259-- Parsed declarations
src/Idris/ElabDecls.hs+39
@@ -12,6 +12,8 @@ import Idris.ElabTerm
12import Idris.Coverage
12import Idris.Coverage
13import Idris.DataOpts
13import Idris.DataOpts
14import Idris.Providers
14import Idris.Providers
15+import Idris.Primitives
16+import IRTS.Lang
15import Paths_idris
17import Paths_idris
16
18
17import Core.TT
19import Core.TT
@@ -210,6 +212,43 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
210 | otherwise = count n ts
212 | otherwise = count n ts
211 mParam args (_ : rest) = Nothing : mParam args rest
213 mParam args (_ : rest) = Nothing : mParam args rest
212
214
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+
213-- | Elaborate a type provider
252-- | Elaborate a type provider
214elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
253elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
215elabProvider info syn fc n ty tm
254elabProvider info syn fc n ty tm
src/Idris/IBC.hs+3−2
@@ -134,11 +134,12 @@ process :: IBCFile -> FilePath -> Idris ()
134process i fn
134process i fn
135 | ver i /= ibcVersion = do iLOG "ibc out of date"
135 | ver i /= ibcVersion = do iLOG "ibc out of date"
136 fail "Incorrect ibc version"
136 fail "Incorrect ibc version"
137− | otherwise =
137+ | otherwise =
138 do srcok <- liftIO $ doesFileExist (sourcefile i)
138 do srcok <- liftIO $ doesFileExist (sourcefile i)
139 when srcok $ liftIO $ timestampOlder (sourcefile i) fn
139 when srcok $ liftIO $ timestampOlder (sourcefile i) fn
140 v <- verbose
140 v <- verbose
141+ quiet <- getQuiet
141− when (v && srcok) $ iputStrLn $ "Skipping " ++ sourcefile i
142+ when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
142 pImports (ibc_imports i)
143 pImports (ibc_imports i)
143 pImps (ibc_implicits i)
144 pImps (ibc_implicits i)
144 pFixes (ibc_fixes i)
145 pFixes (ibc_fixes i)
src/Idris/Primitives.hs+148−172
@@ -1,9 +1,7 @@
1{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
1{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
2
2
3−module Idris.Primitives(elabPrims) where
3+module Idris.Primitives(primitives, Prim(..)) where
4
4
5−import Idris.ElabDecls
6−import Idris.ElabTerm
7import Idris.AbsSyntax
5import Idris.AbsSyntax
8
6
9import IRTS.Lang
7import IRTS.Lang
@@ -17,7 +15,7 @@ import Data.Int
17data Prim = Prim { p_name :: Name,
15data Prim = Prim { p_name :: Name,
18 p_type :: Type,
16 p_type :: Type,
19 p_arity :: Int,
17 p_arity :: Int,
20− p_def :: [Value] -> Maybe Value,
18+ p_def :: [Const] -> Maybe Const,
21 p_lexp :: (Int, PrimFn),
19 p_lexp :: (Int, PrimFn),
22 p_total :: Totality
20 p_total :: Totality
23 }
21 }
@@ -26,11 +24,6 @@ ty :: [Const] -> Const -> Type
26ty [] x = Constant x
24ty [] x = Constant x
27ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
25ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
28
26
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−
34total, partial :: Totality
27total, partial :: Totality
35total = Total []
28total = Total []
36partial = Partial NotCovering
29partial = Partial NotCovering
@@ -180,9 +173,7 @@ primitives =
180 (0, LVMPtr) total,
173 (0, LVMPtr) total,
181 -- Streams
174 -- Streams
182 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
175 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
183− (0, LStdIn) partial,
176+ (0, LStdIn) partial
184− Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
185− (3, LNoOp) partial -- ahem
186 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
177 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
187
178
188intOps :: IntTy -> [Prim]
179intOps :: IntTy -> [Prim]
@@ -221,213 +212,209 @@ intTyName ITNative = "Int"
221intTyName ITBig = "BigInt"
212intTyName ITBig = "BigInt"
222intTyName sized = "B" ++ show (intTyWidth sized)
213intTyName sized = "B" ++ show (intTyWidth sized)
223
214
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
225iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
216iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
226iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
217iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
227iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
218iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
228
219
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
230iCoerce from to op impl irop =
221iCoerce from to op impl irop =
231 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
222 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
232 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
223 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
233
224
234−p_believeMe :: [a] -> Maybe a
235−p_believeMe [_,_,x] = Just x
236−p_believeMe _ = Nothing
237−
238−iUn :: (Int -> Int) -> [Value] -> Maybe Value
225+iUn :: (Int -> Int) -> [Const] -> Maybe Const
239−iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
226+iUn op [I x] = Just $ I (op x)
240iUn _ _ = Nothing
227iUn _ _ = Nothing
241
228
242−iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value
229+iBin :: (Int -> Int -> Int) -> [Const] -> Maybe Const
243−iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
230+iBin op [I x, I y] = Just $ I (op x y)
244iBin _ _ = Nothing
231iBin _ _ = Nothing
245
232
246−bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value
233+bBin :: (Integer -> Integer -> Integer) -> [Const] -> Maybe Const
247−bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
234+bBin op [BI x, BI y] = Just $ BI (op x y)
248bBin _ _ = Nothing
235bBin _ _ = Nothing
249
236
250−bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value
237+bBini :: (Integer -> Integer -> Int) -> [Const] -> Maybe Const
251−bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
238+bBini op [BI x, BI y] = Just $ I (op x y)
252bBini _ _ = Nothing
239bBini _ _ = Nothing
253
240
254−biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value
241+biBin :: (Int -> Int -> Bool) -> [Const] -> Maybe Const
255biBin op = iBin (\x y -> if (op x y) then 1 else 0)
242biBin op = iBin (\x y -> if (op x y) then 1 else 0)
256
243
257−bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value
244+bbBin :: (Integer -> Integer -> Bool) -> [Const] -> Maybe Const
258bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
245bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
259
246
260−fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value
247+fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const
261−fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
248+fBin op [Fl x, Fl y] = Just $ Fl (op x y)
262fBin _ _ = Nothing
249fBin _ _ = Nothing
263
250
264−bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value
251+bfBin :: (Double -> Double -> Bool) -> [Const] -> Maybe Const
265−bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
252+bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
266− Just $ VConstant (I i)
253+ Just $ I i
267bfBin _ _ = Nothing
254bfBin _ _ = Nothing
268
255
269−bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value
256+bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
270−bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
257+bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
271− Just $ VConstant (I i)
258+ Just $ I i
272bcBin _ _ = Nothing
259bcBin _ _ = Nothing
273
260
274−bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value
261+bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
275−bsBin op [VConstant (Str x), VConstant (Str y)]
262+bsBin op [Str x, Str y]
276 = let i = (if op x y then 1 else 0) in
263 = let i = (if op x y then 1 else 0) in
277− Just $ VConstant (I i)
264+ Just $ I i
278bsBin _ _ = Nothing
265bsBin _ _ = Nothing
279
266
280−sBin :: (String -> String -> String) -> [Value] -> Maybe Value
267+sBin :: (String -> String -> String) -> [Const] -> Maybe Const
281−sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
268+sBin op [Str x, Str y] = Just $ Str (op x y)
282sBin _ _ = Nothing
269sBin _ _ = Nothing
283
270
284−bsrem :: IntTy -> [Value] -> Maybe Value
271+bsrem :: IntTy -> [Const] -> Maybe Const
285−bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]
272+bsrem IT8 [B8 x, B8 y]
286− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))
273+ = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))
287−bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]
274+bsrem IT16 [B16 x, B16 y]
288− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)))
275+ = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))
289−bsrem IT32 [VConstant (B32 x), VConstant (B32 y)]
276+bsrem IT32 [B32 x, B32 y]
290− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)))
277+ = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))
291−bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]
278+bsrem IT64 [B64 x, B64 y]
292− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)))
279+ = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))
293−bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))
280+bsrem ITNative [I x, I y] = Just $ I (x `rem` y)
294bsrem _ _ = Nothing
281bsrem _ _ = Nothing
295
282
296−bsdiv :: IntTy -> [Value] -> Maybe Value
283+bsdiv :: IntTy -> [Const] -> Maybe Const
297−bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]
284+bsdiv IT8 [B8 x, B8 y]
298− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))
285+ = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
299−bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]
286+bsdiv IT16 [B16 x, B16 y]
300− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)))
287+ = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
301−bsdiv IT32 [VConstant (B32 x), VConstant (B32 y)]
288+bsdiv IT32 [B32 x, B32 y]
302− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)))
289+ = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
303−bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]
290+bsdiv IT64 [B64 x, B64 y]
304− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)))
291+ = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
305−bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))
292+bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
306bsdiv _ _ = Nothing
293bsdiv _ _ = Nothing
307
294
308−bashr :: IntTy -> [Value] -> Maybe Value
295+bashr :: IntTy -> [Const] -> Maybe Const
309−bashr IT8 [VConstant (B8 x), VConstant (B8 y)]
296+bashr IT8 [B8 x, B8 y]
310− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))
297+ = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))
311−bashr IT16 [VConstant (B16 x), VConstant (B16 y)]
298+bashr IT16 [B16 x, B16 y]
312− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16)))
299+ = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))
313−bashr IT32 [VConstant (B32 x), VConstant (B32 y)]
300+bashr IT32 [B32 x, B32 y]
314− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32)))
301+ = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))
315−bashr IT64 [VConstant (B64 x), VConstant (B64 y)]
302+bashr IT64 [B64 x, B64 y]
316− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64)))
303+ = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))
317−bashr ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `shiftR` y))
304+bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)
318bashr _ _ = Nothing
305bashr _ _ = Nothing
319
306
320−bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Value] -> Maybe Value
307+bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const
321−bUn IT8 op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))
308+bUn IT8 op [B8 x] = Just $ B8 (op x)
322−bUn IT16 op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))
309+bUn IT16 op [B16 x] = Just $ B16 (op x)
323−bUn IT32 op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))
310+bUn IT32 op [B32 x] = Just $ B32 (op x)
324−bUn IT64 op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))
311+bUn IT64 op [B64 x] = Just $ B64 (op x)
325−bUn ITBig op [VConstant (BI x)] = Just $ VConstant (BI (op x))
312+bUn ITBig op [BI x] = Just $ BI (op x)
326−bUn ITNative op [VConstant (I x)] = Just $ VConstant (I (op x))
313+bUn ITNative op [I x] = Just $ I (op x)
327−bUn _ _ _ = Nothing
314+bUn _ _ _ = Nothing
328−
315+
329−bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Value] -> Maybe Value
316+bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const
330−bitBin IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))
317+bitBin IT8 op [B8 x, B8 y] = Just $ B8 (op x y)
331−bitBin IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))
318+bitBin IT16 op [B16 x, B16 y] = Just $ B16 (op x y)
332−bitBin IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))
319+bitBin IT32 op [B32 x, B32 y] = Just $ B32 (op x y)
333−bitBin IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))
320+bitBin IT64 op [B64 x, B64 y] = Just $ B64 (op x y)
334−bitBin ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
321+bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)
335−bitBin ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
322+bitBin ITNative op [I x, I y] = Just $ I (op x y)
336−bitBin _ _ _ = Nothing
323+bitBin _ _ _ = Nothing
337−
324+
338−bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Value] -> Maybe Value
325+bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Const] -> Maybe Const
339−bCmp IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
326+bCmp IT8 op [B8 x, B8 y] = Just $ 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))
327+bCmp IT16 op [B16 x, B16 y] = Just $ 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))
328+bCmp IT32 op [B32 x, B32 y] = Just $ 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))
329+bCmp IT64 op [B64 x, B64 y] = Just $ 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))
330+bCmp ITBig op [BI x, BI y] = Just $ 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))
331+bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)
345−bCmp _ _ _ = Nothing
332+bCmp _ _ _ = Nothing
346−
333+
347−toInt :: Integral a => IntTy -> a -> Value
334+toInt :: Integral a => IntTy -> a -> Const
348−toInt IT8 x = VConstant (B8 (fromIntegral x))
335+toInt IT8 x = B8 (fromIntegral x)
349−toInt IT16 x = VConstant (B16 (fromIntegral x))
336+toInt IT16 x = B16 (fromIntegral x)
350−toInt IT32 x = VConstant (B32 (fromIntegral x))
337+toInt IT32 x = B32 (fromIntegral x)
351−toInt IT64 x = VConstant (B64 (fromIntegral x))
338+toInt IT64 x = B64 (fromIntegral x)
352−toInt ITBig x = VConstant (BI (fromIntegral x))
339+toInt ITBig x = BI (fromIntegral x)
353−toInt ITNative x = VConstant (I (fromIntegral x))
340+toInt ITNative x = I (fromIntegral x)
354−
341+
355−intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value
342+intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const
356−intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x
343+intToInt IT8 out [B8 x] = Just $ toInt out x
357−intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x
344+intToInt IT16 out [B16 x] = Just $ toInt out x
358−intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x
345+intToInt IT32 out [B32 x] = Just $ toInt out x
359−intToInt IT64 out [VConstant (B64 x)] = Just $ toInt out x
346+intToInt IT64 out [B64 x] = Just $ toInt out x
360−intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x
347+intToInt ITBig out [BI x] = Just $ toInt out x
361−intToInt ITNative out [VConstant (I x)] = Just $ toInt out x
348+intToInt ITNative out [I x] = Just $ toInt out x
362intToInt _ _ _ = Nothing
349intToInt _ _ _ = Nothing
363
350
364−zext :: IntTy -> IntTy -> [Value] -> Maybe Value
351+zext :: IntTy -> IntTy -> [Const] -> Maybe Const
365zext from ITBig val = intToInt from ITBig val
352zext from ITBig val = intToInt from ITBig val
366zext ITBig _ _ = Nothing
353zext ITBig _ _ = Nothing
367zext from to val
354zext from to val
368 | intTyWidth from < intTyWidth to = intToInt from to val
355 | intTyWidth from < intTyWidth to = intToInt from to val
369zext _ _ _ = Nothing
356zext _ _ _ = Nothing
370
357
371−sext :: IntTy -> IntTy -> [Value] -> Maybe Value
358+sext :: IntTy -> IntTy -> [Const] -> Maybe Const
372−sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)
359+sext IT8 out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)
373−sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)
360+sext IT16 out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)
374−sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)
361+sext IT32 out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)
375−sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)
362+sext IT64 out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)
376−sext ITBig _ _ = Nothing
363+sext ITBig _ _ = Nothing
377−sext from to val = intToInt from to val
364+sext from to val = intToInt from to val
378
365
379−trunc :: IntTy -> IntTy -> [Value] -> Maybe Value
366+trunc :: IntTy -> IntTy -> [Const] -> Maybe Const
380trunc ITBig to val = intToInt ITBig to val
367trunc ITBig to val = intToInt ITBig to val
381trunc _ ITBig _ = Nothing
368trunc _ ITBig _ = Nothing
382trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
369trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
383trunc _ _ _ = Nothing
370trunc _ _ _ = Nothing
384
371
385−getInt :: [Value] -> Maybe Integer
372+getInt :: [Const] -> Maybe Integer
386−getInt [VConstant (B8 x)] = Just . toInteger $ x
373+getInt [B8 x] = Just . toInteger $ x
387−getInt [VConstant (B16 x)] = Just . toInteger $ x
374+getInt [B16 x] = Just . toInteger $ x
388−getInt [VConstant (B32 x)] = Just . toInteger $ x
375+getInt [B32 x] = Just . toInteger $ x
389−getInt [VConstant (B64 x)] = Just . toInteger $ x
376+getInt [B64 x] = Just . toInteger $ x
390−getInt [VConstant (I x)] = Just . toInteger $ x
377+getInt [I x] = Just . toInteger $ x
391−getInt [VConstant (BI x)] = Just x
378+getInt [BI x] = Just x
392−getInt _ = Nothing
379+getInt _ = Nothing
393−
380+
394−intToStr :: [Value] -> Maybe Value
381+intToStr :: [Const] -> Maybe Const
395−intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))
382+intToStr val | Just i <- getInt val = Just $ Str (show i)
396intToStr _ = Nothing
383intToStr _ = Nothing
397
384
398−strToInt :: IntTy -> [Value] -> Maybe Value
385+strToInt :: IntTy -> [Const] -> Maybe Const
399−strToInt ity [VConstant (Str x)] = case reads x of
386+strToInt ity [Str x] = case reads x of
400− [(n,"")] -> Just $ toInt ity (n :: Integer)
387+ [(n,"")] -> Just $ toInt ity (n :: Integer)
401− _ -> Just $ VConstant (I 0)
388+ _ -> Just $ I 0
402strToInt _ _ = Nothing
389strToInt _ _ = Nothing
403
390
404−intToFloat :: [Value] -> Maybe Value
391+intToFloat :: [Const] -> Maybe Const
405−intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))
392+intToFloat val | Just i <- getInt val = Just $ Fl (fromIntegral i)
406intToFloat _ = Nothing
393intToFloat _ = Nothing
407
394
408−floatToInt :: IntTy -> [Value] -> Maybe Value
395+floatToInt :: IntTy -> [Const] -> Maybe Const
409−floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)
396+floatToInt ity [Fl x] = Just $ toInt ity (truncate x :: Integer)
410floatToInt _ _ = Nothing
397floatToInt _ _ = Nothing
411
398
412−c_intToChar :: [Value] -> Maybe Value
399+c_intToChar, c_charToInt :: [Const] -> Maybe Const
413−c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
400+c_intToChar [(I x)] = Just . Ch . toEnum $ x
414c_intToChar _ = Nothing
401c_intToChar _ = Nothing
415−c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
402+c_charToInt [(Ch x)] = Just . I . fromEnum $ x
416c_charToInt _ = Nothing
403c_charToInt _ = Nothing
417
404
418−c_floatToStr :: [Value] -> Maybe Value
405+c_floatToStr :: [Const] -> Maybe Const
419−c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
406+c_floatToStr [Fl x] = Just $ Str (show x)
420c_floatToStr _ = Nothing
407c_floatToStr _ = Nothing
421−c_strToFloat [VConstant (Str x)] = case reads x of
408+c_strToFloat [Str x] = case reads x of
422− [(n,"")] -> Just $ VConstant (Fl n)
409+ [(n,"")] -> Just $ Fl n
423− _ -> Just $ VConstant (Fl 0)
410+ _ -> Just $ Fl 0
424c_strToFloat _ = Nothing
411c_strToFloat _ = Nothing
425
412
426−p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value
413+p_fPrim :: (Double -> Double) -> [Const] -> Maybe Const
427−p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
414+p_fPrim f [Fl x] = Just $ Fl (f x)
428p_fPrim f _ = Nothing
415p_fPrim f _ = Nothing
429
416
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
431p_floatExp = p_fPrim exp
418p_floatExp = p_fPrim exp
432p_floatLog = p_fPrim log
419p_floatLog = p_fPrim log
433p_floatSin = p_fPrim sin
420p_floatSin = p_fPrim sin
@@ -440,34 +427,23 @@ p_floatSqrt = p_fPrim sqrt
440p_floatFloor = p_fPrim (fromInteger . floor)
427p_floatFloor = p_fPrim (fromInteger . floor)
441p_floatCeil = p_fPrim (fromInteger . ceiling)
428p_floatCeil = p_fPrim (fromInteger . ceiling)
442
429
443−p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value
430+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const
444−p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
431+p_strLen [Str xs] = Just $ I (length xs)
445p_strLen _ = Nothing
432p_strLen _ = Nothing
446−p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
433+p_strHead [Str (x:xs)] = Just $ Ch x
447p_strHead _ = Nothing
434p_strHead _ = Nothing
448−p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
435+p_strTail [Str (x:xs)] = Just $ Str xs
449p_strTail _ = Nothing
436p_strTail _ = Nothing
450−p_strIndex [VConstant (Str xs), VConstant (I i)]
437+p_strIndex [Str xs, I i]
451− | i < length xs = Just $ VConstant (Ch (xs!!i))
438+ | i < length xs = Just $ Ch (xs!!i)
452p_strIndex _ = Nothing
439p_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)
454p_strCons _ = Nothing
441p_strCons _ = Nothing
455−p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
442+p_strRev [Str xs] = Just $ Str (reverse xs)
456p_strRev _ = Nothing
443p_strRev _ = Nothing
457
444
458p_cantreduce :: a -> Maybe b
445p_cantreduce :: a -> Maybe b
459p_cantreduce _ = Nothing
446p_cantreduce _ = Nothing
460
447
461−elabPrim :: Prim -> Idris ()
448+
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
473
449
src/Idris/Providers.hs−1
@@ -3,7 +3,6 @@ module Idris.Providers (providerTy, getProvided) where
3
3
4import Core.TT
4import Core.TT
5import Core.Evaluate
5import Core.Evaluate
6−import Core.Execute
7import Idris.AbsSyntax
6import Idris.AbsSyntax
8import Idris.AbsSyntaxTree
7import Idris.AbsSyntaxTree
9import Idris.Error
8import Idris.Error
src/Idris/REPL.hs+28−4
@@ -605,6 +605,8 @@ parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
605parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
605parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
606parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
606parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
607parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)
607parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)
608+parseArgs ["--exec"] = InterpretScript "Main.main" : []
609+parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
608parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)
610parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)
609parseArgs (n:ns) = Filename n : (parseArgs ns)
611parseArgs (n:ns) = Filename n : (parseArgs ns)
610
612
@@ -640,11 +642,16 @@ idrisMain opts =
640 let tgt = case opt getTarget opts of
642 let tgt = case opt getTarget opts of
641 [] -> ViaC
643 [] -> ViaC
642 xs -> last xs
644 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)
643 when (DefaultTotal `elem` opts) $ do i <- getIState
650 when (DefaultTotal `elem` opts) $ do i <- getIState
644 putIState (i { default_total = True })
651 putIState (i { default_total = True })
645 mapM_ addLangExt (opt getLanguageExt opts)
652 mapM_ addLangExt (opt getLanguageExt opts)
646 setREPL runrepl
653 setREPL runrepl
647− setQuiet quiet
654+ setQuiet (quiet || isJust script)
648 setIdeSlave idesl
655 setIdeSlave idesl
649 setVerbose runrepl
656 setVerbose runrepl
650 setCmdLine opts
657 setCmdLine opts
@@ -670,16 +677,19 @@ idrisMain opts =
670 elabPrims
677 elabPrims
671 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
678 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
672 return ()
679 return ()
673− when (runrepl && not quiet && not idesl) $ iputStrLn banner
680+ when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
674 ist <- getIState
681 ist <- getIState
675 mods <- mapM loadModule inputs
682 mods <- mapM loadModule inputs
676 ok <- noErrors
683 ok <- noErrors
677 when ok $ case output of
684 when ok $ case output of
678 [] -> return ()
685 [] -> return ()
679− (o:_) -> process "" (Compile tgt o)
686+ (o:_) -> process "" (Compile tgt o)
680 when ok $ case newoutput of
687 when ok $ case newoutput of
681 [] -> return ()
688 [] -> return ()
682− (o:_) -> process "" (NewCompile o)
689+ (o:_) -> process "" (NewCompile o)
690+ case script of
691+ Nothing -> return ()
692+ Just expr -> execScript expr
683 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
693 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
684 when (idesl) $ ideslaveStart ist inputs
694 when (idesl) $ ideslaveStart ist inputs
685 ok <- noErrors
695 ok <- noErrors
@@ -696,6 +706,16 @@ idrisMain opts =
696 addPkgDir p = do ddir <- liftIO $ getDataDir
706 addPkgDir p = do ddir <- liftIO $ getDataDir
697 addImportDir (ddir </> p)
707 addImportDir (ddir </> p)
698
708
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+
699getFile :: Opt -> Maybe String
719getFile :: Opt -> Maybe String
700getFile (Filename str) = Just str
720getFile (Filename str) = Just str
701getFile _ = Nothing
721getFile _ = Nothing
@@ -741,6 +761,10 @@ getTarget :: Opt -> Maybe Target
741getTarget (UseTarget x) = Just x
761getTarget (UseTarget x) = Just x
742getTarget _ = Nothing
762getTarget _ = Nothing
743
763
764+getExecScript :: Opt -> Maybe String
765+getExecScript (InterpretScript expr) = Just expr
766+getExecScript _ = Nothing
767+
744getOutputTy :: Opt -> Maybe OutputType
768getOutputTy :: Opt -> Maybe OutputType
745getOutputTy (OutputTy t) = Just t
769getOutputTy (OutputTy t) = Just t
746getOutputTy _ = Nothing
770getOutputTy _ = Nothing
src/Main.hs+2
@@ -91,6 +91,8 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++
91 "\t--log [level] Type debugging log level\n" ++
91 "\t--log [level] Type debugging log level\n" ++
92 "\t-S Do no further compilation of code generator output\n" ++
92 "\t-S Do no further compilation of code generator output\n" ++
93 "\t-c Compile to object files rather than an executable\n" ++
93 "\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" ++
94 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in s-expressions)\n" ++
96 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in s-expressions)\n" ++
95 "\t--libdir Show library install directory and exit\n" ++
97 "\t--libdir Show library install directory and exit\n" ++
96 "\t--link Show C library directories and exit (for C linking)\n" ++
98 "\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)
15import System.Environment
15import System.Environment
16import System.IO
16import System.IO
17import System.IO.Error
17import System.IO.Error
18−#if MIN_VERSION_base(4,0,0)
19import Control.Exception as CE
18import Control.Exception as CE
20−#endif
21
19
22import Paths_idris
20import Paths_idris
23
21
24−#if MIN_VERSION_base(4,0,0)
25catchIO :: IO a -> (IOError -> IO a) -> IO a
22catchIO :: IO a -> (IOError -> IO a) -> IO a
26catchIO = CE.catch
23catchIO = CE.catch
27
24
28throwIO :: IOError -> IO a
25throwIO :: IOError -> IO a
29throwIO = CE.throw
26throwIO = CE.throw
30−#else
31−catchIO = catch
32−throwIO = throw
33−#endif
34
27
35
28
36
29