diff --git a/src/lib/dune b/src/lib/dune index 12b197a39..e4fcd2c6c 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 687f4f600..8edb4645e 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 7c417b946..3893446a3 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -515,87 +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.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.attach_orders [adt]; - let uid = Uid.of_ty_cst ty_c in - 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 - (Uid.of_term_cst 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 record_constr = Uid.of_term_cst cstr in - let ty = Ty.trecord ~record_constr tyvl uid lbs in - Cache.store_ty ty_c ty - | Some (Adt { cases; _ } as adt) -> Nest.attach_orders [adt]; let uid = Uid.of_ty_cst ty_c in @@ -653,29 +583,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 lbs = - Array.fold_right ( - fun c acc -> - match c with - | Some (DE.{ id_ty; _ } as id) -> - let pty = dty_to_ty id_ty in - (Uid.of_term_cst 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; _ }) -> + | Tadt (hs, tyl, _), Some (Adt { cases; ty = ty_c; _ }) -> let cs = Array.fold_right ( fun DE.{ cstr; dstrs; _ } accl -> @@ -696,38 +604,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.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 uid = Uid.of_ty_cst ty_c in - let record_constr = Uid.of_term_cst cases.(0).cstr in - let ty = - if (record || Array.length cases = 1) && not contains_adts - then - Ty.trecord ~record_constr 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 @@ -954,14 +840,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_term_cst 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_term_cst tcst) [] ty | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1002,10 +882,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_term_cst destr)) - | Tadt _ -> - Sy.destruct (Uid.of_term_cst destr) + | Tadt _ -> Sy.destruct (Uid.of_term_cst destr) | _ -> assert false in E.mk_term sy [e] ty @@ -1037,11 +914,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 @@ -1308,19 +1180,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 (Uid.of_term_cst 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 @@ Uid.of_term_cst 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 8c885caac..6ca77da84 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -41,7 +41,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 -> @@ -150,26 +150,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 569b4f85d..170c4e746 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.Term_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 constrs = List.map (fun Ty.{ constr; _ } -> constr) cases in List.fold_left @@ -297,7 +293,7 @@ module Env = struct let find_builtin_constr ty n = match ty with - | Ty.Tadt (name, []) -> + | Ty.Tadt (name, [], _) -> let cases = Ty.type_body name [] in let constrs = List.map (fun Ty.{ constr; _ } -> constr) cases in List.find (Uid.equal n) constrs @@ -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 @@ -631,24 +622,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 = @@ -860,22 +839,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), - My_list.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 = @@ -888,7 +851,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 = @@ -897,7 +864,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 @@ -911,20 +878,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 @@ -932,10 +901,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) -> @@ -981,6 +950,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 @@ -990,9 +981,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 @@ -1003,9 +991,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 = @@ -1270,20 +1257,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 @@ -1409,10 +1384,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 @@ -2097,10 +2069,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) @@ -2353,7 +2323,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 @@ -2369,14 +2339,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 @@ -2385,16 +2355,14 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = List.fold_left (fun (acc, env) (constr, lbl_args_ty) -> let args_ty = List.map snd lbl_args_ty in - let tty, env = - Env.add_constr ~record:false env constr args_ty pur_ty loc - in + let tty, env = Env.add_constr env constr args_ty pur_ty loc in let acc = ({c = TLogic(loc, [constr], tty); annot=new_id ()}, env) :: acc in 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 3c1dafd98..10ce9beee 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -59,7 +59,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 @@ -178,7 +178,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 @@ -199,9 +199,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 9e52bb78f..46e26fe0c 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -90,7 +90,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 = @@ -175,7 +175,7 @@ module Domains = struct contains the type of constructor and in particular its arity. *) let is_enum_constr r c = match X.type_info r with - | Tadt (name, args) -> + | Tadt (name, args, _) -> let cases = Ty.type_body name args in Compat.List.is_empty @@ Ty.assoc_destrs c cases | _ -> assert false @@ -499,7 +499,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 @@ -585,7 +585,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 e7faf625e..b89f91996 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/relation.ml b/src/lib/reasoners/relation.ml index d36a88526..78eb6699a 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 8b308859b..12d5a07b8 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 42d9d7bfa..bd4fbc8d9 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 31973c37d..ebb7d3dcb 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -159,18 +159,13 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> mp | Tvar _ -> assert false - | Text (_, hs) | Trecord { name = hs; _ } when - Uid.Ty_map.mem hs mp -> mp + | Text (_, hs) when Uid.Ty_map.mem hs mp -> mp | Text (l, hs) -> let l = List.map (fun _ -> Ty.fresh_tvar()) l in Uid.Ty_map.add hs (Text(l, hs)) mp - | Trecord { name; _ } -> - (* cannot do better for records ? *) - Uid.Ty_map.add name ty mp - - | Tadt (hs, _) -> + | Tadt (hs, _, _) -> (* cannot do better for ADT ? *) Uid.Ty_map.add hs ty mp )sty Uid.Ty_map.empty @@ -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 e07fc3e1c..1a3195341 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -443,20 +443,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 -> @@ -618,7 +604,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 @@ -645,25 +631,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 @@ -1110,7 +1077,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 @@ -1303,8 +1270,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 constr = Uid.of_term_cst Dolmen.Std.Expr.Term.Cstr.void in mk_constr constr [] Ty.tunit @@ -1944,11 +1909,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)) @@ -2031,14 +1994,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 @@ -2047,11 +2002,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 @@ -2661,7 +2611,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 = @@ -2670,9 +2619,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 8c639480c..5160a17c4 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -286,7 +286,6 @@ val mk_ite : t -> t -> t -> t val mk_constr : Uid.term_cst -> t list -> Ty.t -> t val mk_tester : Uid.term_cst -> 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 3b00b1e45..cb55fa9d3 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -35,8 +35,7 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Uid.term_cst | Record - | Constr of Uid.term_cst (* enums, adts *) + | Constr of Uid.term_cst | Destruct of Uid.term_cst (* Arrays *) | Get | Set @@ -184,7 +183,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) -> @@ -193,7 +192,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 @@ -371,8 +370,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 @@ -478,8 +475,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 0aedea950..0a3f13bc3 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -35,8 +35,7 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Uid.term_cst | Record - | Constr of Uid.term_cst (* enums, adts *) + | Constr of Uid.term_cst | Destruct of Uid.term_cst (* Arrays *) | Get | Set diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 8daf7a735..784241504 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -33,19 +33,10 @@ type t = | Tbitv of int | Text of t list * Uid.ty_cst | Tfarray of t * t - | Tadt of Uid.ty_cst * t list - | Trecord of trecord + | Tadt of Uid.ty_cst * t list * bool and tvar = { v : int ; mutable value : t option } -and trecord = { - mutable args : t list; - name : Uid.ty_cst; - mutable lbs : (Uid.term_cst * t) list; - record_constr : Uid.term_cst; - (* for ADTs that become records. default is "{" *) -} - module Smtlib = struct let rec pp ppf = function | Tint -> Fmt.pf ppf "Int" @@ -54,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 @@ -93,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 @@ -102,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 @@ -118,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 -> () @@ -209,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 @@ -240,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 @@ -286,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 @@ -324,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)) @@ -350,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 = My_list.apply_right (apply_subst s) r.lbs in - let args, same2 = My_list.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 @@ -391,18 +318,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 (* Assume that [shorten] have been applied on [lty]. *) @@ -525,8 +443,8 @@ let fresh_empty_text = in text [] (Uid.of_ty_cst 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 @@ -559,33 +477,14 @@ let tunit = let ty = t_adt ~body (Uid.of_ty_cst DE.Ty.Const.unit) [] 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 @@ -599,7 +498,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 @@ -619,12 +518,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 "] -> @@ -664,10 +560,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 _ ; _ } @@ -682,18 +575,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 = let sep ppf () = Fmt.pf ppf " -> " in diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 688662695..6a4f8e6cd 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.ty_cst * t list + | Tadt of Uid.ty_cst * 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.ty_cst; - (** Name of the record type *) - mutable lbs : (Uid.term_cst * t) list; - (** List of fields of the record. Each field has a name, - and an associated type. *) - record_constr : Uid.term_cst; - (** record constructor. Useful is case it's a specialization of an - algeberaic datatype. Default value is "\{__[name]" *) -} -(** Record types. *) - type adt_constr = { constr : Uid.term_cst ; (** constructor of an ADT type *) @@ -165,6 +148,7 @@ val text : t list -> Uid.ty_cst -> t given. *) val t_adt : + ?record:bool -> ?body:((Uid.term_cst * (Uid.term_cst * t) list) list) option -> Uid.ty_cst -> t list -> t (** Create an algebraic datatype. The body is a list of @@ -174,18 +158,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.term_cst -> - t list -> Uid.ty_cst -> (Uid.term_cst * 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 eb2dc0381..5c6ac7bfa 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 525e2712f..bf05d9f9a 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 66d877467..eb57b6820 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -96,6 +96,10 @@ let compare (type a b) (u1 : a t) (u2 : b t) = | Ty_var id1, Ty_var 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 Term_set = Set.Make (struct type nonrec t = term_cst diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index 866357b3a..0385bd48e 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -43,6 +43,8 @@ val of_ty_var : DE.ty_var -> ty_var val of_string : string -> 'a t val of_hstring : Hstring.t -> 'a t +val list_assoc : 'a t -> ('a t * 'b) list -> 'b + val hash : 'a t -> int val pp : 'a t Fmt.t val show : 'a t -> string