From a41ccd2f52130f5ca85391a25162c51aaf0b42c7 Mon Sep 17 00:00:00 2001 From: Henry <77937076+yung-turabian@users.noreply.github.com> Date: Tue, 18 Feb 2025 17:00:15 -0500 Subject: [PATCH] Fixed rules violations, more than just my own, and tests --- core/lib.ml | 12 ++++++------ core/transformSugar.ml | 2 +- core/typeSugar.ml | 6 +++--- lens/lens_format.mli | 9 ++++++--- lens/phrase.mli | 2 +- tests/numeric-operations.tests | 16 ++++++++++++++++ tests/unit/ir/schinks.mli | 6 +++--- 7 files changed, 36 insertions(+), 17 deletions(-) diff --git a/core/lib.ml b/core/lib.ml index d3862cf68..893874565 100644 --- a/core/lib.ml +++ b/core/lib.ml @@ -62,11 +62,11 @@ let string_op impl pure : located_primitive * Types.datatype * pure = let numeric_op impli implf purei puref : located_primitive * Types.datatype * pure = (`PFun (fun _ args -> match args with - | [x; y] -> + | [x; y] -> (match (x,y) with | (`Int _, `Int _) -> Lwt.return (`Int (impli (Value.unbox_int x) (Value.unbox_int y))) | (`Float _, `Float _) -> Lwt.return (`Float (implf (Value.unbox_float x) (Value.unbox_float y))) - | _ -> raise (runtime_type_error "type error in numeric operation")) + | _ -> raise (runtime_type_error "type error in numeric operation")) | _ -> raise (internal_error "arity error in numeric operation"))), datatype "(a::Numeric, a) -> a", F2 (fun l r -> match (l, r) with @@ -260,13 +260,13 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ "^^", string_op ( ^ ) PURE; - (* moved abs to make use of ad hoc ability, - ideally there could be a way to bootstrap prelude similar to #786 *) + (* moved abs to make use of ad hoc ability, + ideally there could be a way to bootstrap Prelude similar to #786 *) "abs", (p1 (fun n -> match n with | `Int _ -> Value.box_int ( let x = (Value.unbox_int n) in if x > 0 then x else -x ) | `Float _ -> Value.box_float ( let x = (Value.unbox_float n) in if x > 0.0 then x else -.x ) - | _ -> raise (runtime_type_error ("Cannot computer absolute value: " ^ Value.string_of_value n))), + | _ -> raise (runtime_type_error ("Cannot computer absolute value: " ^ Value.string_of_value n))), datatype "(a::Numeric) -> a", PURE); @@ -763,7 +763,7 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ (p1 (fun n -> match n with | `Int _ -> Value.box_int (- (Value.unbox_int n)) | `Float _ -> Value.box_float (-. (Value.unbox_float n)) - | _ -> raise (runtime_type_error ("Cannot negate: " ^ Value.string_of_value n))), + | _ -> raise (runtime_type_error ("Cannot negate: " ^ Value.string_of_value n))), datatype "(a::Numeric) -> a", PURE); diff --git a/core/transformSugar.ml b/core/transformSugar.ml index 01900a932..46df81eba 100644 --- a/core/transformSugar.ml +++ b/core/transformSugar.ml @@ -68,7 +68,7 @@ let type_binary_op env tycon_env = | Name "!" -> TyEnv.find "Send" env | Name "+" | Name "*" - | Name "/" + | Name "/" | Name "^" -> datatype "(a::Numeric, a) -> a" | Name n -> TyEnv.find n env diff --git a/core/typeSugar.ml b/core/typeSugar.ml index ae9109e57..2b2a0e49a 100644 --- a/core/typeSugar.ml +++ b/core/typeSugar.ml @@ -2021,9 +2021,9 @@ let type_binary_op pos ctxt = Function (Types.make_tuple_type [a; a], eff, Primitive Primitive.Bool), Usage.empty) | Name "!" -> add_empty_usages (Utils.instantiate ctxt.var_env "Send") - | Name "+" - | Name "*" - | Name "/" + | Name "+" + | Name "*" + | Name "/" | Name "^" -> add_empty_usages (datatype "(a::Numeric, a) -> a") | Name n -> try diff --git a/lens/lens_format.mli b/lens/lens_format.mli index faa7893d6..cafdb35ed 100644 --- a/lens/lens_format.mli +++ b/lens/lens_format.mli @@ -16,7 +16,8 @@ val pp_comma : unit fmt_fn (** Format a list as comma separated values. - Example: {[ + Example: + {[ Format.asprintf "%a" (Format.pp_comma_list Format.pp_print_int) [5, 6, 7] ]} @@ -26,7 +27,8 @@ val pp_comma_list : 'a fmt_fn -> 'a list fmt_fn (** Format a list of string as comma separated values. - Example: {[ + Example: + {[ Format.asprintf "%a" Format.pp_comma_string_list ["hello", "world"] ]} @@ -39,7 +41,8 @@ val pp_newline_list : 'a fmt_fn -> 'a list fmt_fn (** Pad a string so it has [length] characters. - Example: {[ + Example: + {[ Format.asprintf "%a - %s" (Format.pp_padded ~length:8 Format.pp_print_string) "hello" "world" ]} diff --git a/lens/phrase.mli b/lens/phrase.mli index ed917be26..652a7a60a 100644 --- a/lens/phrase.mli +++ b/lens/phrase.mli @@ -199,7 +199,7 @@ module Grouped_variables : sig Example: - When called on the set `{ A; A B; C D; }` with the cols `A B`, the + When called on the set `{! A; A B; C D; }` with the cols `A B`, the result is false because `A B` only occurs in groups without further variables. If it is called with cols `C`, then it returns true, because the group `C D` contains the column `D` in addition to the column `C`. *) diff --git a/tests/numeric-operations.tests b/tests/numeric-operations.tests index 65f65b3b1..abfa5f76a 100644 --- a/tests/numeric-operations.tests +++ b/tests/numeric-operations.tests @@ -82,3 +82,19 @@ stdout : inf : Float Float division by zero [2] (-1.0) / 0.0 stdout : -inf : Float + +Large floating-point numbers +1.0e308 + 1.0e308 +stdout : inf : Float + +Small floating-point numbers +1.0e-308 + 1.0e-308 +stdout : 2e-308 : Float + +Additive identity +5 + 0 +stdout : 5 : Int + +Multiplicative identity +5.0 * 1.0 +stdout : 5.0 : Float diff --git a/tests/unit/ir/schinks.mli b/tests/unit/ir/schinks.mli index c60ba604e..c9946ddfe 100644 --- a/tests/unit/ir/schinks.mli +++ b/tests/unit/ir/schinks.mli @@ -75,18 +75,18 @@ val fun_t : ?effects:Types.row t -> Types.typ t list -> Types.typ t -> Types.typ t (** Syntactic sugar for fun_t. - a .-->{e} b becomes Function(a,e,b). + a .-->{!e} b becomes Function(a,e,b). This operator is left-associative, use parantheses when nesting! *) val ( .-->{} ) : Types.typ t list -> Types.row t -> Types.typ t -> Types.typ t -(** Equivalent to {}-> in Links' syntactic sugar for function types +(** Equivalent to \{\}-> in Links' syntactic sugar for function types Shorthand for closed function types (using tuple for parameters) *) val fun_ct : Types.typ t list -> Types.typ t -> Types.typ t (** alias for fun_ct *) val ( |--> ) : Types.typ t list -> Types.typ t -> Types.typ t -(** Equivalent to {}~> in Links' syntactic sugar for function types *) +(** Equivalent to \{\}~> in Links' syntactic sugar for function types *) val wild_fun_ct : Types.typ t list -> Types.typ t -> Types.typ t (** alias for wild_fun_ct *)