From 3ba843d6166ce2a0bb7a0d83cc990c5e10610441 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Sun, 14 Apr 2024 13:05:16 +0200 Subject: [PATCH] Merge `Records` into `ADT` --- src/lib/dune | 2 +- src/lib/frontend/cnf.ml | 16 +- src/lib/frontend/d_cnf.ml | 160 +----------- src/lib/frontend/models.ml | 22 +- src/lib/frontend/typechecker.ml | 164 +++++------- src/lib/reasoners/adt.ml | 7 +- src/lib/reasoners/adt_rel.ml | 8 +- src/lib/reasoners/matching.ml | 20 +- src/lib/reasoners/records.ml | 419 ------------------------------ src/lib/reasoners/records.mli | 37 --- src/lib/reasoners/records_rel.ml | 46 ---- src/lib/reasoners/records_rel.mli | 28 -- src/lib/reasoners/relation.ml | 49 ++-- src/lib/reasoners/shostak.ml | 105 ++------ src/lib/reasoners/shostak.mli | 3 - src/lib/reasoners/theory.ml | 25 +- src/lib/structures/expr.ml | 62 +---- src/lib/structures/expr.mli | 1 - src/lib/structures/symbols.ml | 10 +- src/lib/structures/symbols.mli | 1 - src/lib/structures/ty.ml | 153 ++--------- src/lib/structures/ty.mli | 33 +-- src/lib/structures/typed.ml | 7 +- src/lib/structures/typed.mli | 4 +- src/lib/structures/uid.ml | 4 + src/lib/structures/uid.mli | 1 + 26 files changed, 193 insertions(+), 1194 deletions(-) delete mode 100644 src/lib/reasoners/records.ml delete mode 100644 src/lib/reasoners/records.mli delete mode 100644 src/lib/reasoners/records_rel.ml delete mode 100644 src/lib/reasoners/records_rel.mli diff --git a/src/lib/dune b/src/lib/dune index 3f0c555f7..867448c33 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -51,7 +51,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 Rel_utils Bitlist ; structures diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index be8ba7b11..a48d3506a 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -110,12 +110,18 @@ 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_record lbs ty + let cstr = + match ty with + | Tadt (name, params, true) -> + begin match Ty.type_body name params 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 = diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 751abd6a4..370f28ef5 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -530,86 +530,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. *) - Nest.add_nest [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) -> Nest.add_nest [adt]; let uid = Uid.of_dolmen ty_c in @@ -668,30 +599,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; _ } -> @@ -713,37 +621,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 Nest.add_nest 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 @@ -970,14 +857,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 (Uid.of_dolmen tcst) [] ty - | ty -> - Fmt.failwith "unexpected type %a@." Ty.print ty - end + let ty = dty_to_ty term_ty in + E.mk_constr (Uid.of_dolmen tcst) [] ty | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1018,10 +899,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 @@ -1053,11 +931,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 @@ -1342,20 +1215,9 @@ let rec mk_expr | B.Constructor _, _ -> let ty = dty_to_ty term_ty in - begin match ty with - | Ty.Tadt _ -> - let sy = 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_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 @@ Uid.of_dolmen 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 diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 7b39d1bc6..607f7ed74 100644 --- a/src/lib/frontend/models.ml +++ b/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 -> @@ -159,26 +159,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 || diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 3c8f971e5..f46f1725c 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -68,8 +68,7 @@ module Types = struct let check_number_args loc lty ty = match ty with | Ty.Text (lty', s) - | Ty.Trecord { Ty.args = lty'; name = s; _ } - | Ty.Tadt (s,lty') -> + | Ty.Tadt (s,lty', _) -> if List.length lty <> List.length lty' then Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc; lty' @@ -148,18 +147,16 @@ module Types = struct let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in ty, { env with to_ty = MString.add id ty env.to_ty } | Record (record_constr, lbs) -> + let lbs' = + List.map (fun (x, pp) -> Uid.of_string x, ty_of_pp loc env None pp) lbs + in let lbs = - List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in - let sort_fields = String.equal record_constr "{" in - let record_constr = - if sort_fields then - Uid.of_string @@ Fmt.str "%s___%s" record_constr id - else - Uid.of_string record_constr + List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in + let record_constr = Uid.of_string record_constr in let ty = - Ty.trecord ~sort_fields ~record_constr ty_vars - (Uid.of_string id) (List.map (fun (s, ty) -> Uid.of_string s, ty) lbs) + Ty.t_adt ~record:true ~body:(Some [record_constr, lbs']) + (Uid.of_string id) ty_vars in ty, { to_ty = MString.add id ty env.to_ty; builtins = env.builtins; @@ -197,7 +194,9 @@ module Types = struct in check_duplicates Uid.Set.empty lbs; match ty with - | Ty.Trecord { Ty.lbs = l; _ } -> + | Ty.Tadt (name, params, true) -> + let cases = Ty.type_body name params in + let l = match cases with [{ destrs; _ }] -> destrs | _ -> assert false in if List.length lbs <> List.length l then Errors.typing_error WrongNumberOfLabels loc; List.iter @@ -238,10 +237,7 @@ module Env = struct type profile = { args : Ty.t list; result : Ty.t } type logic_kind = - | RecordConstr - | RecordDestr | AdtConstr - | EnumConstr | AdtDestr | Other @@ -271,7 +267,7 @@ module Env = struct let add_fpa_enum map = let ty = Fpa_rounding.fpa_rounding_mode in match ty with - | Ty.Tadt (name, []) -> + | Ty.Tadt (name, [], _) -> let cases = Ty.type_body name [] in let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in List.fold_left @@ -297,7 +293,7 @@ module Env = struct let find_builtin_cstr ty n = match ty with - | Ty.Tadt (name, []) -> + | Ty.Tadt (name, [], _) -> let cases = Ty.type_body name [] in let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in List.find (Uid.equal n) cstrs @@ -500,20 +496,15 @@ module Env = struct in decl, { env with logics } - let add_constr ~record env constr args_ty ty loc = + let add_constr env constr args_ty ty loc = let pp_profile = PFunction (args_ty, ty) in - let kind = if record then RecordConstr else AdtConstr in - let mk_constr = fun s -> Symbols.constr @@ Uid.of_string s in - add_logics ~kind env mk_constr [constr, ""] pp_profile loc + let mk_constr s = Symbols.constr @@ Uid.of_string s in + add_logics ~kind:AdtConstr env mk_constr [constr, ""] pp_profile loc - let add_destr ~record env destr pur_ty lbl_ty loc = + let add_destr env destr pur_ty lbl_ty loc = let pp_profile = PFunction ([pur_ty], lbl_ty) in - let mk_sy s = - if record then (Symbols.Op (Access (Uid.of_string s))) - else Symbols.destruct (Uid.of_string s) - in - let kind = if record then RecordDestr else AdtDestr in - add_logics ~kind env mk_sy [destr, ""] pp_profile loc + let mk_sy s = Symbols.destruct @@ Uid.of_string s in + add_logics ~kind:AdtDestr env mk_sy [destr, ""] pp_profile loc let find { var_map = m; _ } n = MString.find n m @@ -569,7 +560,7 @@ let type_var_desc env p loc = match Env.fresh_type env p loc with | s, { Env.args = []; result = ty}, - (Env.Other | Env.AdtConstr | Env.EnumConstr) -> + (Env.Other | Env.AdtConstr) -> TTapp (s, []) , ty | _ -> Errors.typing_error (ShouldBeApply p) loc @@ -629,24 +620,12 @@ let check_pattern_matching missing dead loc = let mk_adequate_app p s te_args ty logic_kind = let hp = Hstring.make p in match logic_kind, te_args, ty with - | (Env.AdtConstr | Env.EnumConstr | Env.Other), _, _ -> + | (Env.AdtConstr | Env.Other), _, _ -> (* symbol 's' alreadt contains the information *) TTapp(s, te_args) - | Env.RecordConstr, _, Ty.Trecord { Ty.lbs; _ } -> - let lbs = - try - List.map2 (fun (hs, _) e -> Hstring.make @@ Uid.show hs, e) lbs te_args - with Invalid_argument _ -> assert false - in - TTrecord lbs - - | Env.RecordDestr, [te], _ -> TTdot(te, hp) - | Env.AdtDestr, [te], _ -> TTproject (te, hp) - | Env.RecordDestr, _, _ -> assert false - | Env.RecordConstr, _, _ -> assert false | Env.AdtDestr, _, _ -> assert false let fresh_type_app env p loc = @@ -858,22 +837,6 @@ let rec type_term ?(call_from_type_form=false) env f = Options.tool_req 1 (append_type "TR-Typing-Ite type" ty2); TTite (cond, te2, te3) , ty2 end - | PPdot(t, a) -> - begin - let te = type_term env t in - let ty = Ty.shorten te.c.tt_ty in - match ty with - | Ty.Trecord { Ty.name = g; lbs; _ } -> - begin - try - TTdot(te, Hstring.make a), - Lists.assoc Uid.equal (Uid.of_string a) lbs - with Not_found -> - let g = Uid.show g in - Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc - end - | _ -> Errors.typing_error (ShouldHaveTypeRecord ty) t.pp_loc - end | PPrecord lbs -> begin let lbs = @@ -886,7 +849,11 @@ let rec type_term ?(call_from_type_form=false) env f = let ty = Types.from_labels env.Env.types fake_lbs loc in let ty, _ = Ty.fresh (Ty.shorten ty) Ty.esubst in match ty with - | Ty.Trecord { Ty.lbs=ty_lbs; _ } -> + | Ty.Tadt (name, params, true) -> + let cases = Ty.type_body name params in + let ty_lbs = + match cases with [{ destrs; _ }] -> destrs | _ -> assert false + in begin try let lbs = @@ -895,7 +862,7 @@ let rec type_term ?(call_from_type_form=false) env f = Ty.unify te.c.tt_ty ty_lb; Hstring.make @@ Uid.show lb, te) lbs ty_lbs in - TTrecord(lbs), ty + TTrecord (ty, lbs), ty with Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc end @@ -909,20 +876,22 @@ let rec type_term ?(call_from_type_form=false) env f = (fun (lb, t) -> Hstring.make lb, (type_term env t, t.pp_loc)) lbs in let ty = Ty.shorten te.c.tt_ty in match ty with - | Ty.Trecord { Ty.lbs = ty_lbs; _ } -> + | Ty.Tadt (name, params, true) -> + let cases = Ty.type_body name params in let ty_lbs = - List.map (fun (uid, ty) -> Hstring.make @@ Uid.show uid, ty) ty_lbs + match cases with [{ destrs; _ }] -> destrs | _ -> assert false in let nlbs = List.map (fun (lb, ty_lb) -> + let lb = Hstring.make @@ Uid.show lb in try let v, _ = Hstring.list_assoc lb lbs in Ty.unify ty_lb v.c.tt_ty; lb, v with | Not_found -> - lb, {c = { tt_desc = TTdot(te, lb); tt_ty = ty_lb}; + lb, {c = { tt_desc = TTproject(te, lb); tt_ty = ty_lb}; annot = te.annot } | Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc @@ -930,10 +899,10 @@ let rec type_term ?(call_from_type_form=false) env f = in List.iter (fun (lb, _) -> - try ignore (Hstring.list_assoc lb ty_lbs) + try ignore (Hstring.list_assoc lb nlbs) with Not_found -> Errors.typing_error (NoLabelInType(lb, ty)) loc) lbs; - TTrecord(nlbs), ty + TTrecord (ty, nlbs), ty | _ -> Errors.typing_error ShouldBeARecord loc end | PPlet(l, t2) -> @@ -979,6 +948,28 @@ let rec type_term ?(call_from_type_form=false) env f = | Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc end + | PPdot(t, a) -> + begin + let te = type_term env t in + let ty = Ty.shorten te.c.tt_ty in + match ty with + | Ty.Tadt (name, params, true) -> + let cases = Ty.type_body name params in + let lbs = + match cases with [{ destrs; _ }] -> destrs | _ -> assert false + in + begin + try + let hs = Hstring.make a in + let a = Uid.of_string a in + TTproject (te, hs), Uid.list_assoc a lbs + with Not_found -> + let g = Uid.show name in + Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc + end + | _ -> Errors.typing_error (ShouldHaveTypeRecord ty) t.pp_loc + end + | PPproject (t, lbl) -> let te = type_term env t in begin @@ -988,9 +979,6 @@ let rec type_term ?(call_from_type_form=false) env f = Ty.unify te.c.tt_ty arg; TTproject (te, Hstring.make lbl), Ty.shorten result - | _, {Env.args = [arg] ; result}, Env.RecordDestr -> - Ty.unify te.c.tt_ty arg; - TTdot (te, Hstring.make lbl), Ty.shorten result | _ -> assert false with Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc @@ -1001,9 +989,8 @@ let rec type_term ?(call_from_type_form=false) env f = let e = type_term env e in let ty = Ty.shorten e.c.tt_ty in let ty_body = match ty with - | Ty.Tadt (name, params) -> Ty.type_body name params - | Ty.Trecord { Ty.record_constr; lbs; _ } -> - [{Ty.constr = record_constr; destrs = lbs}] + | Ty.Tadt (name, params, _) -> + Ty.type_body name params | _ -> Errors.typing_error (ShouldBeADT ty) loc in let pats = @@ -1268,20 +1255,8 @@ and type_form ?(in_theory=false) env f = let top = TTisConstr (tt, Hstring.make lbl) in let r = TFatom { c = top; annot = new_id () } in r - | Env.EnumConstr -> - let tt_desc, tt_ty = type_var_desc env lbl f.pp_loc in - let rhs = { c = { tt_desc; tt_ty }; annot = new_id () } in - TFatom (mk_ta_eq tt rhs) | _ -> - begin match result with - | 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. *) - TFatom { c = TAtrue; annot = new_id () } - | _ -> - Errors.typing_error (NotAdtConstr (lbl, result)) f.pp_loc - end + Errors.typing_error (NotAdtConstr (lbl, result)) f.pp_loc with Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) f.pp_loc end @@ -1407,10 +1382,7 @@ and type_form ?(in_theory=false) env f = let e = type_term env e in let ty = e.c.tt_ty in let ty_body = match ty with - | Ty.Tadt (name, params) -> Ty.type_body name params - | Ty.Trecord { Ty.record_constr; lbs; _ } -> - [{Ty.constr = record_constr ; destrs = lbs}] - + | Ty.Tadt (name, params, _) -> Ty.type_body name params | _ -> Errors.typing_error (ShouldBeADT ty) f.pp_loc in @@ -2095,10 +2067,8 @@ let rec mono_term {c = {tt_ty=tt_ty; tt_desc=tt_desc}; annot = id} = TTextract(mono_term t1, i, j) | TTconcat (t1,t2)-> TTconcat (mono_term t1, mono_term t2) - | TTdot (t1, a) -> - TTdot (mono_term t1, a) - | TTrecord lbs -> - TTrecord (List.map (fun (x, t) -> x, mono_term t) lbs) + | TTrecord (ty, lbs) -> + TTrecord (ty, List.map (fun (x, t) -> x, mono_term t) lbs) | TTlet (l,t2)-> let l = List.rev_map (fun (x, t1) -> x, mono_term t1) (List.rev l) in TTlet (l, mono_term t2) @@ -2351,7 +2321,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = let tlogic, env = (* can also use List.fold Env.add_constr *) let constr = fun s -> Symbols.constr @@ Uid.of_string s in - Env.add_logics ~kind:Env.EnumConstr env constr lcl ty loc + Env.add_logics ~kind:Env.AdtConstr env constr lcl ty loc in let td2_a = { c = TLogic(loc, lc, tlogic); annot=new_id () } in (td2_a,env)::acc, env @@ -2367,14 +2337,14 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = else let args_ty = List.map snd lrec in let tlogic, env = - Env.add_constr ~record:true env constr args_ty pur_ty loc + Env.add_constr env constr args_ty pur_ty loc in ({c = TLogic(loc, [constr], tlogic); annot=new_id ()}, env)::acc, env in List.fold_left (* register fields *) (fun (acc, env) (lbl, ty_lbl) -> let tlogic, env = - Env.add_destr ~record:true env lbl pur_ty ty_lbl loc + Env.add_destr env lbl pur_ty ty_lbl loc in ({c = TLogic(loc, [lbl], tlogic); annot=new_id ()}, env) :: acc, env )(acc, env) lrec @@ -2384,7 +2354,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = (fun (acc, env) (cstr, lbl_args_ty) -> let args_ty = List.map snd lbl_args_ty in let tty, env = - Env.add_constr ~record:false env cstr args_ty pur_ty loc + Env.add_constr env cstr args_ty pur_ty loc in let acc = ({c = TLogic(loc, [cstr], tty); annot=new_id ()}, env) :: acc @@ -2392,7 +2362,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = List.fold_left (* register destructors *) (fun (acc, env) (lbl, ty_lbl) -> let tty, env = - Env.add_destr ~record:false env lbl pur_ty ty_lbl loc + Env.add_destr env lbl pur_ty ty_lbl loc in ({c = TLogic(loc, [lbl], tty); annot=new_id ()}, env) :: acc, env )(acc, env) lbl_args_ty diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 834ea2ce3..381238570 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -54,7 +54,7 @@ let constr_of_destr ty dest = ~module_name:"Adt" ~function_name:"constr_of_destr" "ty = %a" Ty.print ty; match ty with - | Ty.Tadt (s, params) -> + | Ty.Tadt (s, params, _) -> begin let cases = Ty.type_body s params in try @@ -173,7 +173,7 @@ module Shostak (X : ALIEN) = struct in let xs = List.rev sx in match f, xs, ty with - | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) -> + | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false @@ -194,9 +194,6 @@ module Shostak (X : ALIEN) = struct else sel_x, ctx (* canonization OK *) *) - | Sy.Op Sy.Constr _, _, Ty.Trecord _ -> - Fmt.failwith "unexpected record constructor %a@." E.print t - | _ -> assert false let hash x = diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 18eb871b3..eb0c465ac 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -83,7 +83,7 @@ module Domain = struct let unknown ty = match ty with - | Ty.Tadt (name, params) -> + | Ty.Tadt (name, params, _) -> (* Return the list of all the constructors of the type of [r]. *) let cases = Ty.type_body name params in let constrs = @@ -168,7 +168,7 @@ module Domains = struct contains the type of constructor and in particular its arity. *) let is_enum_cstr r c = match X.type_info r with - | Tadt (name, args) -> + | Tadt (name, args, _) -> let cases = Ty.type_body name args in Lists.is_empty @@ Ty.assoc_destrs c cases | _ -> assert false @@ -492,7 +492,7 @@ let build_constr_eq r c = match Th.embed r with | Alien r -> begin match X.type_info r with - | Ty.Tadt (name, params) as ty -> + | Ty.Tadt (name, params, _) as ty -> let cases = Ty.type_body name params in let ds = try Ty.assoc_destrs c cases with Not_found -> assert false @@ -593,7 +593,7 @@ let two = Numbers.Q.from_int 2 (* TODO: we should compute this reverse map in `Ty` and store it there. *) let constr_of_destr ty d = match ty with - | Ty.Tadt (name, params) -> + | Ty.Tadt (name, params, _) -> begin let cases = Ty.type_body name params in try diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 101c9d251..54968e67a 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -311,11 +311,11 @@ module Make (X : Arg) : S with type theory = X.t = struct | _ , [] -> l1 | _ -> List.fold_left (fun acc e -> e :: acc) l2 (List.rev l1) - let xs_modulo_records t { Ty.lbs; _ } = - List.rev + (* let xs_modulo_records t { Ty.lbs; _ } = + List.rev (List.rev_map (fun (hs, ty) -> - E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) + E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) *) module SLE = (* sets of lists of terms *) Set.Make(struct @@ -410,13 +410,13 @@ module Make (X : Arg) : S with type theory = X.t = struct (fun t l -> let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in if Symbols.compare f_pat f = 0 then xs::l - else - begin - match f_pat, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord record -> - (xs_modulo_records t record) :: l - | _ -> l - end + else l + (* begin + match f_pat, ty with + | Symbols.Op (Symbols.Record), Ty.Trecord record -> + (xs_modulo_records t record) :: l + | _ -> l + end *) ) cl [] in let cl = filter_classes mconf cl tbox in diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml deleted file mode 100644 index e5d354e2a..000000000 --- a/src/lib/reasoners/records.ml +++ /dev/null @@ -1,419 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -module E = Expr -module Sy = Symbols - -type 'a abstract = - | Record of (Uid.t * 'a abstract) list * Ty.t - | Access of Uid.t * 'a abstract * Ty.t - | Other of 'a * Ty.t - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Shostak (X : ALIEN) = struct - - module XS = Set.Make(struct type t = X.r let compare = X.hash_cmp end) - - let name = "records" - - let timer = Timers.M_Records - - type t = X.r abstract - type r = X.r - - (*BISECT-IGNORE-BEGIN*) - module Debug = struct - - let rec print fmt = function - | Record (lbs, _) -> - Format.fprintf fmt "{"; - let _ = List.fold_left - (fun first (lb, e) -> - Format.fprintf fmt "%s%a = %a" - (if first then "" else "; ") Uid.pp lb print e; - false - ) true lbs in - Format.fprintf fmt "}" - | Access(a, e, _) -> - Format.fprintf fmt "%a.%a" print e Uid.pp a - | Other(t, _) -> X.print fmt t - - end - (*BISECT-IGNORE-END*) - - let print = Debug.print - - let rec raw_compare r1 r2 = - match r1, r2 with - | Other (u1, ty1), Other (u2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c else X.str_cmp u1 u2 - | Other _, _ -> -1 - | _, Other _ -> 1 - | Access (s1, u1, ty1), Access (s2, u2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c - else - let c = Uid.compare s1 s2 in - if c <> 0 then c - else raw_compare u1 u2 - | Access _, _ -> -1 - | _, Access _ -> 1 - | Record (lbs1, ty1), Record (lbs2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c else raw_compare_list lbs1 lbs2 - - and raw_compare_list l1 l2 = - match l1, l2 with - | [], [] -> 0 - | [], _ -> 1 - | _, [] -> -1 - | (_, x1)::l1, (_, x2)::l2 -> - let c = raw_compare x1 x2 in - if c<>0 then c else raw_compare_list l1 l2 - - let rec normalize v = - match v with - | Record (lbs, ty) -> - begin - let lbs_n = List.map (fun (lb, x) -> lb, normalize x) lbs in - match lbs_n with - | (lb1, Access(lb2, x, _)) :: l when Uid.equal lb1 lb2 -> - if List.for_all - (function - | (lb1, Access(lb2, y, _)) -> - Uid.equal lb1 lb2 && raw_compare x y = 0 - | _ -> false) l - then x - else Record (lbs_n, ty) - | _ -> Record (lbs_n, ty) - end - | Access (a, x, ty) -> - begin - match normalize x with - | Record (lbs, _) -> Lists.assoc Uid.equal a lbs - | x_n -> Access (a, x_n, ty) - end - | Other _ -> v - - let embed r = - match X.extract r with - | Some p -> p - | None -> Other(r, X.type_info r) - - let compare_mine t u = raw_compare (normalize t) (normalize u) - - let compare x y = compare_mine (embed x) (embed y) - - let rec equal r1 r2 = - match r1, r2 with - | Other (u1, ty1), Other (u2, ty2) -> - Ty.equal ty1 ty2 && X.equal u1 u2 - - | Access (s1, u1, ty1), Access (s2, u2, ty2) -> - Uid.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2 - - | Record (lbs1, ty1), Record (lbs2, ty2) -> - Ty.equal ty1 ty2 && equal_list lbs1 lbs2 - - | Other _, _ | _, Other _ | Access _, _ | _, Access _ -> false - - and equal_list l1 l2 = - try List.for_all2 (fun (_,r1) (_,r2) -> equal r1 r2) l1 l2 - with Invalid_argument _ -> false - - let is_mine t = - match normalize t with - | Other(r, _) -> r - | x -> X.embed x - - let type_info = function - | Record (_, ty) | Access (_, _, ty) | Other (_, ty) -> ty - - let make t = - let rec make_rec t ctx = - let { E.f; xs; ty; _ } = E.term_view t in - match f, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord { Ty.lbs; _ } -> - assert (List.length xs = List.length lbs); - let l, ctx = - List.fold_right2 - (fun x (lb, _) (l, ctx) -> - let r, ctx = make_rec x ctx in - let tyr = type_info r in - let dlb = E.mk_term (Symbols.Op (Symbols.Access lb)) [t] tyr in - let c = E.mk_eq ~iff:false dlb x in - (lb, r)::l, c::ctx - ) - xs lbs ([], ctx) - in - Record (l, ty), ctx - | Symbols.Op (Symbols.Access a), _ -> - begin - match xs with - | [x] -> - let r, ctx = make_rec x ctx in - Access (a, r, ty), ctx - | _ -> assert false - end - - | _, _ -> - let r, ctx' = X.make t in - Other (r, ty), ctx'@ctx - in - let r, ctx = make_rec t [] in - let is_m = is_mine r in - is_m, ctx - - let color _ = assert false - - let embed r = - match X.extract r with - | Some p -> p - | None -> Other(r, X.type_info r) - - let xs_of_list = List.fold_left (fun s x -> XS.add x s) XS.empty - - let leaves t = - let rec leaves t = - match normalize t with - | Record (lbs, _) -> - List.fold_left (fun s (_, x) -> XS.union (leaves x) s) XS.empty lbs - | Access (_, x, _) -> leaves x - | Other (x, _) -> xs_of_list (X.leaves x) - in - XS.elements (leaves t) - - let is_constant = - let rec is_constant t = - match normalize t with - | Record (lbs, _) -> - List.for_all (fun (_, x) -> is_constant x) lbs - | Access (_, x, _) -> is_constant x - | Other (x, _) -> X.is_constant x - in is_constant - - let rec hash = function - | Record (lbs, ty) -> - List.fold_left - (fun h (lb, x) -> 17 * hash x + 13 * Uid.hash lb + h) - (Ty.hash ty) lbs - | Access (a, x, ty) -> - 19 * hash x + 17 * Uid.hash a + Ty.hash ty - | Other (x, ty) -> - Ty.hash ty + 23 * X.hash x - - let rec subst_rec p v r = - match r with - | Other (t, _) -> - embed (if X.equal p t then v else X.subst p v t) - | Access (a, t, ty) -> - Access (a, subst_rec p v t, ty) - | Record (lbs, ty) -> - let lbs = List.map (fun (lb, t) -> lb, subst_rec p v t) lbs in - Record (lbs, ty) - - let subst p v r = is_mine (subst_rec p v r) - - let is_mine_symb sy = - match sy with - | Symbols.Op (Symbols.Record | Symbols.Access _) -> true - | _ -> false - - let abstract_access field e ty acc = - let xe = is_mine e in - let abs_right_xe, acc = - try Lists.assoc X.equal xe acc, acc - with Not_found -> - let left_abs_xe2, acc = X.abstract_selectors xe acc in - match X.type_info left_abs_xe2 with - | (Ty.Trecord { Ty.lbs; _ }) as tyr -> - let flds = - List.map - (fun (lb,ty) -> lb, embed (X.term_embed (E.fresh_name ty))) lbs - in - let record = is_mine (Record (flds, tyr)) in - record, (left_abs_xe2, record) :: acc - | ty -> - Fmt.failwith - "Not a record type: `%a" Ty.print_full ty - in - let abs_access = normalize (Access (field, embed abs_right_xe, ty)) in - is_mine abs_access, acc - - let abstract_selectors v acc = - match v with - (* Handled by combine. Should not happen! *) - | Other _ -> assert false - - (* This is not a selector *) - | Record (fields,ty) -> - let flds, acc = - List.fold_left - (fun (flds,acc) (lbl,e) -> - let e, acc = X.abstract_selectors (is_mine e) acc in - (lbl, embed e)::flds, acc - )([], acc) fields - [@ocaml.ppwarning "TODO: should not rebuild if not changed !"] - in - is_mine (Record (List.rev flds, ty)), acc - - (* Selector ! Interesting case !*) - | Access (field, e, ty) -> abstract_access field e ty acc - - - (* Shostak'pair solver adapted to records *) - - (* unused -- - let mk_fresh_record x info = - let ty = type_info x in - let lbs = match ty with Ty.Trecord r -> r.Ty.lbs | _ -> assert false in - let lbs = - List.map - (fun (lb, ty) -> - match info with - | Some (a, v) when Uid.equal lb a -> lb, v - | _ -> let n = embed (X.term_embed (E.fresh_name ty)) in lb, n) - lbs - in - Record (lbs, ty), lbs - *) - - (* unused -- - let rec occurs x = function - | Record (lbs, _) -> - List.exists (fun (_, v) -> occurs x v) lbs - | Access (_, v, _) -> occurs x v - | Other _ as v -> compare_mine x v = 0 (* XXX *) - *) - - (* unused -- - let rec subst_access x s e = - match e with - | Record (lbs, ty) -> - Record (List.map (fun (n,e') -> n, subst_access x s e') lbs, ty) - | Access (lb, e', _) when compare_mine x e' = 0 -> - Lists.assoc Uid.equal lb s - | Access (lb', e', ty) -> Access (lb', subst_access x s e', ty) - | Other _ -> e - *) - - let fully_interpreted = is_mine_symb - - let rec term_extract r = - match X.extract r with - | Some v -> begin match v with - | Record (lbs, ty) -> - begin - try - let lbs = - List.map - (fun (_, r) -> - match term_extract (is_mine r) with - | None, _ -> raise Not_found - | Some t, _ -> t) - lbs - in - Some (E.mk_term (Symbols.Op Symbols.Record) lbs ty), false - with Not_found -> None, false - end - | Access (a, r, ty) -> - begin - match X.term_extract (is_mine r) with - | None, _ -> None, false - | Some t, _ -> - Some (E.mk_term (Symbols.Op (Symbols.Access a)) [t] ty), false - end - | Other (r, _) -> X.term_extract r - end - | None -> X.term_extract r - - - let orient_solved p v pb = - if Lists.mem X.equal p (X.leaves v) then raise Util.Unsolvable; - Sig.{ pb with sbt = (p,v) :: pb.sbt } - - let solve r1 r2 (pb : _ Sig.solve_pb) = - match embed r1, embed r2 with - | Record (l1, _), Record (l2, _) -> - let eqs = - List.fold_left2 - (fun eqs (a,b) (x,y) -> - assert (Uid.compare a x = 0); - (is_mine y, is_mine b) :: eqs - )pb.eqs l1 l2 - in - {pb with eqs=eqs} - - | Other _, Other _ -> - if X.str_cmp r1 r2 > 0 then { pb with sbt = (r1,r2)::pb.sbt } - else { pb with sbt = (r2,r1)::pb.sbt } - - | Other _, Record _ -> orient_solved r1 r2 pb - | Record _, Other _ -> orient_solved r2 r1 pb - | Access _ , _ -> assert false - | _ , Access _ -> assert false - - let assign_value t _ eq = - match embed t with - | Access _ -> None - - | Record (_, ty) -> - if List.exists (fun (t,_) -> Expr.is_model_term t) eq - then None - else Some (Expr.fresh_name ty, false) - - | Other (_,ty) -> - match ty with - | Ty.Trecord { Ty.lbs; _ } -> - let rev_lbs = List.rev_map (fun (_, ty) -> Expr.fresh_name ty) lbs in - let s = E.mk_term (Symbols.Op Symbols.Record) (List.rev rev_lbs) ty in - Some (s, false) (* false <-> not a case-split *) - | _ -> assert false - - let to_model_term = - let rec to_model_term r = - match r with - | Record (fields, ty) -> - (* We can ignore the names of fields as they are inlined in the - type [ty] of the record. *) - let l = - Lists.try_map (fun (_name, rf) -> to_model_term rf) fields - in - Option.bind l @@ fun l -> - Some (E.mk_term Sy.(Op Record) l ty) - - | Other (a, _) -> - X.to_model_term a - | Access _ -> None - in fun r -> to_model_term (embed r) -end diff --git a/src/lib/reasoners/records.mli b/src/lib/reasoners/records.mli deleted file mode 100644 index 77451e0f0..000000000 --- a/src/lib/reasoners/records.mli +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type 'a abstract - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Shostak - (X : ALIEN) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml deleted file mode 100644 index 7951d9085..000000000 --- a/src/lib/reasoners/records_rel.ml +++ /dev/null @@ -1,46 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type t = unit - -let timer = Timers.M_Records - -let empty uf = (), Uf.domains uf -let assume _ uf _ = - (), Uf.domains uf, { Sig_rel.assume = []; remove = [] } -let query _ _ _ = None -let case_split _env _uf ~for_model:_ = [] -let optimizing_objective _env _uf _o = None -let add env uf _ _ = env, Uf.domains uf, [] -let new_terms _ = Expr.Set.empty -let instantiate ~do_syntactic_matching:_ _ env _ _ = env, [] - -let assume_th_elt t th_elt _ = - match th_elt.Expr.extends with - | Util.Records -> - failwith "This Theory does not support theories extension" - | _ -> t diff --git a/src/lib/reasoners/records_rel.mli b/src/lib/reasoners/records_rel.mli deleted file mode 100644 index 71cfa717c..000000000 --- a/src/lib/reasoners/records_rel.mli +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -include Sig_rel.RELATION diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index 12971f1ce..26ca532fd 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -31,15 +31,13 @@ module X = Shostak.Combine module Rel1 : Sig_rel.RELATION = IntervalCalculus -module Rel2 : Sig_rel.RELATION = Records_rel +module Rel2 : Sig_rel.RELATION = Bitv_rel -module Rel3 : Sig_rel.RELATION = Bitv_rel +module Rel3 : Sig_rel.RELATION = Arrays_rel -module Rel4 : Sig_rel.RELATION = Arrays_rel +module Rel4 : Sig_rel.RELATION = Adt_rel -module Rel5 : Sig_rel.RELATION = Adt_rel - -module Rel6 : Sig_rel.RELATION = Ite_rel +module Rel5 : Sig_rel.RELATION = Ite_rel (* This value is unused. *) let timer = Timers.M_None @@ -50,7 +48,6 @@ type t = { r3: Rel3.t; r4: Rel4.t; r5: Rel5.t; - r6: Rel6.t; } let empty uf = @@ -59,8 +56,7 @@ let empty uf = let r3, doms3 = Rel3.empty (Uf.set_domains uf doms2) in let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in - let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in - {r1; r2; r3; r4; r5; r6}, doms6 + {r1; r2; r3; r4; r5}, doms5 let (|@|) l1 l2 = if l1 == [] then l2 @@ -89,14 +85,10 @@ let assume env uf sa = Timers.with_timer Rel5.timer Timers.F_assume @@ fun () -> Rel5.assume env.r5 (Uf.set_domains uf doms4) sa in - let env6, doms6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) = - Timers.with_timer Rel6.timer Timers.F_assume @@ fun () -> - Rel6.assume env.r6 (Uf.set_domains uf doms5) sa - in - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6}, - doms6, - ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6; - remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 } + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5}, + doms5, + ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5; + remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 } : _ Sig_rel.result) let assume_th_elt env th_elt dep = @@ -106,8 +98,7 @@ let assume_th_elt env th_elt dep = let env3 = Rel3.assume_th_elt env.r3 th_elt dep in let env4 = Rel4.assume_th_elt env.r4 th_elt dep in let env5 = Rel5.assume_th_elt env.r5 th_elt dep in - let env6 = Rel6.assume_th_elt env.r6 th_elt dep in - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6} + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5} let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a k = @@ -122,8 +113,7 @@ let query env uf a = try_query (module Rel2) env.r2 uf a @@ fun () -> try_query (module Rel3) env.r3 uf a @@ fun () -> try_query (module Rel4) env.r4 uf a @@ fun () -> - try_query (module Rel5) env.r5 uf a @@ fun () -> - try_query (module Rel6) env.r6 uf a @@ fun () -> None + try_query (module Rel5) env.r5 uf a @@ fun () -> None let case_split env uf ~for_model = Options.exec_thread_yield (); @@ -132,8 +122,7 @@ let case_split env uf ~for_model = let seq3 = Rel3.case_split env.r3 uf ~for_model in let seq4 = Rel4.case_split env.r4 uf ~for_model in let seq5 = Rel5.case_split env.r5 uf ~for_model in - let seq6 = Rel6.case_split env.r6 uf ~for_model in - let splits = [seq1; seq2; seq3; seq4; seq5; seq6] in + let splits = [seq1; seq2; seq3; seq4; seq5] in let splits = List.fold_left (|@|) [] splits in List.fast_sort (fun (_ ,_ , sz1) (_ ,_ , sz2) -> @@ -158,8 +147,7 @@ let optimizing_objective env uf o = Rel1.optimizing_objective env.r1 uf; Rel2.optimizing_objective env.r2 uf; Rel3.optimizing_objective env.r3 uf; - Rel4.optimizing_objective env.r4 uf; - Rel5.optimizing_objective env.r5 uf + Rel4.optimizing_objective env.r4 uf ] let add env uf r t = @@ -169,9 +157,7 @@ let add env uf r t = let r3, doms3, eqs3 =Rel3.add env.r3 (Uf.set_domains uf doms2) r t in let r4, doms4, eqs4 =Rel4.add env.r4 (Uf.set_domains uf doms3) r t in let r5, doms5, eqs5 =Rel5.add env.r5 (Uf.set_domains uf doms4) r t in - let r6, doms6, eqs6 =Rel6.add env.r6 (Uf.set_domains uf doms5) r t in - {r1;r2;r3;r4;r5;r6}, doms6, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6 - + {r1;r2;r3;r4;r5}, doms5, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5 let instantiate ~do_syntactic_matching t_match env uf selector = Options.exec_thread_yield (); @@ -185,10 +171,8 @@ let instantiate ~do_syntactic_matching t_match env uf selector = Rel4.instantiate ~do_syntactic_matching t_match env.r4 uf selector in let r5, l5 = Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in - let r6, l6 = - Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector in - {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6}, - l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1 + {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5}, + l5 |@| l4 |@| l3 |@| l2 |@| l1 let new_terms env = Rel1.new_terms env.r1 @@ -196,4 +180,3 @@ let new_terms env = |> Expr.Set.union @@ Rel3.new_terms env.r3 |> Expr.Set.union @@ Rel4.new_terms env.r4 |> Expr.Set.union @@ Rel5.new_terms env.r5 - |> Expr.Set.union @@ Rel6.new_terms env.r6 diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 971c215cd..e48282de4 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -37,14 +37,11 @@ module rec CX : sig val extract1 : r -> ARITH.t option val embed1 : ARITH.t -> r - val extract2 : r -> RECORDS.t option - val embed2 : RECORDS.t -> r + val extract2 : r -> BITV.t option + val embed2 : BITV.t -> r - val extract3 : r -> BITV.t option - val embed3 : BITV.t -> r - - val extract4 : r -> ADT.t option - val embed4 : ADT.t -> r + val extract3 : r -> ADT.t option + val embed3 : ADT.t -> r end = struct @@ -53,7 +50,6 @@ struct | Term of Expr.t | Ac of AC.t | Arith of ARITH.t - | Records of RECORDS.t | Bitv of BITV.t | Adt of ADT.t @@ -68,7 +64,6 @@ struct if Options.get_term_like_pp () then begin match r.v with | Arith t -> fprintf fmt "%a" ARITH.print t - | Records t -> fprintf fmt "%a" RECORDS.print t | Bitv t -> fprintf fmt "%a" BITV.print t | Adt t -> fprintf fmt "%a" ADT.print t | Term t -> fprintf fmt "%a" Expr.print t @@ -78,8 +73,6 @@ struct match r.v with | Arith t -> fprintf fmt "Arith(%s):[%a]" ARITH.name ARITH.print t - | Records t -> - fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t | Bitv t -> fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t | Adt t -> @@ -161,7 +154,6 @@ struct let hash r = let res = match r.v with | Arith x -> 1 + 10 * ARITH.hash x - | Records x -> 2 + 10 * RECORDS.hash x | Bitv x -> 3 + 10 * BITV.hash x | Adt x -> 6 + 10 * ADT.hash x | Ac ac -> 9 + 10 * AC.hash ac @@ -172,7 +164,6 @@ struct let eq r1 r2 = match r1.v, r2.v with | Arith x, Arith y -> ARITH.equal x y - | Records x, Records y -> RECORDS.equal x y | Bitv x, Bitv y -> BITV.equal x y | Adt x, Adt y -> ADT.equal x y | Term x, Term y -> Expr.equal x y @@ -198,9 +189,8 @@ struct (* end: Hconsing modules and functions *) let embed1 x = hcons {v = Arith x; id = -1000 (* dummy *)} - let embed2 x = hcons {v = Records x; id = -1000 (* dummy *)} - let embed3 x = hcons {v = Bitv x; id = -1000 (* dummy *)} - let embed4 x = hcons {v = Adt x; id = -1000 (* dummy *)} + let embed2 x = hcons {v = Bitv x; id = -1000 (* dummy *)} + let embed3 x = hcons {v = Adt x; id = -1000 (* dummy *)} let ac_embed ({ Sig.l; _ } as t) = match l with @@ -215,9 +205,8 @@ struct let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)} let extract1 = function { v=Arith r; _ } -> Some r | _ -> None - let extract2 = function { v=Records r; _ } -> Some r | _ -> None - let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None - let extract4 = function { v=Adt r; _ } -> Some r | _ -> None + let extract2 = function { v=Bitv r; _ } -> Some r | _ -> None + let extract3 = function { v=Adt r; _ } -> Some r | _ -> None let ac_extract = function | { v = Ac t; _ } -> Some t @@ -226,7 +215,6 @@ struct let term_extract r = match r.v with | Arith _ -> ARITH.term_extract r - | Records _ -> RECORDS.term_extract r | Bitv _ -> BITV.term_extract r | Adt _ -> ADT.term_extract r | Ac _ -> None, false (* SYLVAIN : TODO *) @@ -236,7 +224,6 @@ struct let res = match r.v with | Arith _ -> ARITH.to_model_term r - | Records _ -> RECORDS.to_model_term r | Bitv _ -> BITV.to_model_term r | Adt _ -> ADT.to_model_term r | Term t when Expr.is_model_term t -> Some t @@ -251,7 +238,6 @@ struct let type_info = function | { v = Arith t; _ } -> ARITH.type_info t - | { v = Records t; _ } -> RECORDS.type_info t | { v = Bitv t; _ } -> BITV.type_info t | { v = Adt t; _ } -> ADT.type_info t | { v = Ac x; _ } -> AC.type_info x @@ -263,9 +249,8 @@ struct | Ac _ -> -1 | Term _ -> -2 | Arith _ -> -3 - | Records _ -> -4 - | Bitv _ -> -5 - | Adt _ -> -7 + | Bitv _ -> -4 + | Adt _ -> -5 let compare_tag a b = theory_num a - theory_num b @@ -274,7 +259,6 @@ struct else match a.v, b.v with | Arith _, Arith _ -> ARITH.compare a b - | Records _, Records _ -> RECORDS.compare a b | Bitv _, Bitv _ -> BITV.compare a b | Adt _, Adt _ -> ADT.compare a b | Term x, Term y -> Expr.compare x y @@ -289,7 +273,6 @@ struct | Term t -> Expr.hash t | Ac x -> AC.hash x | Arith x -> ARITH.hash x - | Records x -> RECORDS.hash x | Bitv x -> BITV.hash x | Arrays x -> ARRAYS.hash x | Adt x -> ADT.hash x @@ -318,7 +301,6 @@ struct let leaves r = match r.v with | Arith t -> ARITH.leaves t - | Records t -> RECORDS.leaves t | Bitv t -> BITV.leaves t | Adt t -> ADT.leaves t | Ac t -> r :: (AC.leaves t) @@ -327,7 +309,6 @@ struct let is_constant r = match r.v with | Arith t -> ARITH.is_constant t - | Records t -> RECORDS.is_constant t | Bitv t -> BITV.is_constant t | Adt t -> ADT.is_constant t | Term t -> @@ -344,7 +325,6 @@ struct if equal p v then r else match r.v with | Arith t -> ARITH.subst p v t - | Records t -> RECORDS.subst p v t | Bitv t -> BITV.subst p v t | Adt t -> ADT.subst p v t | Ac t -> if equal p r then v else AC.subst p v t @@ -355,32 +335,27 @@ struct let not_restricted = not @@ Options.get_restricted () in match ARITH.is_mine_symb sb, - not_restricted && RECORDS.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, AC.is_mine_symb sb with - | true, false, false, false, false -> + | true, false, false, false -> Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () -> ARITH.make t - | false, true, false, false, false -> - Timers.with_timer Timers.M_Records Timers.F_make @@ fun () -> - RECORDS.make t - - | false, false, true, false, false -> + | false, true, false, false -> Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () -> BITV.make t - | false, false, false, true, false -> + | false, false, true, false -> Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () -> ADT.make t - | false, false, false, false, true -> + | false, false, false, true -> Timers.with_timer Timers.M_AC Timers.F_make @@ fun () -> AC.make t - | false, false, false, false, false -> + | false, false, false, false -> term_embed t, [] | _ -> assert false @@ -389,30 +364,26 @@ struct let not_restricted = not @@ Options.get_restricted () in match ARITH.is_mine_symb sb, - not_restricted && RECORDS.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, AC.is_mine_symb sb with - | true, false, false, false, false -> + | true, false, false, false -> ARITH.fully_interpreted sb - | false, true, false, false, false -> - RECORDS.fully_interpreted sb - | false, false, true, false, false -> + | false, true, false, false -> BITV.fully_interpreted sb - | false, false, false, true, false -> + | false, false, true, false -> ADT.fully_interpreted sb - | false, false, false, false, true -> + | false, false, false, true -> AC.fully_interpreted sb - | false, false, false, false, false -> + | false, false, false, false -> false | _ -> assert false let is_solvable_theory_symbol sb = ARITH.is_mine_symb sb || not (Options.get_restricted ()) && - (RECORDS.is_mine_symb sb || - BITV.is_mine_symb sb || + (BITV.is_mine_symb sb|| ADT.is_mine_symb sb) let is_a_leaf r = match r.v with @@ -426,18 +397,15 @@ struct | _ -> match ARITH.is_mine_symb ac.Sig.h, - RECORDS.is_mine_symb ac.Sig.h, BITV.is_mine_symb ac.Sig.h, ADT.is_mine_symb ac.Sig.h, AC.is_mine_symb ac.Sig.h with (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *) - | true, false, false, false, false -> + | true, false, false, false -> ARITH.color ac - | false, true, false, false, false -> - RECORDS.color ac - | false, false, true, false, false -> + | false, true, false, false -> BITV.color ac - | false, false, false, true, false -> + | false, false, true, false -> ADT.color ac | _ -> ac_embed ac @@ -445,7 +413,6 @@ struct Debug.debug_abstract_selectors a; match a.v with | Arith a -> ARITH.abstract_selectors a acc - | Records a -> RECORDS.abstract_selectors a acc | Bitv a -> BITV.abstract_selectors a acc | Adt a -> ADT.abstract_selectors a acc | Term _ -> a, acc @@ -527,10 +494,6 @@ struct Timers.with_timer ARITH.timer Timers.F_solve @@ fun () -> ARITH.solve ra rb pb - | Ty.Trecord _ -> - Timers.with_timer RECORDS.timer Timers.F_solve @@ fun () -> - RECORDS.solve ra rb pb - | Ty.Tbitv _ -> Timers.with_timer BITV.timer Timers.F_solve @@ fun () -> BITV.solve ra rb pb @@ -577,7 +540,6 @@ struct let opt = match r.v, type_info r with | _, Ty.Tint | _, Ty.Treal -> ARITH.assign_value r distincts eq - | _, Ty.Trecord _ -> RECORDS.assign_value r distincts eq | _, Ty.Tbitv _ -> BITV.assign_value r distincts eq | Term t, Ty.Tfarray _ -> begin @@ -642,24 +604,14 @@ and ARITH : Sig.SHOSTAK let embed = CX.embed1 end) -and RECORDS : Sig.SHOSTAK - with type r = CX.r - and type t = CX.r Records.abstract = - Records.Shostak - (struct - include CX - let extract = extract2 - let embed = embed2 - end) - and BITV : Sig.SHOSTAK with type r = CX.r and type t = CX.r Bitv.abstract = Bitv.Shostak (struct include CX - let extract = extract3 - let embed = embed3 + let extract = extract2 + let embed = embed2 end) and ADT : Sig.SHOSTAK @@ -668,8 +620,8 @@ and ADT : Sig.SHOSTAK Adt.Shostak (struct include CX - let extract = extract4 - let embed = embed4 + let extract = extract3 + let embed = embed3 end) (* Its signature is not Sig.SHOSTAK because it does not provide a solver *) @@ -708,7 +660,6 @@ module Combine = struct end module Arith = ARITH -module Records = RECORDS module Bitv = BITV module Adt = ADT module Polynome = TARITH diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index 0067e7df9..a44cfba6b 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -38,9 +38,6 @@ module Polynome : Polynome.T module Arith : Sig.SHOSTAK with type r = Combine.r and type t = Polynome.t -module Records : Sig.SHOSTAK - with type r = Combine.r and type t = Combine.r Records.abstract - module Bitv : Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Bitv.abstract diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index c490ed23a..fd0914218 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -159,21 +159,16 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> mp | Tvar _ -> assert false - | Text (_, hs) | Trecord { name = hs; _ } when - Uid.Map.mem hs mp -> mp + | Text (_, hs) when Uid.Map.mem hs mp -> mp | Text (l, hs) -> let l = List.map (fun _ -> Ty.fresh_tvar()) l in Uid.Map.add hs (Text(l, hs)) mp - | Trecord { name; _ } -> - (* cannot do better for records ? *) - Uid.Map.add name ty mp - - | Tadt (hs, _) -> + | Tadt (hs, _, _) -> (* cannot do better for ADT ? *) Uid.Map.add hs ty mp - )sty Uid.Map.empty + ) sty Uid.Map.empty let print_types_decls ?(header=true) types = let open Ty in @@ -184,20 +179,6 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> () | Tvar _ -> assert false | Text _ -> print_dbg ~flushed:false "type %a@ " Ty.print ty - | Trecord { Ty.lbs; _ } -> - print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty; - begin match lbs with - | [] -> assert false - | (lbl, ty)::l -> - let print fmt (lbl,ty) = - Format.fprintf fmt " ; %a :%a" - Uid.pp lbl Ty.print ty in - print_dbg ~flushed:false ~header:false - "{ %a : %a%a" - Uid.pp lbl Ty.print ty - (pp_list_no_space print) l; - print_dbg ~flushed:false ~header:false " }@ " - end | Tadt _ -> print_dbg ~flushed:false ~header:false "%a@ " Ty.print_full ty )types; diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 1e9bbe92e..b4c5022e9 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -414,20 +414,6 @@ module SmtPrinter = struct pp x.let_e pp_boxed x.in_e - | Sy.(Op Record), _ -> - begin - match ty with - | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } -> - assert (List.compare_lengths xs lbs = 0); - Fmt.pf ppf "@[<2>(%a %a@])" - Uid.pp record_constr - Fmt.(list ~sep:sp pp |> box) xs - - | _ -> - (* Excluded by the typechecker. *) - assert false - end - | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f -> @@ -589,7 +575,7 @@ module AEPrinter = struct assert false and pp_silent ppf t = - let { f ; xs ; ty; bind; _ } = t in + let { f ; xs ; bind; _ } = t in match f, xs with | Sy.Form form, xs -> pp_formula ppf form xs bind @@ -616,25 +602,6 @@ module AEPrinter = struct | Sy.(Op Extract (i, j)), [e] -> Fmt.pf ppf "%a^{%d, %d}" pp e i j - | Sy.(Op (Access field)), [e] -> - Fmt.pf ppf "%a.%a" pp e Uid.pp field - - | Sy.(Op Record), _ -> - begin match ty with - | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.compare_lengths xs lbs = 0); - Fmt.pf ppf "{"; - ignore (List.fold_left2 (fun first (field,_) e -> - Fmt.pf ppf "%s%a = %a" (if first then "" else "; ") - Uid.pp field pp e; - false - ) true lbs xs); - Fmt.pf ppf "}"; - | _ -> - (* Excluded by the typechecker. *) - assert false - end - | Sy.(Op ((Pow | Integer_round | Max_real | Min_real | Max_int | Min_int) as op)), [e1; e2] -> Fmt.pf ppf "%a(%a, %a)" Symbols.pp_ae_operator op pp e1 pp e2 @@ -1080,7 +1047,7 @@ let mk_ite cond th el = let rec is_model_term e = match e.f, e.xs with - | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs + | (Op Constr _ | Op Set), xs -> List.for_all is_model_term xs | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero @@ -1273,8 +1240,6 @@ let mk_constr cons xs ty = mk_term (Sy.Op (Constr cons)) xs ty let mk_tester cons t = mk_builtin ~is_pos:true (Sy.IsConstr cons) [t] -let mk_record xs ty = mk_term (Sy.Op Record) xs ty - let void = let cstr = Uid.of_dolmen Dolmen.Std.Expr.Term.Cstr.void in mk_constr cstr [] Ty.tunit @@ -1914,11 +1879,9 @@ module Triggers = struct | { f = Op (Get | Set) ; xs = [t1 ; t2]; _ } -> max (score_term t1) (score_term t2) - | { f = Op (Access _ | Destruct _ | Extract _) ; xs = [t]; _ } -> + | { f = Op (Destruct _ | Extract _) ; xs = [t]; _ } -> 1 + score_term t - | { f = Op Record; xs; _ } -> - 1 + (List.fold_left - (fun acc t -> max (score_term t) acc) 0 xs) + | { f = Op Set; xs = [t1; t2; t3]; _ } -> max (score_term t1) (max (score_term t2) (score_term t3)) @@ -2001,14 +1964,6 @@ module Triggers = struct | { f = Op Concat; _ }, _ -> -1 | _, { f = Op Concat; _ } -> 1 - | { f = Op (Access a1) ; xs=[t1]; _ }, - { f = Op (Access a2) ; xs=[t2]; _ } -> - let c = Uid.compare a1 a2 in - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Access _); _ }, _ -> -1 - | _, { f = Op (Access _); _ } -> 1 - | { f = Op (Destruct a1) ; xs = [t1]; _ }, { f = Op (Destruct a2) ; xs = [t2]; _ } -> let c = Uid.compare a1 a2 in @@ -2017,11 +1972,6 @@ module Triggers = struct | { f = Op (Destruct _); _ }, _ -> -1 | _, { f =Op (Destruct _); _ } -> 1 - | { f = Op Record ; xs= lbs1; _ }, { f = Op Record ; xs = lbs2; _ } -> - Util.cmp_lists lbs1 lbs2 cmp_trig_term - | { f = Op Record; _ }, _ -> -1 - | _, { f = Op Record; _ } -> 1 - | { f = (Op _) as s1; xs=tl1; _ }, { f = (Op _) as s2; xs=tl2; _ } -> (* ops that are not infix or prefix *) let l1 = List.map score_term tl1 in @@ -2631,7 +2581,6 @@ let mk_match e cases = 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 mker = @@ -2640,9 +2589,6 @@ let mk_match e cases = (fun e name -> mk_builtin ~is_pos:true (Sy.IsConstr name) [e]) - | Ty.Trecord _ -> - (fun _e _name -> assert false) (* no need to test for records *) - | _ -> assert false in let res = compile_match mk_destr mker e cases e in diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index a63ff116a..4922692f9 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -282,7 +282,6 @@ val mk_ite : t -> t -> t -> t val mk_constr : Uid.t -> t list -> Ty.t -> t val mk_tester : Uid.t -> t -> t -val mk_record : t list -> Ty.t -> t (** Substitutions *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 7c99a2c0b..91d473301 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -35,7 +35,6 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Uid.t | Record | Constr of Uid.t (* enums, adts *) | Destruct of Uid.t (* Arrays *) @@ -179,7 +178,7 @@ let compare_kinds k1 k2 = let compare_operators op1 op2 = Util.compare_algebraic op1 op2 (function - | Access h1, Access h2 | Constr h1, Constr h2 + | Constr h1, Constr h2 | Destruct h1, Destruct h2 -> Uid.compare h1 h2 | Extract (i1, j1), Extract (i2, j2) -> @@ -188,7 +187,7 @@ let compare_operators op1 op2 = | Int2BV n1, Int2BV n2 -> Int.compare n1 n2 | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int | Concat | Extract _ | Get | Set | Float - | Access _ | Record | Sqrt_real | Abs_int | Abs_real + | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int | Integer_log2 | Pow | Integer_round @@ -366,8 +365,6 @@ module AEPrinter = struct | Set -> Fmt.pf ppf "set" (* DT theory *) - | Record -> Fmt.pf ppf "@Record" - | Access s -> Fmt.pf ppf "@Access_%a" Uid.pp s | Constr s | Destruct s -> Uid.pp ppf s @@ -473,8 +470,7 @@ module SmtPrinter = struct | Set -> Fmt.pf ppf "store" (* DT theory *) - | Record -> () - | Access s | Constr s | Destruct s -> Uid.pp ppf s + | Constr s | Destruct s -> Uid.pp ppf s (* Float theory *) | Float -> Fmt.pf ppf "ae.round" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index bcf0af48a..049c4acbb 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -35,7 +35,6 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Uid.t | Record | Constr of Uid.t (* enums, adts *) | Destruct of Uid.t (* Arrays *) diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index c00ddd47a..d3ce6ecd6 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -33,16 +33,9 @@ type t = | Tbitv of int | Text of t list * Uid.t | Tfarray of t * t - | Tadt of Uid.t * t list - | Trecord of trecord + | Tadt of Uid.t * t list * bool and tvar = { v : int ; mutable value : t option } -and trecord = { - mutable args : t list; - name : Uid.t; - mutable lbs : (Uid.t * t) list; - record_constr : Uid.t; (* for ADTs that become records. default is "{" *) -} module Smtlib = struct let rec pp ppf = function @@ -52,10 +45,8 @@ module Smtlib = struct | Tbitv n -> Fmt.pf ppf "(_ BitVec %d)" n | Tfarray (a_t, r_t) -> Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t - | Text ([], name) - | Trecord { args = []; name; _ } | Tadt (name, []) -> Uid.pp ppf name - | Text (args, name) - | Trecord { args; name; _ } | Tadt (name, args) -> + | Text ([], name) | Tadt (name, [], _) -> Uid.pp ppf name + | Text (args, name) | Tadt (name, args, _) -> Fmt.(pf ppf "(@[%a %a@])" Uid.pp name (list ~sep:sp pp) args) | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v | Tvar { value = Some t; _ } -> pp ppf t @@ -91,7 +82,6 @@ let assoc_destrs hs cases = (*** pretty print ***) let print_generic body_of = - let h = Hashtbl.create 17 in let rec print = let open Format in fun body_of fmt -> function @@ -100,13 +90,6 @@ let print_generic body_of = | Tbool -> fprintf fmt "bool" | Tbitv n -> fprintf fmt "bitv[%d]" n | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v - | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } -> - if Hashtbl.mem h v then - fprintf fmt "%a %a" print_list l Uid.pp n - else - (Hashtbl.add h v (); - (*fprintf fmt "('a_%d->%a)" v print t *) - print body_of fmt t) | Tvar{ value = Some t; _ } -> (*fprintf fmt "('a_%d->%a)" v print t *) print body_of fmt t @@ -116,22 +99,7 @@ let print_generic body_of = fprintf fmt "%a %a" print_list l Uid.pp s | Tfarray (t1, t2) -> fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 - | Trecord { args = lv; name = n; lbs = lbls; _ } -> - begin - fprintf fmt "%a %a" print_list lv Uid.pp n; - if body_of != None then begin - fprintf fmt " = {"; - let first = ref true in - List.iter - (fun (s, t) -> - fprintf fmt "%s%a : %a" (if !first then "" else "; ") - Uid.pp s (print body_of) t; - first := false - ) lbls; - fprintf fmt "}" - end - end - | Tadt (n, lv) -> + | Tadt (n, lv, _) -> fprintf fmt "%a %a" print_list lv Uid.pp n; begin match body_of with | None -> () @@ -207,16 +175,11 @@ let rec shorten ty = if t1 == t1' && t2 == t2' then ty else Tfarray(t1', t2') - | Trecord r -> - r.args <- List.map shorten r.args; - r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs; - ty - - | Tadt (n, args) -> + | Tadt (n, args, record) -> let args' = List.map shorten args in shorten_body n args; (* should not rebuild the type if no changes are made *) - Tadt (n, args') + Tadt (n, args', record) | Tint | Treal | Tbool | Tbitv _ -> ty @@ -238,17 +201,7 @@ let rec compare t1 t2 = if c<>0 then c else compare ta2 tb2 | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1 - | Trecord { args = a1; name = s1; lbs = l1; _ }, - Trecord { args = a2; name = s2; lbs = l2; _ } -> - let c = Uid.compare s1 s2 in - if c <> 0 then c else - let c = compare_list a1 a2 in - if c <> 0 then c else - let l1, l2 = List.map snd l1, List.map snd l2 in - compare_list l1 l2 - | Trecord _, _ -> -1 | _ , Trecord _ -> 1 - - | Tadt (s1, pars1), Tadt (s2, pars2) -> + | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> let c = Uid.compare s1 s2 in if c <> 0 then c else compare_list pars1 pars2 @@ -284,20 +237,10 @@ let rec equal t1 t2 = with Invalid_argument _ -> false) | Tfarray (ta1, ta2), Tfarray (tb1, tb2) -> equal ta1 tb1 && equal ta2 tb2 - | Trecord { args = a1; name = s1; lbs = l1; _ }, - Trecord { args = a2; name = s2; lbs = l2; _ } -> - begin - try - Uid.equal s1 s2 && List.for_all2 equal a1 a2 && - List.for_all2 - (fun (l1, ty1) (l2, ty2) -> - Uid.equal l1 l2 && equal ty1 ty2) l1 l2 - with Invalid_argument _ -> false - end | Tint, Tint | Treal, Treal | Tbool, Tbool -> true | Tbitv n1, Tbitv n2 -> n1 =n2 - | Tadt (s1, pars1), Tadt (s2, pars2) -> + | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> begin try Uid.equal s1 s2 && List.for_all2 equal pars1 pars2 with Invalid_argument _ -> false @@ -322,13 +265,9 @@ let rec matching s pat t = List.fold_left2 matching s l1 l2 | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> matching (matching s ta1 tb1) ta2 tb2 - | Trecord r1, Trecord r2 when Uid.equal r1.name r2.name -> - let s = List.fold_left2 matching s r1.args r2.args in - List.fold_left2 - (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs | Tint , Tint | Tbool , Tbool | Treal , Treal -> s | Tbitv n , Tbitv m when n=m -> s - | Tadt(n1, args1), Tadt(n2, args2) when Uid.equal n1 n2 -> + | Tadt(n1, args1, _), Tadt(n2, args2, _) when Uid.equal n1 n2 -> List.fold_left2 matching s args1 args2 | _ , _ -> raise (TypeClash(pat,t)) @@ -348,20 +287,10 @@ let apply_subst = let t2' = apply_subst s t2 in if t1 == t1' && t2 == t2' then ty else Tfarray (t1', t2') - | Trecord r -> - let lbs, same1 = Lists.apply_right (apply_subst s) r.lbs in - let args, same2 = Lists.apply (apply_subst s) r.args in - if same1 && same2 then ty - else - Trecord - {r with args = args; - name = r.name; - lbs = lbs} - - | Tadt(name, params) + | Tadt(name, params, record) [@ocaml.ppwarning "TODO: detect when there are no changes "] -> - Tadt (name, List.map (apply_subst s) params) + Tadt (name, List.map (apply_subst s) params, record) | Tint | Treal | Tbool | Tbitv _ -> ty in @@ -383,18 +312,9 @@ let rec fresh ty subst = let ty1, subst = fresh ty1 subst in let ty2, subst = fresh ty2 subst in Tfarray (ty1, ty2), subst - | Trecord ({ args; name = n; lbs; _ } as r) -> + | Tadt(s,args, record) -> let args, subst = fresh_list args subst in - let lbs, subst = - List.fold_right - (fun (x,ty) (lbs, subst) -> - let ty, subst = fresh ty subst in - (x, ty)::lbs, subst) lbs ([], subst) - in - Trecord {r with args = args; name = n; lbs = lbs}, subst - | Tadt(s, args) -> - let args, subst = fresh_list args subst in - Tadt (s, args), subst + Tadt (s,args, record), subst | t -> t, subst and fresh_list lty subst = @@ -512,8 +432,8 @@ let fresh_empty_text = in text [] (Uid.of_dolmen id) -let t_adt ?(body=None) s ty_vars = - let ty = Tadt (s, ty_vars) in +let t_adt ?(record=false) ?(body=None) s ty_vars = + let ty = Tadt (s, ty_vars, record) in begin match body with | None -> () | Some [] -> assert false @@ -547,33 +467,14 @@ let tunit = in ty -let trecord ?(sort_fields = false) ~record_constr lv name lbs = - let lbs = - if sort_fields then - List.sort (fun (l1, _) (l2, _) -> Uid.compare l1 l2) lbs - else - lbs - in - Trecord { record_constr; args = lv; name; lbs = lbs} - let rec hash t = match t with | Tvar{ v; _ } -> v | Text(l,s) -> abs (List.fold_left (fun acc x-> acc*19 + hash x) (Uid.hash s) l) | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2) - | Trecord { args; name = s; lbs; _ } -> - let h = - List.fold_left (fun h ty -> 27 * h + hash ty) (Uid.hash s) args - in - let h = - List.fold_left - (fun h (lb, ty) -> 23 * h + 19 * (Uid.hash lb) + hash ty) - (abs h) lbs - in - abs h - | Tadt (s, args) -> + | Tadt (s, args, _) -> (* We do not hash constructors. *) let h = List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args @@ -587,7 +488,7 @@ let occurs { v = n; _ } t = | Tvar { v = m; _ } -> n=m | Text(l,_) -> List.exists occursrec l | Tfarray (t1,t2) -> occursrec t1 || occursrec t2 - | Trecord { args ; _ } | Tadt (_, args) -> List.exists occursrec args + | Tadt (_, args, _) -> List.exists occursrec args | Tint | Treal | Tbool | Tbitv _ -> false in occursrec t @@ -607,12 +508,9 @@ let rec unify t1 t2 = | Text(l1,s1) , Text(l2,s2) when Uid.equal s1 s2 -> List.iter2 unify l1 l2 | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> unify ta1 tb1;unify ta2 tb2 - | Trecord r1, Trecord r2 when Uid.equal r1.name r2.name -> - List.iter2 unify r1.args r2.args | Tint, Tint | Tbool, Tbool | Treal, Treal -> () | Tbitv n , Tbitv m when m=n -> () - - | Tadt(n1, p1), Tadt (n2, p2) when Uid.equal n1 n2 -> + | Tadt(n1, p1, _), Tadt (n2, p2, _) when Uid.equal n1 n2 -> List.iter2 unify p1 p2 | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] -> @@ -652,10 +550,7 @@ let vty_of t = | Tvar { v = i ; value = None } -> Svty.add i acc | Text(l,_) -> List.fold_left vty_of_rec acc l | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2 - | Trecord { args; lbs; _ } -> - let acc = List.fold_left vty_of_rec acc args in - List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs - | Tadt(_, args) -> + | Tadt(_, args, _) -> List.fold_left vty_of_rec acc args | Tvar { value = Some _ ; _ } @@ -670,18 +565,12 @@ let rec monomorphize ty = match ty with | Tint | Treal | Tbool | Tbitv _ -> ty | Text (tyl,hs) -> Text (List.map monomorphize tyl, hs) - | Trecord ({ args = tylv; name = n; lbs = tylb; _ } as r) -> - let m_tylv = List.map monomorphize tylv in - let m_tylb = - List.map (fun (lb, ty_lb) -> lb, monomorphize ty_lb) tylb - in - Trecord {r with args = m_tylv; name = n; lbs = m_tylb} | Tfarray (ty1,ty2) -> Tfarray (monomorphize ty1,monomorphize ty2) | Tvar {v=v; value=None} -> text [] (Uid.of_string ("'_c"^(string_of_int v))) | Tvar ({ value = Some ty1; _ } as r) -> Tvar { r with value = Some (monomorphize ty1)} - | Tadt(name, params) -> - Tadt(name, List.map monomorphize params) + | Tadt(name, params, record) -> + Tadt(name, List.map monomorphize params, record) let print_subst fmt sbt = M.iter (fun n ty -> Format.fprintf fmt "%d -> %a" n print ty) sbt; diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 43b7b8ddd..65be76228 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -51,7 +51,7 @@ type t = (** Functional arrays. [TFarray (src,dst)] maps values of type [src] to values of type [dst]. *) - | Tadt of Uid.t * t list + | Tadt of Uid.t * t list * bool (** Application of algebraic data types. [Tadt (a, params)] denotes the application of the polymorphic datatype [a] to the types parameters [params]. @@ -60,9 +60,6 @@ type t = value [Tadt (Hstring.make "list", [Tint]] where the identifier {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *) - | Trecord of trecord - (** Record type. *) - and tvar = { v : int; (** Unique identifier *) @@ -74,20 +71,6 @@ and tvar = { hence distinct types should have disjoints sets of type variables (see function {!val:fresh}). *) -and trecord = { - mutable args : t list; - (** Arguments passed to the record constructor *) - name : Uid.t; - (** Name of the record type *) - mutable lbs : (Uid.t * t) list; - (** List of fields of the record. Each field has a name, - and an associated type. *) - record_constr : Uid.t; - (** record constructor. Useful is case it's a specialization of an - algeberaic datatype. Default value is "\{__[name]" *) -} -(** Record types. *) - type adt_constr = { constr : Uid.t ; (** constructor of an ADT type *) @@ -165,7 +148,8 @@ val text : t list -> Uid.t -> t given. *) val t_adt : - ?body:((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t + ?record:bool -> + ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t (** Create an algebraic datatype. The body is a list of constructors, where each constructor is associated with the list of its destructors with their respective types. If [body] is none, @@ -173,17 +157,6 @@ val t_adt : argument is the name of the type. The third one provides its list of arguments. *) -val trecord : - ?sort_fields:bool -> - record_constr:Uid.t -> t list -> Uid.t -> (Uid.t * t) list -> t -(** Create a record type. [trecord args name lbs] creates a record - type with name [name], arguments [args] and fields [lbs]. - - If [sort_fields] is true, the record fields are sorted according to - [Hstring.compare]. This is to preserve compatibility with the old - typechecker behavior and should not be used in new code. *) - - (** {2 Substitutions} *) module M : Map.S with type key = int diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 7c495adce..d31b746c3 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -81,8 +81,7 @@ and 'a tt_desc = | TTextract of 'a atterm * int * int | TTconcat of 'a atterm * 'a atterm - | TTdot of 'a atterm * Hstring.t - | TTrecord of (Hstring.t * 'a atterm) list + | TTrecord of Ty.t * (Hstring.t * 'a atterm) list | TTlet of (Symbols.t * 'a atterm) list * 'a atterm | TTnamed of Hstring.t * 'a atterm | TTite of 'a atform * @@ -218,9 +217,7 @@ let rec print_term = fprintf fmt "%a^{%d, %d}" print_term t1 i j | TTconcat (t1, t2) -> fprintf fmt "%a @@ %a" print_term t1 print_term t2 - | TTdot (t1, s) -> - fprintf fmt "%a.%s" print_term t1 (Hstring.view s) - | TTrecord l -> + | TTrecord (_, l) -> fprintf fmt "{ "; List.iter (fun (s, t) -> fprintf fmt "%s = %a" (Hstring.view s) print_term t) l; diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index b051c45cf..133c2e7e9 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -115,9 +115,7 @@ and 'a tt_desc = (** Extract a sub-bitvector *) | TTconcat of 'a atterm * 'a atterm (* Concatenation of bitvectors *) - | TTdot of 'a atterm * Hstring.t - (** Field access on structs/records *) - | TTrecord of (Hstring.t * 'a atterm) list + | TTrecord of Ty.t * (Hstring.t * 'a atterm) list (** Record creation. *) | TTlet of (Symbols.t * 'a atterm) list * 'a atterm (** Let-bindings. Accept a list of mutually recursive le-bindings. *) diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml index a7c474371..729203332 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -58,6 +58,10 @@ let compare u1 u2 = | Dolmen id1, Dolmen id2 -> DE.Id.compare id1 id2 | _ -> String.compare (show u1) (show u2) +let rec list_assoc x = function + | [] -> raise Not_found + | (y, v) :: l -> if equal x y then v else list_assoc x l + module Set = Set.Make (struct type nonrec t = t diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index 09e0a7675..67cfc7312 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -39,6 +39,7 @@ val pp : t Fmt.t val show : t -> string val equal : t -> t -> bool val compare : t -> t -> int +val list_assoc : t -> (t * 'a) list -> 'a module Set : Set.S with type elt = t module Map : Map.S with type key = t