Distinguish [OCSTRUCTURE] and [OSTRUCTURE].

This is not essential, but allows making the input signature of
[OccursCheck.Make] more precise.
This commit is contained in:
François Pottier 2022-01-27 17:26:26 +01:00
parent 1ae78bf033
commit 72aa92ec62
3 changed files with 18 additions and 12 deletions

View File

@ -12,7 +12,7 @@
open Signatures
module Make
(S : OSTRUCTURE)
(S : OCSTRUCTURE)
(U : MUNIFIER with type 'a structure = 'a S.structure)
= struct

View File

@ -11,8 +11,10 @@
open Signatures
(**This module reads the data structure maintained by the unifier and offers
an {i occurs check}, that is, a cycle detection algorithm. *)
module Make
(S : sig (** @inline *) include OSTRUCTURE end)
(S : sig (** @inline *) include OCSTRUCTURE end)
(U : sig (** @inline *) include MUNIFIER
with type 'a structure = 'a S.structure end)
: sig (** @inline *) include OCCURS_CHECK

View File

@ -91,14 +91,9 @@ module type USTRUCTURE = sig
end
(* [OSTRUCTURE] describes an input of [OccursCheck.Make]
and [Decoder.Make]. *)
(* [OCSTRUCTURE] describes an input of [OccursCheck.Make]. *)
(* We could in fact distinguish two signatures, since these two
functors do not have exactly the same requirements, but the
need has not yet arisen. *)
module type OSTRUCTURE = sig
module type OCSTRUCTURE = sig
(** @inline *)
include SSTRUCTURE
@ -106,13 +101,22 @@ module type OSTRUCTURE = sig
(**[iter] applies an action to every child of a structure. *)
val iter: ('a -> unit) -> 'a structure -> unit
(**[id] extracts the unique identifier of a structure. *)
val id: 'a structure -> id
end
(* [OSTRUCTURE] describes an input of [Decoder.Make]. *)
module type OSTRUCTURE = sig
(** @inline *)
include OCSTRUCTURE
(**[map] applies a transformation to the children of a structure,
while preserving the shape of the structure. *)
val map: ('a -> 'b) -> 'a structure -> 'b structure
(**[id] extracts the unique identifier of a structure. *)
val id: 'a structure -> id
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
whether it represents the absence of a logical constraint. This function
is typically used by a decoder to determine which equivalence classes