Make sure end always has a valid scattered definition id

src/lib/type_check.ml

@@ -4861,7 +4861,11 @@ let rec check_typedef : Env.t -> env def_annot -> uannot type_def -> typed_def l
 and check_scattered : Env.t -> env def_annot -> uannot scattered_def -> typed_def list * Env.t =
  fun env def_annot (SD_aux (sdef, (l, uannot))) ->
   match sdef with
-  | SD_function _ | SD_end _ | SD_mapping _ -> ([], env)
+  | SD_function (_, _, id) | SD_mapping (id, _) -> ([], Env.add_scattered_id id env)
+  | SD_end id ->
+      if not (Env.is_scattered_id id env) then
+        typ_error l (string_of_id id ^ " is not a scattered definition, so it cannot be ended")
+      else ([], env)
   | SD_enum id ->
       ([DEF_aux (DEF_scattered (SD_aux (SD_enum id, (l, empty_tannot))), def_annot)], Env.add_scattered_enum id env)
   | SD_enumcl (id, member) ->
@@ -4902,12 +4906,16 @@ and check_scattered : Env.t -> env def_annot -> uannot scattered_def -> typed_de
       let typq, typ = Env.get_val_spec id env in
       let funcl_env = Env.add_typquant fcl_def_annot.loc typq env in
       let funcl = check_funcl funcl_env funcl typ in
-      ([DEF_aux (DEF_scattered (SD_aux (SD_funcl funcl, (l, mk_tannot ~uannot funcl_env typ))), def_annot)], env)
+      ( [DEF_aux (DEF_scattered (SD_aux (SD_funcl funcl, (l, mk_tannot ~uannot funcl_env typ))), def_annot)],
+        Env.add_scattered_id id env
+      )
   | SD_mapcl (id, mapcl) ->
       let typq, typ = Env.get_val_spec id env in
       let mapcl_env = Env.add_typquant l typq env in
       let mapcl = check_mapcl mapcl_env mapcl typ in
-      ([DEF_aux (DEF_scattered (SD_aux (SD_mapcl (id, mapcl), (l, empty_tannot))), def_annot)], env)
+      ( [DEF_aux (DEF_scattered (SD_aux (SD_mapcl (id, mapcl), (l, empty_tannot))), def_annot)],
+        Env.add_scattered_id id env
+      )
 
 and check_outcome : Env.t -> outcome_spec -> untyped_def list -> outcome_spec * typed_def list * Env.t =
  fun env (OV_aux (OV_outcome (id, typschm, params), l)) defs ->

src/lib/type_env.ml

@@ -120,6 +120,7 @@ type global_env = {
   registers : typ env_item Bindings.t;
   overloads : id list multiple_env_item Bindings.t;
   outcomes : (typquant * typ * kinded_id list * id list * (typquant * typ) env_item Bindings.t) env_item Bindings.t;
+  scattered_ids : IdSet.t;
   outcome_instantiation : (Ast.l * typ) KBindings.t;
 }
 
@@ -146,6 +147,7 @@ let empty_global_env =
     registers = Bindings.empty;
     overloads = Bindings.empty;
     outcomes = Bindings.empty;
+    scattered_ids = IdSet.empty;
     outcome_instantiation = KBindings.empty;
   }
 
@@ -1248,10 +1250,17 @@ let add_enum' is_scattered id ids env =
       env
   )
 
-let add_scattered_enum id env = add_enum' true id [] env
+let add_scattered_id id env =
+  update_global (fun global -> { global with scattered_ids = IdSet.add id global.scattered_ids }) env
+
+let is_scattered_id id env = IdSet.mem id env.global.scattered_ids
+
+let add_scattered_enum id env = env |> add_scattered_id id |> add_enum' true id []
+
 let add_enum id ids env = add_enum' false id ids env
 
 let add_enum_clause id member env =
+  let env = add_scattered_id id env in
   match Bindings.find_opt id env.global.enums with
   | Some item ->
       if not (item_in_scope env item) then
@@ -1406,6 +1415,7 @@ let add_variant id (typq, constructors) env =
   )
 
 let add_scattered_variant id typq env =
+  let env = add_scattered_id id env in
   if bound_typ_id env id then already_bound "scattered union" id env
   else (
     typ_print (lazy (adding ^ "scattered variant " ^ string_of_id id)) [@coverage off];
@@ -1421,6 +1431,7 @@ let add_scattered_variant id typq env =
   )
 
 let add_variant_clause id tu env =
+  let env = add_scattered_id id env in
   match Bindings.find_opt id env.global.unions with
   | Some ({ item = typq, tus; _ } as item) ->
       update_global

src/lib/type_env.mli

@@ -235,6 +235,9 @@ val get_enums : t -> IdSet.t Bindings.t
 
 val lookup_id : id -> t -> typ lvar
 
+val add_scattered_id : id -> t -> t
+val is_scattered_id : id -> t -> bool
+
 val expand_synonyms : t -> typ -> typ
 val expand_nexp_synonyms : t -> nexp -> nexp
 val expand_constraint_synonyms : t -> n_constraint -> n_constraint

test/typecheck/fail/unknown_end.expect

@@ -0,0 +1,5 @@
+Type error:
+fail/unknown_end.sail:2.0-18:
+2 |end does_not_exist
+  |^----------------^
+  | does_not_exist is not a scattered definition, so it cannot be ended

test/typecheck/fail/unknown_end.sail

@@ -0,0 +1,2 @@
+
+end does_not_exist