Merge branch 'ergonomics' into dev-loop
sin and cos in the prelude rather than copied per file, with the caveat sqrt does not have: IEEE-754 makes sqrt correctly rounded and requires nothing of the kind for sine, so these are the one place the prelude may disagree bit for bit between native and wasm32. A program hashing output across targets must not route the hash through one. Arithmetic folds left over as many operands as you write, and so does the constant folder, which otherwise refused (defconst n (* 2 3 4)) after the checker had accepted it. One operand is refused by name: there is no unary minus, and the message points at (- 0 x), which is what the prelude writes. The typed let binding is a grammar question and is written up rather than guessed at. The break banner premise had gone stale -- check.sh already runs that demo under a timeout and keeps what it printed.
This commit is contained in:
commit
d803078699
4
BUILT.md
4
BUILT.md
@ -865,8 +865,8 @@ frame that erred with nothing unwound, so the condition and every restart betwee
|
||||
|
||||
```
|
||||
flan: unhandled Missing — stopped, not dead.
|
||||
restart: retry
|
||||
restart: use-placeholder
|
||||
0. restart: retry
|
||||
1. restart: use-placeholder
|
||||
```
|
||||
|
||||
Four decisions, each of which is the reason something is where it is:
|
||||
|
||||
40
NEXT.md
40
NEXT.md
@ -244,10 +244,32 @@ Ranked by how often they were hit, top two first because they are walls rather t
|
||||
3. **`break` is not implemented.** Declined deliberately rather than built — see below.
|
||||
4. **A `let` binding takes no type annotation**, so a fixed array is either a top-level `defvar` or a literal with
|
||||
every element spelled out. `(let [pts [4 rl/Vector2]] …)` parses as a two-element array literal and fails with
|
||||
*unknown name rl/Vector2*. Cost: 32 hand-written `Vector2`s in one example.
|
||||
5. **Arithmetic is strictly binary** — *+ takes 2 arguments, given 5*.
|
||||
6. **No `sin`/`cos`/`abs` for floats.** The prelude has `sqrt-f32` and nothing else transcendental. Two `declare`
|
||||
lines over libm, and `(max x (- 0.0 x))`; the examples each declare their own, which is a copy per file.
|
||||
*unknown name rl/Vector2*. Cost: 32 hand-written `Vector2`s in one example. **Looked at and stopped — it is a
|
||||
grammar question, not a missing feature.** Everything under the surface is already there: `Ast.binding` carries a
|
||||
`bty`, `load.ml` renames through it, and `check.ml:723` consumes it as the `want` for the value. Only the way it
|
||||
is written is open, and the parser says so where it refuses (`parse.ml:366`): `let` is a flat list of pairs, so it
|
||||
cannot disambiguate by *count* the way `defvar` and `defconst` do — those read `[n t v]` as three arguments to a
|
||||
form, and there is no such boundary between one pair and the next. Three surfaces, in the order they are worth
|
||||
considering:
|
||||
- **`(zeroed [4 rl/Vector2])` — `zeroed` takes its type as an argument.** Recommended. It is one extra branch in
|
||||
the arity-0 `zeroed` case in `check.ml`, no parser change, no ambiguity, and it answers the actual complaint,
|
||||
which is not "locals cannot be annotated" but "there is nothing here to infer *from*". It also reads as what it
|
||||
does: the value is a zeroed thing of that type, not a name that has been told what it is.
|
||||
- **A marker between the name and the type**, `(let [pts :- [4 rl/Vector2] …] …)` or similar. Unambiguous, and it
|
||||
buys a general annotation rather than one form's escape hatch. The cost is a new piece of syntax in the binding
|
||||
vector, which is the one place this language has kept looking exactly like Clojure's.
|
||||
- **Bare `(let [pts [4 rl/Vector2] …])`.** The obvious spelling and the one that cannot work: `[4 rl/Vector2]` is
|
||||
a well-formed two-element array literal, and telling the two apart needs types in the parser, which there are
|
||||
none of by design.
|
||||
Note that plan.org's rule is "annotate function signatures, infer locals", so the general annotation is a
|
||||
deliberate absence and not an oversight — which is the other reason the `zeroed` route is the smaller answer.
|
||||
5. ~~**Arithmetic is strictly binary** — *+ takes 2 arguments, given 5*.~~ **Fixed.** `+ - * /`, `min`/`max` and
|
||||
`bit-and`/`bit-or`/`bit-xor` fold left over two operands or more. `%` and the shifts stay at two, and one operand
|
||||
is refused with the form to write instead — there is no unary minus and no reciprocal.
|
||||
6. ~~**No `sin`/`cos`/`abs` for floats.**~~ **Fixed.** `sin-f32` and `cos-f32` are `declare`s in the prelude now,
|
||||
with the caveat written beside them: IEEE-754 makes `sqrt` correctly rounded and requires nothing of the kind for
|
||||
`sinf`, so these are the one place in the prelude where native and wasm32 may disagree bit for bit. Float `abs` is
|
||||
not wrapped, for the reason integer `abs` is not — it is `(max x (- 0.0 x))` over two builtins.
|
||||
|
||||
**A `string` cannot be returned from C at all**, which is what makes `GetGamepadName` unbindable: *a string only
|
||||
crosses as a parameter — a C function that returns one returns something Flan has no owner for*. Same rule refuses
|
||||
@ -317,11 +339,11 @@ plan.org's single line on it (831) names a `for` the language does not have and
|
||||
|
||||
### Bugs found and not yet fixed
|
||||
|
||||
- **`web/examples/breakdemo.out` is stale and `check.sh` fails on it.** Commit `4a6a8fa` made the break banner number
|
||||
its restarts (` 0. restart: retry`) and the `.out` was never repinned; `web/index.html` quotes the same stale
|
||||
banner. Repinning it is not a one-liner — the program stops at a break loop and waits for a choice, so running it
|
||||
from `check.sh` hangs rather than printing. It needs the harness to drive the socket, or the demo needs to end by
|
||||
aborting.
|
||||
- ~~`web/examples/breakdemo.out` is stale and `check.sh` fails on it.~~ **Fixed.** Commit `4a6a8fa` made the break
|
||||
banner number its restarts and the `.out` was never repinned. Nothing had to drive the socket in the end:
|
||||
`check.sh` already builds this one `--dev` and runs it under `timeout 5`, keeping what it printed before it
|
||||
stopped, so the repin was the `.out` plus the two prose copies of the banner — `web/index.html` and `BUILT.md` —
|
||||
and a sentence on the page saying what the numbers are for, since a restart is taken by position.
|
||||
|
||||
- ~~A shadowed restart is offered and cannot be taken.~~ **Fixed.** A restart is taken by *position* now:
|
||||
`(:op "restart-at" :index N :name NAME)` on the daemon, `restart-at N NAME` on the agent, and a numbered
|
||||
|
||||
@ -59,12 +59,6 @@
|
||||
(import rl "vendor:raylib")
|
||||
(import d "digits.flan")
|
||||
|
||||
;; libm, as the prelude declares sqrtf. Not declare-c: these take a float and
|
||||
;; answer a float in C's own convention with no struct anywhere, which is what
|
||||
;; plain `declare` is for.
|
||||
(declare sin-f32 [x f32] f32 "sinf")
|
||||
(declare cos-f32 [x f32] f32 "cosf")
|
||||
|
||||
(defconst screen-width 800)
|
||||
(defconst screen-height 450)
|
||||
|
||||
|
||||
132
lib/check.ml
132
lib/check.ml
@ -1027,20 +1027,73 @@ and arity 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.
|
||||
|
||||
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
|
||||
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
|
||||
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. *)
|
||||
and fold_arity loc name args =
|
||||
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, which is what the prelude does"
|
||||
| [ _ ] when String.equal name "/" ->
|
||||
fail loc
|
||||
"/ takes two arguments or more, given 1 — there is no reciprocal; \
|
||||
write (/ 1.0 x)"
|
||||
| _ ->
|
||||
fail loc "%s takes two arguments or more, given %d" name (List.length args)
|
||||
|
||||
(* 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. *)
|
||||
and fold_left_prim ctx ~want loc name p ok what args =
|
||||
let x, y, rest =
|
||||
match args with x :: y :: rest -> x, y, rest | _ -> assert false
|
||||
in
|
||||
let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
|
||||
if not (ok a.Tast.ty) then
|
||||
fail loc "%s takes %s, found %s" name what (Types.to_string a.Tast.ty);
|
||||
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
|
||||
in
|
||||
expect loc ~want acc
|
||||
|
||||
and named_call ctx ~want loc name args =
|
||||
let prim p ty args = expect loc ~want (mk loc ty (Tast.Prim (p, args))) in
|
||||
match name with
|
||||
(* ── arithmetic and comparison ─────────────────────────────────── *)
|
||||
| "+" | "-" | "*" | "/" | "%" ->
|
||||
| "+" | "-" | "*" | "/" ->
|
||||
let p = match name with
|
||||
| "+" -> Tast.Add | "-" -> Tast.Sub | "*" -> Tast.Mul
|
||||
| "/" -> Tast.Div | _ -> Tast.Rem
|
||||
| _ -> Tast.Div
|
||||
in
|
||||
fold_arity loc name args;
|
||||
fold_left_prim ctx ~want loc name p Types.is_numeric "numbers" args
|
||||
(* Remainder stays at two: (% a b c) is (% (% a b) c), which is a thing
|
||||
nobody writes on purpose. *)
|
||||
| "%" ->
|
||||
arity loc name 2 args;
|
||||
let a, b = binary ctx name loc ~want:(numeric_want want) args in
|
||||
if not (Types.is_numeric a.Tast.ty) then
|
||||
fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
|
||||
prim p a.Tast.ty [ a; b ]
|
||||
prim Tast.Rem a.Tast.ty [ a; b ]
|
||||
| "=" | "!=" | "<" | "<=" | ">" | ">=" ->
|
||||
let p = match name with
|
||||
| "=" -> Tast.Eq | "!=" -> Tast.Ne | "<" -> Tast.Lt
|
||||
@ -1058,11 +1111,19 @@ and named_call ctx ~want loc name args =
|
||||
prim Tast.Not Types.Bool [ check ctx ~want:Types.Bool (List.hd args) ]
|
||||
(* Bitwise operators are integers-only, and the shift count has the same type
|
||||
as the value shifted — there is no implicit widening anywhere else either. *)
|
||||
| "bit-and" | "bit-or" | "bit-xor" | "<<" | ">>" ->
|
||||
| "bit-and" | "bit-or" | "bit-xor" ->
|
||||
let p = match name with
|
||||
| "bit-and" -> Tast.BitAnd | "bit-or" -> Tast.BitOr
|
||||
| "bit-xor" -> Tast.BitXor | "<<" -> Tast.Shl | _ -> Tast.Shr
|
||||
| _ -> Tast.BitXor
|
||||
in
|
||||
fold_arity loc name args;
|
||||
fold_left_prim ctx ~want loc name p
|
||||
(function Types.Int _ -> true | _ -> false) "integers" args
|
||||
(* The shifts stay at two, and not only because a shift chain reads badly:
|
||||
each count would be checked against the same width below, so (<< x 30 30)
|
||||
would pass two legal shifts and still shift the value away entirely. *)
|
||||
| "<<" | ">>" ->
|
||||
let p = if String.equal name "<<" then Tast.Shl else Tast.Shr in
|
||||
arity loc name 2 args;
|
||||
let a, b = binary ctx name loc ~want:(numeric_want want) args in
|
||||
(match a.Tast.ty with
|
||||
@ -1084,20 +1145,34 @@ and named_call ctx ~want loc name args =
|
||||
| _ -> ());
|
||||
prim p a.Tast.ty [ a; b ]
|
||||
(* (min a b) and (max a b) evaluate each operand once — hence the slots —
|
||||
because a min over two calls must not call either of them twice. *)
|
||||
because a min over two calls must not call either of them twice.
|
||||
|
||||
Which is also why this one does not go through [fold_left_prim]: there is
|
||||
no Prim to fold, and the pair it folds is a whole comparison. Each step
|
||||
puts *both* of its sides in slots, the accumulated pick included, so the
|
||||
three-operand form is two nested lets and still exactly one evaluation of
|
||||
each operand — where reusing the previous [If] as an operand of the next
|
||||
would have duplicated everything inside it. *)
|
||||
| "min" | "max" ->
|
||||
arity loc name 2 args;
|
||||
let a, b = binary ctx name loc ~want:(numeric_want want) args in
|
||||
fold_arity loc name args;
|
||||
let x, y, rest =
|
||||
match args with x :: y :: rest -> x, y, rest | _ -> assert false
|
||||
in
|
||||
let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
|
||||
if not (Types.is_numeric a.Tast.ty) then
|
||||
fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
|
||||
let ty = a.Tast.ty in
|
||||
let sa = fresh_slot ctx ty and sb = fresh_slot ctx ty in
|
||||
let la = mk loc ty (Tast.Local sa) and lb = mk loc ty (Tast.Local sb) in
|
||||
let cmp = if String.equal name "min" then Tast.Lt else Tast.Gt in
|
||||
let pick = mk loc Types.Bool (Tast.Prim (cmp, [ la; lb ])) in
|
||||
let pick a b =
|
||||
let sa = fresh_slot ctx ty and sb = fresh_slot ctx ty in
|
||||
let la = mk loc ty (Tast.Local sa) and lb = mk loc ty (Tast.Local sb) in
|
||||
let test = mk loc Types.Bool (Tast.Prim (cmp, [ la; lb ])) in
|
||||
mk loc ty (Tast.Let ([ (sa, a); (sb, b) ],
|
||||
[ mk loc ty (Tast.If (test, la, lb)) ]))
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc ty (Tast.Let ([ (sa, a); (sb, b) ],
|
||||
[ mk loc ty (Tast.If (pick, la, lb)) ])))
|
||||
(List.fold_left (fun acc arg -> pick acc (check ctx ~want:ty arg))
|
||||
(pick a b) rest)
|
||||
(* (zeroed) is the all-bytes-zero value of whatever it is being stored into,
|
||||
so it only means anything where a type is expected of it. *)
|
||||
| "zeroed" ->
|
||||
@ -1479,17 +1554,26 @@ let rec const_int env (e : Ast.expr) : int64 option =
|
||||
| Ast.Int n -> Some n
|
||||
| Ast.Byte b -> Some (Int64.of_int b)
|
||||
| Ast.Var n -> Hashtbl.find_opt env.consts n
|
||||
| Ast.Call ({ Ast.e = Ast.Var op; _ }, [ x; y ]) ->
|
||||
(match const_int env x, const_int env y with
|
||||
| Some a, Some b ->
|
||||
(match op with
|
||||
| "+" -> Some (Int64.add a b)
|
||||
| "-" -> Some (Int64.sub a b)
|
||||
| "*" -> Some (Int64.mul a b)
|
||||
| "/" when b <> 0L -> Some (Int64.div a b)
|
||||
| "%" when b <> 0L -> Some (Int64.rem a b)
|
||||
| _ -> None)
|
||||
| _ -> None)
|
||||
(* Left to right over any number of operands, because that is how the
|
||||
checker reads the same form: an array length that type-checks as a
|
||||
product of three literals and is then not a constant would be a
|
||||
distinction with nothing behind it. [%] is still two, as it is there. *)
|
||||
| Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) ->
|
||||
let step a b =
|
||||
match op with
|
||||
| "+" -> Some (Int64.add a b)
|
||||
| "-" -> Some (Int64.sub a b)
|
||||
| "*" -> Some (Int64.mul a b)
|
||||
| "/" when b <> 0L -> Some (Int64.div a b)
|
||||
| "%" when b <> 0L && rest = [] -> Some (Int64.rem a b)
|
||||
| _ -> None
|
||||
in
|
||||
List.fold_left
|
||||
(fun acc e ->
|
||||
match acc, const_int env e with
|
||||
| Some a, Some b -> step a b
|
||||
| _ -> None)
|
||||
(const_int env x) (y :: rest)
|
||||
| _ -> None
|
||||
|
||||
let collect env (decls : Ast.decl list) =
|
||||
|
||||
@ -197,6 +197,15 @@ let source = {flan|
|
||||
;; the negation wraps. That is what every two's-complement abs does, a
|
||||
;; function here would do it too, and the only fix is not to hand it that
|
||||
;; value — so it is written down rather than wrapped.
|
||||
;;
|
||||
;; The float abs is the same one-liner, (max x (- 0.0 x)), and it is not
|
||||
;; wrapped for the same reason — but the caveat above does not carry over, so
|
||||
;; it is not inherited by silence. f32 negation is exact at every value, there
|
||||
;; is no least representable float that negates to itself, and the two edge
|
||||
;; inputs both come out right: -0.0 answers +0.0 (the max picks the subtracted
|
||||
;; side, since neither zero is greater than the other), and a NaN answers a
|
||||
;; NaN (every comparison fails, so the same max picks the subtracted side,
|
||||
;; which is still a NaN). There is nothing left for a function to fix.
|
||||
|
||||
;; Zero for zero, and zero for NaN — neither is positive nor negative, so
|
||||
;; neither comparison fires. A caller that needs to know which it got should
|
||||
@ -303,6 +312,34 @@ let source = {flan|
|
||||
;; builtin in check.ml and emit.ml is one instruction with no symbol at all.
|
||||
(declare sqrt-f32 [x f32] f32 "sqrtf")
|
||||
|
||||
;; sin and cos go out to libm too, and the argument is *not* the one above —
|
||||
;; it is weaker, and which way it is weaker is the thing to know before
|
||||
;; calling them. IEEE-754 requires sqrt to be correctly rounded, which is why
|
||||
;; sqrtf's answer is the same bit pattern wherever it runs. It requires
|
||||
;; nothing of the kind for sinf and cosf: each implementation is free to be a
|
||||
;; fraction of an ulp off in its own direction, and glibc, musl and wasi-libc
|
||||
;; do differ. So these two are the one place in this file where native and
|
||||
;; wasm32 may not agree bit for bit, and a program whose output is hashed
|
||||
;; across targets — the sand grid of plan.org's "RNG is ours", which is why
|
||||
;; rand-u32 above is written in Flan and not called out of libc — must not
|
||||
;; route that hash through a sine.
|
||||
;;
|
||||
;; They are here anyway, because the alternative on offer today is worse: a
|
||||
;; caller that wants an angle writes the same two `declare` lines at the top
|
||||
;; of its own file (examples/core-input-gestures-testbed.flan did, before
|
||||
;; this), which is the identical libm call with the identical caveat and
|
||||
;; nobody's name on it. One copy with the caveat written down beats a copy per
|
||||
;; file with none.
|
||||
;;
|
||||
;; The fix, if a program ever does need trig that agrees across targets, is a
|
||||
;; body rather than a declare: Cody-Waite reduction onto [-pi/4, pi/4] and a
|
||||
;; minimax polynomial, which is reachable from the four operations and
|
||||
;; floor-f32 and would therefore be exactly as reproducible as rand-u32. That
|
||||
;; is a numerics job with its own accuracy budget, and it waits for a program
|
||||
;; that needs it.
|
||||
(declare sin-f32 [x f32] f32 "sinf")
|
||||
(declare cos-f32 [x f32] f32 "cosf")
|
||||
|
||||
;; ── Byte classes ──────────────────────────────────────────────────────
|
||||
;;
|
||||
;; ASCII only, and deliberately: a byte is a byte here, there is no code point
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
|
||||
flan: unhandled Missing — stopped, not dead.
|
||||
restart: retry
|
||||
restart: use-placeholder
|
||||
0. restart: retry
|
||||
1. restart: use-placeholder
|
||||
|
||||
@ -983,12 +983,14 @@ frame that erred, with nothing unwound, so the condition and every restart betwe
|
||||
and the top are still live:</p>
|
||||
|
||||
<pre><code class="sh">flan: unhandled Missing — stopped, not dead.
|
||||
restart: retry
|
||||
restart: use-placeholder</code></pre>
|
||||
0. restart: retry
|
||||
1. restart: use-placeholder</code></pre>
|
||||
|
||||
<p>From there you fix the function, install it, and take a restart. Control never left
|
||||
the erring frame, so <code>retry</code> calls through the indirection cell and reaches
|
||||
the new body. Installing while stopped is allowed; there is no frame in progress.</p>
|
||||
<p>From there you fix the function, install it, and take a restart. The numbers are
|
||||
how one is taken: a restart is chosen by position, because an inner one may shadow an
|
||||
outer one of the same name and a name alone could not tell you which you were getting.
|
||||
Control never left the erring frame, so <code>retry</code> calls through the
|
||||
indirection cell and reaches the new body. Installing while stopped is allowed; there is no frame in progress.</p>
|
||||
|
||||
<p>The break loop lives in <code>vendor/agent</code>, which is an optional package. A
|
||||
program that does not import it leaves the hook null and stops the old way — the message
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user