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

21 files changed, 313 insertions, 232 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 95954d0f..d0efc0de 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -179,9 +179,9 @@ module Id = struct
   let compare id1 id2 =
     match (id1, id2) with
     | Id_aux (Id x, _), Id_aux (Id y, _) -> String.compare x y
-    | Id_aux (DeIid x, _), Id_aux (DeIid y, _) -> String.compare x y
-    | Id_aux (Id _, _), Id_aux (DeIid _, _) -> -1
-    | Id_aux (DeIid _, _), Id_aux (Id _, _) -> 1
+    | Id_aux (Operator x, _), Id_aux (Operator y, _) -> String.compare x y
+    | Id_aux (Id _, _), Id_aux (Operator _, _) -> -1
+    | Id_aux (Operator _, _), Id_aux (Id _, _) -> 1
 end
 
 module Nexp = struct
@@ -360,7 +360,7 @@ let rec constraint_disj (NC_aux (nc_aux, l) as nc) =
 let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
 let mk_typ_arg arg = A_aux (arg, Parse_ast.Unknown)
 let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
-let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
+let mk_infix_id str = Id_aux (Operator str, Parse_ast.Unknown)
 
 let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
 
@@ -651,23 +651,23 @@ let def_loc = function
 
 let string_of_id = function
   | Id_aux (Id v, _) -> v
-  | Id_aux (DeIid v, _) -> "(operator " ^ v ^ ")"
+  | Id_aux (Operator v, _) -> "(operator " ^ v ^ ")"
 
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
 let kid_of_id = function
   | Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l)
-  | Id_aux (DeIid v, _) -> assert false
+  | Id_aux (Operator v, _) -> assert false
 
 let prepend_id str = function
   | Id_aux (Id v, l) -> Id_aux (Id (str ^ v), l)
-  | Id_aux (DeIid v, l) -> Id_aux (DeIid (str ^ v), l)
+  | Id_aux (Operator v, l) -> Id_aux (Operator (str ^ v), l)
 
 let append_id id str =
   match id with
   | Id_aux (Id v, l) -> Id_aux (Id (v ^ str), l)
-  | Id_aux (DeIid v, l) -> Id_aux (DeIid (v ^ str), l)
+  | Id_aux (Operator v, l) -> Id_aux (Operator (v ^ str), l)
 
 let prepend_kid str = function
   | Kid_aux (Var v, l) -> Kid_aux (Var ("'" ^ str ^ String.sub v 1 (String.length v - 1)), l)
@@ -765,7 +765,7 @@ and string_of_n_constraint = function
      "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_set (kid, ns), _) ->
      string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
-  | NC_aux (NC_app (Id_aux (DeIid op, _), [arg1; arg2]), _) ->
+  | NC_aux (NC_app (Id_aux (Operator op, _), [arg1; arg2]), _) ->
      "(" ^ string_of_typ_arg arg1 ^ " " ^ op ^ " " ^ string_of_typ_arg arg2 ^ ")"
   | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
   | NC_aux (NC_var v, _) -> string_of_kid v
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 6caa5ecd..5c99a534 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -408,7 +408,7 @@ let const_props defs ref_vars =
           let env1 = env_of e1_no_casts in
           let is_equal id =
             List.exists (fun id' -> Id.compare id id' == 0)
-              (Env.get_overloads (Id_aux (DeIid "==", Parse_ast.Unknown))
+              (Env.get_overloads (Id_aux (Operator "==", Parse_ast.Unknown))
                  env1)
           in
           let substs_true =
diff --git a/src/initial_check.ml b/src/initial_check.ml
index dca42c7b..df9af97f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -70,7 +70,7 @@ type ctx = {
 
 let string_of_parse_id_aux = function
   | P.Id v -> v
-  | P.DeIid v -> v
+  | P.Operator v -> v
 
 let string_of_parse_id (P.Id_aux (id, l)) = string_of_parse_id_aux id
 
@@ -93,7 +93,7 @@ let to_ast_id (P.Id_aux(id, l)) =
   else
     Id_aux ((match id with
              | P.Id x -> Id x
-             | P.DeIid x -> DeIid x),
+             | P.Operator x -> Operator x),
             l)
 
 let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l)
@@ -224,7 +224,7 @@ and to_ast_order ctx (P.ATyp_aux (aux, l)) =
 
 and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
   let aux = match aux with
-    | P.ATyp_app (Id_aux (DeIid op, _) as id, [t1; t2]) ->
+    | P.ATyp_app (Id_aux (Operator op, _) as id, [t1; t2]) ->
        begin match op with
        | "==" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
        | "!=" -> NC_not_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
@@ -522,52 +522,100 @@ let rec to_ast_range (P.BF_aux(r,l)) = (* TODO add check that ranges are sensibl
     | P.BF_concat(ir1,ir2) -> BF_concat(to_ast_range ir1, to_ast_range ir2)),
     l)
 
-let to_ast_type_union ctx (P.Tu_aux (P.Tu_ty_id (atyp, id), l)) =
-  let typ = to_ast_typ ctx atyp in
-  Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
+let to_ast_type_union ctx = function
+  | P.Tu_aux (P.Tu_ty_id (atyp, id), l) ->
+     let typ = to_ast_typ ctx atyp in
+     Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
+  | P.Tu_aux (_, l) ->
+     raise (Reporting.err_unreachable l __POS__ "Anonymous record type should have been rewritten by now")
 
 let add_constructor id typq ctx =
   let kinds = List.map (fun kopt -> unaux_kind (kopt_kind kopt)) (quant_kopts typq) in
   { ctx with type_constructors = Bindings.add id kinds ctx.type_constructors }
 
-let to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def ctx_out =
-  let aux, ctx = match aux with
-    | P.TD_abbrev (id, typq, kind, typ_arg) ->
-       let id = to_ast_id id in
-       let typq, typq_ctx = to_ast_typquant ctx typq in
-       let kind = to_ast_kind kind in
-       let typ_arg = to_ast_typ_arg typq_ctx typ_arg (unaux_kind kind) in
-       TD_abbrev (id, typq, typ_arg),
-       add_constructor id typq ctx
-
-    | P.TD_record (id, typq, fields, _) ->
-       let id = to_ast_id id in
-       let typq, typq_ctx = to_ast_typquant ctx typq in
-       let fields = List.map (fun (atyp, id) -> to_ast_typ typq_ctx atyp, to_ast_id id) fields in
-       TD_record (id, typq, fields, false),
-       add_constructor id typq ctx
-
-    | P.TD_variant (id, typq, arms, _) ->
-       let id = to_ast_id id in
-       let typq, typq_ctx = to_ast_typquant ctx typq in
-       let arms = List.map (to_ast_type_union typq_ctx) arms in
-       TD_variant (id, typq, arms, false),
-       add_constructor id typq ctx
-
-    | P.TD_enum (id, enums, _) ->
-       let id = to_ast_id id in
-       let enums = List.map to_ast_id enums in
-       TD_enum (id, enums, false),
-       { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
+let anon_rec_constructor_typ record_id = function
+  | P.TypQ_aux (P.TypQ_no_forall, l) -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
+  | P.TypQ_aux (P.TypQ_tq quants, l) ->
+     let rec quant_arg = function
+       | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_none v, l)), _) -> [P.ATyp_aux (P.ATyp_var v, Generated l)]
+       | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, v), l)), _) -> [P.ATyp_aux (P.ATyp_var v, Generated l)]
+       | P.QI_aux (P.QI_const _, _) -> []
+     in
+     match List.concat (List.map quant_arg quants) with
+     | [] -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
+     | args -> P.ATyp_aux (P.ATyp_app (record_id, args), Generated l)
+
+let rec realise_union_anon_rec_types orig_union arms =
+  match orig_union with
+  | P.TD_variant (union_id, typq, _, flag) ->
+     begin match arms with
+     | [] -> []
+     | arm :: arms ->
+        match arm with
+        | (P.Tu_aux ((P.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
+        | (P.Tu_aux ((P.Tu_ty_anon_rec (fields, id)), l)) ->
+           let open Parse_ast in
+           let record_str = "_" ^ string_of_parse_id union_id ^ "_" ^ string_of_parse_id id ^ "_record" in
+           let record_id = Id_aux (Id record_str, Generated l) in
+           let new_arm = Tu_aux (Tu_ty_id (anon_rec_constructor_typ record_id typq, id), Generated l) in
+           let new_rec_def = TD_aux (TD_record (record_id, typq, fields, flag), Generated l) in
+           (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
+     end
+  | _ ->
+     raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs")
 
-    | P.TD_bitfield (id, typ, ranges) ->
-       let id = to_ast_id id in
-       let typ = to_ast_typ ctx typ in
-       let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
-       TD_bitfield (id, typ, ranges),
-       { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
-  in
-  TD_aux (aux, (l, ())), ctx
+let rec to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def list ctx_out =
+  match aux with
+  | P.TD_abbrev (id, typq, kind, typ_arg) ->
+     let id = to_ast_id id in
+     let typq, typq_ctx = to_ast_typquant ctx typq in
+     let kind = to_ast_kind kind in
+     let typ_arg = to_ast_typ_arg typq_ctx typ_arg (unaux_kind kind) in
+     [TD_aux (TD_abbrev (id, typq, typ_arg), (l, ()))],
+     add_constructor id typq ctx
+
+  | P.TD_record (id, typq, fields, _) ->
+     let id = to_ast_id id in
+     let typq, typq_ctx = to_ast_typquant ctx typq in
+     let fields = List.map (fun (atyp, id) -> to_ast_typ typq_ctx atyp, to_ast_id id) fields in
+     [TD_aux (TD_record (id, typq, fields, false), (l, ()))],
+     add_constructor id typq ctx
+
+  | P.TD_variant (id, typq, arms, _) as union ->
+     (* First generate auxilliary record types for anonymous records in constructors *)
+     let records_and_arms = realise_union_anon_rec_types union arms in
+     let rec filter_records = function
+       | [] -> []
+       | Some x :: xs -> x :: filter_records xs
+       | None :: xs -> filter_records xs
+     in
+     let generated_records = filter_records (List.map fst records_and_arms) in
+     let generated_records, ctx =
+       List.fold_left (fun (prev, ctx) td -> let td, ctx = to_ast_typedef ctx td in prev @ td, ctx)
+         ([], ctx)
+         generated_records
+     in
+     let arms = List.map snd records_and_arms in
+     let union = Parse_ast.TD_variant (id, typq, arms, false) in
+     (* Now generate the AST union type *)
+     let id = to_ast_id id in
+     let typq, typq_ctx = to_ast_typquant ctx typq in
+     let arms = List.map (to_ast_type_union typq_ctx) arms in
+     [TD_aux (TD_variant (id, typq, arms, false), (l, ()))] @ generated_records,
+     add_constructor id typq ctx
+
+  | P.TD_enum (id, enums, _) ->
+     let id = to_ast_id id in
+     let enums = List.map to_ast_id enums in
+     [TD_aux (TD_enum (id, enums, false), (l, ()))],
+     { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
+
+  | P.TD_bitfield (id, typ, ranges) ->
+     let id = to_ast_id id in
+     let typ = to_ast_typ ctx typ in
+     let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
+     [TD_aux (TD_bitfield (id, typ, ranges), (l, ()))],
+     { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
 
 let to_ast_rec ctx (P.Rec_aux(r,l): P.rec_opt) : unit rec_opt =
   Rec_aux((match r with
@@ -714,44 +762,44 @@ let to_ast_prec = function
   | P.InfixL -> InfixL
   | P.InfixR -> InfixR
 
-let to_ast_def ctx def : unit def ctx_out =
+let to_ast_def ctx def : unit def list ctx_out =
   match def with
   | P.DEF_overload (id, ids) ->
-     DEF_overload (to_ast_id id, List.map to_ast_id ids), ctx
+     [DEF_overload (to_ast_id id, List.map to_ast_id ids)], ctx
   | P.DEF_fixity (prec, n, op) ->
-     DEF_fixity (to_ast_prec prec, n, to_ast_id op), ctx
+     [DEF_fixity (to_ast_prec prec, n, to_ast_id op)], ctx
   | P.DEF_type(t_def) ->
-     let td, ctx = to_ast_typedef ctx t_def in
-     DEF_type td, ctx
+     let tds, ctx = to_ast_typedef ctx t_def in
+     List.map (fun td -> DEF_type td) tds, ctx
   | P.DEF_fundef(f_def) ->
      let fd = to_ast_fundef ctx f_def in
-     DEF_fundef fd, ctx
+     [DEF_fundef fd], ctx
   | P.DEF_mapdef(m_def) ->
      let md = to_ast_mapdef ctx m_def in
-     DEF_mapdef md, ctx
+     [DEF_mapdef md], ctx
   | P.DEF_val(lbind) ->
      let lb = to_ast_letbind ctx lbind in
-     DEF_val lb, ctx
+     [DEF_val lb], ctx
   | P.DEF_spec(val_spec) ->
      let vs,ctx = to_ast_spec ctx val_spec in
-     DEF_spec vs, ctx
+     [DEF_spec vs], ctx
   | P.DEF_default(typ_spec) ->
      let default,ctx = to_ast_default ctx typ_spec in
-     DEF_default default, ctx
+     [DEF_default default], ctx
   | P.DEF_reg_dec dec ->
      let d = to_ast_dec ctx dec in
-     DEF_reg_dec d, ctx
+     [DEF_reg_dec d], ctx
   | P.DEF_pragma (pragma, arg, l) ->
-     DEF_pragma (pragma, arg, l), ctx
+     [DEF_pragma (pragma, arg, l)], ctx
   | P.DEF_internal_mutrec _ ->
      (* Should never occur because of remove_mutrec *)
      raise (Reporting.err_unreachable P.Unknown __POS__
                                       "Internal mutual block found when processing scattered defs")
   | P.DEF_scattered sdef ->
      let sdef, ctx = to_ast_scattered ctx sdef in
-     DEF_scattered sdef, ctx
+     [DEF_scattered sdef], ctx
   | P.DEF_measure (id, pat, exp) ->
-     DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp), ctx
+     [DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp)], ctx
 
 let rec remove_mutrec = function
   | [] -> []
@@ -763,7 +811,7 @@ let rec remove_mutrec = function
 let to_ast ctx (P.Defs(defs)) =
   let defs = remove_mutrec defs in
   let defs, ctx =
-    List.fold_left (fun (defs, ctx) def -> let def, ctx = to_ast_def ctx def in (def :: defs, ctx)) ([], ctx) defs
+    List.fold_left (fun (defs, ctx) def -> let def, ctx = to_ast_def ctx def in (def @ defs, ctx)) ([], ctx) defs
   in
   Defs (List.rev defs), ctx
 
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 1e1bb816..f01a3846 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -448,6 +448,11 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      let record = coerce_record (value_of_exp exp) in
      return (exp_of_value (StringMap.find (string_of_id id) record))
 
+  | E_var (lexp, exp, E_aux (E_block body, _)) ->
+     wrap (E_block (E_aux (E_assign (lexp, exp), annot) :: body))
+  | E_var (lexp, exp, body) ->
+     wrap (E_block [E_aux (E_assign (lexp, exp), annot); body])
+     
   | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp'))
   | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp]))
   | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
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
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 5a7a72a6..4d7119d7 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -339,7 +339,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
      in
      let wrap = match id with
        | Id_aux (Id i,l) -> (fun f -> Id_aux (Id (f i),Generated l))
-       | Id_aux (DeIid i,l) -> (fun f -> Id_aux (DeIid (f i),l))
+       | Id_aux (Operator i,l) -> (fun f -> Id_aux (Operator (f i),l))
      in
      let name_seg = function
        | (_,None) -> ""
@@ -442,7 +442,7 @@ let freshen_id =
     let () = counter := n + 1 in
     match id with
     | Id_aux (Id x, l) -> Id_aux (Id (x ^ "#m" ^ string_of_int n),Generated l)
-    | Id_aux (DeIid x, l) -> Id_aux (DeIid (x ^ "#m" ^ string_of_int n),Generated l)
+    | Id_aux (Operator x, l) -> Id_aux (Operator (x ^ "#m" ^ string_of_int n),Generated l)
 
 (* TODO: only freshen bindings that might be shadowed *)
 let rec freshen_pat_bindings p =
@@ -746,7 +746,7 @@ let split_defs all_errors splits defs =
     let split_pat vars p =
       let id_match = function
         | Id_aux (Id x,_) -> (try Some (List.assoc x vars) with Not_found -> None)
-        | Id_aux (DeIid x,_) -> (try Some (List.assoc x vars) with Not_found -> None)
+        | Id_aux (Operator x,_) -> (try Some (List.assoc x vars) with Not_found -> None)
       in
 
       let rec list f = function
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 9e4dbf8a..c68a258d 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -579,7 +579,7 @@ let ocaml_string_of_struct ctx id typq fields =
   let ocaml_field (typ, id) =
     separate space [string (string_of_id id ^ " = \""); string "^"; ocaml_string_typ typ (arg ^^ string "." ^^ zencode ctx id)]
   in
-  separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ zencode ctx id); equals]
+  separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ ocaml_typquant typq ^^ space ^^ zencode ctx id); equals]
   ^//^ (string "\"{" ^^ separate_map (hardline ^^ string "^ \", ") ocaml_field fields ^^ string " ^ \"}\"")
 
 let ocaml_string_of_abbrev ctx id typq typ =
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 2ff7b5e2..818c9340 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -109,7 +109,7 @@ kid_aux =  (* identifiers with kind, ticked to differntiate from program variabl
 type 
 id_aux =  (* Identifier *)
    Id of x
- | DeIid of x (* remove infix status *)
+ | Operator of x (* remove infix status *)
 
 type
 base_effect = 
diff --git a/src/parser.mly b/src/parser.mly
index 4004f53d..39ca75ff 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -69,7 +69,7 @@ let cons_fst h (t,x) = (h::t,x)
 
 let string_of_id = function
   | Id_aux (Id str, _) -> str
-  | Id_aux (DeIid str, _) -> str
+  | Id_aux (Operator str, _) -> str
 
 let prepend_id str1 = function
   | Id_aux (Id str2, loc) -> Id_aux (Id (str1 ^ str2), loc)
@@ -84,8 +84,8 @@ let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
 let deinfix = function
-  | (Id_aux (Id v, l)) -> Id_aux (DeIid v, l)
-  | (Id_aux (DeIid v, l)) -> Id_aux (Id v, l)
+  | (Id_aux (Id v, l)) -> Id_aux (Operator v, l)
+  | (Id_aux (Operator v, l)) -> Id_aux (Id v, l)
 
 let mk_effect e n m = BE_aux (e, loc n m)
 let mk_typ t n m = ATyp_aux (t, loc n m)
@@ -142,7 +142,7 @@ type lchain =
 | LC_lteq
 | LC_nexp of atyp
 
-let tyop op t1 t2 s e = mk_typ (ATyp_app (Id_aux (DeIid op, loc s e), [t1; t2])) s e
+let tyop op t1 t2 s e = mk_typ (ATyp_app (Id_aux (Operator op, loc s e), [t1; t2])) s e
 
 let rec desugar_lchain chain s e =
   match chain with
@@ -230,51 +230,51 @@ let rec desugar_rchain chain s e =
 id:
   | Id { mk_id (Id $1) $startpos $endpos }
 
-  | Op Op0 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op1 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op2 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op3 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op4 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op5 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op6 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op7 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op8 { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op9 { mk_id (DeIid $2) $startpos $endpos }
-
-  | Op Op0l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op1l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op2l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op3l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op4l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op5l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op6l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op7l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op8l { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op9l { mk_id (DeIid $2) $startpos $endpos }
-
-  | Op Op0r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op1r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op2r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op3r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op4r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op5r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op6r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op7r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op8r { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op9r { mk_id (DeIid $2) $startpos $endpos }
-
-  | Op Plus { mk_id (DeIid "+") $startpos $endpos }
-  | Op Minus { mk_id (DeIid "-") $startpos $endpos }
-  | Op Star { mk_id (DeIid "*") $startpos $endpos }
-  | Op EqEq { mk_id (DeIid "==") $startpos $endpos }
-  | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
-  | Op Lt { mk_id (DeIid "<") $startpos $endpos }
-  | Op Gt { mk_id (DeIid ">") $startpos $endpos }
-  | Op LtEq { mk_id (DeIid "<=") $startpos $endpos }
-  | Op GtEq { mk_id (DeIid ">=") $startpos $endpos }
-  | Op Amp { mk_id (DeIid "&") $startpos $endpos }
-  | Op Bar { mk_id (DeIid "|") $startpos $endpos }
-  | Op Caret { mk_id (DeIid "^") $startpos $endpos }
+  | Op Op0 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op1 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op2 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op3 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op4 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op5 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op6 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op7 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op8 { mk_id (Operator $2) $startpos $endpos }
+  | Op Op9 { mk_id (Operator $2) $startpos $endpos }
+
+  | Op Op0l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op1l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op2l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op3l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op4l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op5l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op6l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op7l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op8l { mk_id (Operator $2) $startpos $endpos }
+  | Op Op9l { mk_id (Operator $2) $startpos $endpos }
+
+  | Op Op0r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op1r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op2r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op3r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op4r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op5r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op6r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op7r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op8r { mk_id (Operator $2) $startpos $endpos }
+  | Op Op9r { mk_id (Operator $2) $startpos $endpos }
+
+  | Op Plus   { mk_id (Operator "+")  $startpos $endpos }
+  | Op Minus  { mk_id (Operator "-")  $startpos $endpos }
+  | Op Star   { mk_id (Operator "*")  $startpos $endpos }
+  | Op EqEq   { mk_id (Operator "==") $startpos $endpos }
+  | Op ExclEq { mk_id (Operator "!=") $startpos $endpos }
+  | Op Lt     { mk_id (Operator "<")  $startpos $endpos }
+  | Op Gt     { mk_id (Operator ">")  $startpos $endpos }
+  | Op LtEq   { mk_id (Operator "<=") $startpos $endpos }
+  | Op GtEq   { mk_id (Operator ">=") $startpos $endpos }
+  | Op Amp    { mk_id (Operator "&")  $startpos $endpos }
+  | Op Bar    { mk_id (Operator "|")  $startpos $endpos }
+  | Op Caret  { mk_id (Operator "^")  $startpos $endpos }
 
 op0: Op0 { mk_id (Id $1) $startpos $endpos }
 op1: Op1 { mk_id (Id $1) $startpos $endpos }
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 3a1deed0..c1680878 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -76,25 +76,9 @@ let semi_sp = semi ^^ space
 let comma_sp = comma ^^ space
 let colon_sp = spaces colon
 
-let doc_var (Kid_aux(Var v,_)) = string v
 let doc_int i = string (Big_int.to_string i)
 let doc_op symb a b = infix 2 1 symb a b
 let doc_unop symb a = prefix 2 1 symb a
 
-let doc_id (Id_aux(i,_)) =
-  match i with
-  | Id i -> string i
-  | DeIid x ->
-      (* add an extra space through empty to avoid a closing-comment
-       * token in case of x ending with star. *)
-      parens (separate space [string "deinfix"; string x; empty])
-
-(*
-let rec doc_range (BF_aux(r,_)) = match r with
-  | BF_single i -> doc_int i
-  | BF_range(i1,i2) -> doc_op dotdot (doc_int i1) (doc_int i2)
-  | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
-*)
-
 let print ?(len=100) channel doc = ToChannel.pretty 1. len channel doc
 let to_buf ?(len=100) buf doc = ToBuffer.pretty 1. len buf doc
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 72d7730e..b4f32dce 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -184,7 +184,7 @@ let rec fix_id remove_tick name = match name with
 let string_id (Id_aux(i,_)) =
   match i with
   | Id i -> fix_id false i
-  | DeIid x -> Util.zencode_string ("op " ^ x)
+  | Operator x -> Util.zencode_string ("op " ^ x)
 
 let doc_id id = string (string_id id)
 
@@ -193,12 +193,12 @@ let doc_id_type (Id_aux(i,_)) =
   | Id("int") -> string "Z"
   | Id("real") -> string "R"
   | Id i -> string (fix_id false i)
-  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+  | Operator x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_ctor (Id_aux(i,_)) =
   match i with
   | Id i -> string (fix_id false i)
-  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+  | Operator x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_var ctx kid =
   match KBindings.find kid ctx.kid_id_renames with
@@ -2468,7 +2468,7 @@ let tyvars_of_typquant (TypQ_aux (tq,_)) =
 let mk_kid_renames ids_to_avoid kids =
   let map_id = function
     | Id_aux (Id i, _) -> Some (fix_id false i)
-    | Id_aux (DeIid _, _) -> None
+    | Id_aux (Operator _, _) -> None
   in
   let ids = StringSet.of_list (Util.map_filter map_id (IdSet.elements ids_to_avoid)) in
   let rec check_kid kid (newkids,rebindings) =
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 20c9a69f..6479a028 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -69,12 +69,14 @@ type context = {
   top_env : Env.t
 }
 let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty; top_env = Env.empty }
-
+              
 let print_to_from_interp_value = ref false
 let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
 
+let doc_var (Kid_aux(Var v,_)) = string v
+
 let is_number_char c =
   c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
   c = '6' || c = '7' || c = '8' || c = '9'
@@ -113,7 +115,7 @@ let rec fix_id remove_tick name = match name with
 let doc_id_lem (Id_aux(i,_)) =
   match i with
   | Id i -> string (fix_id false i)
-  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+  | Operator x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_lem_type (Id_aux(i,_)) =
   match i with
@@ -121,7 +123,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
   | Id i -> string (fix_id false i)
-  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+  | Operator x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_lem_ctor (Id_aux(i,_)) =
   match i with
@@ -131,11 +133,11 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
   | Id i -> string (fix_id false (String.capitalize_ascii i))
-  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+  | Operator x -> string (Util.zencode_string ("op " ^ x))
 
 let deinfix = function
-  | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
-  | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l)
+  | Id_aux (Id v, l) -> Id_aux (Operator v, l)
+  | Id_aux (Operator v, l) -> Id_aux (Operator v, l)
 
 let doc_var_lem kid = string (fix_id true (string_of_kid kid))
 
@@ -1046,6 +1048,11 @@ let doc_typquant_sorts idpp (TypQ_aux (typq,_)) =
      else empty
   | TypQ_no_forall -> empty
 
+let doc_sia_id (Id_aux(i,_)) =
+  match i with
+  | Id i -> string i
+  | Operator x -> string ("operator " ^ x)
+
 let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
   | TD_abbrev(id,typq,A_aux (A_typ typ, _)) ->
      let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in
@@ -1125,7 +1132,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
              ((*doc_typquant_lem typq*) ar_doc) in
          let make_id pat id =
            separate space [string "SIA.Id_aux";
-                           parens (string "SIA.Id " ^^ string_lit (doc_id id));
+                           parens (string "SIA.Id " ^^ string_lit (doc_sia_id id));
                            if pat then underscore else string "SIA.Unknown"] in
          let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
          let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
@@ -1161,7 +1168,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
                       [pipe;doc_id_lem_ctor cid;string "v";arrow;
                        string "SI.V_ctor";
                        parens (make_id false cid);
-                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                       parens (string "SIA.T_id " ^^ string_lit (doc_sia_id id));
                        string "SI.C_Union";
                        parens (string "toInterpValue v")])
                   ar) ^/^
@@ -1199,7 +1206,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
          let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
          let make_id pat id =
            separate space [string "SIA.Id_aux";
-                           parens (string "SIA.Id " ^^ string_lit (doc_id id));
+                           parens (string "SIA.Id " ^^ string_lit (doc_sia_id id));
                            if pat then underscore else string "SIA.Unknown"] in
          let fromInterpValuePP =
            (prefix 2 1)
@@ -1252,7 +1259,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
                       [pipe;doc_id_lem_ctor cid;arrow;
                        string "SI.V_ctor";
                        parens (make_id false cid);
-                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                       parens (string "SIA.T_id " ^^ string_lit (doc_sia_id id));
                        parens (string ("SI.C_Enum " ^ string_of_int number));
                        parens (string "toInterpValue ()")])
                   (List.combine enums (nats ((List.length enums) - 1)))) ^/^
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 1fa14a7d..7f3a2b63 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -61,7 +61,7 @@ let doc_op symb a b = infix 2 1 symb a b
 let doc_id (Id_aux (id_aux, _)) =
   string (match id_aux with
           | Id v -> v
-          | DeIid op -> "operator " ^ op)
+          | Operator op -> "operator " ^ op)
 
 let doc_kid kid = string (Ast_util.string_of_kid kid)
 
@@ -92,7 +92,7 @@ let rec doc_nexp =
   let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) =
     match n_aux with
     | Nexp_constant c -> string (Big_int.to_string c)
-    | Nexp_app (Id_aux (DeIid op, _), [n1; n2]) ->
+    | Nexp_app (Id_aux (Operator op, _), [n1; n2]) ->
        separate space [atomic_nexp n1; string op; atomic_nexp n2]
     | Nexp_app (id, nexps) -> string (string_of_nexp nexp)
     (* This segfaults??!!!!
@@ -172,7 +172,7 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
   | Typ_app (id, []) -> doc_id id
-  | Typ_app (Id_aux (DeIid str, _), [x; y]) ->
+  | Typ_app (Id_aux (Operator str, _), [x; y]) ->
      separate space [doc_typ_arg x; doc_typ_arg y]
   | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
      string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
diff --git a/src/process_file.ml b/src/process_file.ml
index c6d900b4..dbe6d62d 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -126,33 +126,6 @@ let cond_pragma l defs =
   in
   scan defs
 
-let astid_to_string (Ast.Id_aux (id, _)) =
-  match id with
-  | Ast.Id x | Ast.DeIid x -> x
-
-let parseid_to_string (Parse_ast.Id_aux (id, _)) =
-  match id with
-  | Parse_ast.Id x | Parse_ast.DeIid x -> x
-
-let rec realise_union_anon_rec_types orig_union arms =
-  match orig_union with
-  | Parse_ast.TD_variant (union_id, typq, _, flag) ->
-     begin match arms with
-     | [] -> []
-     | arm :: arms ->
-        match arm with
-        | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
-        | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) ->
-           let open Parse_ast in
-           let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in
-           let record_id = Id_aux (Id record_str, Generated l) in
-           let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in
-           let new_rec_def = DEF_type (TD_aux (TD_record (record_id, typq, fields, flag), Generated l)) in
-           (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
-     end
-  | _ ->
-     raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs")
-
 let rec preprocess opts = function
   | [] -> []
   | Parse_ast.DEF_pragma ("define", symbol, _) :: defs ->
@@ -218,20 +191,6 @@ let rec preprocess opts = function
   | Parse_ast.DEF_pragma (p, arg, l) :: defs ->
      Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs
 
-  (* realise any anonymous record arms of variants *)
-  | Parse_ast.DEF_type (Parse_ast.TD_aux
-                          (Parse_ast.TD_variant (id, typq, arms, flag) as union, l)
-                       ) :: defs ->
-     let records_and_arms = realise_union_anon_rec_types union arms in
-     let rec filter_records = function [] -> []
-                                 | Some x :: xs -> x :: filter_records xs
-                                 | None :: xs -> filter_records xs
-     in
-     let generated_records = filter_records (List.map fst records_and_arms) in
-     let rewritten_arms = List.map snd records_and_arms in
-     let rewritten_union = Parse_ast.TD_variant (id, typq, rewritten_arms, flag) in
-     generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess opts defs
-
   | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs ->
      begin match atyp with
      | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess opts defs
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 11b1d469..f27e2946 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1018,7 +1018,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
   let mk_exp e_aux = E_aux (e_aux, (l, ())) in
   let mk_num_exp i = mk_lit_exp (L_num i) in
   let check_eq_exp l r =
-    let exp = mk_exp (E_app_infix (l, Id_aux (DeIid "==", Parse_ast.Unknown), r)) in
+    let exp = mk_exp (E_app_infix (l, Id_aux (Operator "==", Parse_ast.Unknown), r)) in
     check_exp env exp bool_typ in
 
   let access_bit_exp rootid l typ idx =
@@ -2767,7 +2767,7 @@ let construct_toplevel_string_append_func env f_id pat =
        let mapping_prefix_func =
          match mapping_id with
          | Id_aux (Id id, _)
-         | Id_aux (DeIid id, _) -> id ^ "_matches_prefix"
+         | Id_aux (Operator id, _) -> id ^ "_matches_prefix"
        in
        let mapping_inner_typ =
          match Env.get_val_spec (mk_id mapping_prefix_func) env with
@@ -2943,7 +2943,7 @@ let rec rewrite_defs_pat_string_append env =
        let mapping_prefix_func =
          match mapping_id with
          | Id_aux (Id id, _)
-         | Id_aux (DeIid id, _) -> id ^ "_matches_prefix"
+         | Id_aux (Operator id, _) -> id ^ "_matches_prefix"
        in
        let mapping_inner_typ =
          match Env.get_val_spec (mk_id mapping_prefix_func) env with
@@ -3165,7 +3165,7 @@ let rewrite_defs_mapping_patterns env =
        let mapping_name =
          match mapping_id with
          | Id_aux (Id id, _)
-         | Id_aux (DeIid id, _) -> id
+         | Id_aux (Operator id, _) -> id
        in
 
        let mapping_matches_id = mk_id (mapping_name ^ "_" ^ mapping_direction ^ "_matches") in
@@ -4488,7 +4488,7 @@ let rewrite_explicit_measure env (Defs defs) =
   (* NB: the Coq backend relies on recognising the #rec# prefix *)
   let rec_id = function
     | Id_aux (Id id,l)
-    | Id_aux (DeIid id,l) -> Id_aux (Id ("#rec#" ^ id),Generated l)
+    | Id_aux (Operator id,l) -> Id_aux (Id ("#rec#" ^ id),Generated l)
   in
   let limit = mk_id "#reclimit" in
   (* Add helper function with extra argument to spec *)
diff --git a/src/type_check.ml b/src/type_check.ml
index 4396728b..d5d42316 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -140,8 +140,8 @@ let typ_error env l m = raise (Type_error (env, l, Err_other m))
 let typ_raise env l err = raise (Type_error (env, l, err))
 
 let deinfix = function
-  | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
-  | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l)
+  | Id_aux (Id v, l) -> Id_aux (Operator v, l)
+  | Id_aux (Operator v, l) -> Id_aux (Operator v, l)
 
 let field_name rec_id id =
   match rec_id, id with
@@ -181,7 +181,7 @@ let is_atom_bool (Typ_aux (typ_aux, _)) =
 
 let rec strip_id = function
   | Id_aux (Id x, _) -> Id_aux (Id x, Parse_ast.Unknown)
-  | Id_aux (DeIid x, _) -> Id_aux (DeIid x, Parse_ast.Unknown)
+  | Id_aux (Operator x, _) -> Id_aux (Operator x, Parse_ast.Unknown)
 and strip_kid = function
   | Kid_aux (Var x, _) -> Kid_aux (Var x, Parse_ast.Unknown)
 and strip_base_effect = function