Config: Support for unions

src/lib/config.ml

@@ -56,7 +56,12 @@ let typ_is_record env = function
   | Typ_aux (Typ_app (id, _), _) -> Env.is_record id env
   | _ -> false
 
-let destruct_record = function
+let typ_is_variant env = function
+  | Typ_aux (Typ_id id, _) -> Env.is_variant id env
+  | Typ_aux (Typ_app (id, _), _) -> Env.is_variant id env
+  | _ -> false
+
+let destruct_typ_args = function
   | Typ_aux (Typ_id id, _) -> Some (id, [])
   | Typ_aux (Typ_app (id, args), _) -> Some (id, args)
   | _ -> None
@@ -287,8 +292,8 @@ end = struct
          existential quantifier might link multiple fields, and we
          can't capture that in the schema. *)
       | [], NC_aux (NC_true, _), _ when typ_is_record env typ ->
-          let* id, args = destruct_record typ in
-          let fields = instantiate_record ~at:loc env id args in
+          let* id, args = destruct_typ_args typ in
+          let fields = instantiate_record env id args in
           let* properties =
             List.map
               (fun (field_typ, field_id) ->
@@ -298,7 +303,7 @@ end = struct
               fields
             |> Util.option_all
           in
-          let record_schema : (string * J.t) list =
+          let record_schema =
             [
               ("type", `String "object");
               ("properties", `Assoc properties);
@@ -307,6 +312,27 @@ end = struct
             ]
           in
           Some (`Assoc record_schema)
+      | [], NC_aux (NC_true, _), _ when typ_is_variant env typ ->
+          let* id, args = destruct_typ_args typ in
+          let constructors = instantiate_variant env id args in
+          let* properties =
+            List.map
+              (fun (constructor, typ) ->
+                let* schema = generate typ in
+                Some (string_of_id constructor, schema)
+              )
+              constructors
+            |> Util.option_all
+          in
+          let variant_schema =
+            [
+              ("type", `String "object");
+              ("properties", `Assoc properties);
+              ("minProperties", `Int 1);
+              ("maxProperties", `Int 1);
+            ]
+          in
+          Some (`Assoc variant_schema)
       | [], NC_aux (NC_true, _), Typ_aux (Typ_id id, _) -> (
           match string_of_id id with
           | "string" -> Some (`Assoc [("type", `String "string")])
@@ -525,7 +551,7 @@ let rec sail_exp_from_json ~at:l env typ =
       let base_typ = match destruct_exist typ with None -> typ | Some (_, _, typ) -> typ in
       let exp_opt =
         if typ_is_record env base_typ then
-          let* id, _ = destruct_record base_typ in
+          let* id, _ = destruct_typ_args base_typ in
           let _, fields = Env.get_record id env in
           let* fexps =
             List.map
@@ -538,6 +564,28 @@ let rec sail_exp_from_json ~at:l env typ =
             |> Util.option_all
           in
           Some (mk_exp ~loc:l (E_struct fexps))
+        else if typ_is_variant env base_typ then
+          let* id, _ = destruct_typ_args base_typ in
+          match obj with
+          | [(constructor, value)] -> (
+              let constructor = mk_id ~loc:l constructor in
+              match Env.union_constructor_info constructor env with
+              | None ->
+                  raise
+                    (Reporting.err_general l
+                       (Printf.sprintf "Constructor %s in JSON configuration is not a valid constructor for union %s"
+                          (string_of_id constructor) (string_of_id id)
+                       )
+                    )
+              | Some (_, _, _, Tu_aux (Tu_ty_id (typ, _), _)) ->
+                  let exp = sail_exp_from_json ~at:l env typ value in
+                  Some (mk_exp ~loc:l (E_app (constructor, [exp])))
+            )
+          | _ ->
+              raise
+                (Reporting.err_general l
+                   (Printf.sprintf "JSON does not appear to contain a valid Sail union member for %s" (string_of_id id))
+                )
         else (
           match base_typ with
           | Typ_aux (Typ_app (id, args), _) -> (

src/lib/jib_compile.ml

@@ -578,7 +578,7 @@ module Make (C : CONFIG) = struct
       optimizations where we can generate a more efficient version of [foo] that doesn't exist
       in the original Sail.
   *)
-  let compile_funcall ?override_id l ctx id args =
+  let compile_funcall_with ?override_id l ctx id compile_arg args =
     let setup = ref [] in
     let cleanup = ref [] in
 
@@ -596,8 +596,8 @@ module Make (C : CONFIG) = struct
 
     let instantiation = ref KBindings.empty in
 
-    let setup_arg ctyp aval =
-      let arg_setup, cval, arg_cleanup = compile_aval l ctx aval in
+    let setup_arg ctyp arg =
+      let arg_setup, cval, arg_cleanup = compile_arg arg in
       instantiation := KBindings.union merge_unifiers (ctyp_unify l ctyp (cval_ctyp cval)) !instantiation;
       setup := List.rev arg_setup @ !setup;
       cleanup := arg_cleanup @ !cleanup;
@@ -620,6 +620,8 @@ module Make (C : CONFIG) = struct
       !cleanup
     )
 
+  let compile_funcall ?override_id l ctx id args = compile_funcall_with ?override_id l ctx id (compile_aval l ctx) args
+
   let compile_extern l ctx id args =
     let setup = ref [] in
     let cleanup = ref [] in
@@ -683,6 +685,52 @@ module Make (C : CONFIG) = struct
       | CT_fbits _ ->
           config_extract CT_lbits json ~validate:("sail_config_is_bits", []) ~extract:"sail_config_unwrap_bits"
       | CT_bool -> config_extract CT_bool json ~validate:("sail_config_is_bool", []) ~extract:"sail_config_unwrap_bool"
+      | CT_variant (_, constructors) as variant_ctyp ->
+          let variant_name = ngensym () in
+          let ctor_checks, ctor_extracts =
+            Util.fold_left_map
+              (fun checks (ctor_id, ctyp) ->
+                let is_ctor = ngensym () in
+                let ctor_json = ngensym () in
+                let value = ngensym () in
+                let check =
+                  [
+                    idecl l CT_bool is_ctor;
+                    iextern l
+                      (CL_id (is_ctor, CT_bool))
+                      (mk_id "sail_config_object_has_key", [])
+                      [V_id (json, CT_json); V_lit (VL_string (string_of_id ctor_id), CT_string)];
+                  ]
+                in
+                let setup, call, cleanup = extract ctor_json ctyp in
+                let ctor_setup, ctor_call, ctor_cleanup =
+                  compile_funcall_with l ctx ctor_id (fun cval -> ([], cval, [])) [V_id (value, ctyp)]
+                in
+                let extract =
+                  [
+                    idecl l CT_json ctor_json;
+                    idecl l ctyp value;
+                    iextern l
+                      (CL_id (ctor_json, CT_json))
+                      (mk_id "sail_config_object_key", [])
+                      [V_id (json, CT_json); V_lit (VL_string (string_of_id ctor_id), CT_string)];
+                  ]
+                  @ setup @ ctor_setup
+                  @ [call (CL_id (value, ctyp))]
+                  @ [ctor_call (CL_id (variant_name, variant_ctyp))]
+                  @ ctor_cleanup @ cleanup
+                in
+                (checks @ check, (is_ctor, extract))
+              )
+              [] constructors
+          in
+          let ctor_extracts =
+            List.fold_left (fun rest (b, instrs) -> [iif l (V_id (b, CT_bool)) instrs rest CT_unit]) [] ctor_extracts
+          in
+          ( [idecl l variant_ctyp variant_name] @ ctor_checks @ ctor_extracts,
+            (fun clexp -> icopy l clexp (V_id (variant_name, variant_ctyp))),
+            [iclear variant_ctyp variant_name]
+          )
       | CT_struct (_, fields) as struct_ctyp ->
           let struct_name = ngensym () in
           let fields_from_json =

src/lib/type_check.ml

@@ -2049,7 +2049,7 @@ let rec reroll_cons ~at:l elems annots last_tail =
   | [], [] -> last_tail
   | _, _ -> Reporting.unreachable l __POS__ "Could not recreate cons list due to element and annotation length mismatch"
 
-let instantiate_record ~at:l env id args =
+let instantiate_record env id args =
   let typq, fields = Env.get_record id env in
   let kopts, _ = quant_split typq in
   let unifiers = List.fold_left2 (fun kb kopt arg -> KBindings.add (kopt_kid kopt) arg kb) KBindings.empty kopts args in
@@ -2060,6 +2060,17 @@ let instantiate_record ~at:l env id args =
     )
     fields
 
+let instantiate_variant env id args =
+  let typq, tus = Env.get_variant id env in
+  let kopts, _ = quant_split typq in
+  let unifiers = List.fold_left2 (fun kb kopt arg -> KBindings.add (kopt_kid kopt) arg kb) KBindings.empty kopts args in
+  List.map
+    (fun (Tu_aux (Tu_ty_id (typ, id), _)) ->
+      let typ = subst_unifiers unifiers typ in
+      (id, typ)
+    )
+    tus
+
 type ('a, 'b) pattern_functions = {
   infer : Env.t -> 'a -> 'b * Env.t * uannot exp list;
   bind : Env.t -> 'a -> typ -> 'b * Env.t * uannot exp list;

src/lib/type_check.mli

@@ -151,6 +151,8 @@ module Env : sig
 
   val add_typ_var : Ast.l -> kinded_id -> t -> t
 
+  val is_variant : id -> t -> bool
+
   val is_record : id -> t -> bool
 
   (** Returns record quantifiers and fields *)
@@ -450,7 +452,9 @@ val exist_typ : Parse_ast.l -> (kid -> n_constraint) -> (kid -> typ) -> typ
 
 val subst_unifiers : typ_arg KBindings.t -> typ -> typ
 
-val instantiate_record : at:Ast.l -> env -> id -> typ_arg list -> (typ * id) list
+val instantiate_record : env -> id -> typ_arg list -> (typ * id) list
+
+val instantiate_variant : env -> id -> typ_arg list -> (id * typ) list
 
 (** [unify l env goals typ1 typ2] returns set of typ_arg bindings such
    that substituting those bindings using every type variable in goals

test/c/config_union.expect

@@ -0,0 +1,2 @@
+n = 33
+None

test/c/config_union.json

@@ -0,0 +1,8 @@
+{
+    "c1" : {
+        "Some" : 33
+    },
+    "c2" : {
+        "None" : null
+    }
+}

test/c/config_union.sail

@@ -0,0 +1,26 @@
+default Order dec
+
+$include <prelude.sail>
+$include <option.sail>
+
+$iftarget c
+$c_in_main sail_config_set_file("config_union.json");
+$c_in_main_post sail_config_cleanup();
+$else
+$option --config ../c/config_union.json
+$endif
+
+val main : unit -> unit
+
+function main() = {
+  let x : option(int) = config c1;
+  match x {
+    Some(n) => print_int("n = ", n),
+    None()  => (),
+  };
+  let y : option(string) = config c2;
+  match y {
+    Some(_) => (),
+    None() => print_endline("None"),
+  }
+}