Add a hack to keep registers with option types working

Print a warning if we encounter this
rems-project · Dec 2, 2023 · 2d6ebaa · 2d6ebaa
1 parent c86472b
commit 2d6ebaa
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 12 deletions.
diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
@@ -1547,8 +1547,11 @@ let generate_undefineds vs_ids defs =
   undefined_builtins @ defs
 
 let rec get_uninitialized_registers = function
-  | DEF_aux (DEF_register (DEC_aux (DEC_reg (typ, id, None), _)), _) :: defs ->
-      (typ, id) :: get_uninitialized_registers defs
+  | DEF_aux (DEF_register (DEC_aux (DEC_reg (typ, id, None), _)), _) :: defs -> begin
+      match typ with
+      | Typ_aux (Typ_app (Id_aux (Id "option", _), [_]), _) -> get_uninitialized_registers defs
+      | _ -> (typ, id) :: get_uninitialized_registers defs
+    end
   | _ :: defs -> get_uninitialized_registers defs
   | [] -> []
 

diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
@@ -4591,16 +4591,23 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t =
   | DEF_instantiation (ispec, substs) -> check_outcome_instantiation env def_annot ispec substs
   | DEF_default default -> check_default env def_annot default
   | DEF_overload (id, ids) -> ([DEF_aux (DEF_overload (id, ids), def_annot)], Env.add_overloads def_annot.loc id ids env)
-  | DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, _))) ->
-      if not (can_be_undefined ~at:l env typ) then
-        typ_error l ("Must provide a default register value for a register of type " ^ string_of_typ typ);
-      let env = Env.add_register id typ env in
-      ( [
-          DEF_aux
-            (DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, mk_expected_tannot env typ (Some typ)))), def_annot);
-        ],
-        env
-      )
+  | DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, uannot))) -> begin
+      match typ with
+      | Typ_aux (Typ_app (Id_aux (Id "option", _), [_]), _) ->
+          Reporting.warn "No default value" l "Registers of type option should explicitly be given a default value";
+          let none_ctor = locate (fun _ -> gen_loc l) (mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit]))) in
+          check_def env (DEF_aux (DEF_register (DEC_aux (DEC_reg (typ, id, Some none_ctor), (l, uannot))), def_annot))
+      | _ ->
+          if not (can_be_undefined ~at:l env typ) then
+            typ_error l ("Must provide a default register value for a register of type " ^ string_of_typ typ);
+          let env = Env.add_register id typ env in
+          ( [
+              DEF_aux
+                (DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, mk_expected_tannot env typ (Some typ)))), def_annot);
+            ],
+            env
+          )
+    end
   | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), (l, _))) ->
       let checked_exp = crule check_exp env exp typ in
       let env = Env.add_register id typ env in