Merge branch 'worktree-agent-a721d74291e5f212c' into dev-loop
This commit is contained in:
commit
16226c71d0
37
BUILT.md
37
BUILT.md
@ -5067,3 +5067,40 @@ nothing: the frame that resumed is still inside the old marked body, past the `(
|
||||
as running whether or not the mark was cleared. Half a second is about a hundred calls through the body just
|
||||
installed. `test/programs/dev-pause.flan` exists because `dev-loop.flan` calls `step` four times, which is too tight
|
||||
for that, and because a program that stops on its own — `dev-break.flan` — would prove nothing about what stopped it.
|
||||
|
||||
## A generic may key a map, and the predicate is what pays for it
|
||||
|
||||
The map operations are the second entry on the one list `check.ml` keeps of forms the abstract pass does **not**
|
||||
answer where they are written. `print` and `println` were the first, and for an afternoon they were the only ones:
|
||||
`hashable?` gated the *type* and not the operations, so a generic could take and return a `(Map $t V)` and could not
|
||||
`get` or `put` into one.
|
||||
|
||||
**The reason was implementation, not design.** A map carries a hash and an equality, and `key_pair` emits them as
|
||||
*concrete symbols* chosen from the key type — `flan_hash_str` for a string, `flan_hash_flat` for anything compared
|
||||
bytewise, a generated `map/hash/Point` walking a struct's fields. While `$t` is still a variable there is no symbol
|
||||
to name and nothing to choose between, so the abstract pass could not build the node. Falling through to the flat
|
||||
pair would have been worse than refusing: it would hash a string's pointer and a struct's padding.
|
||||
|
||||
**What closes it is deferral, and what makes deferral safe is the `where` clause.** `put`, `get`, `has-key?`,
|
||||
`reserve` and `clone` — the five arms that reach `key_fns` — now check their arguments and then, when the key is a
|
||||
type variable, return a placeholder of the operation's own type: `Unit` for `put` and `reserve`, `None` for `get`
|
||||
so the `(Option V)` around it still checks, `false` for `has-key?`, a zeroed map for `clone`. The whole node is
|
||||
thrown away with the rest of the abstract pass, exactly as `println`'s is, and the real one is built when the copy
|
||||
is checked with `$t` concrete.
|
||||
|
||||
Every member of that list moves a refusal from the definition to a call site, which is the thing the abstract pass
|
||||
exists to prevent, so **the membership rule matters more than the membership**. `print` and `println` pay nothing:
|
||||
every type prints, there is no printability predicate because one would always hold, and the deferred check always
|
||||
succeeds. The map operations *can* fail at a concrete type — a float key has no equality a map can use — and they
|
||||
are on the list anyway because `{:where (hashable? $t)}` is in the signature. The refusal then has something to
|
||||
point at: it lands at the call that asked for the type, naming the type, the predicate and the clause, and the
|
||||
author of the generic wrote that requirement down. That is categorically different from an unconstrained
|
||||
`(+ a b)` failing deep in a body with no signature to blame, which stays refused at its definition.
|
||||
|
||||
**So a generic that does not declare the predicate gets no deferral.** `deferred_key` checks `declares` before it
|
||||
answers yes, and in practice `map_type` has already refused the signature where the type was written — `(Map $t
|
||||
i32)` under `{:where (copyable? $t)}` is not a type. `key_pair`'s `Types.Var` arm survives as a backstop for a
|
||||
route neither covers, and says so rather than claiming to be a design.
|
||||
|
||||
`test/programs/generics.flan` runs one written body at two key types; `test/programs/generic-map-reject.flan` is
|
||||
the other half, a call site at `f64` refused against the clause.
|
||||
|
||||
18
NEXT.md
18
NEXT.md
@ -201,6 +201,24 @@ The prelude keeps a per-type layer for the numeric ones. That is the honest numb
|
||||
5. **Generics across a real compilation-unit boundary.** `Load` flattens imports before checking so it works
|
||||
today, but a package boundary that ever becomes a real unit boundary needs the generic's *body* to cross it —
|
||||
which separate compilation cannot do, and is why C++ puts templates in headers.
|
||||
6. ~~**`hashable?` gates the type and not the operations.**~~ **Closed the same day it landed.** It was real for
|
||||
an afternoon: a generic could take and return a `(Map $t V)` and could not `get` or `put` into one, because the
|
||||
hash and the equality pair are emitted as concrete symbols chosen from the key type and there is no symbol to
|
||||
name while `$t` is a variable. The fix is that the five map operations that reach the pair — `put`, `get`,
|
||||
`has-key?`, `reserve`, `clone` — are now **deferred to the instantiation**, joining `print` and `println` on
|
||||
the one list of forms the abstract pass does not answer where they are written.
|
||||
|
||||
**What made that acceptable is the clause, and it is worth stating as a rule rather than as a special case.**
|
||||
Every member of that list moves a refusal from the definition to a call site, which is the thing the abstract
|
||||
pass exists to prevent. `print` and `println` pay nothing for it — every type prints, so the deferred check
|
||||
always succeeds. The map operations *can* fail, and the reason they are still allowed on is that
|
||||
`{:where (hashable? $t)}` is in the signature: an instantiation at a type with no usable equality is refused
|
||||
against a requirement the author wrote down, naming the call site, the type it asked for and the predicate it
|
||||
failed. That is categorically different from an unconstrained `(+ a b)` failing deep in a body with nothing to
|
||||
blame. **A generic that does not declare the predicate gets no deferral** — `deferred_key` checks first, and
|
||||
`map_type` has usually refused the signature before that. The membership rule for the list is therefore not a
|
||||
headcount: either the operation cannot fail after substituting, or a declared predicate gives its failure
|
||||
somewhere to land.
|
||||
|
||||
## Decided by the author, 2026-09-13: a type variable takes a `$` sigil
|
||||
|
||||
|
||||
141
lib/check.ml
141
lib/check.ml
@ -1226,28 +1226,26 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
|
||||
the concrete type does not exist until the instantiation. Refused rather
|
||||
than assumed — falling through to [bytewise_key] would hash whatever
|
||||
bytes the variable turned out to have, which is the wrong answer for a
|
||||
[string] and for any struct with padding. Inside an instantiation this
|
||||
arm is unreachable: [env.subst] has already made [k] concrete.
|
||||
[string] and for any struct with padding.
|
||||
|
||||
**This is a known hole and it is deliberate.** It means [hashable?] gates
|
||||
the *type* and not the operations: a generic may take or return a
|
||||
[(Map $t V)] under it, and may not [put], [get] or [has?] into one. The
|
||||
alternative is to add the map operations to the list of forms the
|
||||
abstract pass defers to instantiation — the list [print] and [println]
|
||||
are the only members of — and every member of that list is a place where
|
||||
a refusal moves from the definition to a call site, which is the thing
|
||||
the abstract pass exists to prevent. Two members is a short list worth
|
||||
keeping short; six is a rule nobody can hold in their head. If a generic
|
||||
over maps is ever wanted, this is the decision to revisit, and it is one
|
||||
line here plus one in [key_fns]. *)
|
||||
**This arm is a backstop and nothing normal reaches it.** Two things get
|
||||
there first. Inside an instantiation [env.subst] has already made [k]
|
||||
concrete, so there is no variable left. Outside one — in the abstract
|
||||
pass over a generic body — the map operations are *deferred*
|
||||
([deferred_key] below): a key that is a variable declared [hashable?]
|
||||
never asks for a pair here, and a variable that is not declared it never
|
||||
gets as far as a [(Map $t V)] to operate on, because [map_type] refuses
|
||||
the type where it is written. What is left for this arm is a key that is
|
||||
a variable by some route neither of those covers, and the honest answer
|
||||
to that is still a refusal rather than a guessed pair. *)
|
||||
| Types.Var v ->
|
||||
Loc.failk "check/generic-map-key" loc
|
||||
"a map keyed by the type variable %s cannot be operated on here: the \
|
||||
hash and the equality are emitted as concrete symbols chosen from the \
|
||||
concrete key type, and there is no concrete key type until this \
|
||||
generic is instantiated. {:where (hashable? $%s)} says the map may be \
|
||||
taken and returned, not that its keys can be hashed here — write the \
|
||||
operation in a function over the concrete key type and call that" v v
|
||||
"a map keyed by the type variable %s has no hash and no equality here: \
|
||||
both are emitted as concrete symbols chosen from the concrete key \
|
||||
type, and there is none until this generic is instantiated. The map \
|
||||
operations are deferred to the instantiation when {:where (hashable? \
|
||||
$%s)} is declared — declare it, or write the operation in a function \
|
||||
over the concrete key type and call that" v v
|
||||
| Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
|
||||
| t when bytewise_key t ->
|
||||
Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
|
||||
@ -1417,6 +1415,38 @@ let key_fns env loc k =
|
||||
let h, e = key_pair env loc k in
|
||||
mk loc Types.Alloc (Tast.FnAddr h), mk loc Types.Alloc (Tast.FnAddr e)
|
||||
|
||||
(* ── The map operations, deferred to the instantiation ─────────────────
|
||||
True when the key is a type variable, which means the operation cannot be
|
||||
built here and must be answered by the copy: [key_fns] emits concrete
|
||||
symbols and there is no concrete key type yet. The caller checks its
|
||||
arguments first and then returns a placeholder of the operation's own type,
|
||||
exactly as [print] does — see the allow-list comment at the [print] arm for
|
||||
what being on that list costs and why these are on it.
|
||||
|
||||
The predicate is *required* before deferring, and that is the whole safety
|
||||
argument: with {:where (hashable? $t)} in the signature, the instantiation
|
||||
refuses at the call site against a requirement the author wrote down. A
|
||||
variable with no such clause is refused here and now, at the definition,
|
||||
which is where the abstract pass wants every refusal that has nothing to
|
||||
point at. In practice [map_type] has already refused such a signature where
|
||||
the type was written; this repeats it rather than relying on that, the same
|
||||
way [key_pair] repeats [map_type]'s key check. *)
|
||||
let deferred_key env loc what (k : Types.t) =
|
||||
match k with
|
||||
| Types.Var v ->
|
||||
if not (declares env.tvpreds v "hashable?") then
|
||||
Loc.failk "check/generic-map-key" loc
|
||||
"%s over a map keyed by the type variable %s is refused: the hash and \
|
||||
the equality are emitted as concrete symbols chosen from the \
|
||||
concrete key type, and nothing here declares %s hashable. Write \
|
||||
{:where (hashable? $%s)} at the head of the body — then the \
|
||||
operation is deferred to each instantiation, and a call site that \
|
||||
asks for a key type that cannot be hashed is refused there, against \
|
||||
the clause"
|
||||
what (Types.to_string k) (Types.to_string k) v;
|
||||
true
|
||||
| _ -> false
|
||||
|
||||
let rec check ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
let loc = e.Ast.loc in
|
||||
(* Read the permission this form was given and withdraw it in the same
|
||||
@ -3639,6 +3669,13 @@ and named_call ctx ~want loc name args =
|
||||
let n64 =
|
||||
mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
|
||||
in
|
||||
(* Deferred: the sizes are known abstractly but the hash is not, so
|
||||
the node is a unit no-op and the copy builds the real one. *)
|
||||
if (match target.Tast.ty with
|
||||
| Types.Map (k, _) -> deferred_key ctx.env loc "reserve" k
|
||||
| _ -> false) then
|
||||
expect loc ~want (mk loc Types.Unit Tast.Unit)
|
||||
else
|
||||
let attempt, note =
|
||||
match target.Tast.ty with
|
||||
(* For a map the number is entries, not slots: the runtime sizes the
|
||||
@ -3744,6 +3781,12 @@ and named_call ctx ~want loc name args =
|
||||
seed is derived from the block's address — see flan_rt.c. That is
|
||||
the runtime's business; from here it is one more allocating call
|
||||
under the same guard. *)
|
||||
| Types.Map (k, v) when deferred_key ctx.env loc "clone" k ->
|
||||
(* Deferred, and the placeholder is a zeroed map of the same type —
|
||||
the value a (map-new) starts from, so everything written around
|
||||
the clone still checks against the type it will have. *)
|
||||
let mty = Types.Map (k, v) in
|
||||
expect loc ~want (mk loc mty (Tast.Zero mty))
|
||||
| Types.Map (k, v) ->
|
||||
let mty = Types.Map (k, v) in
|
||||
let hash, _ = key_fns ctx.env loc k in
|
||||
@ -4045,6 +4088,12 @@ and named_call ctx ~want loc name args =
|
||||
let kt, vt = map_kv loc "put" target.Tast.ty in
|
||||
let k = check ctx ~want:kt k in
|
||||
let v = check ctx ~want:vt v in
|
||||
(* Deferred: the arguments are checked — so a move here is still a move
|
||||
and a borrow still a borrow — and the node itself is a unit no-op,
|
||||
thrown away with the rest of the abstract pass. *)
|
||||
if deferred_key ctx.env loc "put" kt then
|
||||
expect loc ~want (mk loc Types.Unit Tast.Unit)
|
||||
else
|
||||
(* Both are bound before the loop, so that a [retry] re-attempts the
|
||||
allocation and not the expressions that produced the key and the
|
||||
value. The same rule [push] follows for its element. *)
|
||||
@ -4076,6 +4125,12 @@ and named_call ctx ~want loc name args =
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let kt, vt = map_kv loc "get" target.Tast.ty in
|
||||
let k = check ctx ~want:kt k in
|
||||
(* Deferred, and the placeholder is [None] rather than [Unit]: this
|
||||
form answers an (Option V), and the abstract pass still has to
|
||||
type-check whatever the body does with the answer. *)
|
||||
if deferred_key ctx.env loc "get" kt then
|
||||
expect loc ~want (mk loc (Types.Option vt) Tast.None_)
|
||||
else
|
||||
let hash, eq = key_fns ctx.env loc kt in
|
||||
let ks = fresh_slot ctx kt in
|
||||
let out = fresh_slot ctx vt in
|
||||
@ -4157,6 +4212,11 @@ and named_call ctx ~want loc name args =
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let kt, vt = map_kv loc "has-key?" target.Tast.ty in
|
||||
let k = check ctx ~want:kt k in
|
||||
(* Deferred, and the placeholder is a [bool] — the form a condition
|
||||
wants, so the condition around it still has to check. *)
|
||||
if deferred_key ctx.env loc "has-key?" kt then
|
||||
expect loc ~want (mk loc Types.Bool (Tast.Bool false))
|
||||
else
|
||||
let hash, eq = key_fns ctx.env loc kt in
|
||||
let ks = fresh_slot ctx kt in
|
||||
let found =
|
||||
@ -4540,8 +4600,7 @@ and named_call ctx ~want loc name args =
|
||||
printing of one would be its last. *)
|
||||
let target = List.hd args in
|
||||
let a = borrowed ctx target (fun () -> check ctx target) in
|
||||
(* ── The allow-list, and it has exactly two members: [print] and
|
||||
[println]. ──────────────────────────────────────────────────────
|
||||
(* ── The allow-list, and what it takes to get on it ───────────────
|
||||
plan.org names [println] as the one compiler-provided exception — it
|
||||
"selects a structural printer at each concrete instantiation" — and
|
||||
that cannot be reconciled with an abstract pass as written: a pass that
|
||||
@ -4553,10 +4612,33 @@ and named_call ctx ~want loc name args =
|
||||
|
||||
Every member of this list is a place where a refusal moves from the
|
||||
definition to a call site, which is the thing the abstract pass exists
|
||||
to prevent. That is the whole cost of the exception and the reason the
|
||||
list stays two long and is written down here. There is no [where]
|
||||
predicate for printability on purpose: every type prints, so the
|
||||
predicate would always hold and would only be noise on a signature.
|
||||
to prevent. **That cost is not the same for every member, and the list
|
||||
is not closed.** What makes it bearable is whether the call site has a
|
||||
*stated requirement* to be refused against.
|
||||
|
||||
[print] and [println] have none and need none: every type prints, so
|
||||
there is no [where] predicate for printability — one would always hold
|
||||
and would be noise on a signature — and there is correspondingly no
|
||||
call site these can be refused at. They are deferred and then always
|
||||
succeed. That is the cheapest possible membership.
|
||||
|
||||
The map operations — [put], [get], [has-key?], [reserve], [clone],
|
||||
through [deferred_key] beside [key_fns] — are the other kind, and they
|
||||
are here on a different argument. They *can* fail at a concrete type,
|
||||
so deferring them does move a refusal. But [{:where (hashable? $t)}] is
|
||||
in the signature, and it is the author's own written requirement: an
|
||||
instantiation at a non-hashable type is refused against that clause, by
|
||||
name, at the call that asked for the type. That is a refusal the caller
|
||||
can act on and one the generic's author chose to be responsible for —
|
||||
categorically different from an unconstrained [(+ a b)] failing deep in
|
||||
a body with no signature to blame, which is the case the abstract pass
|
||||
exists to prevent and which stays refused at the definition. A generic
|
||||
that does *not* declare the predicate gets no deferral: [deferred_key]
|
||||
checks first, and [map_type] has usually refused the signature already.
|
||||
|
||||
So the rule for adding to this list is not a headcount. It is: either
|
||||
the operation cannot fail after substituting, or a declared predicate
|
||||
gives its failure a place to land. Anything else is answered here.
|
||||
|
||||
The node produced here is a unit no-op, thrown away with the rest of
|
||||
the abstract pass. The real printer is selected when the copy is
|
||||
@ -4871,9 +4953,12 @@ and instantiate env loc gname vars subst cparams cret =
|
||||
| Some t ->
|
||||
if not (pred_holds p.Ast.pname t) then
|
||||
Loc.failk "check/predicate-unsatisfied" loc
|
||||
"%s here would instantiate %s at $%s = %s, and %s is not %s — \
|
||||
the body of %s is written against {:where (%s $%s)}"
|
||||
gname gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
|
||||
"this call instantiates %s at $%s = %s, and %s does not \
|
||||
answer %s — which %s requires, being written {:where (%s \
|
||||
$%s)}. The requirement is the signature's, so the refusal is \
|
||||
here, at the call that asked for the type: pass one the \
|
||||
predicate admits"
|
||||
gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
|
||||
p.Ast.pname gname p.Ast.pname p.Ast.pvar)
|
||||
fn.Ast.fwhere;
|
||||
(* The entry goes in *before* the body is checked, which is what makes a
|
||||
|
||||
26
test/programs/generic-map-reject.flan
Normal file
26
test/programs/generic-map-reject.flan
Normal file
@ -0,0 +1,26 @@
|
||||
;;;; The map operations over a type-variable key, refused at the call site.
|
||||
;;;;
|
||||
;;;; A generic body is checked once with its type variables abstract, and the
|
||||
;;;; map operations are one of the few forms that cannot be answered there:
|
||||
;;;; the hash and the equality are emitted as concrete symbols chosen from the
|
||||
;;;; concrete key type, and there is none until a copy exists. So they are
|
||||
;;;; deferred to the instantiation, the way print and println are.
|
||||
;;;;
|
||||
;;;; What makes deferring them safe — and different from an unconstrained
|
||||
;;;; (+ a b), which stays refused at the definition — is the clause. The
|
||||
;;;; signature says {:where (hashable? $t)}, so a call site that asks for a
|
||||
;;;; key type with no usable equality is refused against a requirement the
|
||||
;;;; author wrote down, at the call that asked for it. A float is that type:
|
||||
;;;; NaN is not equal to itself, and 0.0 and -0.0 are equal while differing
|
||||
;;;; bytewise.
|
||||
(defn seen? [k $t] bool
|
||||
{:where (hashable? $t)}
|
||||
(let [m (map-new t i32)]
|
||||
(put m k 1)
|
||||
(let [answer (has-key? m k)]
|
||||
(free m)
|
||||
answer)))
|
||||
|
||||
(defn main [] ()
|
||||
(println (seen? 3))
|
||||
(println (seen? 1.5)))
|
||||
@ -86,6 +86,27 @@
|
||||
{:where (copyable? $t)}
|
||||
(do x (zeroed)))
|
||||
|
||||
;; The map operations over a key that is a type variable. The hash and the
|
||||
;; equality are concrete symbols chosen from the concrete key type, so there
|
||||
;; is nothing to emit here — these are deferred to the instantiation, the way
|
||||
;; println is, and {:where (hashable? $t)} is what allows it: the refusal for
|
||||
;; a key type that cannot be hashed lands at the call site, against a
|
||||
;; requirement written down in this signature. Without the clause the type
|
||||
;; (Map $t i32) is refused where it is written; see generic-map-reject.flan
|
||||
;; for the call-site half.
|
||||
(defn bump [k $t n i32] i32
|
||||
{:where (hashable? $t)}
|
||||
(let [m (map-new t i32)]
|
||||
(reserve m 8)
|
||||
(put m k n)
|
||||
(put m k (+ n (match (get m k) (Some v) v _ 0)))
|
||||
(let [c (clone m)
|
||||
answer (+ (match (get c k) (Some v) v _ -1)
|
||||
(if (has-key? c k) 1 0))]
|
||||
(free c)
|
||||
(free m)
|
||||
answer)))
|
||||
|
||||
(defn main [] ()
|
||||
(println (ident 3))
|
||||
(println (ident 4.5))
|
||||
@ -126,6 +147,10 @@
|
||||
(println (widen 3 (i64 0)))
|
||||
(println (zero-of 9))
|
||||
|
||||
;; One written body, two key types, two emitted copies.
|
||||
(println (bump 7 10))
|
||||
(println (bump "key" 3))
|
||||
|
||||
(let [a (arena-new 4096)
|
||||
keep (filter (slice ns 0 4) (fn [x] (> x 5)))
|
||||
one (one-of 4.5)]
|
||||
|
||||
@ -1325,7 +1325,7 @@ let () =
|
||||
output is an answer a per-type copy used to give. *)
|
||||
let generics_out =
|
||||
"3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\
|
||||
3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n3\n3\n0\n3\n4.5\n"
|
||||
3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n3\n3\n0\n21\n7\n3\n4.5\n"
|
||||
in
|
||||
outputs "generics" "programs/generics.flan" generics_out;
|
||||
outputs ~opt:"-O0" "generics, -O0" "programs/generics.flan" generics_out;
|
||||
@ -1396,6 +1396,18 @@ let () =
|
||||
refuses "a runaway instantiation names the chain"
|
||||
"programs/generic-runaway.flan" "grow at ([2 i32])";
|
||||
|
||||
(* The other half of the map deferral. The operations over a key that is a
|
||||
type variable are deferred to the instantiation — there is no hash and
|
||||
no equality to emit until the key type is concrete — and what makes
|
||||
that safe is that {:where (hashable? $t)} is in the signature, so the
|
||||
refusal lands at the call that asked for the type, against a
|
||||
requirement the author wrote down. What is asserted is that it names
|
||||
the type passed and the predicate it failed, and not the body. *)
|
||||
refuses "a generic over maps, instantiated at a key that cannot be hashed"
|
||||
"programs/generic-map-reject.flan" "does not answer hashable?";
|
||||
refuses "and it names the type the call site asked for"
|
||||
"programs/generic-map-reject.flan" "at $t = f64";
|
||||
|
||||
refuses "a package's main is not visible" "programs/pkg-hidden-main.flan"
|
||||
"sand/main is not a name";
|
||||
refuses "one directory under two aliases" "programs/pkg-two-aliases.flan"
|
||||
|
||||
@ -2194,20 +2194,30 @@ let () =
|
||||
"(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))";
|
||||
|
||||
(* A map key that is a type variable has no hash and no equality to emit:
|
||||
they are chosen from the concrete type, which does not exist yet. So
|
||||
hashable? gates the *type* and not the operations — a generic may take
|
||||
and return a (Map $t V) and may not put into one. Pinned because it is a
|
||||
deliberate hole and not an oversight: closing it means adding the map
|
||||
operations to the list of forms the abstract pass defers to
|
||||
instantiation, which is print and println and should stay that short. *)
|
||||
they are chosen from the concrete type, which does not exist yet. So the
|
||||
map operations join print and println on the list of forms the abstract
|
||||
pass defers to the instantiation — but only under the predicate, which is
|
||||
what gives the deferred refusal somewhere to land. Without one the type
|
||||
itself is refused where it is written, at the definition. *)
|
||||
rejects_check "a map keyed by a type variable that is not hashable?"
|
||||
~needle:"is not a map key"
|
||||
"(defn f [m (Map $t i32)] i32 {:where (copyable? $t)} (len m))";
|
||||
accepts "and hashable? is what says it is"
|
||||
"(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))";
|
||||
rejects_check "but hashable? does not make the key hashable here"
|
||||
~needle:"not that its keys can be hashed here"
|
||||
accepts "and under it the operations are deferred, not refused"
|
||||
"(defn f [m (Map $t i32) k $t] () {:where (hashable? $t)} (put m k 1))";
|
||||
accepts "get over a type-variable key answers an (Option V)"
|
||||
"(defn f [m (Map $t i32) k $t] i32 {:where (hashable? $t)} \
|
||||
(match (get m k) (Some v) v _ 0))";
|
||||
accepts "and so do has-key?, reserve and clone"
|
||||
"(defn f [m (Map $t i32) k $t] bool {:where (hashable? $t)} \
|
||||
(do (reserve m 8) (let [c (clone m)] (free c) (has-key? m k))))";
|
||||
(* The definition is still where a generic with no clause to point at is
|
||||
refused: nothing has been written down for an instantiation to be judged
|
||||
against, so the refusal has nowhere to move to. *)
|
||||
rejects_check "a map built inside a generic that declares nothing"
|
||||
~needle:"is not a map key"
|
||||
"(defn f [k $t] () (let [m (map-new t i32)] (put m k 1) (free m)))";
|
||||
|
||||
(* ── The acceptance program checks end to end ──────────────────── *)
|
||||
accepts "calc-me.flan type checks"
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user