(- x) negates a typed number, a type variable and a dyn, and a float's negation of zero is -0.0

This commit is contained in:
Joseph Ferano 2026-09-25 11:37:56 +07:00
parent 315125c677
commit 3cb6cebdbe
10 changed files with 88 additions and 22 deletions

View File

@ -143,8 +143,7 @@ CLOSED: [2026-09-25]
=f64-inf=, =f64-nan=, =f32-inf= and =f32-nan= are names the checker supplies =f64-inf=, =f64-nan=, =f32-inf= and =f32-nan= are names the checker supplies
(=Check.special_float=), reached only after every local, global and function has (=Check.special_float=), reached only after every local, global and function has
missed, so a program's own binding of one wins. Negative infinity is missed, so a program's own binding of one wins. Negative infinity is
=(- 0.0 f64-inf)=: the decision wrote =(- f64-inf)=, and there is no unary minus. =(- f64-inf)=. Rules out Clojure's =##Inf= reader literal.
Rules out Clojure's =##Inf= reader literal.
** DONE A u64 constant above 2^63 cannot be written in decimal ** DONE A u64 constant above 2^63 cannot be written in decimal
CLOSED: [2026-09-25] CLOSED: [2026-09-25]

View File

@ -2003,6 +2003,8 @@ let and_sentinel (x : Ast.expr) =
let rec literal_arith (e : Ast.expr) : int64 option = let rec literal_arith (e : Ast.expr) : int64 option =
match e.Ast.e with match e.Ast.e with
| Ast.Int n -> Some n | Ast.Int n -> Some n
| Ast.Call ({ Ast.e = Ast.Var "-"; _ }, [ x ]) ->
Option.map Int64.neg (literal_arith x)
| Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) -> | Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) ->
let step a b = let step a b =
match op with match op with
@ -6355,12 +6357,9 @@ and arity _ctx loc name n args =
Two is the floor, and the two missing cases are refused rather than Two is the floor, and the two missing cases are refused rather than
invented. Zero operands would have to mean an identity element, 0 for + and invented. Zero operands would have to mean an identity element, 0 for + and
1 for *, and a sum with no terms in it is a typo far more often than it is 1 for *, and a sum with no terms in it is a typo far more often than it is
an intent. One operand would have to mean negation for [-] and reciprocal an intent. One operand is refused for every operator but [-], whose one
for [/], and this language has no unary minus anywhere: the prelude writes operand form is negation and is [named_call]'s. For [/] it would be the
every negation as [(- 0 n)] or [(- 0.0 x)], and [(- x)] meaning something reciprocal, and integer division makes that a trap: [(/ 3)] would be 0.
else than the [-] two lines above it is a rule a reader has to carry rather
than see. Integer division makes the reciprocal worse still: [(/ 3)] would
be 0.
A one-operand comparison would have to be [true] — there is no pair to A one-operand comparison would have to be [true] — there is no pair to
disagree, and nothing for a lone value to be distinct from — and a test disagree, and nothing for a lone value to be distinct from — and a test
@ -6369,10 +6368,6 @@ and arity _ctx loc name n args =
and fold_arity loc name args = and fold_arity loc name args =
match args with match args with
| _ :: _ :: _ -> () | _ :: _ :: _ -> ()
| [ _ ] when String.equal name "-" ->
fail loc
"- takes two arguments or more, given 1 — there is no unary minus; \
write (- 0 x) to negate"
| [ _ ] when String.equal name "/" -> | [ _ ] when String.equal name "/" ->
fail loc fail loc
"/ takes two arguments or more, given 1 — there is no reciprocal; \ "/ takes two arguments or more, given 1 — there is no reciprocal; \
@ -7029,6 +7024,31 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| _ when (not qualified) && shadows_builtin ctx loc name -> | _ when (not qualified) && shadows_builtin ctx loc name ->
ordinary_call ctx ~want loc name args ordinary_call ctx ~want loc name args
(* ── arithmetic and comparison ─────────────────────────────────── *) (* ── arithmetic and comparison ─────────────────────────────────── *)
(* (- x) negates, Clojure's rule. A literal operand is the negative literal,
so it takes its type from the site as any literal does. A float is
subtracted from -0.0, which is exact negation — 0.0 - 0.0 would answer
+0.0 — and an integer from 0, which wraps as (- 0 x) does. *)
| "-" when List.length args = 1 ->
let x = List.hd args in
(match x.Ast.e with
| Ast.Int n when n <> Int64.min_int ->
check ctx ?want { Ast.e = Ast.Int (Int64.neg n); loc }
| Ast.Float v -> check ctx ?want { Ast.e = Ast.Float (-.v); loc }
| _ ->
let v = check ctx ?want:(numeric_want want) x in
if v.Tast.ty = Types.Dyn then
expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_neg" [ v; here loc ])
else begin
unconstrained ctx.env loc name ~needs:"numeric?" v.Tast.ty;
if not (Types.is_numeric v.Tast.ty || generic_ty v.Tast.ty) then
not_numeric name "numbers" v;
let zero =
match v.Tast.ty with
| Types.Float k -> mk loc v.Tast.ty (Tast.Float (-0.0, k))
| ty -> int_literal loc ~want:(Some ty) ~preds:ctx.env.tvpreds 0L
in
expect ctx loc ~want (mk loc v.Tast.ty (Tast.Prim (Tast.Sub, [ zero; v ])))
end)
| "+" | "-" | "*" | "/" -> | "+" | "-" | "*" | "/" ->
let p = match name with let p = match name with
| "+" -> Tast.Add | "-" -> Tast.Sub | "*" -> Tast.Mul | "+" -> Tast.Add | "-" -> Tast.Sub | "*" -> Tast.Mul
@ -10087,7 +10107,8 @@ let builtins : (string * string * string) list =
numeric types meet at the wider one when that cannot lose — i32 and i64 \ numeric types meet at the wider one when that cannot lose — i32 and i64 \
add at i64 — and i32 with u32 has no such type and is refused."); add at i64 — and i32 with u32 has no such type and is refused.");
("-", "- [numeric? ...] numeric?", ("-", "- [numeric? ...] numeric?",
"Difference, folded left: (- a b c) is ((a - b) - c)."); "Difference, folded left: (- a b c) is ((a - b) - c). With one operand, \
its negation: (- x).");
("*", "* [numeric? ...] numeric?", ("*", "* [numeric? ...] numeric?",
"Product, folded left over two or more operands of one numeric type."); "Product, folded left over two or more operands of one numeric type.");
("/", "/ [numeric? ...] numeric?", ("/", "/ [numeric? ...] numeric?",

View File

@ -4389,6 +4389,7 @@ declare i64 @flan_dyn_sub(i64, i64, ptr, i64)
declare i64 @flan_dyn_mul(i64, i64, ptr, i64) declare i64 @flan_dyn_mul(i64, i64, ptr, i64)
declare i64 @flan_dyn_div(i64, i64, ptr, i64) declare i64 @flan_dyn_div(i64, i64, ptr, i64)
declare i64 @flan_dyn_rem(i64, i64, ptr, i64) declare i64 @flan_dyn_rem(i64, i64, ptr, i64)
declare i64 @flan_dyn_neg(i64, ptr, i64)
declare i64 @flan_dyn_lt(i64, i64, ptr, i64) declare i64 @flan_dyn_lt(i64, i64, ptr, i64)
declare i64 @flan_dyn_le(i64, i64, ptr, i64) declare i64 @flan_dyn_le(i64, i64, ptr, i64)
declare i64 @flan_dyn_gt(i64, i64, ptr, i64) declare i64 @flan_dyn_gt(i64, i64, ptr, i64)

View File

@ -695,7 +695,7 @@ let source = {flan|
;; The floats are three questions and not two, which is why there is no ;; The floats are three questions and not two, which is why there is no
;; f32-min here to sit beside f32-max. ;; f32-min here to sit beside f32-max.
;; ;;
;; A float's least value is just the negation of its greatest — (- 0.0 f32-max) ;; A float's least value is just the negation of its greatest — (- f32-max)
;; — so a constant for it would say nothing the language cannot. What a caller ;; — so a constant for it would say nothing the language cannot. What a caller
;; actually reaches for under the name "min" is the smallest positive one, and ;; actually reaches for under the name "min" is the smallest positive one, and
;; that is a different number entirely. Naming it f32-min would make the two ;; that is a different number entirely. Naming it f32-min would make the two

View File

@ -1759,6 +1759,14 @@ flan_dyn flan_dyn_sub(flan_dyn a, flan_dyn b, const uint8_t *loc,
int64_t loclen) { int64_t loclen) {
return arith(loc, loclen, "-", a, b); return arith(loc, loclen, "-", a, b);
} }
/* (- x): an int wraps, as (- 0 x) does, and a float flips its sign, so the
* negation of 0.0 is -0.0 and not the 0.0 a subtraction from zero gives. */
flan_dyn flan_dyn_neg(flan_dyn a, const uint8_t *loc, int64_t loclen) {
if (!is_num(a)) trap1(loc, loclen, TYPE_TRAP, "-", "it takes a number", a);
if (flan_dyn_tag(a) == FLAN_DYN_TAG_INT)
return flan_dyn_from_i64((int64_t)(0 - (uint64_t)dyn_int_value(a)));
return flan_dyn_from_f64(-dyn_num_value(a));
}
flan_dyn flan_dyn_mul(flan_dyn a, flan_dyn b, const uint8_t *loc, flan_dyn flan_dyn_mul(flan_dyn a, flan_dyn b, const uint8_t *loc,
int64_t loclen) { int64_t loclen) {
return arith(loc, loclen, "*", a, b); return arith(loc, loclen, "*", a, b);

View File

@ -151,6 +151,7 @@ flan_dyn flan_dyn_sub(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen
flan_dyn flan_dyn_mul(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen); flan_dyn flan_dyn_mul(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen);
flan_dyn flan_dyn_div(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen); flan_dyn flan_dyn_div(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen);
flan_dyn flan_dyn_rem(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen); flan_dyn flan_dyn_rem(flan_dyn a, flan_dyn b, const uint8_t *loc, int64_t loclen);
flan_dyn flan_dyn_neg(flan_dyn a, const uint8_t *loc, int64_t loclen);
/* Answer a bool dyn. Numbers compare as numbers and text compares bytewise; /* Answer a bool dyn. Numbers compare as numbers and text compares bytewise;
* a mixture of the two, or anything else, traps. */ * a mixture of the two, or anything else, traps. */

View File

@ -119,17 +119,17 @@
;; the absence is recorded rather than merely unmentioned: a float's least ;; the absence is recorded rather than merely unmentioned: a float's least
;; value is the negation of its greatest, and there is nothing to derive. ;; value is the negation of its greatest, and there is nothing to derive.
(say "f32's least value negates its greatest" (say "f32's least value negates its greatest"
(< (- (f32 0.0) f32-max) (- (f32 0.0) f32-min-positive))) (< (- f32-max) (- f32-min-positive)))
(say "f64's least value negates its greatest" (say "f64's least value negates its greatest"
(< (- 0.0 f64-max) (- 0.0 f64-min-positive))) (< (- f64-max) (- f64-min-positive)))
;; The infinities and NaNs, which no literal writes. Each infinity is the ;; The infinities and NaNs, which no literal writes. Each infinity is the
;; overflow of its type's greatest value, negated it is below the least ;; overflow of its type's greatest value, negated it is below the least
;; finite one, and a NaN is the one value not equal to itself. ;; finite one, and a NaN is the one value not equal to itself.
(say "f64-inf" (= f64-inf (* f64-max 2.0))) (say "f64-inf" (= f64-inf (* f64-max 2.0)))
(say "f32-inf" (= f32-inf (* f32-max (f32 2.0)))) (say "f32-inf" (= f32-inf (* f32-max (f32 2.0))))
(say "f64-inf negated" (< (- 0.0 f64-inf) (- 0.0 f64-max))) (say "f64-inf negated" (< (- f64-inf) (- f64-max)))
(say "f32-inf negated" (< (- (f32 0.0) f32-inf) (- (f32 0.0) f32-max))) (say "f32-inf negated" (< (- f32-inf) (- f32-max)))
(say "f64-nan" (not (= f64-nan f64-nan))) (say "f64-nan" (not (= f64-nan f64-nan)))
(say "f32-nan" (not (= f32-nan f32-nan))) (say "f32-nan" (not (= f32-nan f32-nan)))
;; != is the one unordered comparison: a NaN is unequal to everything, ;; != is the one unordered comparison: a NaN is unequal to everything,

25
test/programs/negate.flan Normal file
View File

@ -0,0 +1,25 @@
;;;; (- x) negates: an integer wraps, a float flips its sign — the negation of
;;;; 0.0 is -0.0, which 1/x tells apart — and a dyn does either by its tag.
(defn negi [x i32] i32 (- x))
(defn negf [x f64] f64 (- x))
(defn negf32 [x f32] f32 (- x))
(defn negu [x u8] u8 (- x))
(defn negd [x dyn] dyn (- x))
(defn negg [x $t] $t {:where (numeric? $t)} (- x))
(defn main [] i32
(println (negi 3))
(println (negi -7))
(println (negf 2.5))
(println (/ 1.0 (negf 0.0)))
(println (negf32 (f32 1.5)))
(println (negu (u8 1)))
(println (negd 4))
(println (negd 2.5))
(println (/ 1.0 (negd 0.0)))
(println (negg (i64 9000000000)))
(println (negg 0.5))
(let [a (- 5) b (i64 (- 3))]
(println (+ a (i32 b))))
(println (- f64-inf))
(println (< (- f64-inf) (- f64-max)))
0)

View File

@ -558,6 +558,13 @@ let () =
"programs/array-first-element.flan" first_out; "programs/array-first-element.flan" first_out;
outputs ~x86:true "an array literal's first element types the rest, x86" outputs ~x86:true "an array literal's first element types the rest, x86"
"programs/array-first-element.flan" first_out; "programs/array-first-element.flan" first_out;
(* (- x) negates, on every numeric type, a type variable and a dyn. *)
let neg_out =
"-3\n7\n-2.5\n-inf\n-1.5\n255\n-4\n-2.5\n-inf\n-9000000000\n\
-0.5\n-8\n-inf\ntrue\n" in
outputs "unary minus" "programs/negate.flan" neg_out;
outputs ~opt:"-O0" "unary minus, -O0" "programs/negate.flan" neg_out;
outputs ~x86:true "unary minus, x86" "programs/negate.flan" neg_out;
(* A literal arm takes the other arm's type. *) (* A literal arm takes the other arm's type. *)
let arm_out = let arm_out =
"4000000\n9000000000\n5000000000\n7\n9000000000\n3\n9000000000\n2.5\n" in "4000000\n9000000000\n5000000000\n7\n9000000000\n3\n9000000000\n2.5\n" in

View File

@ -1300,14 +1300,18 @@ let () =
infers "min at four" "(min 4 1 3 2)" "i32"; infers "min at four" "(min 4 1 3 2)" "i32";
infers "max at four" "(max 4 1 3 2)" "i32"; infers "max at four" "(max 4 1 3 2)" "i32";
(* And the two counts below the floor. Zero would have to mean an identity (* And the two counts below the floor. Zero would have to mean an identity
element and one a unary operator this language does not have; both are a element, and one is refused for every operator but -, whose one-operand
typo far more often than an intent, so both are refused by name. *) form negates. *)
rejects_check "a sum with no terms" rejects_check "a sum with no terms"
"(defn f [] i32 (+))" ~needle:"+ takes two arguments or more, given 0"; "(defn f [] i32 (+))" ~needle:"+ takes two arguments or more, given 0";
rejects_check "a product with no factors" rejects_check "a product with no factors"
"(defn f [] i32 (*))" ~needle:"* takes two arguments or more, given 0"; "(defn f [] i32 (*))" ~needle:"* takes two arguments or more, given 0";
rejects_check "there is no unary minus" infers "a negated literal" "(- 1)" "i32";
"(defn f [] i32 (- 1))" ~needle:"there is no unary minus"; infers "a negated literal takes its type from the site" "(i64 (- 1))" "i64";
rejects_check "unary minus over a string names the operand"
"(defn f [s string] () (println (- s)))" ~needle:"- takes numbers";
rejects_check "unary minus at an unsigned literal is out of range"
"(defn f [] u8 (- 1))" ~needle:"does not fit in u8";
rejects_check "there is no reciprocal" rejects_check "there is no reciprocal"
"(defn f [] f64 (/ 2.0))" ~needle:"there is no reciprocal"; "(defn f [] f64 (/ 2.0))" ~needle:"there is no reciprocal";
rejects_check "one operand is not a bitwise and" rejects_check "one operand is not a bitwise and"