In the context of #4, we realized that the normal form for field types is:

$$ \begin{array}{c} \bigvee\bigwedge \theta_1\wedge\ldots\theta_n\wedge\lnot\theta'_1\wedge\lnot\ldots\theta'_k\wedge t\\ \vee\\ \bigvee\bigwedge \theta_1\wedge\ldots\theta_n\wedge\lnot\theta'_1\wedge\lnot\ldots\theta'_k\wedge \bot\\ \end{array} $$

(It's a generalization of the previous representation $t\vee\bot$ where field variables $\theta$ may occur at top-level).
The natural representation would be a pair of Bdds. The obvious solution would be:

module FieldTy (N : Node) = struct (* replaces OTy *)
   
   module BTy = Bdd.Make(FieldVar)(N)    (* ← does not work *)
   module BUndef = Bdd.Make(FieldVar)(Bdd.BoolLeaf)

   type t = BTy.t * BUndef.t
   ...

This does not work, since Node does not implement the Leaf signature properly (in particular it has any: unit -> t instead of any : t. Patching node locally with

struct 
   include N
   let any = any ()
   let empty = empty ()
end

does not work since it fails at runtime while initializing the recursive module cycle (when any() is called during module initialization, it is still the dummy stub).

I see two solutions

Solution 1: use VDescr instead of N

Don't use N for the leaf but a module equivalent to VDescr (which is not directly visible from records.ml).

module FieldVar =
struct
  include Id.NamedIdentifier ()
  let simplify t = t
end

module FieldTy(N:Node) = struct
  type node = N.t
  module BTy = Bdd.Make(FieldVar)(Vdescr.Make(N))
  module BUndef = Bdd.Make (FieldVar)(Bdd.BoolLeaf)
 
  type t = BTy.t * BUndef.t

  let any () = (BTy.any, BUndef.any) (* 𝟙∨⊥ *)
  let empty () = (BTy.any, BUndef.empty) (* 𝟘 *)
  let absent () = (BTy.empty, BUndef.any) (* ⊥ *)
  let required t = (N.def t, BUndef.empty)
  let optional t = (N.def t, BUndef.any)
  let get (t,_) = t
  (* cap/cup/neg/not are all done component wise *)

This work but feels slightly off. E.g. we "skip a step" in is_empty since we don't call N.is_empty so we skip a chance to memoize etc… It might also make writing the tallying (as well as operations on records such as get_field) more awkward. This might not be a problem since tallying of these fields will be different also.

Solution 2: Make N implement Leaf properly

I can do it in a self contained way (meaning with code leaving only in node.ml). It involves putting the type Node.Node.t (the mutable record) outside of Node. Last time I check it did not break anything outside of records (to use any instead of any ()).

Non solutions

We could duplicate Bdd to work on leafs that have any (), but we would also need to do it for Dnf I think, and it feels very wrong.

What do you think?