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, 0 insertions, 41 deletions

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