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

1 files changed, 4 insertions, 4 deletions

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) =