From fd6d11fee8ab1559c2cb1d95253b7a44d567c8e8 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 22 Dec 2023 14:24:27 +0100 Subject: [PATCH] Move typed symbols from ModelMap to Id --- src/lib/structures/id.ml | 2 ++ src/lib/structures/id.mli | 7 +++++++ src/lib/structures/modelMap.ml | 6 ++---- src/lib/structures/modelMap.mli | 8 +------- 4 files changed, 12 insertions(+), 11 deletions(-) diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index e34de223f..e6d8a74f3 100644 --- a/src/lib/structures/id.ml +++ b/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 = diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 0b2434918..a011bd36e 100644 --- a/src/lib/structures/id.mli +++ b/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 diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 2b7fb096f..e28af0ef3 100644 --- a/src/lib/structures/modelMap.ml +++ b/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 = { diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index 9d8e9f0ec..b0f90b7f1 100644 --- a/src/lib/structures/modelMap.mli +++ b/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]. *)