Fix: Don't remove uncalled polymorphic constructors if they are matched upon

Previously the specialization would remove any polymorphic union
constructor that was never created anywhere in the
specification. While this wasn't usually problematic, it does leave an
edge case where such a constructor could be matched upon in a pattern,
and then the resulting match would fail to compile as it would be
matching on a constructor kind that doesn't exists.

This should fix that issue by chaging the V_ctor_kind value into an
F_ctor_kind fragment. Previously a polymorphic constructor-kind would
have been represented by its mangled name, e.g.

V_ctor_kind "zSome_unit"

would now be represented as

V_ctor_kind ("Some", unifiers, ty)

where ty is a monomorphic version of the original constructor's type
such that

ctyp_unify original_ty ty = unifiers

and the mangled name we generate is

zencode_string ("Some_" ^ string_of_list "_" string_of_ctyp unifiers)

11 files changed, 54 insertions, 43 deletions

diff --git a/language/jib.ott b/language/jib.ott
index 4f8eeacc..e26389ce 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -60,6 +60,7 @@ fragment :: 'F_' ::=
   | name                                   :: :: id
   | '&' name                               :: :: ref
   | value                                  :: :: lit
+  | kind id ( ctyp0 , ... , ctypn ) ctyp   :: :: ctor_kind
   | fragment op fragment'                  :: :: op
   | op fragment                            :: :: unary
   | string ( fragment0 , ... , fragmentn ) :: :: call
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index d74d3c0b..219e0855 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -422,7 +422,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   let ctx = { ctx with local_env = env } in
   match apat_aux, cval with
   | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env ->
-     [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label],
+     [ijump (F_op (F_field (frag, "kind"), "!=", F_ctor_kind (pid, [], ctyp)), CT_bool) case_label],
      [],
      ctx
 
@@ -465,25 +465,25 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   | AP_app (ctor, apat, variant_typ), (frag, ctyp) ->
      begin match ctyp with
      | CT_variant (_, ctors) ->
-        let ctor_c_id = string_of_id ctor in
         let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in
+        let pat_ctyp = apat_ctyp ctx apat in
         (* These should really be the same, something has gone wrong if they are not. *)
         if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then
           raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ))))
         else ();
-        let ctor_c_id, ctor_ctyp =
+        let unifiers, ctor_ctyp =
           if is_polymorphic ctor_ctyp then
-            let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in
-            (if List.length unification > 0 then
-               ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification
-             else
-               ctor_c_id),
-            ctyp_suprema (apat_ctyp ctx apat)
+            let unifiers = List.map ctyp_suprema (ctyp_unify ctor_ctyp pat_ctyp) in
+            unifiers, ctyp_suprema (apat_ctyp ctx apat)
           else
-            ctor_c_id, ctor_ctyp
+            [], ctor_ctyp
         in
-        let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in
-        [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label]
+        let ctor_field = match unifiers with
+          | [] -> Util.zencode_string (string_of_id ctor)
+          | _ -> Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+        in
+        let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, ctor_field), ctor_ctyp)) case_label in
+        [ijump (F_op (F_field (frag, "kind"), "!=", F_ctor_kind (ctor, unifiers, pat_ctyp)), CT_bool) case_label]
         @ instrs,
         cleanup,
         ctx
@@ -549,11 +549,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        let body_setup, body_call, body_cleanup = compile_aexp ctx body in
        let gs = ngensym () in
        let case_instrs =
-         destructure @ [icomment "end destructuring"]
+         destructure
          @ (if not trivial_guard then
               guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
               @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
-              @ [icomment "end guard"]
             else [])
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
@@ -563,15 +562,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        else
          [iblock case_instrs; ilabel case_label]
      in
-     [icomment "begin match"]
-     @ aval_setup @ [idecl ctyp case_return_id]
+     aval_setup @ [idecl ctyp case_return_id]
      @ List.concat (List.map compile_case cases)
      @ [imatch_failure ()]
      @ [ilabel finish_match_label],
      (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)),
      [iclear ctyp case_return_id]
      @ aval_cleanup
-     @ [icomment "end match"]
 
   (* Compile try statement *)
   | AE_try (aexp, cases, typ) ->
@@ -1280,8 +1277,8 @@ let rec specialize_variants ctx prior =
     function
     | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
        (* Work out how each call to a constructor in instantiated and add that to unifications *)
-       let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
-       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in
+       let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
        unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
 
        (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *)
@@ -1315,6 +1312,12 @@ let rec specialize_variants ctx prior =
     | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
        Reporting.unreachable l __POS__ "Multiple argument constructor found"
 
+    (* We have to be careful this is the only place where an F_ctor_kind can appear before calling specialize variants *)
+    | I_aux (I_jump ((F_op (_, "!=", F_ctor_kind (id, unifiers, pat_ctyp)), CT_bool), _), _) as instr when Id.compare id ctor_id = 0 ->
+       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+       unifications := Bindings.add mono_id (ctyp_suprema pat_ctyp) !unifications;
+       instr
+
     | instr -> instr
   in
 
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index e4891970..cda3924a 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -161,6 +161,7 @@ let rec frag_subst id subst = function
   | F_call (op, frags) -> F_call (op, List.map (frag_subst id subst) frags)
   | F_field (frag, field) -> F_field (frag_subst id subst frag, field)
   | F_raw str -> F_raw str
+  | F_ctor_kind (ctor, unifiers, ctyp) -> F_ctor_kind (ctor, unifiers, ctyp)
   | F_poly frag -> F_poly (frag_subst id subst frag)
 
 let cval_subst id subst (frag, ctyp) = frag_subst id subst frag, ctyp
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index e0ff4849..852f1bbd 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -456,6 +456,7 @@ let rename_variables graph root children =
     | F_call (id, fs) -> F_call (id, List.map fold_frag fs)
     | F_field (f, field) -> F_field (fold_frag f, field)
     | F_raw str -> F_raw str
+    | F_ctor_kind (ctor, unifiers, ctyp) -> F_ctor_kind (ctor, unifiers, ctyp)
     | F_poly f -> F_poly (fold_frag f)
   in
 
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 76d7b5d2..0a1afbef 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -165,6 +165,7 @@ let rec frag_rename from_id to_id = function
   | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f)
   | F_field (f, field) -> F_field (frag_rename from_id to_id f, field)
   | F_raw raw -> F_raw raw
+  | F_ctor_kind (ctor, unifiers, ctyp) -> F_ctor_kind (ctor, unifiers, ctyp)
   | F_poly f -> F_poly (frag_rename from_id to_id f)
 
 let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
@@ -253,9 +254,8 @@ let string_of_value = function
   | V_unit -> "UNIT"
   | V_bit Sail2_values.B0 -> "UINT64_C(0)"
   | V_bit Sail2_values.B1 -> "UINT64_C(1)"
+  | V_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | V_string str -> "\"" ^ str ^ "\""
-  | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
-  | _ -> failwith "Cannot convert value to string"
 
 let string_of_name ?zencode:(zencode=true) =
   let ssa_num n = if n < 0 then "" else ("/" ^ string_of_int n) in
@@ -282,6 +282,9 @@ let rec string_of_fragment ?zencode:(zencode=true) = function
   | F_unary (op, f) ->
      op ^ string_of_fragment' ~zencode:zencode f
   | F_raw raw -> raw
+  | F_ctor_kind (ctor, [], _) -> "Kind_" ^ Util.zencode_string (string_of_id ctor)
+  | F_ctor_kind (ctor, unifiers, _) ->
+     "Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
   | F_poly f -> string_of_fragment ~zencode:zencode f
 and string_of_fragment' ?zencode:(zencode=true) f =
   match f with
@@ -619,6 +622,7 @@ let rec fragment_deps = function
   | F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag
   | F_call (_, frags) -> List.fold_left NameSet.union NameSet.empty (List.map fragment_deps frags)
   | F_op (frag1, _, frag2) -> NameSet.union (fragment_deps frag1) (fragment_deps frag2)
+  | F_ctor_kind _ -> NameSet.empty
   | F_raw _ -> NameSet.empty
 
 let cval_deps = function (frag, _) -> fragment_deps frag
diff --git a/src/sail.ml b/src/sail.ml
index b016e574..9c3a3d5c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -273,7 +273,7 @@ let options = Arg.align ([
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
   ( "-ddump_rewrite_ast",
-    Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
+    Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0); Specialize.opt_ddump_spec_ast := Some (l, 0)),
     "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
   ( "-ddump_flow_graphs",
     Arg.Set Jib_compile.opt_debug_flow_graphs,
diff --git a/src/specialize.ml b/src/specialize.ml
index 5a7624bc..ca33ee85 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -53,7 +53,7 @@ open Ast_util
 open Rewriter
 
 let opt_ddump_spec_ast = ref None
-   
+
 let is_typ_ord_arg = function
   | A_aux (A_typ _, _) -> true
   | A_aux (A_order _, _) -> true
diff --git a/src/specialize.mli b/src/specialize.mli
index 28d118ca..0a64112c 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -54,6 +54,8 @@ open Ast
 open Ast_util
 open Type_check
 
+val opt_ddump_spec_ast : (string * int) option ref
+
 type specialization
 
 (** Only specialize Type- and Ord- kinded polymorphism. *)
diff --git a/src/value2.lem b/src/value2.lem
index e8a8262a..caf355b7 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -49,34 +49,14 @@
 (*========================================================================*)
 
 open import Pervasives
-open import Assert_extra
-open Map
 
 open import Sail2_values
 
 type vl =
-  | V_vector of list vl
-  | V_list of list vl
   | V_bits of list bitU
   | V_bit of bitU
-  | V_tuple of list vl
   | V_bool of bool
-  | V_nondet (* Special nondeterministic boolean *)
   | V_unit
   | V_int of integer
   | V_string of string
-  | V_ctor of string * list vl
-  | V_ctor_kind of string
-  | V_record of list (string * vl)
   | V_null (* Used for unitialized values and null pointers in C compilation *)
-
-
-let value_int_op_int op = function
-  | [V_int v1; V_int v2] -> V_int (op v1 v2)
-  | _ -> V_null
-end
-
-let value_bool_op_int op = function
-  | [V_int v1; V_int v2] -> V_bool (op v1 v2)
-  | _ -> V_null
-end
diff --git a/test/c/unused_poly_ctor.expect b/test/c/unused_poly_ctor.expect
new file mode 100644
index 00000000..e55551e8
--- /dev/null
+++ b/test/c/unused_poly_ctor.expect
@@ -0,0 +1 @@
+y = 0xFFFF
diff --git a/test/c/unused_poly_ctor.sail b/test/c/unused_poly_ctor.sail
new file mode 100644
index 00000000..c752cb33
--- /dev/null
+++ b/test/c/unused_poly_ctor.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+union U('a: Type) = {
+  Err : 'a,
+  Ok : bits(16)
+}
+
+function main((): unit) -> unit = {
+  let x : U(unit) = Ok(0xFFFF);
+  match x {
+    Err() => print_endline("error"),
+    Ok(y) => print_bits("y = ", y)
+  }
+}