Remove more dead code

src/lib/structures/errors.ml

@@ -51,12 +51,9 @@ type typing_error =
   | ShouldHaveTypeBitv of Ty.t
   | ArrayIndexShouldHaveTypeInt
   | ShouldHaveTypeArray
-  | ShouldHaveTypeRecord of Ty.t
-  | ShouldBeARecord
   | ShouldHaveLabel of string * string
   | NoLabelInType of Hstring.t * Ty.t
   | ShouldHaveTypeProp
-  | NoRecordType of Hstring.t
   | DuplicateLabel of Hstring.t
   | DuplicatePattern of string
   | WrongLabel of Hstring.t * Ty.t
@@ -175,19 +172,12 @@ let report_typing_error fmt = function
       Ty.print t
   | ShouldHaveTypeArray ->
     fprintf fmt "this expression should have type farray"
-  | ShouldHaveTypeRecord t ->
-    fprintf fmt "this expression has type %a but it should have a record type"
-      Ty.print t
-  | ShouldBeARecord ->
-    fprintf fmt "this expression should have a record type"
   | ShouldHaveLabel (s, a) ->
     fprintf fmt "this expression has type %s which has no label %s" s a
   | NoLabelInType (lb, ty) ->
     fprintf fmt "no label %s in type %a" (Hstring.view lb) Ty.print ty
   | ShouldHaveTypeProp ->
     fprintf fmt "this expression should have type prop"
-  | NoRecordType s ->
-    fprintf fmt "no record type has label %s" (Hstring.view s)
   | DuplicateLabel s ->
     fprintf fmt "label %s is defined several times" (Hstring.view s)
   | DuplicatePattern s ->

src/lib/structures/errors.mli

@@ -57,12 +57,9 @@ type typing_error =
   | ShouldHaveTypeBitv of Ty.t
   | ArrayIndexShouldHaveTypeInt
   | ShouldHaveTypeArray
-  | ShouldHaveTypeRecord of Ty.t
-  | ShouldBeARecord
   | ShouldHaveLabel of string * string
   | NoLabelInType of Hstring.t * Ty.t
   | ShouldHaveTypeProp
-  | NoRecordType of Hstring.t
   | DuplicateLabel of Hstring.t
   | DuplicatePattern of string
   | WrongLabel of Hstring.t * Ty.t

src/lib/structures/expr.mli

@@ -437,7 +437,6 @@ val is_pure : t -> bool
 val is_model_term : t -> bool
 (** [is_model_term e] checks if the expression [e] is a model terms.
     A model term can be:
-    - A record definition involving only model terms.
     - A constructor application involving only model terms,
     - A literal of a basic type (integer, real, boolean, unit or bitvector),
     - A name. *)

src/lib/structures/profiling.ml

@@ -454,18 +454,6 @@ let columns : (string * string * int * bool option * 'a) list =
        Format.sprintf "%s~%s"
          (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4));
 
-    "Sum", "Time spent in Sum module(s)", 16, Some false,
-    (fun _ gtime sz ->
-       let curr = Timers.get_sum (get_timers ()) Timers.M_Sum in
-       Format.sprintf "%s~%s"
-         (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4));
-
-    "Records", "Time spent in Records module(s)", 16, Some false,
-    (fun _ gtime sz ->
-       let curr = Timers.get_sum (get_timers ()) Timers.M_Records in
-       Format.sprintf "%s~%s"
-         (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4));
-
     "AC", "Time spent in AC module(s)", 16, Some false,
     (fun _ gtime sz ->
        let curr = Timers.get_sum (get_timers ()) Timers.M_AC in
@@ -480,10 +468,8 @@ let columns : (string * string * int * bool option * 'a) list =
        let tcc = Timers.get_sum timers Timers.M_CC in
        let tarith = Timers.get_sum timers Timers.M_Arith in
        let tarrays = Timers.get_sum timers Timers.M_Arrays in
-       let tsum = Timers.get_sum timers Timers.M_Sum in
-       let trecs = Timers.get_sum timers Timers.M_Records in
        let tac = Timers.get_sum timers Timers.M_AC in
-       let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tsum+.trecs+.tac in
+       let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tac in
        float_resize total sz);
   ]
 

src/lib/structures/ty.ml

@@ -451,14 +451,6 @@ let t_adt ?(body=None) s ty_vars =
   begin match body with
     | None -> ()
     | Some [] -> assert false
-    | Some ([_] as cases) ->
-      if Options.get_debug_adt () then
-        Printer.print_dbg ~module_name:"Ty"
-          "should be registered as a record";
-      let cases =
-        List.map (fun (constr, destrs) -> {constr; destrs}) cases
-      in
-      Decls.add s ty_vars cases
     | Some cases ->
       let cases =
         List.map (fun (constr, destrs) -> {constr; destrs}) cases

src/lib/util/timers.ml

@@ -39,8 +39,6 @@ type ty_module =
   | M_UF
   | M_Arith
   | M_Arrays
-  | M_Sum
-  | M_Records
   | M_Adt
   | M_Bitv
   | M_AC
@@ -61,8 +59,6 @@ let all_modules =
     M_UF;
     M_Arith;
     M_Arrays;
-    M_Sum;
-    M_Records;
     M_Adt;
     M_Bitv;
     M_AC;
@@ -136,8 +132,6 @@ let string_of_ty_module k = match k with
   | M_UF       -> "UF"
   | M_Arith    -> "Arith"
   | M_Arrays   -> "Arrays"
-  | M_Sum      -> "Sum"
-  | M_Records  -> "Records"
   | M_Adt      -> "Adt"
   | M_Bitv     -> "Bitv"
   | M_AC       -> "AC"

src/lib/util/timers.mli

@@ -35,8 +35,6 @@ type ty_module =
   | M_UF
   | M_Arith
   | M_Arrays
-  | M_Sum
-  | M_Records
   | M_Adt
   | M_Bitv
   | M_AC

src/lib/util/util.ml

@@ -77,10 +77,8 @@ let pp_sat_solver ppf = function
   | CDCL_Tableaux -> Format.fprintf ppf "CDCL-Tableaux"
 
 type theories_extensions =
-  | Sum
   | Adt
   | Arrays
-  | Records
   | Bitv
   | LIA
   | LRA
@@ -116,10 +114,8 @@ let equal_mode x y = match x, y with
 
 let th_ext_of_string ext =
   match ext with
-  | "Sum" -> Some Sum
   | "Adt" -> Some Adt
   | "Arrays" -> Some Arrays
-  | "Records" -> Some Records
   | "Bitv" -> Some Bitv
   | "LIA" -> Some LIA
   | "LRA" -> Some LRA
@@ -131,10 +127,8 @@ let th_ext_of_string ext =
 
 let string_of_th_ext ext =
   match ext with
-  | Sum -> "Sum"
   | Adt -> "Adt"
   | Arrays -> "Arrays"
-  | Records -> "Records"
   | Bitv -> "Bitv"
   | LIA -> "LIA"
   | LRA -> "LRA"

src/lib/util/util.mli

@@ -59,10 +59,8 @@ type sat_solver =
 val pp_sat_solver : Format.formatter -> sat_solver -> unit
 
 type theories_extensions =
-  | Sum
   | Adt
   | Arrays
-  | Records
   | Bitv
   | LIA
   | LRA