sig
  type tvar
  type levar
  type otvar
  type prevar
  type lsvar
  module rec Vars :
    sig
      module TVar :
        sig
          type obs
          type t
          val create : unit -> t
          val compare : t -> t -> int
          val total_ord : t -> t -> int
          val add_alias : t -> t -> unit
          val do_normalize : t -> unit
          val add_observer : obs -> t -> unit
          val remove_observer : obs -> t -> unit
          val string_of : t -> string
          val reset : unit -> unit
          val get_all_ts : unit -> t list
          type img
          type elm
          val set_lower : elm -> t -> unit
          val set_upper : elm -> t -> unit
          val set_eq : elm -> t -> unit
          val subset : t -> t -> unit
          val get_lower : t -> elm option
          val get_upper : t -> elm option
          val string_of_img : t -> string
          val get_exact : t -> elm option
          val string_of_with_img : t -> string
          val do_on_exact :
            ?nothing:(unit -> unit) -> ?something:(elm -> unit) -> t -> unit
          val do_on_lower :
            ?nothing:(unit -> unit) -> ?something:(elm -> unit) -> t -> unit
          val do_on_upper :
            ?nothing:(unit -> unit) -> ?something:(elm -> unit) -> t -> unit
        end
      module LSVar :
        sig
          type obs
          type t
          val create : unit -> t
          val compare : t -> t -> int
          val total_ord : t -> t -> int
          val add_alias : t -> t -> unit
          val do_normalize : t -> unit
          val add_observer : obs -> t -> unit
          val remove_observer : obs -> t -> unit
          val string_of : t -> string
          val reset : unit -> unit
          val get_all_ts : unit -> t list
          type img
          type elm = Location.LSet.t
          val set_lower : elm -> t -> unit
          val set_upper : elm -> t -> unit
          val set_eq : elm -> t -> unit
          val subset : t -> t -> unit
          val get_lower : t -> elm option
          val get_upper : t -> elm option
          val string_of_img : t -> string
          val get_exact : t -> elm option
          val string_of_with_img : t -> string
          val set_neg : elm -> t -> unit
          val disjoint : t -> t -> unit
          val get_neg : t -> elm option
          val lower_one_element :
            ?nothing:(unit -> unit) ->
            ?exact:(Location.Loc.t -> unit) ->
            ?tomuch:(unit -> unit) -> t -> unit
          val lower_iter : (Location.Loc.t -> unit) -> t -> unit
          val upper_iter : (Location.Loc.t -> unit) -> t -> unit
          val is_one_possible : t -> bool
          val equal_possible : t -> t -> bool
          val equal_possible_lset : t -> Location.LSet.t -> bool
          val subset_possible : t -> t -> bool
          val subset_possible_lset : t -> Location.LSet.t -> bool
          val choose_lower : t -> Location.Loc.t option
          val set_upper_for_all : Location.LSet.t -> unit
        end
      module PrVar :
        sig
          type obs
          type t
          val create : unit -> t
          val compare : t -> t -> int
          val total_ord : t -> t -> int
          val add_alias : t -> t -> unit
          val do_normalize : t -> unit
          val add_observer : obs -> t -> unit
          val remove_observer : obs -> t -> unit
          val string_of : t -> string
          val reset : unit -> unit
          val get_all_ts : unit -> t list
          type img
          type elm
          val set_lower : elm -> t -> unit
          val set_upper : elm -> t -> unit
          val set_eq : elm -> t -> unit
          val subset : t -> t -> unit
          val get_lower : t -> elm option
          val get_upper : t -> elm option
          val string_of_img : t -> string
          val get_exact : t -> elm option
          val string_of_with_img : t -> string
          val do_on_lower :
            ?nothing:(unit -> unit) ->
            ?exact:(unit -> unit) ->
            ?inexact:(unit -> unit) -> ?nv:(NoValue.nv -> unit) -> t -> unit
          val do_on_upper :
            ?nothing:(unit -> unit) ->
            ?exact:(unit -> unit) ->
            ?inexact:(unit -> unit) -> ?nv:(NoValue.nv -> unit) -> t -> unit
        end
      module ObjectType :
        sig type t type key = Syntax.label type img = TVar.t end
      module OTVar :
        sig
          type obs
          type t
          val create : unit -> t
          val compare : t -> t -> int
          val total_ord : t -> t -> int
          val add_alias : t -> t -> unit
          val do_normalize : t -> unit
          val add_observer : obs -> t -> unit
          val remove_observer : obs -> t -> unit
          val string_of : t -> string
          val reset : unit -> unit
          val get_all_ts : unit -> t list
          type img
          module I : sig type key = Syntax.label type img = TVar.t end
          val domain : t -> I.key list
          val find' : I.key -> t -> I.img option
          val find_or_add :
            create:(unit -> I.img) -> key:I.key -> map:t -> I.img
          val iter : (I.key -> I.img -> unit) -> t -> unit
          val fold : (I.key -> I.img -> 'a -> 'a) -> t -> 'a -> 'a
          val make_write_equal :
            (I.key -> I.key -> int) ->
            (I.img -> I.img -> unit) -> t -> t -> I.key -> unit
          val string_of_map : t -> string
          val string_of_with_img : t -> string
          type domain_var
          val get_domain_var : t -> domain_var
        end
      module LEVar :
        sig
          type obs
          type t
          val create : unit -> t
          val compare : t -> t -> int
          val total_ord : t -> t -> int
          val add_alias : t -> t -> unit
          val do_normalize : t -> unit
          val add_observer : obs -> t -> unit
          val remove_observer : obs -> t -> unit
          val string_of : t -> string
          val reset : unit -> unit
          val get_all_ts : unit -> t list
          type img
          module I : sig type key = Location.Loc.t type img = OTVar.t end
          val domain : t -> I.key list
          val find' : I.key -> t -> I.img option
          val find_or_add :
            create:(unit -> I.img) -> key:I.key -> map:t -> I.img
          val iter : (I.key -> I.img -> unit) -> t -> unit
          val fold : (I.key -> I.img -> 'a -> 'a) -> t -> 'a -> 'a
          val make_write_equal :
            (I.key -> I.key -> int) ->
            (I.img -> I.img -> unit) -> t -> t -> I.key -> unit
          val string_of_map : t -> string
          val string_of_with_img : t -> string
          type domain_var = LSVar.t
          val get_domain_var : t -> domain_var
          val synchronize : t -> unit
        end
      val reset : unit -> unit
    end
  and Type :
    sig
      type t
      type tau
      type lenv
      type r
      type phi
      type q
      val t_top : Inf.Type.t
      val t_undef : Inf.Type.t
      val t_int : Inf.Type.t
      val create_t_obj : Inf.Type.q -> Inf.Type.phi -> Inf.Type.t
      val create_t_fun :
        Inf.Vars.LEVar.t ->
        Inf.Type.t ->
        Inf.Type.t ->
        Inf.Type.phi -> Inf.Vars.LEVar.t -> Inf.Type.t -> Inf.Type.t
      val create_t_tv : Inf.Vars.TVar.t -> Inf.Type.t
      val empty_lenv : Inf.Type.lenv
      val add_to_lenv :
        Inf.Type.lenv -> Location.Loc.t -> Inf.Type.r -> Inf.Type.lenv
      val union_lenv : Inf.Type.lenv -> Inf.Type.lenv -> Inf.Type.lenv
      val create_lenv_levar : Inf.levar -> Inf.Type.lenv
      val empty_obj : Inf.Type.r
      val add_to_obj :
        Inf.Type.r -> Syntax.label -> Inf.Vars.TVar.t -> Inf.Type.r
      val create_r_otv : Inf.Vars.OTVar.t -> Inf.Type.r
      val create_phi_ls : Location.LSet.t -> Inf.Type.phi
      val create_phi_lsvar : Inf.Vars.LSVar.t -> Inf.Type.phi
      val q_in : Inf.Type.q
      val q_ex : Inf.Type.q
      val create_q_pv : Inf.Vars.PrVar.t -> Inf.Type.q
      val string_of : Inf.Type.t -> string
      val string_of_p : Inf.Type.q * Inf.Type.phi -> string
      val string_of_lenv : Inf.Type.lenv -> string
      val string_of_r : Inf.Type.r -> string
      val string_of_phi : Inf.Type.phi -> string
      val string_of_q : Inf.Type.q -> string
    end
  module ConstBasic :
    sig
      type t
      type obs
      val c_true : Inf.ConstBasic.t
      val c_false : string option -> Inf.ConstBasic.t
      val create_c_demotation_lenv :
        Inf.Vars.LEVar.t ->
        Inf.Type.phi -> Inf.Vars.LEVar.t -> Inf.ConstBasic.t
      val create_c_demotation_lenv_phi :
        Inf.Vars.LEVar.t ->
        Inf.Type.phi -> Inf.Type.phi -> Inf.Vars.LEVar.t -> Inf.ConstBasic.t
      val create_c_demotation_type :
        Inf.Type.t -> Inf.Type.phi -> Inf.Type.t -> Inf.ConstBasic.t
      val create_c_include :
        Location.Loc.t -> Inf.Type.phi -> Inf.ConstBasic.t
      val create_c_exclude :
        Location.Loc.t -> Inf.Type.phi -> Inf.ConstBasic.t
      val create_c_subset :
        ?prio:int -> Inf.Type.phi -> Inf.Type.phi -> Inf.ConstBasic.t
      val create_c_disjoint :
        ?prio:int -> Inf.Type.phi -> Inf.Type.phi -> Inf.ConstBasic.t
      val create_c_subtype :
        ?prio:int -> Inf.Type.t -> Inf.Type.t -> Inf.ConstBasic.t
      val create_c_eqtype : Inf.Type.t -> Inf.Type.t -> Inf.ConstBasic.t
      val create_c_eqlenv :
        Inf.Type.lenv -> Inf.Type.lenv -> Inf.ConstBasic.t
      val create_c_eqobj : Inf.Type.r -> Inf.Type.r -> Inf.ConstBasic.t
      val create_c_eqset : Inf.Type.phi -> Inf.Type.phi -> Inf.ConstBasic.t
      val create_c_eqpres : Inf.Type.q -> Inf.Type.q -> Inf.ConstBasic.t
      val create_c_domain_eq :
        Inf.Type.phi -> Inf.Vars.LEVar.t -> Inf.ConstBasic.t
      val create_c_lev_empty_obj :
        Inf.Vars.LEVar.t ->
        Inf.Vars.LEVar.t -> Location.Loc.t -> Inf.ConstBasic.t
      val create_c_flow :
        Inf.Vars.LEVar.t -> Inf.Type.t -> Inf.Type.t -> Inf.ConstBasic.t
      val create_c_read :
        Inf.Vars.LEVar.t ->
        Inf.Vars.PrVar.t ->
        Inf.Vars.LSVar.t ->
        Syntax.label -> Inf.Vars.TVar.t -> Inf.ConstBasic.t
      val create_c_write :
        Inf.Vars.LEVar.t ->
        Inf.Vars.TVar.t ->
        Syntax.label ->
        Inf.Vars.TVar.t -> Inf.Vars.LEVar.t -> Inf.ConstBasic.t
      val create_c_locs : Inf.Type.phi -> Inf.Type.t -> Inf.ConstBasic.t
      val string_of : Inf.ConstBasic.t -> string
    end
  module Const :
    sig
      type obs = Inf.ConstBasic.obs
      val add : Inf.ConstBasic.t -> unit
      val is_false : string -> unit
      val remove : Inf.ConstBasic.t -> unit
      val add_wl : Inf.Const.obs -> unit
      val solve : unit -> unit
      val string_of : unit -> string
      val reset : unit -> unit
      val full_visit : unit -> unit
    end
  module GEnv :
    sig val string_of : unit -> string val reset : unit -> unit end
end