From ff87e7ea2f72ef166a1ebfde5a08b2dafc357ab6 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 10 Jul 2024 15:40:35 +0200 Subject: [PATCH] Add an assertion in `of_term_cst` --- src/lib/frontend/d_cnf.ml | 24 ++++++++++++------------ src/lib/structures/uid.ml | 26 ++++++++++++++++++++------ src/lib/structures/uid.mli | 5 +++-- src/lib/util/nest.ml | 17 ++++++++++------- src/lib/util/nest.mli | 5 +++++ 5 files changed, 50 insertions(+), 27 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 177844380..0b79d053a 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -101,22 +101,20 @@ module Cache = struct let find_ty id = HT.find ae_ty_ht (Id id) - let fresh_ty ?(is_var = true) ?id () = + let fresh_ty ?(is_var = true) ?(name = None) () = if is_var then Ty.fresh_tvar () else - match id with - | Some id -> Ty.text [] (Uid.of_string id) + match name with + | Some n -> Ty.text [] (Uid.of_string n) | None -> Ty.fresh_empty_text () - let show (type a) (id : a DE.id) = Fmt.to_to_string DE.Id.print id - - let update_ty_store ?(is_var = true) id = - let ty = fresh_ty ~is_var ~id:(show id) () in + let update_ty_store ?(is_var = true) ?name id = + let ty = fresh_ty ~is_var ~name () in store_ty id ty - let update_ty_store_ret ?(is_var = true) id = - let ty = fresh_ty ~is_var ~id:(show id) () in + let update_ty_store_ret ?(is_var = true) ?name id = + let ty = fresh_ty ~is_var ~name () in store_ty id ty; ty @@ -127,7 +125,8 @@ module Cache = struct update_ty_store_ret ~is_var id let store_tyv ?(is_var = true) t_v = - update_ty_store ~is_var t_v + let name = get_basename t_v.DE.path in + update_ty_store ~is_var ~name t_v let store_tyvl ?(is_var = true) (tyvl: DE.ty_var list) = List.iter (store_tyv ~is_var) tyvl @@ -587,10 +586,11 @@ and handle_ty_app ?(update = false) ty_c l = let mk_ty_decl (ty_c: DE.ty_cst) = match DT.definition ty_c with | Some ( - Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } + (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 rev_lbs = @@ -613,8 +613,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) = Cache.store_ty ty_c ty | Some (Adt { cases; _ } as adt) -> - let uid = Uid.of_ty_cst ty_c in 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); let rev_cs = diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml index cbd2fa3ae..c2647eb63 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -38,17 +38,31 @@ type term_cst = DE.term_cst t type ty_cst = DE.ty_cst t type ty_var = DE.ty_var t -let[@inline always] of_term_cst id = Term_cst id +let order_tag : int DStd.Tag.t = DStd.Tag.create () + +let has_order id = + let is_cstr 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_cstr 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 id then Fmt.failwith "not 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[@inline always] of_hstring hs = Hstring hs let[@inline always] of_string s = of_hstring @@ Hstring.make s -let[@inline always] to_term_cst id = - match id with - | Term_cst t -> t - | _ -> invalid_arg "to_term_cst" - let hash (type a) (u : a t) = match u with | Hstring hs -> Hstring.hash hs diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index e500dfcb4..11d6570ed 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -43,13 +43,14 @@ val of_ty_var : DE.ty_var -> ty_var val of_string : string -> 'a t val of_hstring : Hstring.t -> 'a t -val to_term_cst : term_cst -> DE.term_cst - 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/util/nest.ml b/src/lib/util/nest.ml index b0cbf951c..d497553ea 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -153,10 +153,6 @@ let ty_cst_of_cstr DE.{ builtin; _ } = | B.Constructor { adt; _ } -> adt | _ -> Fmt.failwith "expect an ADT constructor" -(** Tag used to attach the order of constructor. Used to - retrieve efficiency the order of the constructor in [to_int]. *) -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 @@ -166,7 +162,7 @@ let attach_orders defs = let { id; outgoing; in_degree; _ } = Hp.pop_min hp in let ty = ty_cst_of_cstr id in let o = H.add_cstr r ty id in - DE.Term.Const.set_tag id order_tag o; + DE.Term.Const.set_tag id Uid.order_tag o; assert (in_degree = 0); List.iter (fun node -> @@ -180,8 +176,15 @@ let attach_orders defs = let perfect_hash id = match (id : _ Uid.t) with - | Term_cst id -> - Option.get @@ DE.Term.Const.get_tag id order_tag + | Term_cst ({ builtin = B.Constructor _; _ } as id) -> + begin match DE.Term.Const.get_tag id Uid.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" | Hstring hs -> Hstring.hash hs | _ -> . diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index 998a7c255..d8b30d862 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -37,3 +37,8 @@ val attach_orders : DE.ty_def list -> unit mutually recursive definition of ADTs. *) val perfect_hash : Uid.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]. + + @raise Invalid_arg if [u] is not a constructor. *)