(** Smart constructors for {!type:Syntax.endo}. *)
module Endo :
sig

  (** Parameters of smart constructors. *)
  module type Param =
  sig
    (** The interval algebra. *)
    type dim

    (** The type that embeds cofibrations. *)
    type cof

    (** The element 0 in the interval algebra. *)
    val dim0 : dim

* The element 1 in the interval algebra .
    val dim1 : dim

    (** Equality checker for elements in the interval algebra. *)
    val equal_dim : dim -> dim -> bool

    (** The embedding of cofibrations into [cof]. *)
    val cof : (dim, cof) Syntax.endo -> cof

    (** Extract the embedded cofibration, if any. *)
    val uncof : cof -> (dim, cof) Syntax.endo option
  end

  (** The signature of smart constructors. *)
  module type S =
  sig
    (** The interval algebra. *)
    type dim

    (** The type that embeds cofibrations. *)
    type cof

    (** The embedding of cofibrations to [cof]. *)
    val cof : (dim, cof) Syntax.endo -> cof

* Smarter version of { !  : Syntax . Endo.le } .
    val le : dim -> dim -> cof

    (** The bottom cofibration. *)
    val bot : cof

    (** The top cofibration. *)
    val top : cof

* Smarter version of { !  : Syntax . Endo.join } that simplifies cofibrations using syntactic criteria . 
         For example , [ join [ meet [ ] ] ] gives [ cof ( Meet [ ] ) ] . 

         Note that the simplification is attempting to strike a balance between optimality and efficiency , 
         and thus it will not perform all possible syntactic reduction . To obtain more reduced cofibrations , 
         use only smart constructors ( instead of raw constructors ) to build cofibrations . 
    
        For example, [join [meet []]] gives [cof (Meet [])].

        Note that the simplification is attempting to strike a balance between optimality and efficiency,
        and thus it will not perform all possible syntactic reduction. To obtain more reduced cofibrations,
        use only smart constructors (instead of raw constructors) to build cofibrations.
    *)
    val join : cof list -> cof

* Smarter version of { !  : Syntax . Endo.meet } that simplifies cofibrations using syntactic criteria . 
         See { !  : join } .
        See {!val:join}. *)
    val meet : cof list -> cof

* [ eq ] is equivalent to [ meet [ le x y ;    ] ] .
    val eq : dim -> dim -> cof

    (** [eq0 r] is equivalent to [eq r dim0]. *)
    val eq0 : dim -> cof

* [ eq1 r ] is equivalent to [ eq r dim1 ] .
    val eq1 : dim -> cof

    (** [boundary r] is equivalent to [join [eq0 r; eq1 r]]. *)
    val boundary : dim -> cof

* [ forall ( r , cof ) ] computes [ forall   ] , using the syntactic quantifier elimination 
         and potentially other simplification procedures used in { !  : le } , { !  : join } , and { !  : meet } . 

         Note : [ r ] can not be [ dim0 ] or [ dim1 ] . 
    
        and potentially other simplification procedures used in {!val:le}, {!val:join}, and {!val:meet}.

        Note: [r] cannot be [dim0] or [dim1].
    *)
    val forall : dim * cof -> cof
  end

  (** The implementation of smart constructors. *)
  module Make (P : Param) : S with type dim = P.dim and type cof = P.cof
end

(** Smart constructors for {!type:Syntax.free}. *)
module Free :
sig

  (** Parameters of smart constructors. *)
  module type Param =
  sig
    (** The interval algebra. *)
    type dim

    (** The type of cofibration variables. *)
    type var

    (** The element 0 in the interval algebra. *)
    val dim0 : dim

* The element 1 in the interval algebra .
    val dim1 : dim

    (** Equality checker for elements of the interval algebra. *)
    val equal_dim : dim -> dim -> bool
  end

  (** The signature of smart constructors. *)
  module type S =
  sig
    (** The interval algebra. *)
    type dim

    (** The type of cofibration variables. *)
    type var

    (** The type of freely generated cofibrations. *)
    type cof = (dim, var) Syntax.free

*  of { !  : Syntax . Free.var } .
    val var : var -> cof

    (** @open *)
    include Endo.S with type dim := dim and type cof := cof
  end

  (** The implementation of smart constructors. *)
  module Make (P : Param) : S with type dim = P.dim and type var = P.var
end

* Smart constructors for {!type:Syntax.endo}. 
* Parameters of smart constructors. 
* The interval algebra. 
* The type that embeds cofibrations. 
* The element 0 in the interval algebra. 
* Equality checker for elements in the interval algebra. 
* The embedding of cofibrations into [cof]. 
* Extract the embedded cofibration, if any. 
* The signature of smart constructors. 
* The interval algebra. 
* The type that embeds cofibrations. 
* The embedding of cofibrations to [cof]. 
* The bottom cofibration. 
* The top cofibration. 
* [eq0 r] is equivalent to [eq r dim0]. 
* [boundary r] is equivalent to [join [eq0 r; eq1 r]]. 
* The implementation of smart constructors. 
* Smart constructors for {!type:Syntax.free}. 
* Parameters of smart constructors. 
* The interval algebra. 
* The type of cofibration variables. 
* The element 0 in the interval algebra. 
* Equality checker for elements of the interval algebra. 
* The signature of smart constructors. 
* The interval algebra. 
* The type of cofibration variables. 
* The type of freely generated cofibrations. 
* @open 
* The implementation of smart constructors. 
module Endo :
sig

  module type Param =
  sig
    type dim

    type cof

    val dim0 : dim

* The element 1 in the interval algebra .
    val dim1 : dim

    val equal_dim : dim -> dim -> bool

    val cof : (dim, cof) Syntax.endo -> cof

    val uncof : cof -> (dim, cof) Syntax.endo option
  end

  module type S =
  sig
    type dim

    type cof

    val cof : (dim, cof) Syntax.endo -> cof

* Smarter version of { !  : Syntax . Endo.le } .
    val le : dim -> dim -> cof

    val bot : cof

    val top : cof

* Smarter version of { !  : Syntax . Endo.join } that simplifies cofibrations using syntactic criteria . 
         For example , [ join [ meet [ ] ] ] gives [ cof ( Meet [ ] ) ] . 

         Note that the simplification is attempting to strike a balance between optimality and efficiency , 
         and thus it will not perform all possible syntactic reduction . To obtain more reduced cofibrations , 
         use only smart constructors ( instead of raw constructors ) to build cofibrations . 
    
        For example, [join [meet []]] gives [cof (Meet [])].

        Note that the simplification is attempting to strike a balance between optimality and efficiency,
        and thus it will not perform all possible syntactic reduction. To obtain more reduced cofibrations,
        use only smart constructors (instead of raw constructors) to build cofibrations.
    *)
    val join : cof list -> cof

* Smarter version of { !  : Syntax . Endo.meet } that simplifies cofibrations using syntactic criteria . 
         See { !  : join } .
        See {!val:join}. *)
    val meet : cof list -> cof

* [ eq ] is equivalent to [ meet [ le x y ;    ] ] .
    val eq : dim -> dim -> cof

    val eq0 : dim -> cof

* [ eq1 r ] is equivalent to [ eq r dim1 ] .
    val eq1 : dim -> cof

    val boundary : dim -> cof

* [ forall ( r , cof ) ] computes [ forall   ] , using the syntactic quantifier elimination 
         and potentially other simplification procedures used in { !  : le } , { !  : join } , and { !  : meet } . 

         Note : [ r ] can not be [ dim0 ] or [ dim1 ] . 
    
        and potentially other simplification procedures used in {!val:le}, {!val:join}, and {!val:meet}.

        Note: [r] cannot be [dim0] or [dim1].
    *)
    val forall : dim * cof -> cof
  end

  module Make (P : Param) : S with type dim = P.dim and type cof = P.cof
end

module Free :
sig

  module type Param =
  sig
    type dim

    type var

    val dim0 : dim

* The element 1 in the interval algebra .
    val dim1 : dim

    val equal_dim : dim -> dim -> bool
  end

  module type S =
  sig
    type dim

    type var

    type cof = (dim, var) Syntax.free

*  of { !  : Syntax . Free.var } .
    val var : var -> cof

    include Endo.S with type dim := dim and type cof := cof
  end

  module Make (P : Param) : S with type dim = P.dim and type var = P.var
end
