added Float.floor, Int.truncate0, Nat.mod

This commit is contained in:
Paul Chiusano 2018-11-18 15:15:15 -05:00
parent 77ed922047
commit ee94a0c013
2 changed files with 14 additions and 0 deletions

View File

@ -132,12 +132,14 @@ builtins0 = Map.fromList $
, ("Int.is-odd", "Int -> Boolean")
, ("Int.signum", "Int -> Int")
, ("Int.negate", "Int -> Int")
, ("Int.truncate0", "Int -> Nat")
, ("Nat.+", "Nat -> Nat -> Nat")
, ("Nat.drop", "Nat -> Nat -> Nat")
, ("Nat.sub", "Nat -> Nat -> Int")
, ("Nat.*", "Nat -> Nat -> Nat")
, ("Nat./", "Nat -> Nat -> Nat")
, ("Nat.mod", "Nat -> Nat -> Nat")
, ("Nat.<", "Nat -> Nat -> Boolean")
, ("Nat.>", "Nat -> Nat -> Boolean")
, ("Nat.<=", "Nat -> Nat -> Boolean")
@ -156,6 +158,7 @@ builtins0 = Map.fromList $
, ("Float.<=", "Float -> Float -> Boolean")
, ("Float.>=", "Float -> Float -> Boolean")
, ("Float.==", "Float -> Float -> Boolean")
, ("Float.floor", "Float -> Float -> Int")
, ("Boolean.not", "Boolean -> Boolean")

View File

@ -393,6 +393,9 @@ object Builtins {
val Int_negate =
fl_l("Int.negate", "x", -_)
val Int_truncate0 =
fl_l("Int.truncate0", "x", x => if (x < 0) 0 else x)
// Unsigned machine integers
def uint(n: Long): Term = Term.Unboxed(longToUnboxed(n), UnboxedType.Nat)
@ -429,6 +432,9 @@ object Builtins {
val Nat_div =
fnn_n("Nat./", "x", "y", java.lang.Long.divideUnsigned(_,_))
val Nat_mod =
fnn_n("Nat.mod", "x", "y", java.lang.Long.remainderUnsigned(_,_))
val Nat_eq =
fll_b("Nat.==", "x", "y", _ == _)
@ -479,6 +485,8 @@ object Builtins {
val Float_lt = fdd_b("Float.<", "x", "y", _ < _)
val Float_floor = fp_p("Float.floor", "x", (n: Float) => n.floor.toLong)
val numericBuiltins: Map[Name, Computation] = Map(
// arithmetic
Int_inc,
@ -490,6 +498,7 @@ object Builtins {
Int_div,
Int_signum,
Int_negate,
Int_truncate0,
Nat_toInt,
Nat_inc,
@ -500,11 +509,13 @@ object Builtins {
Nat_add,
Nat_sub,
Nat_div,
Nat_mod,
Float_add,
Float_sub,
Float_mul,
Float_div,
Float_floor,
// comparison
Int_eq,