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, 106 insertions, 58 deletions

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