A dyn operand anywhere in an arithmetic, bitwise or comparison fold makes the fold dyn from there on, and min or max refuses one past its first pair as it does in it.
This commit is contained in:
parent
2243b55259
commit
d138155eae
3
TODO.org
3
TODO.org
@ -787,9 +787,6 @@ One spelling for one operation; != stays, and not= is refused with a suggestion
|
||||
of !=.
|
||||
|
||||
* Checker
|
||||
** TODO A dyn operand past the second in a + fold is converted to the running type
|
||||
=(+ 1 2 d)= with d a dyn char prints 100: the dyn is unboxed to i32 before adding, where
|
||||
rule 117 says typed beside dyn gives dyn (=(+ 3 d)= gives =\d=). Predates the char lane.
|
||||
** WAIT Checking a wide fold of let operands is slow
|
||||
Parked 2026-09-26: design first; remeasure on a quiet machine, it was timed under load 20.
|
||||
A 2000-operand (bit-and (let …) …) takes 32 s to check (37 s before the bit operators);
|
||||
|
||||
81
lib/check.ml
81
lib/check.ml
@ -11427,21 +11427,30 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
|
||||
(* Left to right, each step char arithmetic when a char is in it and the
|
||||
ordinary join when none is: (- \z \a 1) is 25 - 1, and (+ 1 2 \a) is
|
||||
3 + \a. *)
|
||||
let step acc (arg : Ast.expr) =
|
||||
let rec steps acc = function
|
||||
| [] -> expect ctx loc ~want acc
|
||||
| (arg : Ast.expr) :: tl ->
|
||||
let lit = char_lit arg in
|
||||
untyped := !untyped && int_lit arg;
|
||||
if is_char acc || maybe_char ctx arg || lit then
|
||||
let v = check ctx arg in
|
||||
if is_char acc || is_char v then char_step ~want:nwant loc name acc v
|
||||
else mk loc acc.Tast.ty (Tast.Prim (p, [ acc; expect ctx arg.Ast.loc ~want:(Some acc.Tast.ty) v ]))
|
||||
if v.Tast.ty = Types.Dyn then dyn_fold ctx ~want loc name [ acc; v ] tl
|
||||
else if is_char acc || is_char v then
|
||||
steps (char_step ~want:nwant loc name acc v) tl
|
||||
else
|
||||
mk loc acc.Tast.ty (Tast.Prim (p, [ acc; check ctx ~want:acc.Tast.ty arg ]))
|
||||
match fold_operand ctx acc.Tast.ty (expect ctx arg.Ast.loc ~want:(Some acc.Tast.ty) v) with
|
||||
| `Typed v -> steps (mk loc acc.Tast.ty (Tast.Prim (p, [ acc; v ]))) tl
|
||||
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
|
||||
else
|
||||
match fold_operand ctx acc.Tast.ty (check ctx ~want:acc.Tast.ty arg) with
|
||||
| `Typed v -> steps (mk loc acc.Tast.ty (Tast.Prim (p, [ acc; v ]))) tl
|
||||
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
|
||||
in
|
||||
let first =
|
||||
if is_char a || is_char b then char_step ~want:nwant loc name a b
|
||||
else mk loc a.Tast.ty (Tast.Prim (p, [ a; b ]))
|
||||
in
|
||||
expect ctx loc ~want (List.fold_left step first rest)
|
||||
steps first rest
|
||||
else if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
|
||||
dyn_fold ctx ~want loc name [ a; b ] rest
|
||||
else begin
|
||||
@ -11457,16 +11466,27 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
|
||||
answered again, per copy, at the instantiation. *)
|
||||
if not (ok a.Tast.ty || generic_ty a.Tast.ty) then not_numeric name what a;
|
||||
let ty = a.Tast.ty in
|
||||
let acc =
|
||||
List.fold_left
|
||||
(fun acc arg ->
|
||||
mk loc ty (Tast.Prim (p, [ acc; check ctx ~want:ty arg ])))
|
||||
(mk loc ty (Tast.Prim (p, [ a; b ])))
|
||||
rest
|
||||
let rec steps acc = function
|
||||
| [] -> expect ctx loc ~want acc
|
||||
| arg :: tl ->
|
||||
match fold_operand ctx ty (check ctx ~want:ty arg) with
|
||||
| `Typed v -> steps (mk loc ty (Tast.Prim (p, [ acc; v ]))) tl
|
||||
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
|
||||
in
|
||||
expect ctx loc ~want acc
|
||||
steps (mk loc ty (Tast.Prim (p, [ a; b ]))) rest
|
||||
end
|
||||
|
||||
(* An operand past a fold's first pair, checked at the type so far. A dyn one
|
||||
is taken back as the dyn it was, not opened at that type: a typed operand
|
||||
beside a dyn gives dyn (rule 117), so from there on the fold is the dyn
|
||||
runtime's, and (+ 1 2 d) is (+ 3 d). *)
|
||||
and fold_operand ctx ty (v : Tast.expr) =
|
||||
if v.Tast.ty = Types.Dyn && not (Types.equal ty Types.Dyn) then `Dyn v
|
||||
else
|
||||
match opened_dyn ~box:(to_dyn ctx) v with
|
||||
| Some d -> `Dyn d
|
||||
| None -> `Typed v
|
||||
|
||||
(* A pair an arithmetic operator refused, when one operand is a char: that
|
||||
is the refusal to give, rather than the mismatch between the two. Asked
|
||||
only after the refusal, so a pair that checks costs nothing more. *)
|
||||
@ -13026,7 +13046,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
two things being unalike is the answer to "are these equal", not an
|
||||
error. The orderings do trap, and rightly — there is no true answer to
|
||||
whether a string is less than a vector. *)
|
||||
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then begin
|
||||
(* [ops] are every operand, boxed. *)
|
||||
let dyn_chain ops =
|
||||
let sym =
|
||||
match name with
|
||||
| "=" | "!=" -> "flan_dyn_eq"
|
||||
@ -13053,15 +13074,15 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
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
|
||||
| _ -> cmp_over ctx loc Types.Dyn ~pairs ~link (ops ())
|
||||
in
|
||||
expect ctx loc ~want r
|
||||
end else begin
|
||||
in
|
||||
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
|
||||
dyn_chain (fun () ->
|
||||
box loc a :: box loc b
|
||||
:: map_lr (fun e -> box loc (check ctx ~want:Types.Dyn e)) rest)
|
||||
else begin
|
||||
(* [=] and [!=] admit types [<] does not. A handle is one: a pair of
|
||||
numbers in one word and where being the same entity is the question the
|
||||
type exists to answer — ordering handles would order a slot index,
|
||||
@ -13096,7 +13117,17 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
| _ ->
|
||||
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
|
||||
let rest = map_lr (fun e -> fold_operand ctx ty (check ctx ~want:ty e)) rest in
|
||||
(* A dyn past the first pair makes the whole chain the dyn runtime's,
|
||||
for [fold_operand]'s reason: a chain is its pairs, and a pair with a
|
||||
dyn in it is a dyn comparison. *)
|
||||
if List.exists (function `Dyn _ -> true | `Typed _ -> false) rest then
|
||||
dyn_chain (fun () ->
|
||||
box loc a :: box loc b
|
||||
:: List.map (function `Dyn d -> d | `Typed v -> box loc v) rest)
|
||||
else
|
||||
let ops =
|
||||
a :: b :: List.map (function `Typed v -> v | `Dyn d -> d) rest in
|
||||
expect ctx loc ~want (cmp_over ctx loc ty ~pairs ~link ops)
|
||||
end
|
||||
| "not" ->
|
||||
@ -13236,7 +13267,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
[ mk loc ty (Tast.If (test, la, lb)) ]))
|
||||
in
|
||||
expect ctx loc ~want
|
||||
(List.fold_left (fun acc arg -> pick acc (check ctx ~want:ty arg))
|
||||
(List.fold_left
|
||||
(fun acc arg ->
|
||||
(* A dyn is refused here as it is in the first pair, rather than
|
||||
opened at the type so far. *)
|
||||
match fold_operand ctx ty (check ctx ~want:ty arg) with
|
||||
| `Typed v -> pick acc v
|
||||
| `Dyn d -> not_numeric name "numbers" d; acc)
|
||||
(pick a b) rest)
|
||||
(* A type handed to the prelude's slice reductions: the reach for the
|
||||
type-limit constants under the name of the reduction beside them. *)
|
||||
|
||||
33
test/programs/dyn-fold-position.flan
Normal file
33
test/programs/dyn-fold-position.flan
Normal file
@ -0,0 +1,33 @@
|
||||
;;;; A dyn operand anywhere in a fold makes the fold dyn from there on: the
|
||||
;;;; typed operands before it are folded typed, and the dyn runtime takes the
|
||||
;;;; rest. (+ 1 2 d) is (+ 3 d), whichever position the dyn is in.
|
||||
|
||||
(defn as-i32 [x i32] i32 x)
|
||||
(defn as-f64 [x f64] f64 x)
|
||||
|
||||
(defn main [] i32
|
||||
(let [d (the dyn \a)
|
||||
f (the dyn 2.5)
|
||||
n (the dyn 4)
|
||||
c \a]
|
||||
;; + and - over a dyn char: first, middle, last.
|
||||
(println (+ d 1 2) (+ 1 d 2) (+ 1 2 d))
|
||||
(println (- d 1 2) (- 10 n 1) (- 10 1 n))
|
||||
;; A dyn float past an integer pair promotes, as (* 6 f) does.
|
||||
(println (* f 2 3) (* 2 f 3) (* 2 3 f))
|
||||
(println (/ f 2 5) (/ 9 f 2) (/ 9 2 f))
|
||||
(println (+ 1 2 3 f) (- 10 1 2 f))
|
||||
;; A char fold with a dyn past the pair.
|
||||
(println (+ c 1 n) (- c 1 n) (+ c 1 2 n))
|
||||
;; The bitwise folds.
|
||||
(println (bit-or n 1 2) (bit-or 1 n 2) (bit-or 1 2 n))
|
||||
(println (bit-and n 7 6) (bit-and 7 n 6) (bit-and 7 6 n))
|
||||
(println (bit-xor n 1 2) (bit-xor 1 n 2) (bit-xor 1 2 n))
|
||||
;; Comparison chains: a float past an integer pair is compared as one.
|
||||
(println (< f 3 4) (< 1 f 3) (< 1 2 f) (< 1 3 f))
|
||||
(println (<= 2 2 f) (> 3 2 f) (>= 3 3 f) (>= 3 3 n))
|
||||
(println (= 4 4 n) (= 4 n 4) (= n 4 4) (= 4 4 f))
|
||||
(println (!= 1 2 n) (!= 1 4 n) (!= 2 f 3))
|
||||
;; At a typed want the dyn answer is opened at the end.
|
||||
(println (as-i32 (+ 1 2 n)) (as-f64 (* 2 3 f))))
|
||||
0)
|
||||
@ -5610,6 +5610,19 @@ level "1"
|
||||
char_arith_out;
|
||||
outputs ~x86:true "char: arithmetic, --x86" "programs/char-arith.flan"
|
||||
char_arith_out;
|
||||
(* A dyn anywhere in a fold makes it dyn from there on (rule 117): each
|
||||
family with the dyn first, in the middle and last. *)
|
||||
let fold_out =
|
||||
"d d d\n^ 5 5\n15 15 15\n0.25 1.8 1.6\n8.5 4.5\nf \\ h\n7 7 7\n\
|
||||
4 4 4\n7 7 7\ntrue true true false\ntrue false true false\n\
|
||||
true true true false\ntrue false true\n7 15\n"
|
||||
in
|
||||
outputs "dyn: a dyn in any fold position" "programs/dyn-fold-position.flan"
|
||||
fold_out;
|
||||
outputs ~opt:"-O0" "dyn: a dyn in any fold position, -O0"
|
||||
"programs/dyn-fold-position.flan" fold_out;
|
||||
outputs ~x86:true "dyn: a dyn in any fold position, --x86"
|
||||
"programs/dyn-fold-position.flan" fold_out;
|
||||
List.iter
|
||||
(fun x86 ->
|
||||
let exe = compile ~x86 "programs/char-arith.flan" in
|
||||
|
||||
@ -8450,5 +8450,14 @@ let () =
|
||||
"(defn f [n i32] (Option i32) (cond (= n 1) 10 (= n 2) 20))\n(defn main [] ())";
|
||||
rejects_check "a map's get takes one key" ~needle:"a map's get takes one key"
|
||||
"(defn main [] () (let [m (map-new i32 i32)] (println (get m 1 2))))";
|
||||
(* min and max have no dyn lowering: a dyn past the first pair is refused
|
||||
as one in it is, not opened at the type so far. *)
|
||||
List.iter
|
||||
(fun op ->
|
||||
rejects_check (op ^ " refuses a dyn past its first pair")
|
||||
~needle:(op ^ " takes numbers, found dyn")
|
||||
(Printf.sprintf
|
||||
"(defn main [] () (let [f (the dyn 2.5)] (println (%s 3 4 f))))" op))
|
||||
[ "min"; "max" ];
|
||||
|
||||
Test_support.report ()
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user