idris-0.1.7: lib/prelude.idr

-- malloc evaluates an expression using a manual allocator, allocating 'bytes'
-- Needs to be compiled specially, naturally.

malloc : Int -> a -> a;
malloc bytes val = val;

%freeze malloc;

-- Used by the 'believe' tactic to make a temporary proof. Programs
-- using this are not to be trusted! (Or maybe use externally trusted code)
-- Generate a refl so that __eq_repl can reduce.

__Suspend_Disbelief : (m:A) -> (n:A) -> (n = m);
__Suspend_Disbelief m n = __Prove_Anything _ _ (refl n);

flip : (a -> b -> c) -> b -> a -> c;
flip f x y = f y x;

infixl 5 ==, /=, ==.;
infixl 6 <, <=, >, >=, <., <=., >., >=.;
infixl 7 <<, >>;
infixl 8 +,-,++,+.,-.;
infixl 9 *,/,*.,/.;

-- Integer primitives

(+) : Int -> Int -> Int; [inline]
(+) x y = __addInt x y;

(-) : Int -> Int -> Int; [inline]
(-) x y = __subInt x y;

(*) : Int -> Int -> Int; [inline]
(*) x y = __mulInt x y;

(/) : Int -> Int -> Int; [inline]
(/) x y = __divInt x y;

mod : Int -> Int -> Int; [inline]
mod x y = __modInt x y;

(<) : Int -> Int -> Bool; [inline]
(<) x y = __intlt x y;

(<=) : Int -> Int -> Bool; [inline]
(<=) x y = __intleq x y;

(>) : Int -> Int -> Bool; [inline]
(>) x y = __intgt x y;

(>=) : Int -> Int -> Bool; [inline]
(>=) x y = __intgeq x y;

(==) : Int -> Int -> Bool; [inline]
(==) x y = __eq x y;

(/=) : Int -> Int -> Bool; [inline]
(/=) x y = not (__eq x y);

(<<) : Int -> Int -> Int; [inline]
(<<) x y = __shl x y;

(>>) : Int -> Int -> Int; [inline]
(>>) x y = __shr x y;

-- Floating point primitives

(+.) : Float -> Float -> Float; [inline]
(+.) x y = __addFloat x y;

(-.) : Float -> Float -> Float; [inline]
(-.) x y = __subFloat x y;

(*.) : Float -> Float -> Float; [inline]
(*.) x y = __mulFloat x y;

(/.) : Float -> Float -> Float; [inline]
(/.) x y = __divFloat x y;

(<.) : Float -> Float -> Bool; [inline]
(<.) x y = __floatlt x y;

(<=.) : Float -> Float -> Bool; [inline]
(<=.) x y = __floatleq x y;

(>.) : Float -> Float -> Bool; [inline]
(>.) x y = __floatgt x y;

(>=.) : Float -> Float -> Bool; [inline]
(>=.) x y = __floatgeq x y;

(==.) : Float -> Float -> Bool; [inline]
(==.) x y = __feq x y;

-- String primitives

(++) : String -> String -> String; [inline]
(++) x y = __concat x y;


-- Function composition

infixl 9 .;

(.) : (b -> c) -> (a -> b) -> a -> c;
(.) f g x = f (g x);

fst : (a & b) -> a; [inline]
fst (x, y) = x;

snd : (a & b) -> b; [inline]
snd (x, y) = y;

include "nat.idr";
include "maybe.idr";
include "io.idr";
include "either.idr";
include "tactics.idr";
include "vect.idr";
include "string.idr";