From 7a2b101f58c34e32927b9ba63eac46dd06944d2e Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Thu, 11 Mar 2021 10:44:22 +0100 Subject: [PATCH 1/3] Add a nums stdlib --- src/stdlib.rs | 3 ++- stdlib/nums.ncl | 64 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 66 insertions(+), 1 deletion(-) create mode 100644 stdlib/nums.ncl diff --git a/src/stdlib.rs b/src/stdlib.rs index 4ce0f371..89e5d7fb 100644 --- a/src/stdlib.rs +++ b/src/stdlib.rs @@ -13,10 +13,11 @@ pub const CONTRACTS: (&str, &str) = ( ); pub const LISTS: (&str, &str) = ("", include_str!("../stdlib/lists.ncl")); pub const RECORDS: (&str, &str) = ("", include_str!("../stdlib/records.ncl")); +pub const NUMS: (&str, &str) = ("", include_str!("../stdlib/nums.ncl")); /// Return the list `(name, source_code)` of all the stdlib modules. pub fn modules() -> Vec<(&'static str, &'static str)> { - vec![BUILTINS, CONTRACTS, LISTS, RECORDS] + vec![BUILTINS, CONTRACTS, LISTS, RECORDS, NUMS] } /// Accessors to the builtin contracts. diff --git a/stdlib/nums.ncl b/stdlib/nums.ncl new file mode 100644 index 00000000..446409a4 --- /dev/null +++ b/stdlib/nums.ncl @@ -0,0 +1,64 @@ +{ + nums = { + Int = fun label value => + if %isNum% value then + if value % 1 == 0 then + value + else + %blame% (%tag% "not an integer" label) + else + %blame% (%tag% "not a number" label); + + Nat = fun label value => + if %isNum% value then + if value % 1 == 0 && value >= 0 then + value + else + %blame% (%tag% "not a natural" label) + else + %blame% (%tag% "not a number" label); + + PosInt = fun label value => + if %isNum% value then + if value % 1 == 0 && value > 0 then + value + else + %blame% (%tag% "not a positive integer" label) + else + %blame% (%tag% "not a number" label); + + NonZero = fun label value => + if %isNum% value then + if value != 0 then + value + else + %blame% (%tag% "non-zero" label) + else + %blame% (%tag% "not a number" label); + + min : Num -> Num -> Num = fun x y => + if x <= y then x else y; + + max : Num -> Num -> Num = fun x y => + if x >= y then x else y; + + floor : Num -> Num = fun x => + x - 1 + (x % 1); + + abs : Num -> Num = fun x => + if x < 0 then -x else x; + + frac : Num -> Num = fun x => + x % 1; + + trunc : Num -> Num = fun x => + if x > 0 then x - (x % 1) + else x + (x % 1); + + pow : Num -> Num -> Num = fun x n => + %pow% x n; + + isInt : Num -> Bool => fun x => + %isNum% x && (x % 1 == 0) + } +} From b23df115a1ce915f23a076839aeced696150e2b9 Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Thu, 11 Mar 2021 11:10:55 +0100 Subject: [PATCH 2/3] Add the pow primop --- src/grammar.lalrpop | 2 ++ src/operation.rs | 30 ++++++++++++++++++++++++++++++ src/parser/lexer.rs | 2 ++ src/term.rs | 2 ++ src/typecheck.rs | 5 +++++ 5 files changed, 41 insertions(+) diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop index 84b7f091..8381216f 100644 --- a/src/grammar.lalrpop +++ b/src/grammar.lalrpop @@ -455,6 +455,7 @@ BOpPre: BinaryOp = { "hash" => BinaryOp::Hash(), "serialize" => BinaryOp::Serialize(), "deserialize" => BinaryOp::Deserialize(), + "pow" => BinaryOp::Pow(), } Types: Types = { @@ -627,6 +628,7 @@ extern { "tail" => Token::Normal(NormalToken::Tail), "length" => Token::Normal(NormalToken::Length), "fieldsOf" => Token::Normal(NormalToken::FieldsOf), + "pow" => Token::Normal(NormalToken::Pow), "hasField" => Token::Normal(NormalToken::HasField), "map" => Token::Normal(NormalToken::Map), diff --git a/src/operation.rs b/src/operation.rs index 2d043e4f..d540272a 100644 --- a/src/operation.rs +++ b/src/operation.rs @@ -876,6 +876,36 @@ fn process_binary_operation( )) } } + BinaryOp::Pow() => { + if let Term::Num(n1) = *t1 { + if let Term::Num(n2) = *t2 { + Ok(Closure::atomic_closure(RichTerm::new( + Term::Num(n1.powf(n2)), + pos_op_inh, + ))) + } else { + Err(EvalError::TypeError( + String::from("Num"), + String::from("pow, 2nd argument"), + snd_pos, + RichTerm { + term: t2, + pos: pos2, + }, + )) + } + } else { + Err(EvalError::TypeError( + String::from("Num"), + String::from("pow, 1st argument"), + fst_pos, + RichTerm { + term: t1, + pos: pos1, + }, + )) + } + } BinaryOp::PlusStr() => { if let Term::Str(s1) = *t1 { if let Term::Str(s2) = *t2 { diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs index 45c1b5ff..9d55c7e9 100644 --- a/src/parser/lexer.rs +++ b/src/parser/lexer.rs @@ -193,6 +193,8 @@ pub enum NormalToken<'input> { Length, #[token("%fieldsOf%")] FieldsOf, + #[token("%pow%")] + Pow, #[token("%hasField%")] HasField, diff --git a/src/term.rs b/src/term.rs index 574e05f1..0fab4434 100644 --- a/src/term.rs +++ b/src/term.rs @@ -583,6 +583,8 @@ pub enum BinaryOp { Div(), /// Modulo of numerals. Modulo(), + /// Raise a number to a power. + Pow(), /// Concatenation of strings. PlusStr(), /// Polymorphic equality. diff --git a/src/typecheck.rs b/src/typecheck.rs index 17d1933d..c2534cfc 100644 --- a/src/typecheck.rs +++ b/src/typecheck.rs @@ -1707,6 +1707,11 @@ pub fn get_bop_type(state: &mut State, op: &BinaryOp) -> Result mk_tyw_arrow!( + mk_typewrapper::num(), + mk_typewrapper::num(), + mk_typewrapper::num() + ), }) } From 16b02c60c70f5a8c0229b8bdcd30db879c80759e Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Thu, 11 Mar 2021 11:11:18 +0100 Subject: [PATCH 3/3] Fixes in the nums stdlib --- stdlib/nums.ncl | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/stdlib/nums.ncl b/stdlib/nums.ncl index 446409a4..8b8efd58 100644 --- a/stdlib/nums.ncl +++ b/stdlib/nums.ncl @@ -18,12 +18,12 @@ else %blame% (%tag% "not a number" label); - PosInt = fun label value => + PosNat = fun label value => if %isNum% value then if value % 1 == 0 && value > 0 then value else - %blame% (%tag% "not a positive integer" label) + %blame% (%tag% "not positive integer" label) else %blame% (%tag% "not a number" label); @@ -36,6 +36,9 @@ else %blame% (%tag% "not a number" label); + isInt : Num -> Bool = fun x => + %isNum% x && (x % 1 == 0); + min : Num -> Num -> Num = fun x y => if x <= y then x else y; @@ -43,22 +46,19 @@ if x >= y then x else y; floor : Num -> Num = fun x => - x - 1 + (x % 1); + if x >= 0 then x - (x % 1) + else x - 1 - (x % 1); abs : Num -> Num = fun x => if x < 0 then -x else x; - frac : Num -> Num = fun x => + fract : Num -> Num = fun x => x % 1; trunc : Num -> Num = fun x => - if x > 0 then x - (x % 1) - else x + (x % 1); + x - (x % 1); pow : Num -> Num -> Num = fun x n => %pow% x n; - - isInt : Num -> Bool => fun x => - %isNum% x && (x % 1 == 0) } }