From 54d4975f2de51bbab0e028f6fd8d437ebabe7865 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 8 Oct 2024 16:14:11 +0200 Subject: [PATCH 1/9] Do not use Uid.of_hstring for Fpa constructors --- src/lib/frontend/translate.ml | 11 ++++---- src/lib/structures/fpa_rounding.ml | 43 ++++++++++++++++++++++++----- src/lib/structures/fpa_rounding.mli | 5 ++-- 3 files changed, 44 insertions(+), 15 deletions(-) diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index d63c835dd..cd3da963c 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -187,7 +187,7 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes = | `App ((`Generic ty_cst), []) -> let constrs = Fpa_rounding.d_constrs in let add_constrs map = - List.fold_left (fun map ((c : DE.term_cst), _) -> + List.fold_left (fun map (c : DE.term_cst) -> let name = get_basename c.path in DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> @@ -273,8 +273,8 @@ let ae_fpa_builtins = DE.Term.apply_cst float_cst [] [prec; exp; mode; x] in let mode m = - let cst, _ = - List.find (fun (cst, _args) -> + let cst = + List.find (fun cst -> match cst.DE.path with | Absolute { name; _ } -> String.equal name m | Local _ -> false) @@ -924,10 +924,9 @@ let mk_add translate sy ty l = E.mk_term sy args ty let mk_rounding fpar = - let name = Hstring.make @@ Fpa_rounding.string_of_rounding_mode fpar in + let tcst = Uid.of_term_cst @@ Fpa_rounding.tcst_of_rounding_mode fpar in let ty = Fpa_rounding.fpa_rounding_mode in - let sy = Sy.Op (Sy.Constr (Uid.of_hstring name)) in - E.mk_term sy [] ty + E.mk_constr tcst [] ty (** [mk_expr ~loc ~name_base ~toplevel ~decl_kind term] diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index 3c04170b3..bfb0a4174 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -25,7 +25,8 @@ (* *) (**************************************************************************) -module DE = Dolmen.Std.Expr +module DStd = Dolmen.Std +module DE = DStd.Expr module Hs = Hstring module Q = Numbers.Q module Z = Numbers.Z @@ -83,22 +84,50 @@ let hstring_ae_reprs = (fun c -> Hs.make (to_ae_string c)) constrs +let get_basename = function + | DStd.Path.Local { name; } + | Absolute { name; path = []; } -> name + | Absolute { name; path; } -> + Fmt.failwith + "Expected an empty path to the basename: \"%s\" but got: [%a]." + name (fun fmt l -> + match l with + | h :: t -> + Format.fprintf fmt "%s" h; + List.iter (Format.fprintf fmt "; %s") t + | _ -> () + ) path + (* The rounding mode is the enum with the SMT values. The Alt-Ergo values are injected in this type. *) -let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode = +let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode = let module DStd = Dolmen.Std in (* We may use the builtin type `DStd.Expr.Ty.roundingMode` here. *) let ty_cst = DE.Ty.Const.mk (DStd.Path.global "RoundingMode") 0 in let constrs = List.map (fun c -> DStd.Path.global @@ to_smt_string c, []) constrs in - let def, d_constrs = DE.Term.define_adt ty_cst [] constrs in - Nest.attach_orders [def]; - let body = - List.map (fun (c, _) -> Uid.of_term_cst c, []) d_constrs + let def, d_constrs = + let def, l = DE.Term.define_adt ty_cst [] constrs in + let constrs = List.map (fun (c, _) -> c) l in + def, constrs in + Nest.attach_orders [def]; + let body = List.map (fun c -> Uid.of_term_cst c, []) d_constrs in let ty = Ty.t_adt ~body:(Some body) (Uid.of_ty_cst ty_cst) [] in - DE.Ty.apply ty_cst [], d_constrs, ty + let tcst_of_rounding_mode m = + let name = string_of_rounding_mode m in + let opt = + List.find_map + (fun (DE.{ path; _ } as tcst) -> + let n = get_basename path in + if String.equal name n then Some tcst + else None + ) d_constrs + in + match opt with Some o -> o | None -> assert false + in + DE.Ty.apply ty_cst [], d_constrs, ty, tcst_of_rounding_mode let rounding_mode_of_smt_hs = let table = Hashtbl.create 5 in diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index ad69bf1cf..6b0a14557 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -51,8 +51,7 @@ val fpa_rounding_mode_ae_type_name : string val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.t (** The Dolmen constructors of [rounding_mode]. *) -val d_constrs : - (Uid.DE.term_cst * (Uid.DE.ty * Uid.DE.term_cst option) list) list +val d_constrs : Uid.DE.term_cst list (** The rounding mode type. *) val fpa_rounding_mode : Ty.t @@ -71,6 +70,8 @@ val translate_smt_rounding_mode : Hstring.t -> Hstring.t option (** Returns the string representation of the [rounding_mode] (SMT2 standard) *) val string_of_rounding_mode : rounding_mode -> string +val tcst_of_rounding_mode : rounding_mode -> Dolmen.Std.Expr.term_cst + (** Integer part of binary logarithm for NON-ZERO POSITIVE number **) val integer_log_2 : Numbers.Q.t -> int From 58830b00b0c3b3d86284eae20938a647bb72fb5f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 8 Oct 2024 16:18:52 +0200 Subject: [PATCH 2/9] Remove unification in Ty --- src/lib/structures/ty.ml | 69 --------------------------------------- src/lib/structures/ty.mli | 50 ++-------------------------- 2 files changed, 2 insertions(+), 117 deletions(-) diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 8daf7a735..16740982f 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -594,56 +594,6 @@ let rec hash t = | _ -> Hashtbl.hash t -let occurs { v = n; _ } t = - let rec occursrec = function - | 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 - | Tint | Treal | Tbool | Tbitv _ -> false - in occursrec t - -(*** destructive unification ***) -let rec unify t1 t2 = - let t1 = shorten t1 in - let t2 = shorten t2 in - match t1 , t2 with - Tvar ({v=n;value=None} as tv1), Tvar {v=m;value=None} -> - if n<>m then tv1.value <- Some t2 - | _ , Tvar ({ value = None; _ } as tv) -> - if (occurs tv t1) then raise (TypeClash(t1,t2)); - tv.value <- Some t1 - | Tvar ({ value = None; _ } as tv) , _ -> - if (occurs tv t2) then raise (TypeClash(t1,t2)); - tv.value <- Some 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 -> - List.iter2 unify p1 p2 - - | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] -> - raise (TypeClash(t1,t2)) - -let instantiate lvar lty ty = - let s = - List.fold_left2 - (fun s x t -> - match x with - | Tvar { v = n; _ } -> - M.add n t s - | _ -> assert false) M.empty lvar lty - in - apply_subst s ty - -let union_subst s1 s2 = - M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2) s1) s2 - let compare_subst = M.compare compare let equal_subst = M.equal equal @@ -676,25 +626,6 @@ let vty_of t = in vty_of_rec Svty.empty t - - [@ocaml.ppwarning "TODO: detect when there are no changes "] -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) - let print_subst = let sep ppf () = Fmt.pf ppf " -> " in Fmt.(box @@ braces diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 688662695..9b0a72db3 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -210,65 +210,19 @@ val esubst : subst val apply_subst : subst -> t -> t (** Substitution application. *) -val union_subst : subst -> subst -> subst -(** [union_subst u v] applies [v] to [u], resulting in [u']. - It then computes the union of [u'] and [v], prioritizing - bindings from [u'] in case of conflict. *) - - -(** {2 Unification/Matching} *) +(** {2 Matching} *) exception TypeClash of t * t -(** Exception raised during matching or unification. +(** Exception raised during matching. [TypeClash (u, v)] is raised when [u] and [v] could not be matched or unified ([u] and [v] may be sub-types of the types being actually unified or matched). *) -val unify : t -> t -> unit -(** Destructive unification. Mutates the [value] fields of - type variables. - @raise TypeClash when unification is impossible. In this - case, the [value] fields of already mutated type variables - are left modified, which may prevent future unifications. *) - val matching : subst -> t -> t -> subst (** Matching of types (non-destructive). [matching pat t] returns a substitution [subst] such that [apply_subst subst pat] is equal to [t]. *) -val shorten : t -> t -(** Shorten paths in type variables values. - Unification in particular can create chains where the [value] - field of one type variable points to another and so on... - This function short-circuits such chains so that the value - of a type variable can be accessed directly. *) - - -(** {2 Manipulations on types} *) - -val fresh : t -> subst -> t * subst -(** Apply the given substitution, all while generating fresh variables - for the variables not already bound in the substitution. Returns - a substitution containing bindings from old variable to their - fresh counterpart. *) - -val fresh_list : t list -> subst -> t list * subst -(** Same as {!val:fresh} but on lists of types. *) - -val instantiate : t list -> t list -> t -> t -(** [instantiate vars args t] builds the substitutions mapping - each type variable in [vars] to the corresponding term in [args], - then apply that substitution to [t]. - @raise Invalid_argument if the lists [vars] and [args] - do not have the same length - @raise Assertion_failure if one type in [vars] is not - a type variable. -*) - -val monomorphize: t -> t -(** Return a monomorphized variant of the given type, where - type variable without values have been replaced by abstract types. *) - type goal_sort = | Cut (** Introduce a cut in a goal. Once the cut proved, From 5d8cba873e070818fb937ee59f3e4f653d4e451f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 8 Oct 2024 16:20:54 +0200 Subject: [PATCH 3/9] Remove Hstring constructor in Uid --- src/lib/structures/uid.ml | 7 ------- src/lib/structures/uid.mli | 3 --- src/lib/util/nest.ml | 2 -- 3 files changed, 12 deletions(-) diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml index 66d877467..2d352db0e 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -29,7 +29,6 @@ module DStd = Dolmen.Std module DE = Dolmen.Std.Expr type _ t = - | Hstring : Hstring.t -> 'a t | Term_cst : DE.term_cst -> DE.term_cst t | Ty_cst : DE.ty_cst -> DE.ty_cst t | Ty_var : DE.ty_var -> DE.ty_var t @@ -61,19 +60,15 @@ let[@inline always] of_term_cst id = let[@inline always] of_ty_cst id = Ty_cst id let[@inline always] of_ty_var id = Ty_var id -let[@inline always] of_hstring hs = Hstring hs -let[@inline always] of_string s = of_hstring @@ Hstring.make s let hash (type a) (u : a t) = match u with - | Hstring hs -> Hstring.hash hs | Term_cst id -> DE.Id.hash id | Ty_cst id -> DE.Id.hash id | Ty_var id -> DE.Id.hash id let pp (type a) ppf (u : a t) = match u with - | Hstring hs -> Hstring.print ppf hs | Term_cst id -> DE.Id.print ppf id | Ty_cst id -> DE.Id.print ppf id | Ty_var id -> DE.Id.print ppf id @@ -82,7 +77,6 @@ let show (type a) (u : a t) = Fmt.to_to_string pp u let equal (type a b) (u1 : a t) (u2 : b t) = match u1, u2 with - | Hstring hs1, Hstring hs2 -> Hstring.equal hs1 hs2 | Term_cst id1, Term_cst id2 -> DE.Id.equal id1 id2 | Ty_cst id1, Ty_cst id2 -> DE.Id.equal id1 id2 | Ty_var id1, Ty_var id2 -> DE.Id.equal id1 id2 @@ -90,7 +84,6 @@ let equal (type a b) (u1 : a t) (u2 : b t) = let compare (type a b) (u1 : a t) (u2 : b t) = match u1, u2 with - | Hstring hs1, Hstring hs2 -> Hstring.compare hs1 hs2 | Term_cst id1, Term_cst id2 -> DE.Id.compare id1 id2 | Ty_cst id1, Ty_cst id2 -> DE.Id.compare id1 id2 | Ty_var id1, Ty_var id2 -> DE.Id.compare id1 id2 diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index 866357b3a..501e8b88d 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -28,7 +28,6 @@ module DE = Dolmen.Std.Expr type _ t = private - | Hstring : Hstring.t -> 'a t | Term_cst : DE.term_cst -> DE.term_cst t | Ty_cst : DE.ty_cst -> DE.ty_cst t | Ty_var : DE.ty_var -> DE.ty_var t @@ -40,8 +39,6 @@ type ty_var = DE.ty_var t val of_term_cst : DE.term_cst -> term_cst val of_ty_cst : DE.ty_cst -> ty_cst val of_ty_var : DE.ty_var -> ty_var -val of_string : string -> 'a t -val of_hstring : Hstring.t -> 'a t val hash : 'a t -> int val pp : 'a t Fmt.t diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index b20b8c6e0..6a75ecd24 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -185,6 +185,4 @@ let perfect_hash id = assert false end | Term_cst _ -> invalid_arg "Nest.perfect_hash" - | Hstring hs -> - Hstring.hash hs | _ -> . From c6f00a64e45c3a4fb5c9205cbcb0b31f79c04b51 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 8 Oct 2024 17:46:26 +0200 Subject: [PATCH 4/9] Remove Uid module This PR removes the interface Uid. We know use `term_cst` and `ty_cst` of Dolmen directly! --- src/lib/dune | 2 +- src/lib/frontend/models.ml | 19 +++--- src/lib/frontend/translate.ml | 55 +++++++-------- src/lib/reasoners/adt.ml | 39 ++++++----- src/lib/reasoners/adt.mli | 6 +- src/lib/reasoners/adt_rel.ml | 12 ++-- src/lib/reasoners/records.ml | 31 +++++---- src/lib/reasoners/theory.ml | 19 +++--- src/lib/structures/expr.ml | 31 ++++----- src/lib/structures/expr.mli | 4 +- src/lib/structures/fpa_rounding.ml | 36 +++++----- src/lib/structures/fpa_rounding.mli | 10 +-- src/lib/structures/symbols.ml | 27 ++++---- src/lib/structures/symbols.mli | 12 ++-- src/lib/structures/ty.ml | 98 ++++++++++++-------------- src/lib/structures/ty.mli | 29 ++++---- src/lib/structures/typed.ml | 6 +- src/lib/structures/typed.mli | 5 +- src/lib/structures/uid.ml | 102 ---------------------------- src/lib/structures/uid.mli | 53 --------------- src/lib/structures/xliteral.ml | 10 +-- src/lib/structures/xliteral.mli | 2 +- src/lib/util/nest.ml | 13 ++-- src/lib/util/nest.mli | 2 +- 24 files changed, 234 insertions(+), 389 deletions(-) delete mode 100644 src/lib/structures/uid.ml delete mode 100644 src/lib/structures/uid.mli diff --git a/src/lib/dune b/src/lib/dune index f91c8ecea..0d8ecc3c6 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -57,7 +57,7 @@ ; structures Commands Errors Explanation Fpa_rounding Parsed Profiling Satml_types Symbols - Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal + Expr Var Ty Typed Xliteral ModelMap Id Objective Literal ; util Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue Options Timers Util Vec Version Steps Printer diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 8c885caac..afa71e83d 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -20,6 +20,7 @@ module Sy = Symbols module X = Shostak.Combine module E = Expr module MS = Map.Make(String) +module DE = Dolmen.Std.Expr let constraints = ref MS.empty @@ -110,15 +111,15 @@ module Pp_smtlib_term = struct | Sy.L_built (Sy.IsConstr hs), [e] -> if Options.get_output_smtlib () then - fprintf fmt "((_ is %a) %a)" Uid.pp hs print e + fprintf fmt "((_ is %a) %a)" DE.Term.Const.print hs print e else - fprintf fmt "(%a ? %a)" print e Uid.pp hs + fprintf fmt "(%a ? %a)" print e DE.Term.Const.print hs | Sy.L_neg_built (Sy.IsConstr hs), [e] -> if Options.get_output_smtlib () then - fprintf fmt "(not ((_ is %a) %a))" Uid.pp hs print e + fprintf fmt "(not ((_ is %a) %a))" DE.Term.Const.print hs print e else - fprintf fmt "not (%a ? %a)" print e Uid.pp hs + fprintf fmt "not (%a ? %a)" print e DE.Term.Const.print hs | (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE) | Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE) @@ -152,9 +153,9 @@ module Pp_smtlib_term = struct | Sy.Op (Sy.Access field), [e] -> if Options.get_output_smtlib () then - fprintf fmt "(%a %a)" Uid.pp field print e + fprintf fmt "(%a %a)" DE.Term.Const.print field print e else - fprintf fmt "%a.%a" print e Uid.pp field + fprintf fmt "%a.%a" print e DE.Term.Const.print field | Sy.Op (Sy.Record), _ -> begin match ty with @@ -163,7 +164,7 @@ module Pp_smtlib_term = struct fprintf fmt "{"; ignore (List.fold_left2 (fun first (field,_) e -> fprintf fmt "%s%a = %a" (if first then "" else "; ") - Uid.pp field print e; + DE.Term.Const.print field print e; false ) true lbs xs); fprintf fmt "}"; @@ -178,7 +179,7 @@ module Pp_smtlib_term = struct (* TODO: introduce PrefixOp in the future to simplify this ? *) | Sy.Op (Sy.Constr hs), ((_::_) as l) -> - fprintf fmt "%a(%a)" Uid.pp hs print_list l + fprintf fmt "%a(%a)" DE.Term.Const.print hs print_list l | Sy.Op _, [e1; e2] -> if Options.get_output_smtlib () then @@ -187,7 +188,7 @@ module Pp_smtlib_term = struct fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2 | Sy.Op Sy.Destruct hs, [e] -> - fprintf fmt "%a#%a" print e Uid.pp hs + fprintf fmt "%a#%a" print e DE.Term.Const.print hs | Sy.In(lb, rb), [t] -> diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index cd3da963c..95effbb55 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -237,7 +237,7 @@ let inject_ae_to_smt2 id = in {id with name} else - match Fpa_rounding.rounding_mode_of_ae_hs (Hstring.make n) with + match Fpa_rounding.rounding_mode_of_ae n with | rm -> let name = Dolmen_std.Name.simple (Fpa_rounding.string_of_rounding_mode rm) @@ -580,7 +580,6 @@ let mk_ty_decl (ty_c: DE.ty_cst) = (* 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 ( @@ -588,7 +587,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) = match c with | Some (DE.{ id_ty; _ } as id) -> let pty = dty_to_ty id_ty in - (Uid.of_term_cst id, pty) :: acc + (id, pty) :: acc | _ -> Fmt.failwith "Unexpected null label for some field of the record type %a" @@ -596,15 +595,13 @@ let mk_ty_decl (ty_c: DE.ty_cst) = ) dstrs [] in - let record_constr = Uid.of_term_cst cstr in - let ty = Ty.trecord ~record_constr tyvl uid lbs in + let ty = Ty.trecord ~record_constr:cstr tyvl ty_c lbs in Cache.store_ty ty_c ty | Some (Adt { cases; _ } as adt) -> Nest.attach_orders [adt]; - let uid = Uid.of_ty_cst ty_c in let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in - Cache.store_ty ty_c (Ty.t_adt uid tyvl); + Cache.store_ty ty_c (Ty.t_adt ty_c tyvl); let cs = Array.fold_right ( fun DE.{ cstr; dstrs; _ } accl -> @@ -613,21 +610,21 @@ let mk_ty_decl (ty_c: DE.ty_cst) = fun tc_o acc -> match tc_o with | Some (DE.{ id_ty; _ } as field) -> - (Uid.of_term_cst field, dty_to_ty id_ty) :: acc + (field, dty_to_ty id_ty) :: acc | None -> assert false ) dstrs [] in - (Uid.of_term_cst cstr, fields) :: accl + (cstr, fields) :: accl ) cases [] in - let ty = Ty.t_adt ~body:(Some cs) uid tyvl in + let ty = Ty.t_adt ~body:(Some cs) ty_c tyvl in Cache.store_ty ty_c ty | None | Some Abstract -> let ty_params = [] (* List.init ty_c.id_ty.arity (fun _ -> Ty.fresh_tvar ()) *) in - let ty = Ty.text ty_params (Uid.of_ty_cst ty_c) in + let ty = Ty.text ty_params ty_c in Cache.store_ty ty_c ty (** Handles term declaration by storing the eventual present type variables @@ -667,7 +664,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = match c with | Some (DE.{ id_ty; _ } as id) -> let pty = dty_to_ty id_ty in - (Uid.of_term_cst id, pty) :: acc + (id, pty) :: acc | _ -> Fmt.failwith "Unexpected null label for some field of the record type %a" @@ -688,11 +685,11 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = fun tc_o acc -> match tc_o with | Some (DE.{ id_ty; _ } as id) -> - (Uid.of_term_cst id, dty_to_ty id_ty) :: acc + (id, dty_to_ty id_ty) :: acc | None -> assert false ) dstrs [] in - (Uid.of_term_cst cstr, fields) :: accl + (cstr, fields) :: accl ) cases [] in let ty = Ty.t_adt ~body:(Some cs) hs tyl in @@ -723,14 +720,13 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = match tdef with | DE.Adt { cases; record; 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 record_constr = cases.(0).cstr in let ty = if (record || Array.length cases = 1) && not contains_adts then - Ty.trecord ~record_constr tyvl uid [] + Ty.trecord ~record_constr tyvl ty_c [] else - Ty.t_adt uid tyvl + Ty.t_adt ty_c tyvl in Cache.store_ty ty_c ty; (ty, Some adt) :: acc @@ -748,14 +744,14 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) = match term_descr with | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Uid.show id in + let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in let sy = Sy.Var v in Cache.store_sy ty_c sy; v, id, ty | Var ({ builtin = B.Base; id_ty; _ } as ty_v) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Uid.show id in + let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in let sy = Sy.Var v in Cache.store_sy ty_v sy; v, id, ty @@ -781,7 +777,7 @@ let mk_pattern DE.{ term_descr; _ } = Array.fold_right ( fun v acc -> match v with - | Some dstr -> Uid.of_term_cst dstr :: acc + | Some dstr -> dstr :: acc | _ -> assert false ) dstrs [] | _ -> @@ -799,10 +795,10 @@ let mk_pattern DE.{ term_descr; _ } = ) [] vnames pargs in let args = List.rev rev_args in - Typed.Constr {name = Uid.of_term_cst cst; args} + Typed.Constr {name = cst; args} | Cst ({ builtin = B.Constructor _; _ } as cst) -> - Typed.Constr {name = Uid.of_term_cst cst; args = []} + Typed.Constr {name = cst; args = []} | Var ({ builtin = B.Base; path; _ } as t_v) -> (* Should the type be passed as an argument @@ -924,7 +920,7 @@ let mk_add translate sy ty l = E.mk_term sy args ty let mk_rounding fpar = - let tcst = Uid.of_term_cst @@ Fpa_rounding.tcst_of_rounding_mode fpar in + let tcst = Fpa_rounding.tcst_of_rounding_mode fpar in let ty = Fpa_rounding.fpa_rounding_mode in E.mk_constr tcst [] ty @@ -961,7 +957,7 @@ let rec mk_expr | Trecord _ as ty -> E.mk_record [] ty | Tadt _ as ty -> - E.mk_constr (Uid.of_term_cst tcst) [] ty + E.mk_constr tcst [] ty | ty -> Fmt.failwith "unexpected type %a@." Ty.print ty end @@ -1006,9 +1002,9 @@ let rec mk_expr let sy = match Cache.find_ty adt with | Trecord _ -> - Sy.Op (Sy.Access (Uid.of_term_cst destr)) + Sy.Op (Sy.Access destr) | Tadt _ -> - Sy.destruct (Uid.of_term_cst destr) + Sy.destruct destr | _ -> assert false in E.mk_term sy [e] ty @@ -1028,7 +1024,6 @@ let rec mk_expr cstr = { builtin = B.Constructor { adt; _ }; _ } as cstr; _ }, [x] -> begin - let builtin = Sy.IsConstr (Uid.of_term_cst cstr) in let ty_c = match DT.definition adt with | Some ( @@ -1038,7 +1033,7 @@ let rec mk_expr in match Cache.find_ty ty_c with | Ty.Tadt _ -> - E.mk_builtin ~is_pos:true builtin [aux_mk_expr x] + E.mk_tester cstr (aux_mk_expr x) | Ty.Trecord _ -> (* The typechecker allows only testers whose the @@ -1314,7 +1309,7 @@ let rec mk_expr 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 + E.mk_constr tcst l ty | Ty.Trecord _ -> let l = List.map (fun t -> aux_mk_expr t) args in E.mk_record l ty diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 9c443c0f7..fca71829f 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -27,20 +27,21 @@ module Sy = Symbols module E = Expr +module DE = Dolmen.Std.Expr let src = Logs.Src.create ~doc:"Adt" __MODULE__ module Log = (val Logs.src_log src : Logs.LOG) type 'a abstract = | Constr of { - c_name : Uid.term_cst; + c_name : DE.term_cst; c_ty : Ty.t; - c_args : (Uid.term_cst * 'a) list + c_args : (DE.term_cst * 'a) list } (* [Cons { c_name; c_ty; c_args }] reprensents the application of the constructor [c_name] of the ADT [ty] with the arguments [c_args]. *) - | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a } + | Select of { d_name : DE.term_cst ; d_ty : Ty.t ; d_arg : 'a } (* [Select { d_name; d_ty; d_arg }] represents the destructor [d_name] of the ADT [d_ty] on the ADT value [d_arg]. *) @@ -67,7 +68,7 @@ let constr_of_destr ty dest = try List.find (fun { Ty.destrs; _ } -> - List.exists (fun (d, _) -> Uid.equal dest d) destrs + List.exists (fun (d, _) -> DE.Term.Const.equal dest d) destrs ) cases with Not_found -> assert false (* invariant *) end @@ -105,7 +106,7 @@ module Shostak (X : ALIEN) = struct | None -> Alien r let pp_field ppf (lbl, v) = - Fmt.pf ppf "%a : %a" Uid.pp lbl X.print v + Fmt.pf ppf "%a : %a" DE.Term.Const.print lbl X.print v let print ppf = function | Alien x -> @@ -113,11 +114,11 @@ module Shostak (X : ALIEN) = struct | Constr { c_name; c_args; _ } -> Fmt.pf ppf "%a@[(%a@])" - Uid.pp c_name + DE.Term.Const.print c_name Fmt.(list ~sep:semi pp_field) c_args | Select d -> - Fmt.pf ppf "%a#!!%a" X.print d.d_arg Uid.pp d.d_name + Fmt.pf ppf "%a#!!%a" X.print d.d_arg DE.Term.Const.print d.d_name let is_mine u = @@ -131,7 +132,8 @@ module Shostak (X : ALIEN) = struct match embed d_arg with | Constr c -> begin - try snd @@ List.find (fun (lbl, _) -> Uid.equal d_name lbl) c.c_args + try snd @@ List.find + (fun (lbl, _) -> DE.Term.Const.equal d_name lbl) c.c_args with Not_found -> Printer.print_err "is_mine %a failed" print u; assert false @@ -142,13 +144,13 @@ module Shostak (X : ALIEN) = struct match s1, s2 with | Alien r1, Alien r2 -> X.equal r1 r2 | Constr c1, Constr c2 -> - Uid.equal c1.c_name c2.c_name && + DE.Term.Const.equal c1.c_name c2.c_name && Ty.equal c1.c_ty c2.c_ty && begin try List.iter2 (fun (hs1, v1) (hs2, v2) -> - assert (Uid.equal hs1 hs2); + assert (DE.Term.Const.equal hs1 hs2); if not (X.equal v1 v2) then raise Exit ) c1.c_args c2.c_args; true @@ -158,7 +160,7 @@ module Shostak (X : ALIEN) = struct end | Select d1, Select d2 -> - Uid.equal d1.d_name d2.d_name && + DE.Term.Const.equal d1.d_name d2.d_name && Ty.equal d1.d_ty d2.d_ty && X.equal d1.d_arg d2.d_arg @@ -214,10 +216,10 @@ module Shostak (X : ALIEN) = struct | Constr { c_name ; c_ty ; c_args } -> List.fold_left (fun acc (_, r) -> acc * 7 + X.hash r) - (Uid.hash c_name + 7 * Ty.hash c_ty) c_args + (DE.Term.Const.hash c_name + 7 * Ty.hash c_ty) c_args | Select { d_name ; d_ty ; d_arg } -> - ((Uid.hash d_name + 11 * Ty.hash d_ty)) * 11 + X.hash d_arg + ((DE.Term.Const.hash d_name + 11 * Ty.hash d_ty)) * 11 + X.hash d_arg let leaves r = match r with @@ -263,7 +265,7 @@ module Shostak (X : ALIEN) = struct | _, Alien _ -> -1 | Constr c1, Constr c2 -> - let c = Uid.compare c1.c_name c2.c_name in + let c = DE.Term.Const.compare c1.c_name c2.c_name in if c <> 0 then c else let c = Ty.compare c1.c_ty c2.c_ty in @@ -273,7 +275,7 @@ module Shostak (X : ALIEN) = struct try List.iter2 (fun (hs1, v1) (hs2, v2) -> - assert (Uid.equal hs1 hs2); + assert (DE.Term.Const.equal hs1 hs2); let c = X.str_cmp v1 v2 in if c <> 0 then raise (Util.Cmp c); )c1.c_args c2.c_args; @@ -286,7 +288,7 @@ module Shostak (X : ALIEN) = struct | _, Constr _ -> -1 | Select d1, Select d2 -> - let c = Uid.compare d1.d_name d2.d_name in + let c = DE.Term.Const.compare d1.d_name d2.d_name in if c <> 0 then c else let c = Ty.compare d1.d_ty d2.d_ty in @@ -378,13 +380,14 @@ module Shostak (X : ALIEN) = struct Sig.{ pb with sbt = (r, r1) :: pb.sbt } | Constr c1, Constr c2 -> - if not (Uid.equal c1.c_name c2.c_name) then raise Util.Unsolvable; + if not (DE.Term.Const.equal c1.c_name c2.c_name) then + raise Util.Unsolvable; try Sig.{pb with eqs = List.fold_left2 (fun eqs (hs1, v1) (hs2, v2) -> - assert (Uid.equal hs1 hs2); + assert (DE.Term.Const.equal hs1 hs2); (v1, v2) :: eqs )pb.eqs c1.c_args c2.c_args } diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli index 2cd25de23..e81e50c05 100644 --- a/src/lib/reasoners/adt.mli +++ b/src/lib/reasoners/adt.mli @@ -29,12 +29,12 @@ val src : Logs.src type 'a abstract = | Constr of { - c_name : Uid.term_cst; + c_name : Dolmen.Std.Expr.term_cst; c_ty : Ty.t; - c_args : (Uid.term_cst * 'a) list + c_args : (Dolmen.Std.Expr.term_cst * 'a) list } - | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a } + | Select of { d_name : Dolmen.Std.Expr.term_cst ; d_ty : Ty.t ; d_arg : 'a } | Alien of 'a diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 91a37ecec..25a159b1f 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -46,7 +46,7 @@ module Log = (val Logs.src_log src : Logs.LOG) module TSet = Set.Make (struct - type t = Uid.term_cst + type t = DE.term_cst (* We use a dedicated total order on the constructors to ensure the termination of model generation. *) @@ -113,7 +113,7 @@ module Domain = struct let pp ppf d = Fmt.(braces @@ - iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs; + iter ~sep:comma TSet.iter DE.Term.Const.print) ppf d.constrs; if Options.(get_verbose () || get_unsat_core ()) then Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex @@ -173,7 +173,7 @@ module Domains = struct destructors of the constructor [c] by searching in the list [cases]. A better predicate will be easy to implement after getting rid of - the legacy frontend and switching from [Uid.t] to + the legacy frontend and switching from [DE.t] to [Dolmen.Std.Expr.term_cst] to store the constructors. Indeed, [term_cst] contains the type of constructor and in particular its arity. *) let is_enum_constr r c = @@ -270,7 +270,7 @@ let calc_destructor d e uf = let r, ex = Uf.find uf e in match Th.embed r with | Constr { c_args; _ } -> - begin match My_list.assoc Uid.equal d c_args with + begin match My_list.assoc DE.Term.Const.equal d c_args with | v -> Some (v, ex) | exception Not_found -> None end @@ -559,7 +559,7 @@ let constr_of_destr ty d = let r = List.find (fun Ty.{ destrs; _ } -> - List.exists (fun (d', _) -> Uid.equal d d') destrs + List.exists (fun (d', _) -> DE.Term.Const.equal d d') destrs ) cases in r.constr @@ -568,7 +568,7 @@ let constr_of_destr ty d = | _ -> assert false -exception Found of X.r * Uid.term_cst +exception Found of X.r * DE.term_cst let can_split env n = let m = Options.get_max_split () in diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index cb8e11700..bc6c2a452 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -27,10 +27,11 @@ module E = Expr module Sy = Symbols +module DE = Dolmen.Std.Expr type 'a abstract = - | Record of (Uid.term_cst * 'a abstract) list * Ty.t - | Access of Uid.term_cst * 'a abstract * Ty.t + | Record of (DE.term_cst * 'a abstract) list * Ty.t + | Access of DE.term_cst * 'a abstract * Ty.t | Other of 'a * Ty.t module type ALIEN = sig @@ -59,12 +60,12 @@ module Shostak (X : ALIEN) = struct let _ = List.fold_left (fun first (lb, e) -> Format.fprintf fmt "%s%a = %a" - (if first then "" else "; ") Uid.pp lb print e; + (if first then "" else "; ") DE.Term.Const.print lb print e; false ) true lbs in Format.fprintf fmt "}" | Access(a, e, _) -> - Format.fprintf fmt "%a.%a" print e Uid.pp a + Format.fprintf fmt "%a.%a" print e DE.Term.Const.print a | Other(t, _) -> X.print fmt t end @@ -79,11 +80,11 @@ module Shostak (X : ALIEN) = struct if c <> 0 then c else X.str_cmp u1 u2 | Other _, _ -> -1 | _, Other _ -> 1 - | Access (s1, u1, ty1), Access (s2, u2, ty2) -> + | Access (tcst1, u1, ty1), Access (tcst2, u2, ty2) -> let c = Ty.compare ty1 ty2 in if c <> 0 then c else - let c = Uid.compare s1 s2 in + let c = DE.Term.Const.compare tcst1 tcst2 in if c <> 0 then c else raw_compare u1 u2 | Access _, _ -> -1 @@ -107,11 +108,11 @@ module Shostak (X : ALIEN) = struct 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 -> + | (lb1, Access(lb2, x, _)) :: l when DE.Term.Const.equal lb1 lb2 -> if List.for_all (function | (lb1, Access(lb2, y, _)) -> - Uid.equal lb1 lb2 && raw_compare x y = 0 + DE.Term.Const.equal lb1 lb2 && raw_compare x y = 0 | _ -> false) l then x else Record (lbs_n, ty) @@ -120,7 +121,7 @@ module Shostak (X : ALIEN) = struct | Access (a, x, ty) -> begin match normalize x with - | Record (lbs, _) -> My_list.assoc Uid.equal a lbs + | Record (lbs, _) -> My_list.assoc DE.Term.Const.equal a lbs | x_n -> Access (a, x_n, ty) end | Other _ -> v @@ -140,7 +141,7 @@ module Shostak (X : ALIEN) = struct 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 + DE.Term.Const.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2 | Record (lbs1, ty1), Record (lbs2, ty2) -> Ty.equal ty1 ty2 && equal_list lbs1 lbs2 @@ -225,10 +226,10 @@ module Shostak (X : ALIEN) = struct let rec hash = function | Record (lbs, ty) -> List.fold_left - (fun h (lb, x) -> 17 * hash x + 13 * Uid.hash lb + h) + (fun h (lb, x) -> 17 * hash x + 13 * DE.Term.Const.hash lb + h) (Ty.hash ty) lbs | Access (a, x, ty) -> - 19 * hash x + 17 * Uid.hash a + Ty.hash ty + 19 * hash x + 17 * DE.Term.Const.hash a + Ty.hash ty | Other (x, ty) -> Ty.hash ty + 23 * X.hash x @@ -367,10 +368,10 @@ module Shostak (X : ALIEN) = struct | Record (l1, _), Record (l2, _) -> let eqs = List.fold_left2 - (fun eqs (a,b) (x,y) -> - assert (Uid.compare a x = 0); + (fun eqs (a, b) (x, y) -> + assert (DE.Term.Const.compare a x = 0); (is_mine y, is_mine b) :: eqs - )pb.eqs l1 l2 + ) pb.eqs l1 l2 in {pb with eqs=eqs} diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 1693c209c..ad9ad7962 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -31,6 +31,7 @@ module E = Expr module A = Xliteral module LR = Uf.LX module SE = Expr.Set +module DE = Dolmen.Std.Expr module Sy = Symbols @@ -153,6 +154,8 @@ module Main_Default : S = struct | _ -> mp ) st Hstring.Map.empty + module Ty_map = Map.Make (DE.Ty.Const) + let types_of_assumed sty = let open Ty in Ty.Set.fold @@ -162,25 +165,25 @@ module Main_Default : S = struct | Tvar _ -> assert false | Text (_, hs) | Trecord { name = hs; _ } when - Uid.Ty_map.mem hs mp -> mp + 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 + Ty_map.add hs (Text(l, hs)) mp | Trecord { name; _ } -> (* cannot do better for records ? *) - Uid.Ty_map.add name ty mp + Ty_map.add name ty mp | Tadt (hs, _) -> (* cannot do better for ADT ? *) - Uid.Ty_map.add hs ty mp - )sty Uid.Ty_map.empty + Ty_map.add hs ty mp + )sty Ty_map.empty let print_types_decls ?(header=true) types = let open Ty in print_dbg ~flushed:false ~header "@[(* types decls: *)@ "; - Uid.Ty_map.iter + Ty_map.iter (fun _ ty -> match ty with | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> () @@ -193,10 +196,10 @@ module Main_Default : S = struct | (lbl, ty)::l -> let print fmt (lbl,ty) = Format.fprintf fmt " ; %a :%a" - Uid.pp lbl Ty.print ty in + DE.Term.Const.print lbl Ty.print ty in print_dbg ~flushed:false ~header:false "{ %a : %a%a" - Uid.pp lbl Ty.print ty + DE.Term.Const.print lbl Ty.print ty (pp_list_no_space print) l; print_dbg ~flushed:false ~header:false " }@ " end diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 2cd2be58e..6ed300d81 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -26,6 +26,7 @@ (**************************************************************************) module Sy = Symbols +module DE = Dolmen.Std.Expr (** Data structures *) @@ -416,11 +417,11 @@ module SmtPrinter = struct Fmt.pf ppf "@[<2>(not@ %a@])" pp a | Sy.L_built (Sy.IsConstr hs), [e] -> - Fmt.pf ppf "@[<2>((_ is %a)@ %a@])" Uid.pp hs pp e + Fmt.pf ppf "@[<2>((_ is %a)@ %a@])" DE.Term.Const.print hs pp e | Sy.L_neg_built (Sy.IsConstr hs), [e] -> Fmt.pf ppf "(not @[<2>((_ is %a)@ %a@]))" - Uid.pp hs pp e + DE.Term.Const.print hs pp e | (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE) | Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE) @@ -449,7 +450,7 @@ module SmtPrinter = struct | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } -> assert (List.compare_lengths xs lbs = 0); Fmt.pf ppf "@[<2>(%a %a@])" - Uid.pp record_constr + DE.Term.Const.print record_constr Fmt.(list ~sep:sp pp |> box) xs | _ -> @@ -605,10 +606,10 @@ module AEPrinter = struct Fmt.pf ppf "(not %a)" pp a | Sy.L_built (Sy.IsConstr hs), [e] -> - Fmt.pf ppf "(%a ? %a)" pp e Uid.pp hs + Fmt.pf ppf "(%a ? %a)" pp e DE.Term.Const.print hs | Sy.L_neg_built (Sy.IsConstr hs), [e] -> - Fmt.pf ppf "not (%a ? %a)" pp e Uid.pp hs + Fmt.pf ppf "not (%a ? %a)" pp e DE.Term.Const.print hs | (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE) | Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE) @@ -646,7 +647,7 @@ module AEPrinter = struct 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 + Fmt.pf ppf "%a.%a" pp e DE.Term.Const.print field | Sy.(Op Record), _ -> begin match ty with @@ -655,7 +656,7 @@ module AEPrinter = struct 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; + DE.Term.Const.print field pp e; false ) true lbs xs); Fmt.pf ppf "}"; @@ -673,7 +674,7 @@ module AEPrinter = struct | Sy.(Op Destruct hs), [e] -> Fmt.pf ppf "%a#%a" - pp e Uid.pp hs + pp e DE.Term.Const.print hs | Sy.Op op, [e1; e2] -> Fmt.pf ppf "(%a %a %a)" pp e1 Symbols.pp_ae_operator op pp e2 @@ -1305,9 +1306,7 @@ let mk_tester 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 +let void = mk_constr Dolmen.Std.Expr.Term.Cstr.void [] Ty.tunit (** Substitutions *) @@ -2033,7 +2032,7 @@ module Triggers = struct | { f = Op (Access a1) ; xs=[t1]; _ }, { f = Op (Access a2) ; xs=[t2]; _ } -> - let c = Uid.compare a1 a2 in + let c = DE.Term.Const.compare a1 a2 in if c<>0 then c else cmp_trig_term t1 t2 | { f = Op (Access _); _ }, _ -> -1 @@ -2041,7 +2040,7 @@ module Triggers = struct | { f = Op (Destruct a1) ; xs = [t1]; _ }, { f = Op (Destruct a2) ; xs = [t2]; _ } -> - let c = Uid.compare a1 a2 in + let c = DE.Term.Const.compare a1 a2 in if c<>0 then c else cmp_trig_term t1 t2 | { f = Op (Destruct _); _ }, _ -> -1 @@ -2645,7 +2644,7 @@ let debug_compile_match e cases res = | Typed.Constr {name; args} -> Printer.print_dbg ~flushed:false ~header:false "| %a %a -> %a@ " - Uid.pp name + DE.Term.Const.print name p_list_vars args print v; | Typed.Var x -> @@ -2948,8 +2947,8 @@ let const_view t = end | { f = Op (Constr c); ty; _ } when Ty.equal ty Fpa_rounding.fpa_rounding_mode -> - let c = Uid.show c |> Hstring.make in - RoundingMode (Fpa_rounding.rounding_mode_of_smt_hs c) + let c = Fmt.str "%a" DE.Term.Const.print c in + RoundingMode (Fpa_rounding.rounding_mode_of_smt c) | _ -> Fmt.failwith "unsupported constant: %a" print t let int_view t = diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 7b30236e4..3204ca936 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -284,8 +284,8 @@ val mk_ite : t -> t -> t -> t (** smart constructor for datatypes. *) -val mk_constr : Uid.term_cst -> t list -> Ty.t -> t -val mk_tester : Uid.term_cst -> t -> t +val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t +val mk_tester : Dolmen.Std.Expr.term_cst -> t -> t val mk_record : t list -> Ty.t -> t (** Substitutions *) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index bfb0a4174..194a5730e 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -27,7 +27,6 @@ module DStd = Dolmen.Std module DE = DStd.Expr -module Hs = Hstring module Q = Numbers.Q module Z = Numbers.Z @@ -66,7 +65,6 @@ let to_ae_string = function | Down -> "Down" | NearestTiesToAway -> "NearestTiesToAway" - let fpa_rounding_mode_ae_type_name = "fpa_rounding_mode" let fpa_rounding_mode_type_name = "RoundingMode" @@ -74,14 +72,14 @@ let fpa_rounding_mode_type_name = "RoundingMode" (* The exported 'to string' function is the SMT one. *) let string_of_rounding_mode = to_smt_string -let hstring_smt_reprs = +let string_smt_reprs = List.map (fun c -> to_smt_string c, []) constrs -let hstring_ae_reprs = +let string_ae_reprs = List.map - (fun c -> Hs.make (to_ae_string c)) + (fun c -> to_ae_string c) constrs let get_basename = function @@ -113,8 +111,8 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode = def, constrs in Nest.attach_orders [def]; - let body = List.map (fun c -> Uid.of_term_cst c, []) d_constrs in - let ty = Ty.t_adt ~body:(Some body) (Uid.of_ty_cst ty_cst) [] in + let body = List.map (fun c -> c, []) d_constrs in + let ty = Ty.t_adt ~body:(Some body) ty_cst [] in let tcst_of_rounding_mode m = let name = string_of_rounding_mode m in let opt = @@ -129,37 +127,37 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode = in DE.Ty.apply ty_cst [], d_constrs, ty, tcst_of_rounding_mode -let rounding_mode_of_smt_hs = +let rounding_mode_of_smt = let table = Hashtbl.create 5 in List.iter2 ( fun (key, _) bnd -> Hashtbl.add table key bnd - ) hstring_smt_reprs constrs; + ) string_smt_reprs constrs; fun key -> - try Hashtbl.find table (Hstring.view key) with + try Hashtbl.find table key with | Not_found -> Fmt.failwith - "Error while searching for SMT2 FPA value %a." - Hstring.print key + "Error while searching for SMT2 FPA value %s." + key fpa_rounding_mode_type_name -let rounding_mode_of_ae_hs = +let rounding_mode_of_ae = let table = Hashtbl.create 5 in List.iter2 ( fun key bnd -> Hashtbl.add table key bnd - ) hstring_ae_reprs constrs; - fun key -> + ) string_ae_reprs constrs; + fun (key : string) -> try Hashtbl.find table key with | Not_found -> Fmt.failwith - "Error while searching for Legacy FPA value %a." - Hstring.print key + "Error while searching for Legacy FPA value %s." + key fpa_rounding_mode_type_name let translate_smt_rounding_mode hs = - match rounding_mode_of_smt_hs hs with - | res -> Some (Hstring.make (to_ae_string res)) + match rounding_mode_of_smt hs with + | res -> Some (to_ae_string res) | exception (Failure _) -> None (** Helper functions **) diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index 6b0a14557..ed032e196 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -51,21 +51,21 @@ val fpa_rounding_mode_ae_type_name : string val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.t (** The Dolmen constructors of [rounding_mode]. *) -val d_constrs : Uid.DE.term_cst list +val d_constrs : DE.term_cst list (** The rounding mode type. *) val fpa_rounding_mode : Ty.t -(** Transforms the Hstring corresponding to a RoundingMode element into +(** Transforms the string corresponding to a RoundingMode element into the [rounding_mode] equivalent. Raises 'Failure' if the string does not correspond to a valid rounding mode. *) -val rounding_mode_of_smt_hs : Hstring.t -> rounding_mode +val rounding_mode_of_smt : string -> rounding_mode (** Same, but for legacy's [rounding_mode] equivalent. *) -val rounding_mode_of_ae_hs : Hstring.t -> rounding_mode +val rounding_mode_of_ae : string -> rounding_mode (** Same, but from AE modes to SMT2 modes. *) -val translate_smt_rounding_mode : Hstring.t -> Hstring.t option +val translate_smt_rounding_mode : string -> string option (** Returns the string representation of the [rounding_mode] (SMT2 standard) *) val string_of_rounding_mode : rounding_mode -> string diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 902d33f94..87e47fb45 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -25,9 +25,11 @@ (* *) (**************************************************************************) +module DE = Dolmen.Std.Expr + type builtin = LE | LT (* arithmetic *) - | IsConstr of Uid.term_cst (* ADT tester *) + | IsConstr of DE.term_cst (* ADT tester *) | BVULE (* unsigned bit-vector arithmetic *) type operator = @@ -35,9 +37,9 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Uid.term_cst | Record - | Constr of Uid.term_cst (* enums, adts *) - | Destruct of Uid.term_cst + | Access of DE.term_cst | Record + | Constr of DE.term_cst (* enums, adts *) + | Destruct of DE.term_cst (* Arrays *) | Get | Set (* BV *) @@ -188,7 +190,7 @@ let compare_operators op1 op2 = (function | Access h1, Access h2 | Constr h1, Constr h2 | Destruct h1, Destruct h2 -> - Uid.compare h1 h2 + DE.Term.Const.compare h1 h2 | Extract (i1, j1), Extract (i2, j2) -> let r = Int.compare i1 i2 in if r = 0 then Int.compare j1 j2 else r @@ -213,7 +215,7 @@ let compare_operators op1 op2 = let compare_builtin b1 b2 = Util.compare_algebraic b1 b2 (function - | IsConstr h1, IsConstr h2 -> Uid.compare h1 h2 + | IsConstr tcst1, IsConstr tcst2 -> DE.Term.Const.compare tcst1 tcst2 | _, (LT | LE | BVULE | IsConstr _) -> assert false ) @@ -379,9 +381,9 @@ module AEPrinter = struct (* 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 + | Access tcst -> Fmt.pf ppf "@Access_%a" DE.Term.Const.print tcst + | Constr tcst + | Destruct tcst -> DE.Term.Const.print ppf tcst (* Float theory *) | Float -> Fmt.pf ppf "float" @@ -402,9 +404,9 @@ module AEPrinter = struct | L_built BVULE -> Fmt.pf ppf "<=" | L_neg_built BVULE -> Fmt.pf ppf ">" | L_built (IsConstr h) -> - Fmt.pf ppf "? %a" Uid.pp h + Fmt.pf ppf "? %a" DE.Term.Const.print h | L_neg_built (IsConstr h) -> - Fmt.pf ppf "?not? %a" Uid.pp h + Fmt.pf ppf "?not? %a" DE.Term.Const.print h let pp_form ppf f = match f with @@ -488,7 +490,8 @@ module SmtPrinter = struct (* DT theory *) | Record -> () - | Access s | Constr s | Destruct s -> Uid.pp ppf s + | Access tcst | Constr tcst | Destruct tcst -> + DE.Term.Const.print ppf tcst (* Float theory *) | Float -> Fmt.pf ppf "ae.round" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 145e72bc1..eb93fb3e7 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -27,7 +27,7 @@ type builtin = LE | LT (* arithmetic *) - | IsConstr of Uid.term_cst (* ADT tester *) + | IsConstr of Dolmen.Std.Expr.term_cst (* ADT tester *) | BVULE (* unsigned bit-vector arithmetic *) type operator = @@ -35,9 +35,9 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Uid.term_cst | Record - | Constr of Uid.term_cst (* enums, adts *) - | Destruct of Uid.term_cst + | Access of Dolmen.Std.Expr.term_cst | Record + | Constr of Dolmen.Std.Expr.term_cst (* enums, adts *) + | Destruct of Dolmen.Std.Expr.term_cst (* Arrays *) | Get | Set (* BV *) @@ -180,8 +180,8 @@ val var : Var.t -> t val int : string -> t val bitv : string -> t val real : string -> t -val constr : Uid.term_cst -> t -val destruct : Uid.term_cst -> t +val constr : Dolmen.Std.Expr.term_cst -> t +val destruct : Dolmen.Std.Expr.term_cst -> t val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound val mk_in : bound -> bound -> t val mk_maps_to : Var.t -> t diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 16740982f..31716e50a 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -25,24 +25,26 @@ (* *) (**************************************************************************) +module DE = Dolmen.Std.Expr + type t = | Tint | Treal | Tbool | Tvar of tvar | Tbitv of int - | Text of t list * Uid.ty_cst + | Text of t list * DE.ty_cst | Tfarray of t * t - | Tadt of Uid.ty_cst * t list + | Tadt of DE.ty_cst * t list | Trecord of trecord 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; + name : DE.ty_cst; + mutable lbs : (DE.term_cst * t) list; + record_constr : DE.term_cst; (* for ADTs that become records. default is "{" *) } @@ -55,10 +57,11 @@ module Smtlib = struct | 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 + | Trecord { args = []; name; _ } | Tadt (name, []) -> + DE.Ty.Const.print ppf name | Text (args, name) | Trecord { args; name; _ } | Tadt (name, args) -> - Fmt.(pf ppf "(@[%a %a@])" Uid.pp name (list ~sep:sp pp) args) + Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args) | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v | Tvar { value = Some t; _ } -> pp ppf t end @@ -69,8 +72,8 @@ exception TypeClash of t*t exception Shorten of t type adt_constr = - { constr : Uid.term_cst ; - destrs : (Uid.term_cst * t) list } + { constr : DE.term_cst ; + destrs : (DE.term_cst * t) list } type type_body = adt_constr list @@ -79,7 +82,7 @@ let assoc_destrs hs cases = try List.iter (fun {constr = s ; destrs = t} -> - if Uid.equal hs s then begin + if DE.Term.Const.equal hs s then begin res := Some t; raise Exit end @@ -104,7 +107,7 @@ let print_generic body_of = | 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 + fprintf fmt "%a %a" print_list l DE.Ty.Const.print n else (Hashtbl.add h v (); (*fprintf fmt "('a_%d->%a)" v print t *) @@ -113,28 +116,28 @@ let print_generic body_of = (*fprintf fmt "('a_%d->%a)" v print t *) print body_of fmt t | Text(l, s) when l == [] -> - fprintf fmt "%a" Uid.pp s + fprintf fmt "%a" DE.Ty.Const.print s | Text(l,s) -> - fprintf fmt "%a %a" print_list l Uid.pp s + fprintf fmt "%a %a" print_list l DE.Ty.Const.print 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; + fprintf fmt "%a %a" print_list lv DE.Ty.Const.print 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; + DE.Term.Const.print s (print body_of) t; first := false ) lbls; fprintf fmt "}" end end | Tadt (n, lv) -> - fprintf fmt "%a %a" print_list lv Uid.pp n; + fprintf fmt "%a %a" print_list lv DE.Ty.Const.print n; begin match body_of with | None -> () | Some type_body -> @@ -144,7 +147,7 @@ let print_generic body_of = List.iter (fun {constr = s ; destrs = t} -> fprintf fmt "%s%a%a" (if !first then "" else " | ") - Uid.pp s print_adt_tuple t; + DE.Term.Const.print s print_adt_tuple t; first := false ) cases; fprintf fmt "}" @@ -153,10 +156,10 @@ let print_generic body_of = and print_adt_tuple fmt = function | [] -> () | (d, e)::l -> - Format.fprintf fmt " of { %a : %a " Uid.pp d (print None) e; + Format.fprintf fmt " of { %a : %a " DE.Term.Const.print d (print None) e; List.iter (fun (d, e) -> - Format.fprintf fmt "; %a : %a " Uid.pp d (print None) e + Format.fprintf fmt "; %a : %a " DE.Term.Const.print d (print None) e ) l; Format.fprintf fmt "}" @@ -231,7 +234,7 @@ let rec compare t1 t2 = | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Int.compare v1 v2 | Tvar _, _ -> -1 | _ , Tvar _ -> 1 | Text(l1, s1) , Text(l2, s2) -> - let c = Uid.compare s1 s2 in + let c = DE.Ty.Const.compare s1 s2 in if c<>0 then c else compare_list l1 l2 | Text _, _ -> -1 | _ , Text _ -> 1 @@ -242,7 +245,7 @@ let rec compare t1 t2 = | 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 + let c = DE.Ty.Const.compare s1 s2 in if c <> 0 then c else let c = compare_list a1 a2 in if c <> 0 then c else @@ -251,7 +254,7 @@ let rec compare t1 t2 = | Trecord _, _ -> -1 | _ , Trecord _ -> 1 | Tadt (s1, pars1), Tadt (s2, pars2) -> - let c = Uid.compare s1 s2 in + let c = DE.Ty.Const.compare s1 s2 in if c <> 0 then c else compare_list pars1 pars2 (* no need to compare bodies *) @@ -282,7 +285,7 @@ let rec equal t1 t2 = match shorten t1 , shorten t2 with | Tvar{ v = v1; _ }, Tvar{ v = v2; _ } -> v1 = v2 | Text(l1, s1), Text(l2, s2) -> - (try Uid.equal s1 s2 && List.for_all2 equal l1 l2 + (try DE.Ty.Const.equal s1 s2 && List.for_all2 equal l1 l2 with Invalid_argument _ -> false) | Tfarray (ta1, ta2), Tfarray (tb1, tb2) -> equal ta1 tb1 && equal ta2 tb2 @@ -290,10 +293,10 @@ let rec equal t1 t2 = Trecord { args = a2; name = s2; lbs = l2; _ } -> begin try - Uid.equal s1 s2 && List.for_all2 equal a1 a2 && + DE.Ty.Const.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 + DE.Term.Const.equal l1 l2 && equal ty1 ty2) l1 l2 with Invalid_argument _ -> false end | Tint, Tint | Treal, Treal | Tbool, Tbool -> true @@ -301,7 +304,7 @@ let rec equal t1 t2 = | Tadt (s1, pars1), Tadt (s2, pars2) -> begin - try Uid.equal s1 s2 && List.for_all2 equal pars1 pars2 + try DE.Ty.Const.equal s1 s2 && List.for_all2 equal pars1 pars2 with Invalid_argument _ -> false (* no need to compare bodies *) end @@ -320,17 +323,17 @@ let rec matching s pat t = (try if not (equal (M.find n s) t) then raise (TypeClash(pat,t)); s with Not_found -> M.add n t s) | Tvar { value = _; _ }, _ -> raise (Shorten pat) - | Text (l1,s1) , Text (l2,s2) when Uid.equal s1 s2 -> + | Text (l1,s1) , Text (l2,s2) when DE.Ty.Const.equal s1 s2 -> 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 -> + | Trecord r1, Trecord r2 when DE.Ty.Const.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 DE.Ty.Const.equal n1 n2 -> List.fold_left2 matching s args1 args2 | _ , _ -> raise (TypeClash(pat,t)) @@ -418,7 +421,7 @@ let fresh_list lty subst = fresh_list (List.map shorten lty) subst module Decls = struct - module MH = Uid.Ty_map + module MH = Map.Make (DE.Ty.Const) module MTY = Map.Make(struct type ty = t @@ -501,7 +504,7 @@ module Decls = struct add name params cases; cases with Not_found -> - Printer.print_err "%a not found" Uid.pp name; + Printer.print_err "%a not found" DE.Ty.Const.print name; assert false let reinit () = decls := MH.empty @@ -523,7 +526,7 @@ let fresh_empty_text = let path = DStd.Path.global @@ Fmt.str "'_c%d" !cpt in DStd.Expr.Ty.Const.mk path 0 in - text [] (Uid.of_ty_cst id) + text [] id let t_adt ?(body=None) s ty_vars = let ty = Tadt (s, ty_vars) in @@ -546,49 +549,36 @@ let t_adt ?(body=None) s ty_vars = end; ty -module DE = Dolmen.Std.Expr - let tunit = let () = match Dolmen.Std.Expr.Ty.definition DE.Ty.Const.unit with | Some def -> Nest.attach_orders [def] | None -> assert false in - let void = Uid.of_term_cst DE.Term.Cstr.void in - let body = Some [void, []] in - let ty = t_adt ~body (Uid.of_ty_cst DE.Ty.Const.unit) [] in + let body = Some [DE.Term.Cstr.void, []] in + let ty = t_adt ~body 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 +let trecord ~record_constr lv name lbs = 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) + abs (List.fold_left (fun acc x-> acc*19 + hash x) (DE.Ty.Const.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 + | Trecord { args; name = s; _ } -> + (* We do not hash constructors. *) let h = - List.fold_left - (fun h (lb, ty) -> 23 * h + 19 * (Uid.hash lb) + hash ty) - (abs h) lbs + List.fold_left (fun h ty -> 27 * h + hash ty) (DE.Ty.Const.hash s) args in abs h - | Tadt (s, args) -> + | Tadt (ty, args) -> (* We do not hash constructors. *) let h = - List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args + List.fold_left (fun h ty -> 31 * h + hash ty) (DE.Ty.Const.hash ty) args in abs h diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 9b0a72db3..dbd03cd4a 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -42,7 +42,7 @@ type t = (** Type variables *) | Tbitv of int (** Bitvectors of a given length *) - | Text of t list * Uid.ty_cst + | Text of t list * Dolmen.Std.Expr.ty_cst (** Abstract types applied to arguments. [Text (args, s)] is the application of the abstract type constructor [s] to arguments [args]. *) @@ -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 Dolmen.Std.Expr.ty_cst * t list (** Application of algebraic data types. [Tadt (a, params)] denotes the application of the polymorphic datatype [a] to the types parameters [params]. @@ -77,22 +77,22 @@ and tvar = { and trecord = { mutable args : t list; (** Arguments passed to the record constructor *) - name : Uid.ty_cst; + name : Dolmen.Std.Expr.ty_cst; (** Name of the record type *) - mutable lbs : (Uid.term_cst * t) list; + mutable lbs : (Dolmen.Std.Expr.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_constr : Dolmen.Std.Expr.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 ; + { constr : Dolmen.Std.Expr.term_cst ; (** constructor of an ADT type *) - destrs : (Uid.term_cst * t) list + destrs : (Dolmen.Std.Expr.term_cst * t) list (** the list of destructors associated with the constructor and their respective types *) } @@ -109,12 +109,12 @@ module Set : Set.S with type elt = t (** Sets of types *) -val assoc_destrs : Uid.term_cst -> adt_constr list -> (Uid.term_cst * t) list +val assoc_destrs : Dolmen.Std.Expr.term_cst -> adt_constr list -> (Dolmen.Std.Expr.term_cst * t) list (** [assoc_destrs cons cases] returns the list of destructors associated with the constructor [cons] in the ADT defined by [cases]. @raises Not_found if the constructor is not in the given list. *) -val type_body : Uid.ty_cst -> t list -> type_body +val type_body : Dolmen.Std.Expr.ty_cst -> t list -> type_body (** {2 Type inspection} *) @@ -160,13 +160,13 @@ val fresh_tvar : unit -> t val fresh_empty_text : unit -> t (** Return a fesh abstract type. *) -val text : t list -> Uid.ty_cst -> t +val text : t list -> Dolmen.Std.Expr.ty_cst -> t (** Apply the abstract type constructor to the list of type arguments given. *) val t_adt : - ?body:((Uid.term_cst * (Uid.term_cst * t) list) list) option -> - Uid.ty_cst -> t list -> t + ?body:((Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list) option -> + Dolmen.Std.Expr.ty_cst -> 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, @@ -175,9 +175,8 @@ val t_adt : of arguments. *) val trecord : - ?sort_fields:bool -> - record_constr:Uid.term_cst -> - t list -> Uid.ty_cst -> (Uid.term_cst * t) list -> t + record_constr:Dolmen.Std.Expr.term_cst -> + t list -> Dolmen.Std.Expr.ty_cst -> (Dolmen.Std.Expr.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]. diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index eb2dc0381..168e7c8a0 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -27,6 +27,8 @@ (** Anotations (used by the GUI). *) +module DE = Dolmen.Std.Expr + type ('a, 'b) annoted = { c : 'a; annot : 'b } @@ -52,7 +54,7 @@ type oplogic = (** type of pattern in match construct of ADTs *) type pattern = - | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list} + | Constr of { name : DE.term_cst ; args : (Var.t * DE.term_cst * Ty.t) list} (** A pattern case which is a constructor. [name] is the name of constructor. [args] contains the variables bound by this pattern with their correponsing destructors and types *) @@ -264,7 +266,7 @@ let rec print_term = (fun (p, v) -> match p with | Constr {name = n; args = l} -> - fprintf fmt "| %a %a -> %a\n" Uid.pp n pp_vars l + fprintf fmt "| %a %a -> %a\n" DE.Term.Const.print n pp_vars l print_term v | Var x -> fprintf fmt "| %a -> %a\n" Var.print x print_term v; diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index 525e2712f..f23992689 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -72,7 +72,10 @@ type oplogic = (** Logic operators. *) type pattern = - | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list} + | Constr of { + name : Dolmen.Std.Expr.term_cst ; + args : (Var.t * Dolmen.Std.Expr.term_cst * Ty.t) list + } | Var of Var.t diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml deleted file mode 100644 index 2d352db0e..000000000 --- a/src/lib/structures/uid.ml +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2022-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 DStd = Dolmen.Std -module DE = Dolmen.Std.Expr - -type _ t = - | Term_cst : DE.term_cst -> DE.term_cst t - | Ty_cst : DE.ty_cst -> DE.ty_cst t - | Ty_var : DE.ty_var -> DE.ty_var t - -type term_cst = DE.term_cst t -type ty_cst = DE.ty_cst t -type ty_var = DE.ty_var t - -let order_tag : int DStd.Tag.t = DStd.Tag.create () - -let has_order_if_constr id = - let is_constr DE.{ builtin; _ } = - match builtin with - | DStd.Builtin.Constructor _ -> true - | _ -> false - in - let has_attached_order id = - DE.Term.Const.get_tag id order_tag |> Option.is_some - in - (not (is_constr id)) || has_attached_order id - -let[@inline always] of_term_cst id = - (* This assertion ensures that the API of the [Nest] module have been - correctly used, that is [Nest.attach_orders] have been called on - the nest of [id] if [id] is a constructor of ADT. *) - if not @@ has_order_if_constr id then - Fmt.invalid_arg "no order on %a" DE.Id.print id; - Term_cst id - -let[@inline always] of_ty_cst id = Ty_cst id -let[@inline always] of_ty_var id = Ty_var id - -let hash (type a) (u : a t) = - match u with - | Term_cst id -> DE.Id.hash id - | Ty_cst id -> DE.Id.hash id - | Ty_var id -> DE.Id.hash id - -let pp (type a) ppf (u : a t) = - match u with - | Term_cst id -> DE.Id.print ppf id - | Ty_cst id -> DE.Id.print ppf id - | Ty_var id -> DE.Id.print ppf id - -let show (type a) (u : a t) = Fmt.to_to_string pp u - -let equal (type a b) (u1 : a t) (u2 : b t) = - match u1, u2 with - | Term_cst id1, Term_cst id2 -> DE.Id.equal id1 id2 - | Ty_cst id1, Ty_cst id2 -> DE.Id.equal id1 id2 - | Ty_var id1, Ty_var id2 -> DE.Id.equal id1 id2 - | _ -> String.equal (show u1) (show u2) - -let compare (type a b) (u1 : a t) (u2 : b t) = - match u1, u2 with - | Term_cst id1, Term_cst id2 -> DE.Id.compare id1 id2 - | Ty_cst id1, Ty_cst id2 -> DE.Id.compare id1 id2 - | Ty_var id1, Ty_var id2 -> DE.Id.compare id1 id2 - | _ -> String.compare (show u1) (show u2) - -module Term_set = Set.Make - (struct - type nonrec t = term_cst - let compare = compare - end) - -module Ty_map = Map.Make - (struct - type nonrec t = ty_cst - let compare = compare - end) diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli deleted file mode 100644 index 501e8b88d..000000000 --- a/src/lib/structures/uid.mli +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- 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 DE = Dolmen.Std.Expr - -type _ t = private - | Term_cst : DE.term_cst -> DE.term_cst t - | Ty_cst : DE.ty_cst -> DE.ty_cst t - | Ty_var : DE.ty_var -> DE.ty_var t - -type term_cst = DE.term_cst t -type ty_cst = DE.ty_cst t -type ty_var = DE.ty_var t - -val of_term_cst : DE.term_cst -> term_cst -val of_ty_cst : DE.ty_cst -> ty_cst -val of_ty_var : DE.ty_var -> ty_var - -val hash : 'a t -> int -val pp : 'a t Fmt.t -val show : 'a t -> string -val equal : 'a t -> 'a t -> bool -val compare : 'a t -> 'a t -> int - -val order_tag : int Dolmen.Std.Tag.t -(** Tag used to attach the order of constructor. *) - -module Term_set : Set.S with type elt = term_cst -module Ty_map : Map.S with type key = ty_cst diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml index b11106e4e..b108422c2 100644 --- a/src/lib/structures/xliteral.ml +++ b/src/lib/structures/xliteral.ml @@ -25,9 +25,11 @@ (* *) (**************************************************************************) +module DE = Dolmen.Std.Expr + type builtin = Symbols.builtin = LE | LT | (* arithmetic *) - IsConstr of Uid.term_cst (* ADT tester *) + IsConstr of DE.term_cst (* ADT tester *) | BVULE (* unsigned bit-vector arithmetic *) type 'a view = @@ -126,9 +128,9 @@ let print_view ?(lbl="") pr_elt fmt vw = | Builtin (_, BVULE, _) -> assert false (* not reachable *) - | Builtin (pos, IsConstr hs, [e]) -> + | Builtin (pos, IsConstr tcst, [e]) -> Format.fprintf fmt "%s(%a ? %a)" - (if pos then "" else "not ") pr_elt e Uid.pp hs + (if pos then "" else "not ") pr_elt e DE.Term.Const.print tcst | Builtin (_, IsConstr _, _) -> assert false (* not reachable *) @@ -193,7 +195,7 @@ module Make (X : OrderedType) : S with type elt = X.t = struct let equal_builtins n1 n2 = match n1, n2 with | LT, LT | LE, LE -> true - | IsConstr h1, IsConstr h2 -> Uid.equal h1 h2 + | IsConstr tcst1, IsConstr tcst2 -> DE.Term.Const.equal tcst1 tcst2 | _ -> false module V = struct diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli index 4abdbd29b..8e7afe376 100644 --- a/src/lib/structures/xliteral.mli +++ b/src/lib/structures/xliteral.mli @@ -27,7 +27,7 @@ type builtin = Symbols.builtin = LE | LT | (* arithmetic *) - IsConstr of Uid.term_cst (* ADT tester *) + IsConstr of Dolmen.Std.Expr.term_cst (* ADT tester *) | BVULE (* unsigned bit-vector arithmetic *) type 'a view = (*private*) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 6a75ecd24..6b84e2ce0 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -153,6 +153,8 @@ let ty_cst_of_constr DE.{ builtin; _ } = | B.Constructor { adt; _ } -> adt | _ -> Fmt.failwith "expect an ADT constructor" +let order_tag : int DStd.Tag.t = DStd.Tag.create () + let attach_orders defs = let hp = build_graph defs in let r : (int * DE.term_cst list) H.t = H.create 17 in @@ -162,7 +164,7 @@ let attach_orders defs = let { id; outgoing; in_degree; _ } = Hp.pop_min hp in let ty = ty_cst_of_constr id in let o = H.add_constr r ty id in - DE.Term.Const.set_tag id Uid.order_tag o; + DE.Term.Const.set_tag id order_tag o; assert (in_degree = 0); List.iter (fun node -> @@ -175,14 +177,13 @@ let attach_orders defs = done let perfect_hash id = - match (id : _ Uid.t) with - | Term_cst ({ builtin = B.Constructor _; _ } as id) -> - begin match DE.Term.Const.get_tag id Uid.order_tag with + match (id : DE.term_cst) with + | { builtin = B.Constructor _; _ } as id -> + begin match DE.Term.Const.get_tag id order_tag with | Some h -> h | None -> (* Cannot occur as we eliminate this case in the smart constructor [Uid.of_term_cst]. *) assert false end - | Term_cst _ -> invalid_arg "Nest.perfect_hash" - | _ -> . + | _ -> invalid_arg "Nest.perfect_hash" diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index d8b30d862..c9e8ca74b 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -36,7 +36,7 @@ val attach_orders : DE.ty_def list -> unit (in any order). By nest, we mean the set of all the constructors in a mutually recursive definition of ADTs. *) -val perfect_hash : Uid.term_cst -> int +val perfect_hash : Dolmen.Std.Expr.term_cst -> int (** [perfect_hash u] returns an integer between [0] and [n] exclusive where [u] is a constructor and [n] is the number of constructors of the ADT of [u]. From da5d51c7e69d21dc40927abc32886130aa91ae15 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 8 Oct 2024 18:02:31 +0200 Subject: [PATCH 5/9] Too long lines --- src/lib/structures/ty.mli | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index dbd03cd4a..e56013129 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -109,7 +109,10 @@ module Set : Set.S with type elt = t (** Sets of types *) -val assoc_destrs : Dolmen.Std.Expr.term_cst -> adt_constr list -> (Dolmen.Std.Expr.term_cst * t) list +val assoc_destrs : + Dolmen.Std.Expr.term_cst -> + adt_constr list -> + (Dolmen.Std.Expr.term_cst * t) list (** [assoc_destrs cons cases] returns the list of destructors associated with the constructor [cons] in the ADT defined by [cases]. @raises Not_found if the constructor is not in the given list. *) @@ -165,8 +168,11 @@ val text : t list -> Dolmen.Std.Expr.ty_cst -> t given. *) val t_adt : - ?body:((Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list) option -> - Dolmen.Std.Expr.ty_cst -> t list -> t + ?body:((Dolmen.Std.Expr.term_cst * + (Dolmen.Std.Expr.term_cst * t) list) list) option -> + Dolmen.Std.Expr.ty_cst -> + 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, From e3a6539e6bcf1b45dee6bc8012cf00116fa56284 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 10:44:43 +0200 Subject: [PATCH 6/9] Use Compat.List.find_map --- src/lib/structures/fpa_rounding.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index 194a5730e..6d49e6491 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -116,7 +116,7 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode = let tcst_of_rounding_mode m = let name = string_of_rounding_mode m in let opt = - List.find_map + Compat.List.find_map (fun (DE.{ path; _ } as tcst) -> let n = get_basename path in if String.equal name n then Some tcst From 12175c70bf7626aec9576fa45c940b352612d0f3 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 11:06:59 +0200 Subject: [PATCH 7/9] More defensive programming! --- src/lib/reasoners/adt_rel.ml | 2 +- src/lib/structures/expr.ml | 19 ++++++++++++++++++- src/lib/structures/expr.mli | 8 ++++++++ src/lib/structures/ty.mli | 4 ++-- src/lib/util/nest.mli | 2 ++ 5 files changed, 31 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 25a159b1f..f156fd4da 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -173,7 +173,7 @@ module Domains = struct destructors of the constructor [c] by searching in the list [cases]. A better predicate will be easy to implement after getting rid of - the legacy frontend and switching from [DE.t] to + the legacy frontend and switching from [Uid.t] to [Dolmen.Std.Expr.term_cst] to store the constructors. Indeed, [term_cst] contains the type of constructor and in particular its arity. *) let is_enum_constr r c = diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 6ed300d81..7945afddd 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -27,6 +27,7 @@ module Sy = Symbols module DE = Dolmen.Std.Expr +module DStd = Dolmen.Std (** Data structures *) @@ -1299,7 +1300,23 @@ let mk_builtin ~is_pos n l = (** smart constructors for datatypes. *) -let mk_constr cons xs ty = mk_term (Sy.Op (Constr cons)) xs ty +let is_constr DE.{ builtin; _ } = + match builtin with + | DStd.Builtin.Constructor _ -> true + | _ -> false + +let has_attached_order id = + DE.Term.Const.get_tag id Nest.order_tag |> Option.is_some + +let mk_constr c xs ty = + if not @@ is_constr c then + Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c; + (* This assertion ensures that the API of the [Nest] module have been + correctly used, that is [Nest.attach_orders] have been called on + the nest of [id] if [id] is a constructor of ADT. *) + if not @@ has_attached_order c then + Fmt.invalid_arg "no order on constructor %a" DE.Id.print c; + mk_term (Sy.Op (Constr c)) xs ty let mk_tester cons t = mk_builtin ~is_pos:true (Sy.IsConstr cons) [t] diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 3204ca936..bdb726682 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -285,6 +285,14 @@ val mk_ite : t -> t -> t -> t (** smart constructor for datatypes. *) val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t +(** [mk_constr c args ty] converts the Dolmen constructor [c] into + an expression with arguments [args]. + + @raise Invalid_argument if [c] is not a Dolmen constructor. + + @raise Invalid_argument if no order have been attached to [c] with + [Nest.attach_orders]. *) + val mk_tester : Dolmen.Std.Expr.term_cst -> t -> t val mk_record : t list -> Ty.t -> t diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index e56013129..4bb69218b 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -220,8 +220,8 @@ val apply_subst : subst -> t -> t exception TypeClash of t * t (** Exception raised during matching. [TypeClash (u, v)] is raised when [u] and [v] could not be - matched or unified ([u] and [v] may be sub-types of the - types being actually unified or matched). *) + matched ([u] and [v] may be sub-types of the types being actually + matched). *) val matching : subst -> t -> t -> subst (** Matching of types (non-destructive). [matching pat t] returns a diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index c9e8ca74b..74c03c244 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -28,6 +28,8 @@ module DE = Dolmen.Std.Expr number of constructors. The total order on ADT constructors is given by the hash function. *) +val order_tag : int Dolmen.Std.Tag.t + val attach_orders : DE.ty_def list -> unit (** [attach_orders defs] generate and attach orders on the constructors for each ADT of [defs]. From a84dc94c5a05ae057a3008894edb9936b151948d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 11:22:14 +0200 Subject: [PATCH 8/9] clean up --- src/lib/structures/fpa_rounding.ml | 46 +++++++++++------------------ src/lib/structures/fpa_rounding.mli | 1 + 2 files changed, 18 insertions(+), 29 deletions(-) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index 6d49e6491..8d28fa6cc 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -58,6 +58,8 @@ let to_smt_string = | Down -> "RTN" | NearestTiesToAway -> "RNA" +let pp_rounding_mode = Fmt.of_to_string to_smt_string + let to_ae_string = function | NearestTiesToEven -> "NearestTiesToEven" | ToZero -> "ToZero" @@ -82,24 +84,9 @@ let string_ae_reprs = (fun c -> to_ae_string c) constrs -let get_basename = function - | DStd.Path.Local { name; } - | Absolute { name; path = []; } -> name - | Absolute { name; path; } -> - Fmt.failwith - "Expected an empty path to the basename: \"%s\" but got: [%a]." - name (fun fmt l -> - match l with - | h :: t -> - Format.fprintf fmt "%s" h; - List.iter (Format.fprintf fmt "; %s") t - | _ -> () - ) path - (* The rounding mode is the enum with the SMT values. The Alt-Ergo values are injected in this type. *) -let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode = - let module DStd = Dolmen.Std in +let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode = (* We may use the builtin type `DStd.Expr.Ty.roundingMode` here. *) let ty_cst = DE.Ty.Const.mk (DStd.Path.global "RoundingMode") 0 in let constrs = @@ -113,19 +100,20 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode = Nest.attach_orders [def]; let body = List.map (fun c -> c, []) d_constrs in let ty = Ty.t_adt ~body:(Some body) ty_cst [] in - let tcst_of_rounding_mode m = - let name = string_of_rounding_mode m in - let opt = - Compat.List.find_map - (fun (DE.{ path; _ } as tcst) -> - let n = get_basename path in - if String.equal name n then Some tcst - else None - ) d_constrs - in - match opt with Some o -> o | None -> assert false - in - DE.Ty.apply ty_cst [], d_constrs, ty, tcst_of_rounding_mode + DE.Ty.apply ty_cst [], d_constrs, ty + +let tcst_of_rounding_mode = + let table = Hashtbl.create 5 in + List.iter2 ( + fun key bnd -> + Hashtbl.add table key bnd + ) constrs d_constrs; + fun key -> + try Hashtbl.find table key with + | Not_found -> + Fmt.failwith + "Error while searching for mode %a." + pp_rounding_mode key let rounding_mode_of_smt = let table = Hashtbl.create 5 in diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index ed032e196..352f90b6e 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -70,6 +70,7 @@ val translate_smt_rounding_mode : string -> string option (** Returns the string representation of the [rounding_mode] (SMT2 standard) *) val string_of_rounding_mode : rounding_mode -> string +(** Returns the Dolmen constructor associated with the rounding mode. *) val tcst_of_rounding_mode : rounding_mode -> Dolmen.Std.Expr.term_cst (** Integer part of binary logarithm for NON-ZERO POSITIVE number **) From 8224c9d91ce7c36e7c507be4152c37dab57f4b71 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 12:17:11 +0200 Subject: [PATCH 9/9] Review changes --- src/lib/frontend/translate.ml | 6 +++--- src/lib/structures/fpa_rounding.ml | 2 +- src/lib/structures/fpa_rounding.mli | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 95effbb55..262eff96d 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -744,14 +744,14 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) = match term_descr with | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in + let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in let sy = Sy.Var v in Cache.store_sy ty_c sy; v, id, ty | Var ({ builtin = B.Base; id_ty; _ } as ty_v) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in + let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in let sy = Sy.Var v in Cache.store_sy ty_v sy; v, id, ty @@ -920,7 +920,7 @@ let mk_add translate sy ty l = E.mk_term sy args ty let mk_rounding fpar = - let tcst = Fpa_rounding.tcst_of_rounding_mode fpar in + let tcst = Fpa_rounding.term_cst_of_rounding_mode fpar in let ty = Fpa_rounding.fpa_rounding_mode in E.mk_constr tcst [] ty diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index 8d28fa6cc..26d87ac7e 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -102,7 +102,7 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode = let ty = Ty.t_adt ~body:(Some body) ty_cst [] in DE.Ty.apply ty_cst [], d_constrs, ty -let tcst_of_rounding_mode = +let term_cst_of_rounding_mode = let table = Hashtbl.create 5 in List.iter2 ( fun key bnd -> diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index 352f90b6e..85ad8b944 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -71,7 +71,7 @@ val translate_smt_rounding_mode : string -> string option val string_of_rounding_mode : rounding_mode -> string (** Returns the Dolmen constructor associated with the rounding mode. *) -val tcst_of_rounding_mode : rounding_mode -> Dolmen.Std.Expr.term_cst +val term_cst_of_rounding_mode : rounding_mode -> Dolmen.Std.Expr.term_cst (** Integer part of binary logarithm for NON-ZERO POSITIVE number **) val integer_log_2 : Numbers.Q.t -> int