Move typed symbols from ModelMap to Id

src/lib/structures/id.ml

@@ -30,6 +30,8 @@
 
 type t = Hstring.t [@@deriving ord]
 
+type typed = t * Ty.t list * Ty.t [@@deriving ord]
+
 let equal = Hstring.equal
 
 let pp ppf id =

src/lib/structures/id.mli

@@ -30,6 +30,13 @@
 
 type t = Hstring.t [@@deriving ord]
 
+type typed = t * Ty.t list * Ty.t
+(** Typed identifier of function. In order:
+    - The identifier.
+    - Types of its arguments.
+    - The returned type. *)
+
+val compare_typed : typed -> typed -> int
 val equal : t -> t -> bool
 val show : t -> string
 val pp : t Fmt.t

src/lib/structures/modelMap.ml

@@ -31,8 +31,6 @@
 module X = Shostak.Combine
 module Sy = Symbols
 
-type sy = Id.t * Ty.t list * Ty.t [@@deriving ord]
-
 module Graph = struct
   module M = Map.Make
       (struct
@@ -113,9 +111,9 @@ end
 
 module P = Map.Make
     (struct
-      type t = sy
+      type t = Id.typed
 
-      let compare = compare_sy
+      let compare = Id.compare_typed
     end)
 
 type t = {

src/lib/structures/modelMap.mli

@@ -28,16 +28,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type sy = Id.t * Ty.t list * Ty.t
-(** Typed symbol of function defined in the model. In order:
-    - The identifier of the symbol.
-    - The types of its arguments.
-    - The returned type. *)
-
 type t
 (** Type of model. *)
 
-val add : sy -> Expr.t list -> Expr.t -> t -> t
+val add : Id.typed -> Expr.t list -> Expr.t -> t -> t
 (** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph
     associated with the symbol [sy]. *)