Add an assertion in of_term_cst

Author: Halbaroth

src/lib/frontend/d_cnf.ml

@@ -587,10 +587,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 +614,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 =

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

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

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
   | _ -> .

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. *)