Merge Records into ADT

src/lib/dune

@@ -52,7 +52,7 @@
     Ac Arith Arrays_rel Bitv Ccx Shostak Relation
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Matching Matching_types
-    Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
+    Polynome Satml_frontend_hybrid Satml_frontend Satml
     Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils Bitlist
     ; structures
     Commands Errors Explanation Fpa_rounding

src/lib/frontend/cnf.ml

@@ -110,12 +110,20 @@ let rec make_term quant_basename t =
       E.mk_term (Sy.Op Sy.Concat)
         [mk_term t1; mk_term t2] ty
 
-    | TTdot (t, s) ->
-      E.mk_term (Sy.Op (Sy.Access (Uid.of_hstring s))) [mk_term t] ty
-
-    | TTrecord lbs ->
+    | TTrecord (ty, lbs) ->
       let lbs = List.map (fun (_, t) -> mk_term t) lbs in
-      E.mk_term (Sy.Op Sy.Record) lbs ty
+      let cstr =
+        match ty with
+        | Tadt (name, params, true) ->
+          begin
+            let Adt cases = Ty.type_body name params in
+            match cases with
+            | [{ constr; _ }] -> Uid.show constr
+            | _ -> assert false
+          end
+        | _ -> assert false
+      in
+      E.mk_constr (Uid.of_string cstr) lbs ty
 
     | TTlet (binders, t2) ->
       let binders =

src/lib/frontend/d_cnf.ml

@@ -492,86 +492,17 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty =
   | _ -> unsupported "Type %a" DE.Ty.print dty
 
 and handle_ty_app ?(update = false) ty_c l =
-  (* Applies the substitutions in [tysubsts] to each encountered type
-     variable. *)
-  let rec apply_ty_substs tysubsts ty =
-    match ty with
-    | Ty.Tvar { v; _ } ->
-      Ty.M.find v tysubsts
-
-    | Text (tyl, hs) ->
-      Ty.Text (List.map (apply_ty_substs tysubsts) tyl, hs)
-
-    | Tfarray (ti, tv) ->
-      Tfarray (
-        apply_ty_substs tysubsts ti,
-        apply_ty_substs tysubsts tv
-      )
-
-    | Tadt (hs, tyl) ->
-      Tadt (hs, List.map (apply_ty_substs tysubsts) tyl)
-
-    | Trecord ({ args; lbs; _ } as rcrd) ->
-      Trecord {
-        rcrd with
-        args = List.map (apply_ty_substs tysubsts) args;
-        lbs = List.map (
-            fun (hs, t) ->
-              hs, apply_ty_substs tysubsts t
-          ) lbs;
-      }
-
-    | _ -> ty
-  in
   let tyl = List.map (dty_to_ty ~update) l in
   (* Recover the initial versions of the types and apply them on the provided
      type arguments stored in [tyl]. *)
   match Cache.find_ty ty_c with
-  | Tadt (hs, _) -> Tadt (hs, tyl)
-
-  | Trecord { args; _ } as ty ->
-    let tysubsts =
-      List.fold_left2 (
-        fun acc tv ty ->
-          match tv with
-          | Ty.Tvar { v; _ } -> Ty.M.add v ty acc
-          | _ -> assert false
-      ) Ty.M.empty args tyl
-    in
-    apply_ty_substs tysubsts ty
-
+  | Tadt (hs, _, record) -> Tadt (hs, tyl, record)
   | Text (_, s) -> Text (tyl, s)
   | _ -> assert false
 
 (** Handles a simple type declaration. *)
 let mk_ty_decl (ty_c: DE.ty_cst) =
   match DT.definition ty_c with
-  | Some (
-      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt
-    ) ->
-    (* Records and adts that only have one case are treated in the same way,
-       and considered as records. *)
-    Topological_order.sort [adt];
-    let tyvl = Cache.store_ty_vars_ret id_ty in
-    let rev_lbs =
-      Array.fold_left (
-        fun acc c ->
-          match c with
-          | Some (DE.{ id_ty; _ } as id) ->
-            let pty = dty_to_ty id_ty in
-            (Uid.of_dolmen id, pty) :: acc
-          | _ ->
-            Fmt.failwith
-              "Unexpected null label for some field of the record type %a"
-              DE.Ty.Const.print ty_c
-
-      ) [] dstrs
-    in
-    let lbs = List.rev rev_lbs in
-    let record_constr = Uid.of_dolmen cstr in
-    let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
-    Cache.store_ty ty_c ty
-
   | Some (Adt { cases; _ } as adt) ->
     Topological_order.sort [adt];
     let uid = Uid.of_dolmen ty_c in
@@ -630,30 +561,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
 let mk_mr_ty_decls (tdl: DE.ty_cst list) =
   let handle_ty_decl (ty: Ty.t) (tdef: DE.Ty.def option) =
     match ty, tdef with
-    | Trecord { args; name; record_constr; _ },
-      Some (
-        Adt { cases = [| { dstrs; _ } |]; ty = ty_c; _ }
-      ) ->
-      let rev_lbs =
-        Array.fold_left (
-          fun acc c ->
-            match c with
-            | Some (DE.{ id_ty; _ } as id) ->
-              let pty = dty_to_ty id_ty in
-              (Uid.of_dolmen id, pty) :: acc
-            | _ ->
-              Fmt.failwith
-                "Unexpected null label for some field of the record type %a"
-                DE.Ty.Const.print ty_c
-        ) [] dstrs
-      in
-      let lbs = List.rev rev_lbs in
-      let ty =
-        Ty.trecord ~record_constr args name lbs
-      in
-      Cache.store_ty ty_c ty
-
-    | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
+    | Tadt (hs, tyl, _), Some (Adt { cases; ty = ty_c; _ }) ->
       let rev_cs =
         Array.fold_left (
           fun accl DE.{ cstr; dstrs; _ } ->
@@ -675,36 +583,16 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
 
     | _ -> assert false
   in
-  (* If there are adts in the list of type declarations then records are
-     converted to adts, because that's how it's done in the legacy typechecker.
-     But it might be more efficient not to do that. *)
-  let rev_tdefs, contains_adts =
-    List.fold_left (
-      fun (acc, ca) ty_c ->
-        match DT.definition ty_c with
-        | Some (Adt { record; cases; _ } as df)
-          when not record && Array.length cases > 1 ->
-          df :: acc, true
-        | Some (Adt _ as df) ->
-          df :: acc, ca
-        | Some Abstract | None ->
-          assert false
-    ) ([], false) tdl
-  in
+  let rev_tdefs = List.rev_map (fun td -> Option.get @@ DT.definition td) tdl in
   Topological_order.sort rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
-        | DE.Adt { cases; record; ty = ty_c; } as adt ->
+        | DE.Adt { cases; ty = ty_c; _ } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
           let uid = Uid.of_dolmen ty_c in
-          let ty =
-            if (record || Array.length cases = 1) && not contains_adts
-            then
-              Ty.trecord ~record_constr:uid tyvl uid []
-            else Ty.t_adt uid tyvl
-          in
+          let ty = Ty.t_adt uid tyvl in
           Cache.store_ty ty_c ty;
           (ty, Some adt) :: acc
 
@@ -974,10 +862,7 @@ let rec mk_expr
                     let e = aux_mk_expr x in
                     let sy =
                       match Cache.find_ty adt with
-                      | Trecord _ ->
-                        Sy.Op (Sy.Access (Uid.of_dolmen destr))
-                      | Tadt _ ->
-                        Sy.destruct (Uid.of_dolmen destr)
+                      | Tadt _ -> Sy.destruct (Uid.of_dolmen destr)
                       | _ -> assert false
                     in
                     E.mk_term sy [e] ty
@@ -1009,11 +894,6 @@ let rec mk_expr
               | Ty.Tadt _ ->
                 E.mk_builtin ~is_pos:true builtin [aux_mk_expr x]
 
-              | Ty.Trecord _ ->
-                (* The typechecker allows only testers whose the
-                   two arguments have the same type. Thus, we can always
-                   replace the tester of a record by the true literal. *)
-                E.vrai
               | _ -> assert false
             end
 
@@ -1299,13 +1179,10 @@ let rec mk_expr
           | B.Constructor _, _ ->
             let ty = dty_to_ty term_ty in
             begin match ty with
-              | Ty.Tadt (_, _) ->
+              | Ty.Tadt _ ->
                 let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_term sy l ty
-              | Ty.Trecord _ ->
-                let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_term (Sy.Op Sy.Record) l ty
               | _ ->
                 Fmt.failwith
                   "Constructor error: %a does not belong to a record nor an\

src/lib/frontend/models.ml

@@ -50,7 +50,7 @@ module Pp_smtlib_term = struct
     asprintf "%a" Ty.pp_smtlib t
 
   let rec print fmt t =
-    let {Expr.f;xs;ty; _} = Expr.term_view t in
+    let {Expr.f;xs; _} = Expr.term_view t in
     match f, xs with
 
     | Sy.Lit lit, xs ->
@@ -146,26 +146,6 @@ module Pp_smtlib_term = struct
     | Sy.Op Sy.Extract (i, j), [e] ->
       fprintf fmt "%a^{%d,%d}" print e i j
 
-    | Sy.Op (Sy.Access field), [e] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(%a %a)" Uid.pp field print e
-      else
-        fprintf fmt "%a.%a" print e Uid.pp field
-
-    | Sy.Op (Sy.Record), _ ->
-      begin match ty with
-        | Ty.Trecord { Ty.lbs = lbs; _ } ->
-          assert (List.length xs = List.length lbs);
-          fprintf fmt "{";
-          ignore (List.fold_left2 (fun first (field,_) e ->
-              fprintf fmt "%s%a = %a"  (if first then "" else "; ")
-                Uid.pp field print e;
-              false
-            ) true lbs xs);
-          fprintf fmt "}";
-        | _ -> assert false
-      end
-
     (* TODO: introduce PrefixOp in the future to simplify this ? *)
     | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round ||
                               op == Sy.Max_real || op == Sy.Max_int ||