Restarts take parameters, and the check for them is where it has to be

spec-conditions.md §3's remaining half: a clause binds parameters, an
invoke-restart supplies them, and what a restart takes is compared at run
time because a restart is found by name on a dynamic stack — neither end
of the transfer can see the other.

The parameters live in a buffer the restart-case owns, not the invoker's
frame. A clause runs after every frame between the two has returned (§5),
so anything on the invoking side is gone by then; the invoker stores into
the target frame while both are still alive, which is the one moment they
are.

The frame carries the parameter count and a hash of how the types are
spelled, and every frame carries them whether it takes parameters or not:
a clause taking none has to refuse arguments as loudly as one taking two
of the wrong type. The count is not redundant with the hash — it is what
makes a 32-bit collision between two different signatures harmless — and
the spelling itself rides along so that a mismatch can say what was
wanted and what was given, which neither end alone knows.

The arguments are evaluated into slots before the invoke node rather than
hanging off it. An argument that transfers on its own is then guarded
before anything aims the channel, and a call written in an argument is on
the ordinary walk Reach and Load already do — a node they treat as a leaf
would have dropped the function and failed to link.

The other way a transfer starts is the break loop, which chooses by
position and has nothing to fill parameters in with. It reaches a clause
through the same channel, so nothing downstream could tell the two apart:
the frame is pushed with the buffer marked unfilled and a clause with
parameters checks that mark before reading it. Refused with the reason
rather than run on values no one supplied.

runtime/flan_rt.c gains two message functions and nothing else; the
restart frame's first four fields, which are the ones C declares, do not
move.

lib/ast.ml

@@ -57,10 +57,11 @@ and expr_kind =
      A clause binds a name for the condition, so this cannot be a call. *)
   | HandlerBind of hclause list * expr list
   | Signal  of sigkind * expr                 (* (signal c) / (error c)        *)
-  (* (restart-case body (name [] body ...) ...) and (invoke-restart 'name).
+  (* (restart-case body (name [p T] body ...) ...) and
-     Both alter control flow, so neither can be a call. *)
+     (invoke-restart 'name arg ...). Both alter control flow, so neither can be
+     a call, and a clause binds its parameters — §3. *)
   | RestartCase of expr * rclause list
-  | InvokeRestart of string
+  | InvokeRestart of string * expr list
 
 (* Two ways to signal, because they are two different things — §1 and §2.
    [signal] returns Unit whatever it finds; [error] has type Never and, with
@@ -68,7 +69,16 @@ and expr_kind =
 and sigkind = Ssignal | Serror
 
 and hclause = { hty : texpr; hname : string; hbody : expr list; hloc : Loc.t }
-and rclause = { rname : string; rbody : expr list; rloc : Loc.t }
+(* [rparams] are §3's inline annotations, the same name/type pairs a [defn]
+   takes. They are bound in the clause body and filled in by whatever invoked
+   the restart, which is why their count and types are checked at run time
+   (§3): a restart is found by name on a dynamic stack. *)
+and rclause =
+  { rname : string; rparams : field list; rbody : expr list; rloc : Loc.t }
+
+(* Inline name/type pairs, as in [defn], [let] and [defstruct]. Here because a
+   restart clause's parameters are one, and a clause is part of an expression. *)
+and field = { fname : string; fty : texpr; floc : Loc.t }
 
 (* Two unwrap operators, because they are two different things — plan.org. *)
 and unwrap = Usome | Utry
@@ -90,8 +100,6 @@ and pattern =
 
 (* ── Declarations ──────────────────────────────────────────────────── *)
 
-type field = { fname : string; fty : texpr; floc : Loc.t }
-
 type fn = {
   name    : string;
   params  : field list;

lib/check.ml

@@ -338,6 +338,21 @@ let type_id name =
     name;
   !h
 
+(* How a restart's parameter list is spelled, and with it what the two ends of
+   an [invoke-restart] compare — spec-conditions.md §3's run-time check. A
+   restart is found by name on a dynamic stack, so neither end can see the
+   other and nothing static can be checked: what is compared at run time is
+   this string's hash, alongside the count, and the string itself is carried so
+   that a mismatch can say what was wanted and what was given.
+
+   Comparing a 32-bit hash means two different parameter lists could in
+   principle collide. The count is checked separately, which rules out every
+   practical case (a collision would have to be between two lists of the same
+   length), and the types are parenthesised so that [(Option i32)] cannot read
+   as two parameters. *)
+let restart_sig tys =
+  "(" ^ String.concat " " (List.map Types.to_string tys) ^ ")"
+
 let expect loc ~want (got : Tast.expr) =
   match want with
   | None -> got
@@ -489,18 +504,48 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
      establishes frames around a body, and the other leaves the function it is
      written in — so both are their own nodes all the way down. *)
   | Ast.RestartCase (body, clauses) -> check_restart_case ctx ?want loc body clauses
-  | Ast.InvokeRestart name ->
+  | Ast.InvokeRestart (name, args) ->
     (* Never: control resumes at the restart-case, which yields the clause's
        value to *its* continuation, so nothing here has a value and nothing
        after it runs. The lookup is at run time because restarts are
-       dynamically scoped and named — §4. *)
+       dynamically scoped and named — §4 — and so, for the same reason, is the
+       check that these arguments are the ones the clause takes (§3). *)
     if ctx.in_defer then
       fail loc
         "invoke-restart is not allowed inside a defer — a defer is the cleanup \
          a transfer runs on its way out, so starting one there would leave \
          this function's defers half run with two targets and no way to \
          choose";
-    expect loc ~want (mk loc Types.Never (Tast.InvokeRestart (type_id name, name, loc)))
+    let args = map_lr (fun a -> check ctx a) args in
+    List.iter
+      (fun (a : Tast.expr) ->
+         match a.Tast.ty with
+         | Types.Unit | Types.Never ->
+           fail a.Tast.loc
+             "a restart argument must be a value, and this one is %s"
+             (Types.to_string a.Tast.ty)
+         | _ -> ())
+      args;
+    let sg = restart_sig (List.map (fun (a : Tast.expr) -> a.Tast.ty) args) in
+    (* Evaluated into slots first, so that an argument which transfers on its
+       own is guarded before this form aims the channel, and so that a call
+       written in an argument is on the ordinary walk rather than hidden
+       inside a node that [Reach] and [Load] treat as a leaf. *)
+    let binds =
+      List.map (fun (a : Tast.expr) -> (fresh_slot ctx a.Tast.ty, a)) args
+    in
+    let locals =
+      List.map
+        (fun (s, (a : Tast.expr)) -> mk a.Tast.loc a.Tast.ty (Tast.Local s))
+        binds
+    in
+    let invoke =
+      mk loc Types.Never
+        (Tast.InvokeRestart (type_id name, name, locals, sg, type_id sg, loc))
+    in
+    expect loc ~want
+      (if binds = [] then invoke
+       else mk loc Types.Never (Tast.Let (binds, [ invoke ])))
 
   | Ast.Defer _ ->
     (* Registered by [check_fn], which is the only place that sees a form's
@@ -703,13 +748,36 @@ and check_restart_case ctx ?want loc body clauses =
          if List.mem c.Ast.rname !seen then
            fail c.Ast.rloc "this restart-case offers %s twice" c.Ast.rname;
          seen := c.Ast.rname :: !seen;
-         (* Each is checked against what the form has settled on so far, so a
+         (* §3's parameters. They are slots in *this* function — a clause runs
-            clause that disagrees fails where it is written. The first one to
+            here, not where the invoke was — and the invoker stores into a
-            produce a value is what settles it when nothing outside did. *)
+            buffer this frame owns, because its own frame is gone by the time
-         let b = block ctx ?want:!ty c.Ast.rloc c.Ast.rbody in
+            the clause body starts (§5). Bound like a function's parameters:
+            visible only in the clause, and not assignable. *)
+         let params, b =
+           scoped ctx (fun () ->
+             let params =
+               List.map
+                 (fun (p : Ast.field) ->
+                    let ty = resolve ctx.env p.Ast.fty in
+                    (match ty with
+                     | Types.Unit | Types.Never ->
+                       fail p.Ast.floc
+                         "%s would be a restart parameter of type %s, which is \
+                          not a value" p.Ast.fname (Types.to_string ty)
+                     | _ -> ());
+                    (bind ctx p.Ast.fname ty ~assignable:false, ty))
+                 c.Ast.rparams
+             in
+             (* Each is checked against what the form has settled on so far, so
+                a clause that disagrees fails where it is written. The first one
+                to produce a value is what settles it when nothing outside
+                did. *)
+             (params, block ctx ?want:!ty c.Ast.rloc c.Ast.rbody))
+         in
          if !ty = None && b.Tast.ty <> Types.Never then ty := Some b.Tast.ty;
+         let sg = restart_sig (List.map snd params) in
          { Tast.rname_id = type_id c.Ast.rname; rname = c.Ast.rname;
-           rbody = [ b ] })
+           rparams = params; rsig = sg; rsig_id = type_id sg; rbody = [ b ] })
       clauses
   in
   let ty = match !ty with Some t -> t | None -> Types.Never in

lib/emit.ml

@@ -638,7 +638,11 @@ and value_at f (e : Tast.expr) : string =
   (* §4's lookup, then the transfer itself: the frame that was found goes into
      the channel and this function leaves through its landing block. Type
      Never, so nothing follows. *)
-  | Tast.InvokeRestart (id, name, rloc) ->
+  | Tast.InvokeRestart (id, name, args, sg, sg_id, rloc) ->
+    (* The arguments are already in slots — the checker put them there, so an
+       argument that transferred on its own has been guarded before anything
+       here runs. *)
+    let vals = List.map (fun a -> (value f a, a.Tast.ty)) args in
     let t = fresh f in
     ins f "%s = call ptr @flan_find_restart(i32 %d)" t id;
     let ok = fresh f in
@@ -649,6 +653,52 @@ and value_at f (e : Tast.expr) : string =
       let nid, nn = string_bytes f.md name in
       ins f "call void @flan_restart_fail(ptr %s, i64 %d, ptr %s, i64 %d)"
         id n nid nn);
+    (* §3's run-time check. A restart is found by name on a dynamic stack, so
+       what it takes is not knowable here: the frame carries its parameter
+       count and the hash of how they are spelled, and both are compared.
+       The count is not redundant with the hash — it is what makes a 32-bit
+       collision between two different signatures harmless in practice — and
+       it is also the cheaper half. *)
+    let arity = fresh f in
+    ins f "%s = load i32, ptr %s" arity (restart_field f t 5);
+    let a_ok = fresh f in
+    ins f "%s = icmp eq i32 %s, %d" a_ok arity (List.length args);
+    let want = fresh f in
+    ins f "%s = load i32, ptr %s" want (restart_field f t 6);
+    let s_ok = fresh f in
+    ins f "%s = icmp eq i32 %s, %d" s_ok want sg_id;
+    let both = fresh f in
+    ins f "%s = and i1 %s, %s" both a_ok s_ok;
+    fail_block f rloc both (fun id n ->
+      let nid, nn = string_bytes f.md name in
+      (* What the frame says it takes is read off the frame, because only the
+         frame knows; what was given is this call site's own spelling. *)
+      let wp = fresh f in
+      ins f "%s = load ptr, ptr %s" wp (restart_field f t 8);
+      let wl = fresh f in
+      ins f "%s = load i64, ptr %s" wl (restart_field f t 9);
+      let gid, gn = string_bytes f.md sg in
+      ins f
+        "call void @flan_restart_args_fail(ptr %s, i64 %d, ptr %s, i64 %d, \
+         ptr %s, i64 %s, ptr %s, i64 %d)" id n nid nn wp wl gid gn);
+    (* Into the buffer the target frame owns, field by field: this frame is
+       about to go, and the clause runs after it has. The layout is the one the
+       signature just agreed on. *)
+    if vals <> [] then begin
+      let buf = fresh f in
+      ins f "%s = load ptr, ptr %s" buf (restart_field f t 4);
+      let sty =
+        "{ " ^ String.concat ", " (List.map (fun (_, ty) -> ll ty) vals) ^ " }"
+      in
+      List.iteri
+        (fun i (v, ty) ->
+           let p = fresh f in
+           ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d"
+             p sty buf i;
+           ins f "store %s %s, ptr %s" (ll ty) v p)
+        vals;
+      ins f "store i32 1, ptr %s" (restart_field f t 7)
+    end;
     ins f "store ptr %s, ptr %s" t xfer_param;
     term f "br label %%%s" (current_pad f);
     "zeroinitializer"
@@ -898,7 +948,19 @@ and emit_handled f frames body =
   if not reached then begin f.live <- false; "zeroinitializer" end
   else begin label f ld; "zeroinitializer" end
 
-(* (restart-case BODY (name [] BODY-1) ...) — §3, §4 and §6 together.
+(* A clause's parameters, as one LLVM struct: what the invoker stores into and
+   what the clause loads out of. The two ends never see each other, so the
+   layout is agreed by the signature hash they compare first — same types in
+   the same order is the same struct. *)
+and args_type (c : Tast.rclause) =
+  "{ " ^ String.concat ", " (List.map (fun (_, t) -> ll t) c.Tast.rparams) ^ " }"
+
+and restart_field f slot i =
+  let p = fresh f in
+  ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 %d" p slot i;
+  p
+
+(* (restart-case BODY (name [p T] BODY-1) ...) — §3, §4 and §6 together.
 
    One frame per clause, so that the frame a transfer names says which clause
    to run: the address is the identity, which is exact where a number would
@@ -909,33 +971,55 @@ and emit_handled f frames body =
 
    §5's defers between here and the invoke have already run — each function on
    the way out ran its own before returning. What is left here is to take these
-   frames off and start the clause. *)
+   frames off, copy §3's parameters out of the buffer the invoker filled, and
+   start the clause.
+
+   The parameters live in a buffer this frame owns, not the invoker's: by the
+   time a clause runs, every frame between the two has returned, so anything on
+   the invoking side is gone. The invoker stores into it while both are alive,
+   which is the one moment they are. *)
 and emit_restart_case f ty clauses body =
   let result = if is_void ty then None else Some (alloca f ty) in
   let frames =
     map_lr
       (fun (c : Tast.rclause) ->
          let slot = alloca_raw f "%restart" in
-         let nid = fresh f in
+         ins f "store i32 %d, ptr %s" c.Tast.rname_id (restart_field f slot 1);
-         ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 1"
-           nid slot;
-         ins f "store i32 %d, ptr %s" c.Tast.rname_id nid;
          (* The name itself, beside the hash. A hash is all that matching
             needs, but a break loop has to *show* someone their choices, and
             nothing at run time can turn a hash back into a name. *)
          let sid, slen = string_bytes f.md c.Tast.rname in
-         let np = fresh f in
+         ins f "store ptr %s, ptr %s" sid (restart_field f slot 2);
-         ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 2"
+         ins f "store i64 %d, ptr %s" slen (restart_field f slot 3);
-           np slot;
+         (* §3's signature, which every frame carries whether it takes
-         ins f "store ptr %s, ptr %s" sid np;
+            parameters or not: an [invoke-restart] compares against whatever
-         let nl = fresh f in
+            frame the name found, and a clause taking none has to be able to
-         ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 3"
+            refuse arguments as loudly as one taking two of the wrong type. *)
-           nl slot;
+         ins f "store i32 %d, ptr %s"
-         ins f "store i64 %d, ptr %s" slen nl;
+           (List.length c.Tast.rparams) (restart_field f slot 5);
+         ins f "store i32 %d, ptr %s" c.Tast.rsig_id (restart_field f slot 6);
+         let gid, glen = string_bytes f.md c.Tast.rsig in
+         ins f "store ptr %s, ptr %s" gid (restart_field f slot 8);
+         ins f "store i64 %d, ptr %s" glen (restart_field f slot 9);
+         let args =
+           if c.Tast.rparams = [] then None
+           else begin
+             let buf = alloca_raw f (args_type c) in
+             ins f "store ptr %s, ptr %s" buf (restart_field f slot 4);
+             (* Nothing has filled it in yet. Whoever aims a transfer at this
+                frame without going through an [invoke-restart] — the break
+                loop, today — leaves this zero, and the clause traps rather
+                than running on values no one supplied. *)
+             ins f "store i32 0, ptr %s" (restart_field f slot 7);
+             Some buf
+           end
+         in
          ins f "call void @flan_restart_push(ptr %s)" slot;
-         slot)
+         (slot, args))
       clauses
   in
+  let args_of slot = List.assoc slot frames in
+  let frames = List.map fst frames in
   let pop () =
     List.iter
       (fun slot -> ins f "call void @flan_restart_pop(ptr %s)" slot)
@@ -966,6 +1050,37 @@ and emit_restart_case f ty clauses body =
      guarded like any other; it must not start with the channel still set. *)
   ins f "store ptr null, ptr %s" xfer_param;
   pop ();
+  (* §3's parameters, copied out of the frame's buffer into the clause's own
+     slots before its body starts. The frame is still addressable — it is an
+     alloca of *this* function — and the buffer is whatever the invoker left
+     there. *)
+  let bind_params slot (c : Tast.rclause) =
+    match args_of slot with
+    | None -> ()
+    | Some buf ->
+      let armed = fresh f in
+      ins f "%s = load i32, ptr %s" armed (restart_field f slot 7);
+      let ok = fresh f in
+      ins f "%s = icmp ne i32 %s, 0" ok armed;
+      (* Aimed here by something that supplied no arguments — there is no such
+         path from an [invoke-restart], so this is the break loop taking a
+         restart it cannot yet fill in. Refused with the reason, rather than
+         running the clause on a buffer nobody wrote. *)
+      fail_block f (List.hd c.Tast.rbody).Tast.loc ok (fun id n ->
+        let nid, nn = string_bytes f.md c.Tast.rname in
+        let gid, gn = string_bytes f.md c.Tast.rsig in
+        ins f
+          "call void @flan_restart_unarmed(ptr %s, i64 %d, ptr %s, i64 %d, \
+           ptr %s, i64 %d)" id n nid nn gid gn);
+      List.iteri
+        (fun i (slot_i, ty) ->
+           let p = fresh f in
+           ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d"
+             p (args_type c) buf i;
+           let v = load f p ty in
+           ins f "store %s %s, ptr %s" (ll ty) v f.slots.(slot_i))
+        c.Tast.rparams
+  in
   let rec dispatch = function
     | [] ->
       ins f "store ptr %s, ptr %s" tgt xfer_param;
@@ -976,6 +1091,7 @@ and emit_restart_case f ty clauses body =
       ins f "%s = icmp eq ptr %s, %s" t tgt slot;
       term f "br i1 %s, label %%%s, label %%%s" t hit next;
       label f hit;
+      bind_params slot c;
       yield (block f c.Tast.rbody);
       label f next;
       dispatch rest
@@ -1545,7 +1661,14 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
 ; target field, because the frame's own address *is* the target — which makes
 ; a transfer's aim exact, and makes re-entering a restart-case work with
 ; nothing extra, since each activation allocates its own.
-%restart = type { ptr, i32, ptr, i64 }
+;
+; Then §3's parameters: the buffer the clause reads them out of — owned by the
+; restart-case, because the invoker's frame is gone by the time a clause runs —
+; how many there are, the hash of how they are spelled, whether anything has
+; filled the buffer in, and that spelling itself for the message when the two
+; ends disagree. The first four fields are what the runtime's own
+; [flan_restart] declares and their offsets do not move.
+%restart = type { ptr, i32, ptr, i64, ptr, i32, i32, i32, ptr, i64 }
 
 declare void @flan_rt_init(i32, ptr)
 declare void @flan_argv(ptr)
@@ -1565,6 +1688,8 @@ declare void @flan_restart_push(ptr)
 declare void @flan_restart_pop(ptr)
 declare ptr @flan_find_restart(i32)
 declare void @flan_restart_fail(ptr, i64, ptr, i64) noreturn cold
+declare void @flan_restart_args_fail(ptr, i64, ptr, i64, ptr, i64, ptr, i64) noreturn cold
+declare void @flan_restart_unarmed(ptr, i64, ptr, i64, ptr, i64) noreturn cold
 declare void @flan_transfer_fail(ptr, i64) noreturn cold
 declare void @flan_bounds_fail(ptr, i64, i64, i64) noreturn cold
 declare void @flan_slice_fail(ptr, i64, i64, i64, i64) noreturn cold

lib/load.ml

@@ -202,15 +202,29 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr =
     | Ast.Unwrap (u, v) -> Ast.Unwrap (u, go v)
     | Ast.Signal (k, c) -> Ast.Signal (k, go c)
     (* A restart name is not a top-level name — it is looked up on the restart
-       stack, not in the environment — so an import does not qualify it. Only
+       stack, not in the environment — so an import does not qualify it. The
-       the bodies are rewritten. *)
+       bodies are rewritten, and so are a clause's parameter types, which name
+       types like any other annotation; the parameters themselves bind inside
+       the clause and shadow a package name there. *)
     | Ast.RestartCase (body, clauses) ->
       Ast.RestartCase
         (go body,
          List.map
-           (fun (c : Ast.rclause) -> { c with Ast.rbody = gos c.Ast.rbody })
+           (fun (c : Ast.rclause) ->
+              let ps =
+                List.map
+                  (fun (p : Ast.field) ->
+                     { p with Ast.fty = rename_texpr owned alias p.Ast.fty })
+                  c.Ast.rparams
+              in
+              let bound =
+                List.map (fun (p : Ast.field) -> p.Ast.fname) ps @ bound
+              in
+              { c with
+                Ast.rparams = ps;
+                rbody = List.map (rename_expr owned alias bound) c.Ast.rbody })
            clauses)
-    | Ast.InvokeRestart _ -> e.Ast.e
+    | Ast.InvokeRestart (n, args) -> Ast.InvokeRestart (n, gos args)
     (* A clause names a condition *type*, which an import renames like any
        other, and binds a name for the condition inside its own body. *)
     | Ast.HandlerBind (clauses, body) ->
@@ -336,8 +350,11 @@ let rec expr_uses acc (e : Ast.expr) =
   let go = expr_uses acc in
   let gos = List.iter go in
   match e.Ast.e with
-  | Ast.Int _ | Ast.Float _ | Ast.Byte _ | Ast.Str _ | Ast.Kw _ | Ast.Quote _
+  | Ast.Int _ | Ast.Float _ | Ast.Byte _ | Ast.Str _ | Ast.Kw _ | Ast.Quote _ ->
-  | Ast.InvokeRestart _ -> ()
+    ()
+  (* The name is not one an import can supply, but the arguments are ordinary
+     expressions and may well use one. *)
+  | Ast.InvokeRestart (_, args) -> gos args
   | Ast.Var n -> acc := (n, e.Ast.loc) :: !acc
   | Ast.Do body -> gos body
   | Ast.Let (bs, body) ->
@@ -365,7 +382,11 @@ let rec expr_uses acc (e : Ast.expr) =
   | Ast.Signal (_, c) -> go c
   | Ast.RestartCase (body, clauses) ->
     go body;
-    List.iter (fun (c : Ast.rclause) -> gos c.Ast.rbody) clauses
+    List.iter
+      (fun (c : Ast.rclause) ->
+         List.iter (fun (p : Ast.field) -> texpr_uses acc p.Ast.fty) c.Ast.rparams;
+         gos c.Ast.rbody)
+      clauses
   | Ast.HandlerBind (clauses, body) ->
     List.iter
       (fun (c : Ast.hclause) -> texpr_uses acc c.Ast.hty; gos c.Ast.hbody)

lib/parse.ml

@@ -256,47 +256,41 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     in
     mk (Ast.HandlerBind (List.map clause clauses, body_of body))
 
-  (* (restart-case BODY (name [] BODY-1) ...) — spec-conditions.md §3.
+  (* (restart-case BODY (name [p T ...] BODY-1) ...) — spec-conditions.md §3.
-     The body and every clause have the same type, which is the form's.
+     The body and every clause have the same type, which is the form's. A
-     Restarts take no parameters in this version; a clause that declares one is
+     clause's parameters are inline name/type pairs, like any other binding
-     rejected below rather than ignored. *)
+     form; what fills them in is the [invoke-restart] that chose the clause. *)
   | Sym "restart-case" ->
     let body, clauses =
       match args with
       | body :: clauses when clauses <> [] -> (body, clauses)
       | _ ->
-        fail f "restart-case is (restart-case body (name [] body ...) ...)"
+        fail f "restart-case is (restart-case body (name [p T] body ...) ...)"
     in
     let clause (c : Form.t) =
       match c.Form.v with
       | Form.List ({ v = Form.Sym n; _ } :: { v = Form.Vec ps; _ } :: cbody)
         when cbody <> [] ->
-        if ps <> [] then
+        { Ast.rname = n; rparams = fields c ps;
-          fail c
+          rbody = List.map expr cbody; rloc = c.Form.loc }
-            "a restart takes no parameters yet — spec-conditions.md §3 has \
+      | _ -> fail c "a restart-case clause is (name [p T] body ...)"
-             them, and they need argument marshalling and a runtime arity \
-             check that this version does not do";
-        { Ast.rname = n; rbody = List.map expr cbody; rloc = c.Form.loc }
-      | _ -> fail c "a restart-case clause is (name [] body ...)"
     in
     mk (Ast.RestartCase (expr body, List.map clause clauses))
 
-  (* (invoke-restart 'name) : Never. The name is a quoted symbol — that is what
+  (* (invoke-restart 'name arg ...) : Never. The name is a quoted symbol — that
-     the reader's quote is for — and it is resolved on the restart stack at run
+     is what the reader's quote is for — and it is resolved on the restart
-     time, since restarts are dynamically scoped. *)
+     stack at run time, since restarts are dynamically scoped. The arguments
+     fill in the clause's parameters, and how many there are and what they are
+     is settled at run time too, against the frame the name found (§3). *)
   | Sym "invoke-restart" ->
     (match args with
-     | [ { v = Form.List [ { v = Form.Sym "quote"; _ }; { v = Form.Sym n; _ } ]; _ } ] ->
+     | { v = Form.List [ { v = Form.Sym "quote"; _ }; { v = Form.Sym n; _ } ]; _ }
-       mk (Ast.InvokeRestart n)
+       :: rest ->
-     | [ _ ] ->
+       mk (Ast.InvokeRestart (n, List.map expr rest))
-       fail f
-         "invoke-restart takes a quoted restart name, as in \
-          (invoke-restart 'use-placeholder)"
      | _ ->
        fail f
-         "a restart takes no arguments yet — spec-conditions.md §3 has them, \
+         "invoke-restart takes a quoted restart name and then its arguments, \
-          and they need argument marshalling and a runtime arity check that \
+          as in (invoke-restart 'use-value 42)")
-          this version does not do")
 
   (* ── macros ────────────────────────────────────────────────────── *)
   (* The reader now produces these three, so they arrive here as ordinary heads

lib/tast.ml

@@ -81,9 +81,20 @@ and expr_kind =
      *its* frames it runs that clause instead, and the whole form yields either
      way. [InvokeRestart] looks the name up on the restart stack, writes the
      frame it found into the transfer channel and leaves — it has type Never,
-     so nothing follows it. *)
+     so nothing follows it.
+
+     [InvokeRestart]'s arguments are already evaluated: the checker binds each
+     to a slot and wraps the node in a [Let], so what is left here is a list of
+     locals to copy into the frame. Two reasons, and both matter. An argument
+     that transfers on its own must be guarded before this one aims the
+     channel; and a call written in an argument has to be on the walk [Reach]
+     and [Load] already do, which a list hanging off a node they treat as a
+     leaf would not be. [rsig] is the argument types as written, and [rsig_id]
+     their hash — §3's run-time check, since the name is resolved on a stack
+     nothing static can see. *)
   | RestartCase of rclause list * expr
-  | InvokeRestart of int * string * Loc.t   (* name id, name, where *)
+  (* name id, name, arguments, their spelling, its hash, where *)
+  | InvokeRestart of int * string * expr list * string * int * Loc.t
 
 (* [Serror] is §2's diverging variant: the same lookup, type Never, and with
    nothing transferring the program stops rather than carrying on. *)
@@ -102,8 +113,15 @@ and hframe = { htype : int; hfn : string }
 
 (* A restart clause. [rname_id] is what [invoke-restart] matches by name; the
    body is a branch in the function that wrote it, because unlike a handler a
-   clause runs at the restart-case, which is where it was written. *)
+   clause runs at the restart-case, which is where it was written.
-and rclause = { rname_id : int; rname : string; rbody : expr list }
+
+   [rparams] are the slots §3's parameters are bound to, in order, with their
+   types; the invoker stores into a buffer this frame owns and the clause loads
+   them from it. [rsig] is how those types are spelled and [rsig_id] its hash:
+   what the two ends compare, since neither can see the other. *)
+and rclause =
+  { rname_id : int; rname : string; rparams : (int * Types.t) list;
+    rsig : string; rsig_id : int; rbody : expr list }
 
 (* [binds] are the slots the pattern's fields are bound to, in field order. *)
 and arm = { acase : string option; binds : int list; abody : expr list }

runtime/flan_rt.c

@@ -398,6 +398,40 @@ _Noreturn void flan_restart_fail(const uint8_t *loc, int64_t loclen,
   rt_die();
 }
 
+/* The frame the name found does not take these arguments — spec-conditions.md
+ * §3's run-time check. It has to be at run time: a restart is resolved on a
+ * dynamic stack, so the invoke site cannot see what it will find, and the
+ * frame cannot see who will find it. What each end knows is its own parameter
+ * list, so the message is both of them side by side. */
+_Noreturn void flan_restart_args_fail(const uint8_t *loc, int64_t loclen,
+                                      const uint8_t *name, int64_t namelen,
+                                      const uint8_t *want, int64_t wantlen,
+                                      const uint8_t *got, int64_t gotlen) {
+  fflush(stdout);
+  fprintf(stderr, "%.*s: restart %.*s takes %.*s, given %.*s\n",
+          (int)loclen, (const char *)loc, (int)namelen, (const char *)name,
+          (int)wantlen, (const char *)want, (int)gotlen, (const char *)got);
+  rt_die();
+}
+
+/* A clause with parameters was reached by a transfer that filled none of them
+ * in. No [invoke-restart] can do that — it writes the arguments before it aims
+ * the channel — so this is the other way a transfer starts: the break loop,
+ * which today takes a restart by position and has no way to supply a value.
+ * Refused at the clause rather than run on a buffer nobody wrote. */
+_Noreturn void flan_restart_unarmed(const uint8_t *loc, int64_t loclen,
+                                    const uint8_t *name, int64_t namelen,
+                                    const uint8_t *want, int64_t wantlen) {
+  fflush(stdout);
+  fprintf(stderr,
+          "%.*s: restart %.*s takes %.*s, and whatever took it supplied no "
+          "arguments — a restart with parameters cannot be taken from the "
+          "break loop yet\n",
+          (int)loclen, (const char *)loc, (int)namelen, (const char *)name,
+          (int)wantlen, (const char *)want);
+  rt_die();
+}
+
 /* Something a defer called invoked a restart. A defer is the cleanup a
  * transfer runs on its way out (§5), so a transfer starting there would leave
  * this frame's defers half run with two targets and no way to choose. The

test/programs/restarts.flan

@@ -3,7 +3,12 @@
 ;;;; The transfer. A handler runs where the signal was, decides, and control
 ;;;; resumes at a restart-case further out: every function in between returns
 ;;;; early with the target in the channel, running its defers on the way (§5).
-;;;; Restarts take no parameters in this version.
+;;;;
+;;;; §3's parameters are here too, along with the run-time check they need: the
+;;;; supply-a-value half of the vocabulary, which is the half whose answer comes
+;;;; from outside the program. With no argument this program is the exit-0 case
+;;;; the table pins; with one it selects a mismatch, which traps and is asserted
+;;;; on its reason.
 (defstruct AssetMissing [id i32])
 
 (defvar log i64)
@@ -46,7 +51,53 @@
         0)
     (use-placeholder [] -2)))
 
-(defn main [] i32
+;;; Called from nowhere but inside an [invoke-restart]'s argument list.
+(defn half [x i32] i32 (/ x 2))
+
+;;; §3: a clause with parameters. The value comes from the handler, which is
+;;; the whole point — [use-value] and [store-value] are the two restarts whose
+;;; answer is not in the program. The parameters are slots of *this* function
+;;; and the invoker fills a buffer this frame owns, because by the time the
+;;; clause runs the invoking frame has gone (§5).
+(defn supplied [n i32] i32
+  (restart-case (middle n)
+    (use-value [v i32] (* v 2))
+    (use-pair  [a i32 b i32] (+ a b))
+    (retry     [] 7)))
+
+;;; Parameters of more than one type, and one that is not a machine word: a
+;;; string is ptr+len and crosses the transfer as the two of them.
+(defn labelled [n i32] i32
+  (restart-case (middle n)
+    (use-labelled [label string v i32]
+      (do (print label) (println "") v))))
+
+;;; The mismatch cases. Each is selected by the argument, because each stops
+;;; the program: what a restart takes is not knowable where it is invoked, so
+;;; §3 checks it at run time and this is what that check refuses.
+(defn mismatched [n i32] i32
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value))]
+    (supplied n)))
+
+(defn mistyped [n i32] i32
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value "forty-one"))]
+    (supplied n)))
+
+(defn overfull [n i32] i32
+  (handler-bind [(AssetMissing [c] (invoke-restart 'retry 1))]
+    (supplied n)))
+
+(defn main [args [string]] i32
+  ;; One argument selects a trap; none runs the table's case.
+  (if (> (len args) 1)
+    (let [k (i32 (bytes->i64 (bytes (at args 1))))]
+      (cond
+        (= k 1) (print (mismatched 90))
+        (= k 2) (print (mistyped 91))
+        (= k 3) (print (overfull 92))
+        :else (println "?"))
+      (return 0)))
+
   ;; Nothing handles it, so signal is a no-op and the body's own value stands.
   (print (fetch 1)) (println "")                          ; 101
   (print log) (println "")                                ; 1
@@ -77,4 +128,27 @@
   ;; the trap case in the acceptance table rather than a line here.
   (handler-bind [(AssetMissing [c] (invoke-restart 'use-placeholder))]
     (print (strict 6)) (println ""))                        ; -2
+
+  ;; §3: the handler supplies the value, and the clause computes with it —
+  ;; the arithmetic is in the clause so that a transfer which forgot to copy
+  ;; the argument could not pass by returning what it was given.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value 21))]
+    (print (supplied 7)) (println ""))                      ; 42
+  ;; Two parameters, so their order is pinned: 1 and 2 would sum the same
+  ;; whichever way round they landed.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-pair 30 4))]
+    (print (supplied 8)) (println ""))                      ; 34
+  ;; A clause with no parameters is still reachable from a restart-case that
+  ;; has some, and an invoke with no arguments still matches it.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'retry))]
+    (print (supplied 9)) (println ""))                      ; 7
+  ;; A string and an integer together: two different widths, and the string is
+  ;; ptr+len rather than a machine word.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-labelled "supplied" 5))]
+    (print (labelled 10)) (println ""))                     ; supplied / 5
+  ;; The argument is an ordinary expression, evaluated where the invoke is —
+  ;; here a call, and [half] is reached from nowhere else, so a walk that did
+  ;; not look inside an invoke-restart would drop it and fail to link.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value (half 42)))]
+    (print (supplied 12)) (println ""))                     ; 21 * 2
   0)

test/test_acceptance.ml

@@ -256,11 +256,100 @@ let () =
        shadowing an outer one of the same name, and a handler that returns
        normally still transferring nothing. At -O0 as well, because the guard
        after every call is control flow the optimiser would otherwise launder;
-       and as a dev build, where every one of those calls goes through a cell. *)
+       and as a dev build, where every one of those calls goes through a cell.
-    let restarts_out = "101\n1\n-1\n2\n7\n1010\n101\n105\n-2\n" in
+
+       Then §3's parameters: one, two of them in an order a sum would not pin,
+       a string beside an integer, a clause taking none in the same form as
+       clauses taking some, and an argument that is a call to a function
+       reached from nowhere else. The last one is the reachability claim — an
+       invoke-restart whose arguments were not walked would drop [half] and
+       fail to link, which is why the arguments are evaluated into slots before
+       the node rather than hanging off it. *)
+    let restarts_out =
+      "101\n1\n-1\n2\n7\n1010\n101\n105\n-2\n42\n34\n7\nsupplied\n5\n42\n"
+    in
     outputs "restarts" "programs/restarts.flan" restarts_out;
     outputs ~opt:"-O0" "restarts, -O0" "programs/restarts.flan" restarts_out;
     outputs ~dev:true "restarts, dev" "programs/restarts.flan" restarts_out;
+    (* §3's run-time check, which is the price of a restart being found by name
+       on a dynamic stack: neither end of an invoke can see the other, so what
+       a clause takes against what was given is settled where the transfer
+       starts. Each of these stops the program, so each is asserted on its
+       reason rather than on the exit status alone — too few arguments, the
+       right count of the wrong type, and arguments handed to a clause that
+       takes none. *)
+    let restart_mismatch ?opt () =
+      let exe = compile ?opt "programs/restarts.flan" in
+      let refuses name arg reason =
+        let code, text = run exe (Some arg) in
+        if code <> 134
+           || not (contains text "programs/restarts.flan:")
+           || not (contains text reason)
+        then begin
+          incr failures;
+          Printf.printf
+            "FAIL  %s\n        got: %S (exit %d)\n     wanted: %S (exit 134)\n"
+            name text code reason
+        end
+      in
+      refuses "a restart invoked with too few arguments" "1"
+        "restart use-value takes (i32), given ()";
+      refuses "a restart invoked with the wrong type" "2"
+        "restart use-value takes (i32), given (string)";
+      refuses "arguments given to a restart that takes none" "3"
+        "restart retry takes (), given (i32)";
+      (try Sys.remove exe with Sys_error _ -> ())
+    in
+    restart_mismatch ();
+    restart_mismatch ~opt:"-O0" ();
+    (* The other way a transfer starts is the break loop, which chooses a
+       restart by position and has nothing to fill parameters in with. It
+       reaches the clause through the same channel an invoke-restart writes, so
+       nothing downstream could tell the two apart — except that the clause's
+       buffer is still the zero the frame was pushed with. Asserted on the IR,
+       because driving it needs a stopped program and a socket, and what is
+       being claimed is that the guard exists at all. *)
+    let p =
+      Reader.read_file "programs/restarts.flan" |> Parse.program |> Check.program
+    in
+    if not (contains (Emit.program p) "call void @flan_restart_unarmed(") then begin
+      incr failures;
+      print_endline
+        "FAIL  a clause with parameters has no guard against being taken \
+         without any"
+    end;
+    (* What is refused before anything runs, and why. Not everything about a
+       restart's arguments waits for run time: the shape of the form and
+       whether an argument is a value at all are here, and each is asserted on
+       its reason. *)
+    let refuses_src name src needle =
+      match Check.program (Parse.program (Reader.read_all ~file:"<restarts>" src)) with
+      | _ ->
+        incr failures;
+        Printf.printf "FAIL  %s\n        it was accepted\n" name
+      | exception Loc.Error (_, m) ->
+        if not (contains m needle) then begin
+          incr failures;
+          Printf.printf "FAIL  %s\n        said: %S\n     wanted: %S in it\n"
+            name m needle
+        end
+    in
+    (* The name is still a quoted symbol, and now it is the *first* of several
+       things, so an unquoted one has to say what the form is rather than read
+       as a call with a spare argument. *)
+    refuses_src "invoke-restart without a quoted name"
+      "(defn main [] i32 (invoke-restart use-value 1) 0)"
+      "a quoted restart name and then its arguments";
+    (* A clause parameter is a binding, so it needs something to hold. *)
+    refuses_src "a restart parameter that is not a value"
+      "(defn main [] i32 (restart-case 0 (use-value [v Unit] 1)))"
+      "which is not a value";
+    (* And so does an argument: a [println] is Unit, and there would be nothing
+       to store into the clause's buffer. *)
+    refuses_src "a restart argument that is not a value"
+      "(defn main [] i32 (restart-case 0 (use-value [v i32] v))\n\
+      \  (invoke-restart 'use-value (println \"\")) 0)"
+      "a restart argument must be a value";
     (* §2's other half, which cannot be an [outputs] case because it does not
        exit 0: a handler runs, returns normally, and has still not answered the
        error, so the program stops and names the condition. *)
@@ -1512,10 +1601,11 @@ ERR@7 unexpected token: not the kind the caller was reading
          (defn fetch [n i32] i32\n\
         \  (restart-case\n\
         \    (do (error (Missing {:id n})) 0)\n\
+        \    (use-value [v i32  s string] (do (print s) v))\n\
         \    (use-placeholder [] -1)))\n\
          (defn run [] i32\n\
         \  (defer (set seen (+ seen 1)))\n\
-        \  (handler-bind [(Missing [m] (invoke-restart 'use-placeholder))]\n\
+        \  (handler-bind [(Missing [m] (invoke-restart 'use-value 4 \"\"))]\n\
         \    (fetch 3)))\n\
          (defn main [] i32\n\
         \  (set (at arr 2) 9)\n\

test/test_flan.ml

@@ -811,17 +811,22 @@ let () =
   rejects_check "return inside restart-case"
     "(defn f [] i32 (restart-case (return 1) (skip [] 2)))"
     ~needle:"return is not allowed inside restart-case";
-  (* The two halves of §3 this version does not do, each refused by name with
+  (* §3's parameters. A clause binds them like a function's, so the body sees
-     the reason rather than parsed into something that means less. *)
+     them and nothing outside does; what they are is checked against the
-  rejects_check "a restart with parameters"
+     invoke at run time, because the two ends meet on a dynamic stack. *)
-    "(defn f [] i32 (restart-case 1 (skip [n i32] n)))"
+  accepts "a restart with parameters"
-    ~needle:"a restart takes no parameters yet";
+    "(defn f [] i32 (restart-case 1 (skip [n i32] n)))";
-  rejects_check "invoke-restart with arguments"
+  accepts "invoke-restart with arguments"
-    "(defn f [] (invoke-restart 'skip 1))"
+    "(defn f [] (invoke-restart 'skip 1))";
-    ~needle:"a restart takes no arguments yet";
+  rejects_check "a restart parameter outside its clause"
+    "(defn f [] i32 (+ (restart-case 1 (skip [n i32] n)) n))"
+    ~needle:"unknown name n";
+  rejects_check "a restart argument that is not a value"
+    "(defn f [] (invoke-restart 'skip (println \"\")))"
+    ~needle:"a restart argument must be a value";
   rejects_check "invoke-restart on an unquoted name"
     "(defn f [] (invoke-restart skip))"
-    ~needle:"quoted restart name";
+    ~needle:"a quoted restart name and then its arguments";
   (* §5 runs the defers on the way out, so a defer is already the cleanup path
      a transfer uses. One that starts its own transfer has no answer. *)
   rejects_check "invoke-restart inside a defer"