File "src/Theory/FNITheory.ml", line 3, characters 103-597:
Error: Signature mismatch:
       ...
       In module T.Var:
       Type declarations do not match:
         type t = TheoryUtils.Make_Term(Var)(TT).Var.t
       is not included in
         type t = Var.t





(* TheoryInterface.mli *)

open Types

(** Theory interface *)

module type THEORY_TERM = Hashtbl.HashedType

module type TERM = sig
  module Var : Variable.S
  module TT : THEORY_TERM
  include Hashtbl.HashedType with type t = (Var.t, TT.t) term
end

module type THEORY_ATOM = Hashtbl.HashedType

module type ATOM = sig
  module T : TERM
  module TA : THEORY_ATOM
  include Variable.S with type t = (T.t, TA.t) atom
end

module type THEORY = sig
  module Var : Variable.S
  module TT : THEORY_TERM
  module T : TERM with module Var = Var and module TT = TT
  module TA : THEORY_ATOM
  module A : ATOM with module T = T and module TA = TA
  module Val : Valuation.S with module A = A
  val sat : Val.t -> bool
end

module type S = THEORY





(* TheoryUtils.ml *)

open Types

module Make_Term (Var : Variable.S) (TT : TheoryInterface.THEORY_TERM) : TheoryInterface.TERM = struct
  module Var = Var
  module TT = TT
  type t = (Var.t, TT.t) term
  let equal x y =
    match x, y with
    | Variable _, Term _ -> false
    | Term _, Variable _ -> false
    | Variable v1, Variable v2 -> Var.equal v1 v2
    | Term t1, Term t2 -> TT.equal t1 t2
  let hash = Hashtbl.hash
end

module Make_Atom (T : TheoryInterface.TERM) (TA : TheoryInterface.THEORY_ATOM) : TheoryInterface.ATOM = struct
  module T = T
  module TA = TA
  type t = (T.t, TA.t) atom
  let to_string _ = failwith "TODO"
  let equal x y = true(*
    match x, y with
    | Equal _, Atom _ -> false
    | Atom _, Equal _ -> false
    | Equal (x1, y2), Equal (x2, y2) -> T.equal x1 x2 && T.equal y1 y2
    | Atom a1, Atom a2 -> TA.equal a1 a2*)
  let hash = Hashtbl.hash
end







(* FNITheory.ml *)

open TheoryUtils

module Make (Var : Variable.S) (ValFunct : functor(X:Variable.S) -> Valuation.S) : TheoryInterface.S = struct
  (** Variable *)
  module Var = Var

  (** Theory term *)
  module TT = struct
    type t = unit (* TODO *)
    let equal = (=)
    let hash = Hashtbl.hash
  end

  (** Term *)
  module T = Make_Term (Var) (TT)

  (** Theory atom *)
  module TA = struct
    type t = unit (* TODO *)
    let equal = (=)
    let hash = Hashtbl.hash
  end

  (** Atom *)
  module A = Make_Atom (T) (TA)

  (** Valuation *)
  module Val = ValFunct (A)


  let sat _ = failwith "TODO" (* TODO clement *)
end