Merge branch 'worktree-agent-a1a1e7420cccc5fa6' into dev-loop
# Conflicts: # FIX.org
This commit is contained in:
commit
b98108791d
88
FIX.org
88
FIX.org
@ -5198,3 +5198,91 @@ Anything that pinned a hash re-pins it once.
|
||||
and even ~(u64 2935910691)~ are refused for not fitting in an i32, while the
|
||||
literal written straight into a u64 operand is fine. That is why the
|
||||
multiplier sits in the multiply rather than in a let.
|
||||
|
||||
* Chained comparisons, 2026-09-21
|
||||
|
||||
From the game, at sand.flan:45:7:
|
||||
|
||||
: < takes 2 arguments, given 3
|
||||
|
||||
and the ruling:
|
||||
|
||||
#+begin_quote
|
||||
dispatch an agent that's going to do a pass through the stdlib and make
|
||||
functions variadic, lisp style. We should have +, *, -, and < > et all should
|
||||
be variadic
|
||||
#+end_quote
|
||||
|
||||
Most of that was already true. [+ - * /], [bit-and], [bit-or], [bit-xor],
|
||||
[min] and [max] have taken two operands or more since [fold_left_prim] went
|
||||
in; the six comparisons had not, and they are the ones the game hit. So the
|
||||
change is one arm: [= != < <= > >=] take two operands or more, [= < <= > >=]
|
||||
chaining and [!=] asking about every pair — the ruling below.
|
||||
|
||||
(< a b c) asks whether a is below b and b is below c. The left fold the
|
||||
folding operators use would compare a bool against a number, so there was
|
||||
never a second reading to choose between.
|
||||
|
||||
The middle operand is the whole of the difficulty. Two links name it, and the
|
||||
spelling anyone would reach for by hand — (and (< a b) (< b c)) — evaluates it
|
||||
twice, which is wrong the moment it is a call. So the chain binds every
|
||||
operand to a slot first, in source order, and compares the slots. The links
|
||||
then stop early with nothing observable riding on it: by the time any link
|
||||
runs, every operand has already been evaluated.
|
||||
|
||||
The refusals stayed refusals. (< x) would have to be true whatever it was
|
||||
handed, which is a typo that carries a value, so it is refused beside (+) and
|
||||
(- x) — see the note above [fold_arity] for why those two are refused, which
|
||||
this follows rather than reopens. Lisp answers true there; this language does
|
||||
not, and the message says what to write instead.
|
||||
|
||||
[%] and the shifts are still two operands, for the reasons already written
|
||||
against them: a chain of remainders has no agreed reading, and (<< x 30 30)
|
||||
would be two legal shifts that between them shift the value away.
|
||||
|
||||
There is no three-way join, and none was invented. The first pair joins the
|
||||
way any pair of operands joins — the widening rule of 2026-09-20 — and every
|
||||
operand after it is checked against the type that join produced, so a third
|
||||
operand that does not fit is refused the way a second one would be. That is
|
||||
[fold_left_prim]'s rule exactly, and the comparisons now answer the question
|
||||
the same way the arithmetic does rather than a second way of their own.
|
||||
|
||||
!= was built as a chain first and the author ruled against it:
|
||||
|
||||
#+begin_quote
|
||||
adjacent chaining makes little sense to me, (!= 1 2 1) should be false
|
||||
#+end_quote
|
||||
|
||||
So != is all-distinct, Common Lisp's /=: (!= a b c) is true when every operand
|
||||
differs from every other. The other five keep adjacent chaining.
|
||||
|
||||
The two differ because they are different questions. Asking whether a sequence
|
||||
is increasing is a question about neighbours — c has nothing to say about a,
|
||||
and (< a b c) is done when it has looked at two pairs. Asking whether a set of
|
||||
values are all different is a question about the set, and the pair chaining
|
||||
would never look at, first against last, is exactly the one (!= 1 2 1) turns
|
||||
on. Only the first question is a chain.
|
||||
|
||||
The cost of that is pairwise: n operands means n(n-1)/2 comparisons rather
|
||||
than n-1. Fine at the sizes anyone writes — four operands is six compares of
|
||||
values already sitting in slots — and invisible to every program there is
|
||||
today, because at two operands the two readings are one pair and the
|
||||
two-operand form does not go through the n-ary lowering at all. It emits what
|
||||
it always did.
|
||||
|
||||
Single evaluation is unchanged by the switch, and is the reason the pairwise
|
||||
reading costs nothing worse than compares: every operand is in its slot before
|
||||
any pair is looked at, so the extra pairs read slots. The conjunction still
|
||||
stops at the first pair that fails, having already run everything.
|
||||
|
||||
The slots are slots of whatever type the operands have, which strings are what
|
||||
says: = and != admit them and the orderings do not, so (= "a" "a" "a") is the
|
||||
one row here that is not about machine words. A dyn ordering carries the trap
|
||||
site every pair of it, because the whole comparison is written at one place
|
||||
and a trap from any of its pairs happened there.
|
||||
|
||||
test/programs/chain.flan, on both backends and at -O0 and -O2. What it asserts
|
||||
that a checker test cannot is the tag transcripts: a chain whose first link is
|
||||
already false still prints abc, a != whose *first* pair already says no still
|
||||
prints abcd, and the call counts (10, 12, 15) are what an operand evaluated
|
||||
once per pair that names it would break — the 12 would be 24.
|
||||
|
||||
167
lib/check.ml
167
lib/check.ml
@ -5695,11 +5695,13 @@ and arity _ctx loc name n args =
|
||||
fail loc "%s takes %d argument%s, given %d" name n
|
||||
(if n = 1 then "" else "s") (List.length args)
|
||||
|
||||
(* The operators that fold: [+ - * /], [min]/[max] and the three bitwise
|
||||
combining operators all take two operands or more, and mean the same thing
|
||||
applied left to right. [%] and the shifts are not in that set — a chain of
|
||||
remainders or of shifts has no reading a reader would agree on in advance,
|
||||
so there the arity error is the useful answer.
|
||||
(* The operators that take two operands or more: [+ - * /], [min]/[max], the
|
||||
three bitwise combining operators, and the six comparisons. The first ten
|
||||
fold left; the ordered comparisons chain and [!=] asks about every pair,
|
||||
which [cmp_over] and the two pair-pickers under it explain. [%] and the
|
||||
shifts are not in that set — a chain of remainders or of shifts has no
|
||||
reading a reader would agree on in advance, so there the arity error is the
|
||||
useful answer.
|
||||
|
||||
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
|
||||
@ -5708,7 +5710,13 @@ and arity _ctx loc name n args =
|
||||
for [/], and this language has no unary minus anywhere: the prelude writes
|
||||
every negation as [(- 0 n)] or [(- 0.0 x)], and [(- x)] meaning something
|
||||
else than the [-] two lines above it is a rule a reader has to carry rather
|
||||
than see. *)
|
||||
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
|
||||
disagree, and nothing for a lone value to be distinct from — and a test
|
||||
that is true whatever it is handed is a typo with a value, which is the
|
||||
worst kind. So it is refused here with the rest. *)
|
||||
and fold_arity loc name args =
|
||||
match args with
|
||||
| _ :: _ :: _ -> ()
|
||||
@ -5720,9 +5728,21 @@ and fold_arity loc name args =
|
||||
fail loc
|
||||
"/ takes two arguments or more, given 1 — there is no reciprocal; \
|
||||
write (/ 1.0 x)"
|
||||
| [ _ ] when String.equal name "!=" ->
|
||||
fail loc
|
||||
"!= takes two arguments or more, given 1 — a test for distinctness \
|
||||
needs something to be distinct from, as in (!= x y)"
|
||||
| [ _ ] when is_comparison name ->
|
||||
fail loc
|
||||
"%s takes two arguments or more, given 1 — a comparison needs a second \
|
||||
value to compare against, as in (%s x y)" name name
|
||||
| _ ->
|
||||
fail loc "%s takes two arguments or more, given %d" name (List.length args)
|
||||
|
||||
and is_comparison = function
|
||||
| "=" | "!=" | "<" | "<=" | ">" | ">=" -> true
|
||||
| _ -> false
|
||||
|
||||
(* The first two operands decide the type — [binary] picks which of them is
|
||||
allowed to, and that decision is not re-made per pair — and every operand
|
||||
after them is checked against it. *)
|
||||
@ -5872,6 +5892,61 @@ and dyn_fold ctx ~want loc name first rest =
|
||||
in
|
||||
expect ctx loc ~want acc
|
||||
|
||||
(* A comparison over three operands or more asks about more than one pair, and
|
||||
every operand is bound to a slot before any pair is looked at. That is what
|
||||
makes "left to right, exactly once" true of the lowering and not only of
|
||||
the source: an operand two pairs name is written down once. The spelling a
|
||||
reader would reach for, [(and (< a b) (< b c))], evaluates b twice, which
|
||||
is wrong the moment b is a call — that is the whole reason this is a form
|
||||
the compiler builds rather than a macro.
|
||||
|
||||
The pairs are then required to hold, and the conjunction stops at the first
|
||||
one that does not. That costs nothing observable, because by the time any
|
||||
pair is compared every operand has already been evaluated — stopping skips
|
||||
a machine compare, never a call.
|
||||
|
||||
[pairs] says which pairs this operator asks about and [link] builds one
|
||||
comparison, so the two readings below and the dyn lowering of each are the
|
||||
same code with two arguments changed. *)
|
||||
and cmp_over ctx loc ty ~pairs ~link ops =
|
||||
let binds = List.map (fun (e : Tast.expr) -> fresh_slot ctx ty, e) ops in
|
||||
let locals = List.map (fun (s, _) -> mk loc ty (Tast.Local s)) binds in
|
||||
let rec conj = function
|
||||
| [ t ] -> t
|
||||
| t :: rest ->
|
||||
mk loc Types.Bool
|
||||
(Tast.If (t, conj rest, mk loc Types.Bool (Tast.Bool false)))
|
||||
| [] -> assert false
|
||||
in
|
||||
let tests = List.map (fun (a, b) -> link a b) (pairs locals) in
|
||||
mk loc Types.Bool (Tast.Let (binds, [ conj tests ]))
|
||||
|
||||
(* The ordered comparisons chain: [(< a b c)] asks whether a is below b and b
|
||||
is below c. The other reading, the left fold [(< (< a b) c)], compares a
|
||||
bool against a number, and there is no program that meant it. So the pairs
|
||||
are the adjacent ones, n-1 of them, and the operand in the middle is the
|
||||
one two of them share. *)
|
||||
and adjacent_pairs xs =
|
||||
match xs with
|
||||
| a :: (b :: _ as rest) -> (a, b) :: adjacent_pairs rest
|
||||
| _ -> []
|
||||
|
||||
(* [!=] is the one that does not chain. "Is this sequence increasing" and "are
|
||||
these values all different" are different questions, and only the first is
|
||||
about adjacent pairs: under chaining [(!= 1 2 1)] would be true, because
|
||||
each neighbour differs from the next, while the thing anyone means by it is
|
||||
false. So [!=] asks about *every* pair — Common Lisp's [/=] — which is
|
||||
n(n-1)/2 comparisons rather than n-1.
|
||||
|
||||
That growth is fine at the sizes anyone writes: four operands is six
|
||||
compares of values already in slots. It is also invisible to every program
|
||||
there is today, because two operands is one pair either way and does not
|
||||
come through here at all. *)
|
||||
and all_pairs xs =
|
||||
match xs with
|
||||
| [] -> []
|
||||
| x :: rest -> List.map (fun y -> (x, y)) rest @ all_pairs rest
|
||||
|
||||
(* ── Allocation failure, spec-memory.md ────────────────────────────────
|
||||
No allocating operation returns an error and none can fail silently. When
|
||||
the allocator cannot satisfy a request the operation signals
|
||||
@ -6284,8 +6359,21 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
| "=" -> Tast.Eq | "!=" -> Tast.Ne | "<" -> Tast.Lt
|
||||
| "<=" -> Tast.Le | ">" -> Tast.Gt | _ -> Tast.Ge
|
||||
in
|
||||
arity ctx loc name 2 args;
|
||||
let a, b = binary ctx ~dyn_ok:true name loc ~want:None args in
|
||||
fold_arity loc name args;
|
||||
let x, y, rest =
|
||||
match args with x :: y :: rest -> x, y, rest | _ -> assert false
|
||||
in
|
||||
(* The first pair decides the type, and whether this is a dyn comparison
|
||||
at all, exactly as it does for the folding operators: [binary] joins
|
||||
the two, and every operand after them is checked against the answer.
|
||||
Past the first pair nothing widens, which is [fold_left_prim]'s rule
|
||||
and not a second one. *)
|
||||
let a, b = binary ctx ~dyn_ok:true name loc ~want:None [ x; y ] in
|
||||
(* Which pairs this operator asks about. Every one but [!=] chains, and
|
||||
[!=] asks about all of them — see [all_pairs]. At two operands the two
|
||||
readings are one pair and the same answer, which is why the two-operand
|
||||
path below is the same code it always was. *)
|
||||
let pairs = if String.equal name "!=" then all_pairs else adjacent_pairs in
|
||||
(* A comparison with a dyn operand answers a *bool*, not a dyn, even though
|
||||
the runtime's own entry point answers a dyn holding one. The reason is
|
||||
where the result goes: a comparison is overwhelmingly the test of an
|
||||
@ -6307,18 +6395,30 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
| ">" -> "flan_dyn_gt" | _ -> "flan_dyn_ge"
|
||||
in
|
||||
(* [eq] never traps and takes no site; the four orderings do, and get
|
||||
one, for the reason [dyn_fold] gives. *)
|
||||
one, for the reason [dyn_fold] gives. Every pair of a chain gets the
|
||||
same site — the whole comparison is written at one place, and a trap
|
||||
from any of its pairs happened there. *)
|
||||
let site = if String.equal sym "flan_dyn_eq" then [] else [ here loc ] in
|
||||
let cmp =
|
||||
unbox loc Types.Bool
|
||||
(rt loc Types.Dyn sym ([ box loc a; box loc b ] @ site))
|
||||
in
|
||||
(* [!=] has no entry point of its own: there is one structural equality
|
||||
and the negation is an [i1] flip the backend folds away. *)
|
||||
let r =
|
||||
if String.equal name "!=" then mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ]))
|
||||
let link u v =
|
||||
let cmp =
|
||||
unbox loc Types.Bool (rt loc Types.Dyn sym ([ u; v ] @ site))
|
||||
in
|
||||
if String.equal name "!=" then
|
||||
mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ]))
|
||||
else cmp
|
||||
in
|
||||
let r =
|
||||
match rest with
|
||||
| [] -> link (box loc a) (box loc b)
|
||||
| _ ->
|
||||
let ops =
|
||||
box loc a :: box loc b
|
||||
:: map_lr (fun e -> box loc (check ctx ~want:Types.Dyn e)) rest
|
||||
in
|
||||
cmp_over ctx loc Types.Dyn ~pairs ~link ops
|
||||
in
|
||||
expect ctx loc ~want r
|
||||
end else begin
|
||||
(* [=] and [!=] admit types [<] does not. A handle is one: a pair of
|
||||
@ -6349,7 +6449,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
fail loc
|
||||
"%s orders machine numbers and enums, and %s is neither" name
|
||||
(Types.to_string a.Tast.ty));
|
||||
prim p Types.Bool [ a; b ]
|
||||
match rest with
|
||||
| [] -> prim p Types.Bool [ a; b ]
|
||||
| _ ->
|
||||
let ty = a.Tast.ty in
|
||||
let link u v = mk loc Types.Bool (Tast.Prim (p, [ u; v ])) in
|
||||
let ops = a :: b :: map_lr (fun e -> check ctx ~want:ty e) rest in
|
||||
expect ctx loc ~want (cmp_over ctx loc ty ~pairs ~link ops)
|
||||
end
|
||||
| "not" ->
|
||||
arity ctx loc name 1 args;
|
||||
@ -9114,18 +9220,23 @@ let builtins : (string * string * string) list =
|
||||
("%", "% [numeric? numeric?] numeric?",
|
||||
"Remainder, and it stays at two operands: (% a b c) would mean \
|
||||
(% (% a b) c), which is a thing nobody writes on purpose.");
|
||||
("=", "= [equal? equal?] bool",
|
||||
"Equality. It admits two types < does not: a handle, where \"the same \
|
||||
entity\" is the question the type exists to answer, and a string, \
|
||||
compared bytewise by content rather than ordered.");
|
||||
("!=", "!= [equal? equal?] bool",
|
||||
"Inequality, over everything = accepts.");
|
||||
("<", "< [ordered? ordered?] bool",
|
||||
"Less than. Machine numbers only: ordering a handle would order a \
|
||||
free-list slot index, which means nothing.");
|
||||
("<=", "<= [ordered? ordered?] bool", "Less than or equal.");
|
||||
(">", "> [ordered? ordered?] bool", "Greater than.");
|
||||
(">=", ">= [ordered? ordered?] bool", "Greater than or equal.");
|
||||
("=", "= [equal? ...] bool",
|
||||
"Equality, chained over two operands or more: (= a b c) is a = b and \
|
||||
b = c, which is every operand alike. It admits two types < does not: a \
|
||||
handle, where \"the same entity\" is the question the type exists to \
|
||||
answer, and a string, compared bytewise by content rather than \
|
||||
ordered.");
|
||||
("!=", "!= [equal? ...] bool",
|
||||
"All different: (!= a b c) is true when every operand differs from every \
|
||||
other, so (!= 1 2 1) is false. Over everything = accepts.");
|
||||
("<", "< [ordered? ...] bool",
|
||||
"Less than, chained: (< a b c) is a < b and b < c, and every operand is \
|
||||
evaluated once. Machine numbers and enums only — ordering a handle \
|
||||
would order a free-list slot index, which means nothing.");
|
||||
("<=", "<= [ordered? ...] bool", "Less than or equal, chained like <.");
|
||||
(">", "> [ordered? ...] bool", "Greater than, chained like <.");
|
||||
(">=", ">= [ordered? ...] bool",
|
||||
"Greater than or equal, chained like <.");
|
||||
("not", "not [bool] bool",
|
||||
"Negates a bool. Nothing else in this language is a truth value.");
|
||||
("bit-and", "bit-and [int ...] int",
|
||||
|
||||
173
test/programs/chain.flan
Normal file
173
test/programs/chain.flan
Normal file
@ -0,0 +1,173 @@
|
||||
;;;; Chained comparisons, and the property no checker test can assert: how
|
||||
;;;; many times each operand runs.
|
||||
;;;;
|
||||
;;;; (< a b c) means a < b and b < c. The reading a compiler could otherwise
|
||||
;;;; have picked, the left fold ((a < b) < c), compares a bool against a
|
||||
;;;; number and nothing means it. The interesting half is the middle operand:
|
||||
;;;; two links mention b, and the spelling a reader would write by hand,
|
||||
;;;; (and (< a b) (< b c)), evaluates it twice. So every operand here comes
|
||||
;;;; through [mark], which prints its tag, and the printed tags are what say
|
||||
;;;; each operand ran once and in source order.
|
||||
;;;;
|
||||
;;;; The folding operators are marked the same way, because "left to right,
|
||||
;;;; exactly once" is one claim and it is made about both families.
|
||||
|
||||
(defonce calls i32)
|
||||
|
||||
;; Prints its tag and answers its value. Every operand below is one of these,
|
||||
;; so the tag line is a transcript of the evaluation.
|
||||
(defn mark [tag string v i32] i32
|
||||
(set calls (+ calls 1))
|
||||
(print tag)
|
||||
v)
|
||||
|
||||
(defn markf [tag string v f64] f64
|
||||
(print tag)
|
||||
v)
|
||||
|
||||
;; A generic chain, admitted by the predicate its signature carries. The same
|
||||
;; three-link body as everything above, over a type the function does not know.
|
||||
(defn between [a $t b $t c $t] bool {:where (ordered? $t)}
|
||||
(< a b c))
|
||||
|
||||
;; Three unannotated parameters are three dyn ones, so this is the chain the
|
||||
;; runtime compares rather than the machine.
|
||||
(defn dyn-rising [a b c] bool
|
||||
(< a b c))
|
||||
|
||||
;; And the all-pairs reading over dyn operands, which asks the runtime the
|
||||
;; same question three times rather than twice.
|
||||
(defn dyn-distinct [a b c] bool
|
||||
(!= a b c))
|
||||
|
||||
;; Prints y when its two arguments agree and N when they do not. Two bools
|
||||
;; cannot be compared with = — bool is not an ordered or an equatable type —
|
||||
;; so the agreement between a chain and the spelling it stands for is said
|
||||
;; with the operators bool does have.
|
||||
(defn agree [a bool b bool] ()
|
||||
(if (and (or a b) (not (and a b))) (print "N") (print "y")))
|
||||
|
||||
(defn line [b bool] ()
|
||||
(print " -> ")
|
||||
(print b)
|
||||
(println ""))
|
||||
|
||||
(defn main [] i32
|
||||
;; ── the chain itself ──────────────────────────────────────────────
|
||||
(print (< 1 2 3)) (print " ") ; true
|
||||
(print (< 1 5 3)) (print " ") ; false: the second link
|
||||
(print (< 5 1 3)) (print " ") ; false: the first link
|
||||
(print (< 1 2 3 4)) (print " ") ; true, four operands
|
||||
(print (< 1 2 4 3)) (println "") ; false, four operands
|
||||
|
||||
;; Every member of the family, chained. The middle link is the false one in
|
||||
;; each of the second column.
|
||||
(print (<= 1 1 2)) (print " ") (print (<= 1 2 1)) (print " ")
|
||||
(print (> 3 2 1)) (print " ") (print (> 3 1 2)) (print " ")
|
||||
(print (>= 3 3 1)) (print " ") (print (>= 3 1 2)) (print " ")
|
||||
(print (= 2 2 2)) (print " ") (print (= 2 3 2))
|
||||
(println "")
|
||||
|
||||
;; != is the one that does not chain: it asks whether the operands are all
|
||||
;; different, so the pair it looks at is every pair and not only the
|
||||
;; neighbouring ones. (!= 1 2 1) has no two neighbours alike and is still
|
||||
;; false, which is the whole of the difference.
|
||||
(print (!= 1 2 3)) (print " ") ; true
|
||||
(print (!= 1 1 2)) (print " ") ; false, the adjacent pair
|
||||
(print (!= 1 2 1)) (print " ") ; false, the pair chaining misses
|
||||
(print (!= 1 2 3 4)) (print " ") ; true, six pairs
|
||||
(print (!= 1 2 3 1)) (print " ") ; false, first against last
|
||||
(print (!= 1 2 3 2)) (println "") ; false, a pair in the middle
|
||||
|
||||
;; The chain and the spelling it stands for agree, everywhere both are
|
||||
;; legal. Written out rather than trusted, because it is the whole claim.
|
||||
(agree (< 1 2 3) (and (< 1 2) (< 2 3)))
|
||||
(agree (< 1 5 3) (and (< 1 5) (< 5 3)))
|
||||
(agree (< 5 1 3) (and (< 5 1) (< 1 3)))
|
||||
(agree (<= 1 1 2) (and (<= 1 1) (<= 1 2)))
|
||||
(agree (> 3 1 2) (and (> 3 1) (> 1 2)))
|
||||
(agree (= 2 3 2) (and (= 2 3) (= 3 2)))
|
||||
(agree (< 1 2 3 4) (and (< 1 2) (and (< 2 3) (< 3 4))))
|
||||
;; != stands for the all-pairs spelling, not the adjacent one.
|
||||
(agree (!= 1 2 1) (and (!= 1 2) (and (!= 2 1) (!= 1 1))))
|
||||
(agree (!= 1 2 3) (and (!= 1 2) (and (!= 1 3) (!= 2 3))))
|
||||
(println "")
|
||||
|
||||
;; ── one evaluation of each operand, in order ──────────────────────
|
||||
;; The first link is true here, so the chain goes on. Three tags.
|
||||
(set calls 0)
|
||||
(line (< (mark "a" 1) (mark "b" 2) (mark "c" 3)))
|
||||
;; abc -> true
|
||||
|
||||
;; The first link is *false* here, and the tags still say abc: stopping
|
||||
;; early stops comparing, not running. b appears once although two links
|
||||
;; name it, which is the bug the slots exist to prevent.
|
||||
(line (< (mark "a" 9) (mark "b" 1) (mark "c" 5)))
|
||||
;; abc -> false
|
||||
|
||||
;; Four operands, false in the middle, and every one of them runs.
|
||||
(line (< (mark "a" 1) (mark "b" 2) (mark "c" 0) (mark "d" 9)))
|
||||
;; abcd -> false
|
||||
|
||||
;; Ten marks across three chains is the count, and a middle operand
|
||||
;; evaluated twice would make it eleven.
|
||||
(print calls) (println "") ; 10
|
||||
|
||||
;; != makes the same promise over its larger set of pairs. All different,
|
||||
;; six comparisons over four operands, four tags.
|
||||
(set calls 0)
|
||||
(line (!= (mark "a" 1) (mark "b" 2) (mark "c" 3) (mark "d" 4)))
|
||||
;; abcd -> true
|
||||
|
||||
;; The *first* pair it looks at already says no, and the other three
|
||||
;; operands run anyway: every operand is in its slot before any pair is
|
||||
;; compared, so stopping early stops comparing and nothing else.
|
||||
(line (!= (mark "a" 1) (mark "b" 1) (mark "c" 3) (mark "d" 4)))
|
||||
;; abcd -> false
|
||||
|
||||
;; The pair chaining would never have looked at — first against last.
|
||||
(line (!= (mark "a" 1) (mark "b" 2) (mark "c" 3) (mark "d" 1)))
|
||||
;; abcd -> false
|
||||
|
||||
;; Twelve, and each of the three lines above contributed four. An operand
|
||||
;; named by three pairs evaluated once per pair would say twenty-four.
|
||||
(print calls) (println "") ; 12
|
||||
|
||||
;; The folding operators make the same promise.
|
||||
(set calls 0)
|
||||
(print (+ (mark "p" 1) (mark "q" 2) (mark "r" 3))) (println "") ; pqr6
|
||||
(print (- (mark "p" 10) (mark "q" 3) (mark "r" 2))) (println "") ; pqr5
|
||||
(print (* (mark "p" 2) (mark "q" 3) (mark "r" 4))) (println "") ; pqr24
|
||||
(print (min (mark "p" 5) (mark "q" 2) (mark "r" 8))) (println "") ; pqr2
|
||||
(print (max (mark "p" 5) (mark "q" 2) (mark "r" 8))) (println "") ; pqr8
|
||||
(print calls) (println "") ; 15
|
||||
|
||||
;; ── the types a chain admits ──────────────────────────────────────
|
||||
;; One width throughout: the first pair decides, the rest are checked
|
||||
;; against it, and nothing widens implicitly at three operands any more
|
||||
;; than it does at two.
|
||||
(let [x (u8 1) y (u8 2) z (u8 3)]
|
||||
(print (< x y z)) (print " ")) ; true
|
||||
(let [x (i64 -5) y (i64 0) z (i64 5)]
|
||||
(print (< x y z)) (print " ")) ; true
|
||||
(print (< (markf "f" 1.0) (markf "g" 2.0) (markf "h" 3.0))) (println "")
|
||||
;; true, and fgh printed first
|
||||
|
||||
;; Strings, which = and != admit and the orderings do not. They are the one
|
||||
;; operand type here that is not a machine word, so they are what says the
|
||||
;; slots a chain binds are slots of whatever type the operands have.
|
||||
(print (= "a" "a" "a")) (print " ") ; true
|
||||
(print (= "a" "b" "a")) (print " ") ; false
|
||||
(print (!= "a" "b" "c")) (print " ") ; true
|
||||
(print (!= "a" "b" "a")) (println "") ; false, the non-adjacent pair
|
||||
|
||||
;; The generic chain, at two types.
|
||||
(print (between (i32 1) (i32 2) (i32 3))) (print " ") ; true
|
||||
(print (between (f64 3.0) (f64 2.0) (f64 1.0))) (println "") ; false
|
||||
|
||||
;; And the dyn chain, where the runtime does the comparing.
|
||||
(print (dyn-rising 1 2 3)) (print " ") ; true
|
||||
(print (dyn-rising 1 5 3)) (print " ") ; false
|
||||
(print (dyn-distinct 1 2 3)) (print " ") ; true
|
||||
(print (dyn-distinct 1 2 1)) (println "") ; false, the non-adjacent pair
|
||||
0)
|
||||
@ -380,6 +380,37 @@ let () =
|
||||
outputs "value semantics" "programs/values.flan" values_out;
|
||||
outputs "machine surface" "programs/machine.flan" machine_out;
|
||||
outputs "unit main exits 0" "programs/unit-main.flan" "ok\n";
|
||||
(* Comparisons over three operands and more. The lines that carry the
|
||||
whole claim are the tag transcripts: [abc -> false] is a chain whose
|
||||
*first* link already decided the answer and whose middle operand —
|
||||
named by two links — still ran exactly once, and the counts (10, 12
|
||||
and 15) are what a second evaluation of a shared operand would break.
|
||||
The third line is the one [!=] is here for: it is all-pairs, so
|
||||
(!= 1 2 1) is false although no two neighbours are alike. Both
|
||||
backends and both optimisation levels, because the lowering is a Let
|
||||
of slots and a conjunction of Ifs, which is the one shape a backend
|
||||
could get right at -O2 by accident.
|
||||
|
||||
The string line is here because a string is the one operand type in
|
||||
this file that is not a machine word: the slots a comparison binds are
|
||||
slots of whatever type the operands have, and nothing else would say
|
||||
so. *)
|
||||
let chain_out =
|
||||
"true false false true false\n\
|
||||
true false true false true false true false\n\
|
||||
true false false true false false\n\
|
||||
yyyyyyyyy\n\
|
||||
abc -> true\nabc -> false\nabcd -> false\n10\n\
|
||||
abcd -> true\nabcd -> false\nabcd -> false\n12\n\
|
||||
pqr6\npqr5\npqr24\npqr2\npqr8\n15\n\
|
||||
true true fghtrue\ntrue false true false\n\
|
||||
true false\ntrue false true false\n"
|
||||
in
|
||||
outputs "chained comparisons" "programs/chain.flan" chain_out;
|
||||
outputs ~opt:"-O0" "chained comparisons, -O0" "programs/chain.flan"
|
||||
chain_out;
|
||||
outputs ~x86:true "chained comparisons, --x86" "programs/chain.flan"
|
||||
chain_out;
|
||||
(* A global of move-only type, which this compiler used to refuse outright.
|
||||
What the numbers assert is the half of the rule no checker test can: the
|
||||
global is loaded once and *stays* loaded across a second entry, which is
|
||||
|
||||
@ -1271,6 +1271,102 @@ let () =
|
||||
accepts "a typed if with a bare keyword condition now compiles"
|
||||
"(defn f [] i32 (if :kw 1 2))";
|
||||
|
||||
(* ── Two operands or more, and the two counts below it ─────────── *)
|
||||
(* The operators that take a run of operands, each at three and at four, so
|
||||
the floor and the arms above it are both pinned. The comparisons are the
|
||||
block after this one. *)
|
||||
infers "+ at three" "(+ 1 2 3)" "i32";
|
||||
infers "+ at four" "(+ 1 2 3 4)" "i32";
|
||||
infers "- at four" "(- 10 1 2 3)" "i32";
|
||||
infers "* at four" "(* 1 2 3 4)" "i32";
|
||||
infers "/ at three" "(/ 100 5 2)" "i32";
|
||||
infers "/ at four" "(/ 1000 5 2 2)" "i32";
|
||||
infers "bit-and at three" "(bit-and 7 6 4)" "i32";
|
||||
infers "bit-or at four" "(bit-or 1 2 4 8)" "i32";
|
||||
infers "bit-xor at three" "(bit-xor 1 2 4)" "i32";
|
||||
infers "min at four" "(min 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
|
||||
element and one a unary operator this language does not have; both are a
|
||||
typo far more often than an intent, so both are refused by name. *)
|
||||
rejects_check "a sum with no terms"
|
||||
"(defn f [] i32 (+))" ~needle:"+ takes two arguments or more, given 0";
|
||||
rejects_check "a product with no factors"
|
||||
"(defn f [] i32 (*))" ~needle:"* takes two arguments or more, given 0";
|
||||
rejects_check "there is no unary minus"
|
||||
"(defn f [] i32 (- 1))" ~needle:"there is no unary minus";
|
||||
rejects_check "there is no reciprocal"
|
||||
"(defn f [] f64 (/ 2.0))" ~needle:"there is no reciprocal";
|
||||
rejects_check "one operand is not a bitwise and"
|
||||
"(defn f [] i32 (bit-and 7))"
|
||||
~needle:"bit-and takes two arguments or more, given 1";
|
||||
rejects_check "no operands are not a bitwise or"
|
||||
"(defn f [] i32 (bit-or))"
|
||||
~needle:"bit-or takes two arguments or more, given 0";
|
||||
rejects_check "one operand is not a min"
|
||||
"(defn f [] i32 (min 7))" ~needle:"min takes two arguments or more, given 1";
|
||||
|
||||
(* ── Chained comparisons ───────────────────────────────────────── *)
|
||||
(* (< a b c) is a < b and b < c. The left fold — ((a < b) < c) — would be
|
||||
comparing a bool against a number, so there is one reading and this is
|
||||
it. What the run-time half means is asserted in programs/chain.flan. *)
|
||||
infers "a three-way comparison is still bool" "(< 1 2 3)" "bool";
|
||||
infers "a four-way comparison is still bool" "(< 1 2 3 4)" "bool";
|
||||
accepts "every comparison takes three"
|
||||
"(defn f [] bool (and (= 1 1 1) (!= 1 2 3) (<= 1 2 2) (> 3 2 1) \
|
||||
(>= 3 3 2)))";
|
||||
(* [!=] is the one that does not chain. "Is this sequence increasing" and
|
||||
"are these all different" are different questions, and only the first is
|
||||
about neighbours: under chaining (!= 1 2 1) would be true. It asks about
|
||||
every pair instead. The answers themselves are asserted where they can
|
||||
be run, in programs/chain.flan. *)
|
||||
infers "all-distinct is still bool" "(!= 1 2 1)" "bool";
|
||||
accepts "!= at four operands" "(defn f [] bool (!= 1 2 3 4))";
|
||||
(* Strings, which = and != admit and the orderings do not. The slots a
|
||||
comparison binds are slots of the operands' own type, so this is the one
|
||||
row that is not about machine words. *)
|
||||
infers "= over strings at three" "(= \"a\" \"a\" \"a\")" "bool";
|
||||
infers "!= over strings at three" "(!= \"a\" \"b\" \"c\")" "bool";
|
||||
rejects_check "the orderings still refuse strings at three"
|
||||
"(defn f [] bool (< \"a\" \"b\" \"c\"))" ~needle:"orders machine numbers";
|
||||
(* The operands after the first pair are checked against the type that pair
|
||||
decided, and nothing widens on the way — the same rule two operands have
|
||||
had all along, applied one more time. *)
|
||||
accepts "a chain over one width" "(defn f [x u8 y u8 z u8] bool (< x y z))";
|
||||
rejects_check "a chain does not widen its third operand"
|
||||
"(defn f [x u8 y u8 z i64] bool (< x y z))" ~needle:"expected u8";
|
||||
rejects_check "a chain does not widen its fourth operand"
|
||||
"(defn f [x i32 y i32 z i32 w f64] bool (< x y z w))"
|
||||
~needle:"expected i32";
|
||||
(* A generic operand is admitted by the predicate its signature carries, at
|
||||
three operands as at two. *)
|
||||
rejects_check "all-distinct does not widen its third operand either"
|
||||
"(defn f [x u8 y u8 z i64] bool (!= x y z))" ~needle:"expected u8";
|
||||
accepts "a chain over a type variable"
|
||||
"(defn between [a $t b $t c $t] bool {:where (ordered? $t)} (< a b c))";
|
||||
accepts "all-distinct over a type variable"
|
||||
"(defn three [a $t b $t c $t] bool {:where (equal? $t)} (!= a b c))";
|
||||
rejects_check "a chain still wants the right predicate"
|
||||
~needle:"nothing here says t is ordered?"
|
||||
"(defn between [a $t b $t c $t] bool {:where (equal? $t)} (< a b c))";
|
||||
(* One operand and none. Both would have to be [true] whatever they were
|
||||
handed, which is a typo carrying a value. *)
|
||||
rejects_check "one operand is not a comparison"
|
||||
"(defn f [] bool (< 1))" ~needle:"needs a second value to compare against";
|
||||
rejects_check "no operands are not a comparison"
|
||||
"(defn f [] bool (<))" ~needle:"< takes two arguments or more, given 0";
|
||||
rejects_check "the same for equality"
|
||||
"(defn f [] bool (= 1))" ~needle:"needs a second value to compare against";
|
||||
rejects_check "one value is distinct from nothing"
|
||||
"(defn f [] bool (!= 1))" ~needle:"needs something to be distinct from";
|
||||
rejects_check "no values are not a distinctness test"
|
||||
"(defn f [] bool (!=))" ~needle:"!= takes two arguments or more, given 0";
|
||||
(* Chaining does not reach the operators that are not comparisons. *)
|
||||
rejects_check "a chain of remainders is still refused"
|
||||
"(defn f [] i32 (% 10 3 2))" ~needle:"% takes 2 arguments";
|
||||
rejects_check "a chain of shifts is still refused"
|
||||
"(defn f [] i32 (<< 1 2 3))" ~needle:"<< takes 2 arguments";
|
||||
|
||||
(* ── Unknown types ─────────────────────────────────────────────── *)
|
||||
(* A lowercase name is a type variable (plan.org, Types), so a mistyped
|
||||
primitive would otherwise be reported as unimplemented generics and send
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user