Remove the Record theory (OCamlPro#1095)

This PR removes the `Record` theory, which is now handled by the ADT theory. 
- The context built for record definitions is still required by the matching module. We plan to remove it, but it is not easy to get rid of it. 
- The `xs_modulo_records` function in `Matching` is no longer useful. This PR removes it.
- The test `1008/records.smt2` is now solved, but only with Tableaux.

Author: Halbaroth

docs/sphinx_docs/Alt_ergo_native/05_theories.md

@@ -17,8 +17,7 @@ Alt-Ergo currently provides built-in support for the following theories.
 * Linear arithmetic over integers and rationals
 * (Fragment of) non-linear arithmetic
 * Floating-point arithmetic (as an extension)
-* Enumerated datatypes
-* Record datatypes
+* Algebraic datatypes
 * Polymorphic functional arrays
 * Fixed-size bitvectors
 
@@ -28,7 +27,6 @@ All theories are always considered *modulo equality*.
 * `SUM`: Enumerated datatypes
 * `Adt`: Algebraic datatypes
 * `Arrays`: Polymorphic functional arrays
-* `Records`: Record datatypes
 * `Bitv`: Fixed-size bitvectors
 * `LIA`: Linear arithmetic over integers
 * `LRA`: Linear arithmetic over rationals

rsc/extra/subgraphs.dot

@@ -141,7 +141,6 @@ subgraph cluster_lib {
                         "Enum";
                         "Ite";
                         "Polynome";
-                        "Records";
                         "Sig";
                 }
 

src/lib/dune

@@ -50,7 +50,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_intf Intervals_core Intervals
-    Ite_rel Matching Matching_types Polynome Records Records_rel
+    Ite_rel Matching Matching_types Polynome
     Satml_frontend_hybrid Satml_frontend Satml Sat_solver Sat_solver_sig
     Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist
     ; structures

src/lib/frontend/models.ml

@@ -42,7 +42,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 ->
@@ -151,26 +151,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)" DE.Term.Const.print field print e
-      else
-        fprintf fmt "%a.%a" print e DE.Term.Const.print 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 "; ")
-                DE.Term.Const.print 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 ||

src/lib/frontend/translate.ml

@@ -515,85 +515,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.TvMap.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.TvMap.add v ty acc
-          | _ -> assert false
-      ) Ty.TvMap.empty args tyl
-    in
-    apply_ty_substs tysubsts ty
-
+  | Tadt (hs, _) -> Tadt (hs, tyl )
   | 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. *)
-    Nest.attach_orders [adt];
-    let tyvl = Cache.store_ty_vars_ret id_ty in
-    let lbs =
-      Array.fold_right (
-        fun c acc ->
-          match c with
-          | Some (DE.{ id_ty; _ } as id) ->
-            let pty = dty_to_ty id_ty in
-            (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 ty = Ty.trecord ~record_constr:cstr tyvl ty_c lbs in
-    Cache.store_ty ty_c ty
-
   | Some (Adt { cases; _ } as adt) ->
     Nest.attach_orders [adt];
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
@@ -644,34 +576,10 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
   in
   (Hstring.make name, arg_tys, ret_ty)
 
-(** Handles the definitions of a list of mutually recursive types.
-    - If one of the types is an ADT, the ADTs that have only one case are
-      considered as ADTs as well and not as records. *)
+(** Handles the definitions of a list of mutually recursive types. *)
 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 lbs =
-        Array.fold_right (
-          fun c acc ->
-            match c with
-            | Some (DE.{ id_ty; _ } as id) ->
-              let pty = dty_to_ty id_ty in
-              (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 ty =
-        Ty.trecord ~record_constr args name lbs
-      in
-      Cache.store_ty ty_c ty
-
     | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
       let cs =
         Array.fold_right (
@@ -693,37 +601,15 @@ 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
   Nest.attach_orders 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 record_constr = cases.(0).cstr in
-          let ty =
-            if (record || Array.length cases = 1) && not contains_adts
-            then
-              Ty.trecord ~record_constr tyvl ty_c []
-            else
-              Ty.t_adt ty_c tyvl
-          in
+          let ty = Ty.t_adt ty_c tyvl in
           Cache.store_ty ty_c ty;
           (ty, Some adt) :: acc
 
@@ -850,15 +736,11 @@ end = struct
     let mk_destr =
       match ty with
       | Ty.Tadt _ -> (fun hs -> Sy.destruct hs)
-      | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs))
       | _ -> assert false
     in
     let mk_tester =
       match ty with
       | Ty.Tadt _ -> E.mk_tester
-      | Ty.Trecord _ ->
-        (* no need to test for records *)
-        (fun _e _name -> assert false)
       | _ -> assert false
     in
     let res = compile mk_destr mk_tester e cases e in
@@ -1011,14 +893,8 @@ let rec mk_expr
             E.mk_term sy [] ty
 
           | B.Constructor _ ->
-            begin match dty_to_ty term_ty with
-              | Trecord _ as ty ->
-                E.mk_record [] ty
-              | Tadt _ as ty ->
-                E.mk_constr tcst [] ty
-              | ty ->
-                Fmt.failwith "unexpected type %a@." Ty.print ty
-            end
+            let ty = dty_to_ty term_ty in
+            E.mk_constr tcst [] ty
 
           | _ -> unsupported "Constant term %a" DE.Term.print term
         end
@@ -1059,10 +935,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 destr)
-                      | Tadt _ ->
-                        Sy.destruct destr
+                      | Tadt _ -> Sy.destruct destr
                       | _ -> assert false
                     in
                     E.mk_term sy [e] ty
@@ -1093,11 +966,6 @@ let rec mk_expr
               | Ty.Tadt _ ->
                 E.mk_tester cstr (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
 
@@ -1364,19 +1232,9 @@ let rec mk_expr
 
           | B.Constructor _, _ ->
             let ty = dty_to_ty term_ty in
-            begin match ty with
-              | Ty.Tadt _ ->
-                let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_constr tcst l ty
-              | Ty.Trecord _ ->
-                let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_record l ty
-              | _ ->
-                Fmt.failwith
-                  "Constructor error: %a does not belong to a record nor an\
-                   algebraic data type"
-                  DE.Term.print app_term
-            end
+            let sy = Sy.constr tcst in
+            let l = List.map (fun t -> aux_mk_expr t) args in
+            E.mk_term sy l ty
 
           | B.Coercion, [ x ] ->
             begin match DT.view (DE.Term.ty x), DT.view term_ty with