Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

267 lines (176 sloc) 5.047 kB
%access public
data Exists : (a : Set) -> (P : a -> Set) -> Set where
Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P
getWitness : {P : a -> Set} -> Exists a P -> a
getWitness (a ** v) = a
getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s)
getProof (a ** v) = v
FalseElim : _|_ -> a
-- For rewrite tactic
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y
replace refl prf = prf
sym : {l:a} -> {r:a} -> l = r -> r = l
sym refl = refl
lazy : a -> a
lazy x = x -- compiled specially
malloc : Int -> a -> a
malloc size x = x -- compiled specially
trace_malloc : a -> a
trace_malloc x = x -- compiled specially
believe_me : a -> b -- compiled specially as id, use with care!
believe_me x = prim__believe_me _ _ x
namespace builtins {
id : a -> a
id x = x
const : a -> b -> a
const x _ = x
fst : (s, t) -> s
fst (x, y) = x
snd : (a, b) -> b
snd (x, y) = y
infixl 9 .
(.) : (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)
flip : (a -> b -> c) -> b -> a -> c
flip f x y = f y x
infixr 1 $
($) : (a -> b) -> a -> b
f $ a = f a
cong : {f : t -> u} -> (a = b) -> f a = f b
cong refl = refl
data Bool = False | True
boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a
boolElim True t e = t
boolElim False t e = e
data so : Bool -> Set where oh : so True
syntax if [test] then [t] else [e] = boolElim test t e
syntax [test] "?" [t] ":" [e] = if test then t else e
infixl 4 &&, ||
(||) : Bool -> Bool -> Bool
(||) False x = x
(||) True _ = True
(&&) : Bool -> Bool -> Bool
(&&) True x = x
(&&) False _ = False
not : Bool -> Bool
not True = False
not False = True
infixl 5 ==, /=
infixl 6 <, <=, >, >=
infixl 7 <<, >>
infixl 8 +,-,++
infixl 9 *,/
--- Numeric operators
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True
boolOp : (a -> a -> Int) -> a -> a -> Bool
boolOp op x y = intToBool (op x y)
class Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
x /= y = not (x == y)
x == y = not (x /= y)
instance Eq Int where
(==) = boolOp prim__eqInt
instance Eq Integer where
(==) = boolOp prim__eqBigInt
instance Eq Float where
(==) = boolOp prim__eqFloat
instance Eq Char where
(==) = boolOp prim__eqChar
instance Eq String where
(==) = boolOp prim__eqString
instance (Eq a, Eq b) => Eq (a, b) where
(==) (a, c) (b, d) = (a == b) && (c == d)
data Ordering = LT | EQ | GT
instance Eq Ordering where
LT == LT = True
EQ == EQ = True
GT == GT = True
_ == _ = False
class Eq a => Ord a where
compare : a -> a -> Ordering
(<) : a -> a -> Bool
(<) x y with (compare x y)
(<) x y | LT = True
(<) x y | _ = False
(>) : a -> a -> Bool
(>) x y with (compare x y)
(>) x y | GT = True
(>) x y | _ = False
(<=) : a -> a -> Bool
(<=) x y = x < y || x == y
(>=) : a -> a -> Bool
(>=) x y = x > y || x == y
max : a -> a -> a
max x y = if (x > y) then x else y
min : a -> a -> a
min x y = if (x < y) then x else y
instance Ord Int where
compare x y = if (x == y) then EQ else
if (boolOp prim__ltInt x y) then LT else
GT
instance Ord Integer where
compare x y = if (x == y) then EQ else
if (boolOp prim__ltBigInt x y) then LT else
GT
instance Ord Float where
compare x y = if (x == y) then EQ else
if (boolOp prim__ltFloat x y) then LT else
GT
instance Ord Char where
compare x y = if (x == y) then EQ else
if (boolOp prim__ltChar x y) then LT else
GT
instance Ord String where
compare x y = if (x == y) then EQ else
if (boolOp prim__ltString x y) then LT else
GT
instance (Ord a, Ord b) => Ord (a, b) where
compare (xl, xr) (yl, yr) =
if xl /= yl
then compare xl yl
else compare xr yr
class Num a where
(+) : a -> a -> a
(-) : a -> a -> a
(*) : a -> a -> a
abs : a -> a
fromInteger : Int -> a
instance Num Int where
(+) = prim__addInt
(-) = prim__subInt
(*) = prim__mulInt
fromInteger = id
abs x = if x<0 then -x else x
instance Num Integer where
(+) = prim__addBigInt
(-) = prim__subBigInt
(*) = prim__mulBigInt
abs x = if x<0 then -x else x
fromInteger = prim__intToBigInt
instance Num Float where
(+) = prim__addFloat
(-) = prim__subFloat
(*) = prim__mulFloat
abs x = if x<0 then -x else x
fromInteger = prim__intToFloat
div : Int -> Int -> Int
div = prim__divInt
(/) : Float -> Float -> Float
(/) = prim__divFloat
--- string operators
(++) : String -> String -> String
(++) = prim__concat
strHead : String -> Char
strHead = prim__strHead
strTail : String -> String
strTail = prim__strTail
strCons : Char -> String -> String
strCons = prim__strCons
strIndex : String -> Int -> Char
strIndex = prim__strIndex
reverse : String -> String
reverse = prim__strRev
}
Jump to Line
Something went wrong with that request. Please try again.