Various bugfixes and improvements

- Rename DeIid to Operator. It corresponds to operator <string> in the
  syntax. The previous name is from when it was called deinfix in
  sail1.

- Removed things that weren't actually common from
  pretty_print_common.ml, e.g. printing identifiers is backend
  specific. The doc_id function here was only used for a very specific
  use case in pretty_print_lem, so I simplified it and renamed it to
  doc_sia_id, as it is always used for a SIA.Id whatever that is.

- There is some support for anonymous records in constructors, e.g.

  union Foo ('a : Type) = {
    MkFoo : { field1 : 'a, field2 : int }
  }

  somewhat similar to the enum syntax in Rust. I'm not sure when this
  was added, but there were a few odd things about it. It was
  desugared in the preprocessor, rather than initial_check, and the
  desugaring generated incorrect code for polymorphic anonymous
  records as above.

  I moved the code to initial_check, so the pre-processor now just
  deals with pre-processor things and not generating types, and I
  fixed the code to work with polymorphic types. This revealed some
  issues in the C backend w.r.t. polymorphic structs, which is the
  bulk of this commit. I also added some tests for this feature.

- OCaml backend can now generate a valid string_of function for
  polymorphic structs, previously this would cause the ocaml to fail
  to compile.

- Some cleanup in the Sail ott definition

- Add support for E_var in interpreter previously this would just
  cause the interpreter to fail

6 files changed, 106 insertions, 28 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 5bea0988..0a410249 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -534,8 +534,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp)))
 
   | E_app_infix (x, Id_aux (Id op, l), y) ->
-     anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot))
-  | E_app_infix (x, Id_aux (DeIid op, l), y) ->
+     anf (E_aux (E_app (Id_aux (Operator op, l), [x; y]), exp_annot))
+  | E_app_infix (x, Id_aux (Operator op, l), y) ->
      anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot))
 
   | E_vector exps ->
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 0e73fed8..ee16e2e6 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -95,7 +95,7 @@ let c_error ?loc:(l=Parse_ast.Unknown) message =
 
 let zencode_id = function
   | Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
-  | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
+  | Id_aux (Operator str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
 
 (**************************************************************************)
 (* 2. Converting sail types to C types                                    *)
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 219e0855..4a72ffff 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_ctor_kind (pid, [], ctyp)), CT_bool) case_label],
+     [ijump (F_ctor_kind (frag, pid, [], ctyp), CT_bool) case_label],
      [],
      ctx
 
@@ -478,12 +478,8 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
           else
             [], ctor_ctyp
         in
-        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]
+        let instrs, cleanup, ctx = compile_match ctx apat (F_ctor_unwrap (ctor, unifiers, frag), ctor_ctyp) case_label in
+        [ijump (F_ctor_kind (frag, ctor, unifiers, pat_ctyp), CT_bool) case_label]
         @ instrs,
         cleanup,
         ctx
@@ -783,7 +779,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      (fun clexp -> icomment "unreachable after throw"),
      []
 
-  | AE_field (aval, id, _) ->
+  | AE_field (aval, id, typ) ->
+     let aval_ctyp = ctyp_of_typ ctx typ in
      let setup, cval, cleanup = compile_aval l ctx aval in
      let ctyp = match cval_ctyp cval with
        | CT_struct (struct_id, fields) ->
@@ -796,8 +793,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        | _ ->
           raise (Reporting.err_unreachable l __POS__ "Field access on non-struct type in ANF representation!")
      in
+     let unifiers, ctyp =
+       if is_polymorphic ctyp then
+         let unifiers = List.map ctyp_suprema (ctyp_unify ctyp aval_ctyp) in
+         unifiers, ctyp_suprema aval_ctyp
+       else
+         [], ctyp
+     in
+     let field_str = match unifiers with
+       | [] -> Util.zencode_string (string_of_id id)
+       | _ -> Util.zencode_string (string_of_id id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+     in
      setup,
-     (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)),
+     (fun clexp -> icopy l clexp (F_field (fst cval, field_str), ctyp)),
      cleanup
 
   | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
@@ -1272,9 +1280,15 @@ let rec specialize_variants ctx prior =
     | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors)
     | ctyp -> ctyp
   in
+  let fix_struct_ctyp struct_id new_fields = function
+    | CT_struct (id, ctors) when Id.compare id struct_id = 0 -> CT_struct (id, new_fields)
+    | ctyp -> ctyp
+  in
 
-  let specialize_constructor ctx ctor_id ctyp =
-    function
+  (* specialize_constructor is called on all instructions when we find
+     a constructor in a union type that is polymorphic. It's job is to
+     record all uses of that constructor so we can monomorphise it. *)
+  let specialize_constructor ctx ctor_id ctyp = 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 unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
@@ -1313,7 +1327,7 @@ let rec specialize_variants ctx prior =
        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 ->
+    | I_aux (I_jump ((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
@@ -1321,14 +1335,27 @@ let rec specialize_variants ctx prior =
     | instr -> instr
   in
 
+  (* specialize_field performs the same job as specialize_constructor,
+     but for struct fields rather than union constructors. *)
+  let specialize_field ctx field_id ctyp = function
+    | I_aux (I_copy (CL_field (clexp, field_str), cval), aux) when string_of_id field_id = field_str ->
+       let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+       let mono_id = append_id field_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+       unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
+       I_aux (I_copy (CL_field (clexp, string_of_id mono_id), cval), aux)
+      
+    | instr -> instr
+  in
+  
   function
   | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs ->
      let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in
 
      let cdefs =
-       List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
-                      cdefs
-                      polymorphic_ctors
+       List.fold_left
+         (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
+         cdefs
+         polymorphic_ctors
      in
 
      let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in
@@ -1345,6 +1372,30 @@ let rec specialize_variants ctx prior =
      let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in
      specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs
 
+  | (CDEF_type (CTD_struct (struct_id, fields)) as cdef) :: cdefs ->
+     let polymorphic_fields = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) fields in
+
+     let cdefs =
+       List.fold_left
+         (fun cdefs (field_id, ctyp) -> List.map (cdef_map_instr (specialize_field ctx field_id ctyp)) cdefs)
+         cdefs
+         polymorphic_fields
+     in
+
+     let monomorphic_fields = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) fields in
+     let specialized_fields = Bindings.bindings !unifications in
+     let new_fields = monomorphic_fields @ specialized_fields in
+
+     let ctx = {
+         ctx with records = Bindings.add struct_id
+                              (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_fields)
+                              ctx.records
+       } in
+
+     let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) cdefs in
+     let prior = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) prior in     
+     specialize_variants ctx (CDEF_type (CTD_struct (struct_id, new_fields)) :: prior) cdefs
+     
   | cdef :: cdefs ->
      let remove_poly (I_aux (instr, aux)) =
        match instr with
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index cda3924a..73b175a1 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -161,7 +161,8 @@ 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_ctor_kind (frag, ctor, unifiers, ctyp) -> F_ctor_kind (frag_subst id subst frag, ctor, unifiers, ctyp)
+  | F_ctor_unwrap (ctor, unifiers, frag) -> F_ctor_unwrap (ctor, unifiers, frag_subst id subst frag)
   | 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 852f1bbd..a086f0b9 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -456,7 +456,8 @@ 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_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (fold_frag f, ctor, unifiers, ctyp)
+    | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, fold_frag f)
     | F_poly f -> F_poly (fold_frag f)
   in
 
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 0a1afbef..904e0209 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -165,7 +165,8 @@ 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_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (frag_rename from_id to_id f, ctor, unifiers, ctyp)
+  | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, frag_rename from_id to_id f)
   | 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)
@@ -282,9 +283,20 @@ 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_ctor_kind (f, ctor, [], _) ->
+     string_of_fragment' ~zencode:zencode f ^ ".kind"
+     ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor)
+  | F_ctor_kind (f, ctor, unifiers, _) ->
+     string_of_fragment' ~zencode:zencode f ^ ".kind"
+     ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+  | F_ctor_unwrap (ctor, [], f) ->
+     Printf.sprintf "%s.%s"
+       (string_of_fragment' ~zencode:zencode f)
+       (Util.zencode_string (string_of_id ctor))
+  | F_ctor_unwrap (ctor, unifiers, f) ->
+     Printf.sprintf "%s.%s"
+       (string_of_fragment' ~zencode:zencode f)
+       (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
@@ -319,9 +331,14 @@ and string_of_ctyp = function
    constructors in variants and structs. Used for debug output. *)
 and full_string_of_ctyp = function
   | CT_tup ctyps -> "(" ^ Util.string_of_list ", " full_string_of_ctyp ctyps ^ ")"
-  | CT_struct (id, ctors) | CT_variant (id, ctors) ->
+  | CT_struct (id, ctors) ->
      "struct " ^ string_of_id id
-     ^ "{ "
+     ^ "{"
+     ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
+     ^ "}"
+  | CT_variant (id, ctors) ->
+     "union " ^ string_of_id id
+     ^ "{"
      ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
      ^ "}"
   | CT_vector (true, ctyp) -> "vector(dec, " ^ full_string_of_ctyp ctyp ^ ")"
@@ -442,6 +459,13 @@ let rec ctyp_unify ctyp1 ctyp2 =
 
   | CT_list ctyp1, CT_list ctyp2 -> ctyp_unify ctyp1 ctyp2
 
+  | CT_struct (id1, fields1), CT_struct (id2, fields2)
+       when Id.compare id1 id2 = 0 && List.length fields1 == List.length fields2 ->
+     if List.for_all2 (fun x y -> x = y) (List.map fst fields1) (List.map fst fields2) then
+       List.concat (List.map2 ctyp_unify (List.map snd fields1) (List.map snd fields2))
+     else
+       raise (Invalid_argument "ctyp_unify")
+                                  
   | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_unify ctyp1 ctyp2
 
   | CT_poly, _ -> [ctyp2]
@@ -505,7 +529,7 @@ let pp_name id =
   string (string_of_name ~zencode:false id)
 
 let pp_ctyp ctyp =
-  string (string_of_ctyp ctyp |> Util.yellow |> Util.clear)
+  string (full_string_of_ctyp ctyp |> Util.yellow |> Util.clear)
 
 let pp_keyword str =
   string ((str |> Util.red |> Util.clear) ^ " ")
@@ -622,7 +646,8 @@ 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_ctor_kind (frag, _, _, _) -> fragment_deps frag
+  | F_ctor_unwrap (_, _, frag) -> fragment_deps frag
   | F_raw _ -> NameSet.empty
 
 let cval_deps = function (frag, _) -> fragment_deps frag