Module Types.Record

or_absent t adds the absent component to the type. This is an alias for cup t Absent.any or Absent.update t true.

The top type with the absent component set.

has_absent t tests the value of the absent component. Equivalent to non_empty (cap t Absent.any), but slightly more efficient.

has_record t returns true if and only if the record component of t is not empty. This is an alias for non_empty (cap Rec.any t).

split t l returns a list of pair of types. For each pair, the first component is the type of the label l in t and the second component is the type of the remaining labels in t, given as a record type.

split_normal t l returns the same list as split t l where the first components, that is, the types associated with l are pairwise disjoint.

project t l returns the type associted with the label l in the record component of type t. It is equivalent to :

• computing n = split t l
• computing s, the union of the first components of the list n
• checking whether the absent type is present in s

raises Not_found

if the resulting type may is absent (meaning that l is not necessarily present in t).

project_opt t l is similar to project t l but returns the type and erase the absent component if it is present. In other words, this function returns the the union of all the types associated to l for the records where it is present.

has_empty_record t returns true if and only if the record component of t contains a record with no label explicitely present for sure (that is there is a record r in t which has no explicit label (open or closed), or for which all explicit labels are associated with an absent type). { }, { ..}, { a=?Int b=?Any ..} are examples of such record types.

first_label t returns the first label (in the total ordering of label names) to appear explicitely in any of the records present in t. The function returns Label.dummy if no such label exists.

has_empty_cases t must only be called on types whose record component have no explicit labels. It returns a pair of boolean (some, none), where:

• some is true if and only if the record component is open
• none is true if and only if the type is non empty.

In otherwords :

• true, true indicates that the record component of t contains { ..}
• false, true indicates that the record component of t contains only {}
• false, false indicates that the record component of t is empty.
• true, false is not possible.

merge t1 t2 discards the non record component of t1 and t2 and returns the type of the + operators on records, that is, returns a record type t where the type of label l is the one of t2 if it is present in t2 and the type of t1 otherwise.

remove_field t l returns the type of type t where the label l is marked as explicitely absent from t. There are two ways to do that:

• for closed record types, the label l is simply removed, if present
• for open record types, the type is intersected with {l=?Empty} meaning that either the label l is absent, or if present it is associated to the empty type, that is, if it is present, the whole record is empty.

get t returns a list whose union is the record component of t. Each element of the list is a triple (map, op, none) where map is a map from labels to pairs of a boolean indicating whether the label is optional or not and t the associated (non absent) type. The boolean op indicates whether the record is open. The boolean none is always true and is here for compatibility reasons with other parts of the ℂDuce compiler which return a similar type where none can be false, indicating an empty component. Such components are not returned by get.

The abstract type representing a normalized form for records.

focus d l prepares a normal form where the types associated to l have been isolated.

get_this t returns the type associated with label l. Doing get_this (focus t l) is equivalent to project_opt t l.

need_others t returns true if and only if the focused label yields two distinct types. For instance, focusing t= {x = Int; y = Int } | {x = Bool; y = Int } on x, get_this t yields Int | Bool, and need_other t yields false, since the projection can be represented as a single pair : [ (Int|Bool, { y = Int }) ] .

On the other hand, focusing t= {x = Char; y = Bool } | {x = Bool; y = Int} on x, get_this t yields Char | Bool, and need_other t yields true, since the projection cannot be represented as a single pair : [(Char, { y = Bool }); (Bool, { y= Int }) ] .

constraint_on_others t cstr returns the intersection of all record types for which the type of the focused label has a non-empty intersection with cstr.