module type TAst = sig type t val subs : t -> t list end
module type TIterators =
  sig
    type t
    val subs : t -> t list
    val iter : (t -> unit) -> t -> unit
    val fold_left : ('a -> t -> 'a) -> 'a -> t -> 'a
    val fold_right : (t -> 'a -> 'a) -> t -> 'a -> 'a
    val iter_deep_left : ('a -> t -> 'a) -> 'a -> t -> unit
    val iter_deep_right : (t -> 'a -> 'a) -> t -> 'a -> unit
  end
module Iterators :
  functor (X : TAst) ->
    sig
      type t = X.t
      val subs : t -> t list
      val iter : (t -> unit) -> t -> unit
      val fold_left : ('a -> t -> 'a) -> 'a -> t -> 'a
      val fold_right : (t -> 'a -> 'a) -> t -> 'a -> 'a
      val iter_deep_left : ('a -> t -> 'a) -> 'a -> t -> unit
      val iter_deep_right : (t -> 'a -> 'a) -> t -> 'a -> unit
    end
val replace_sub_expr :
  < loc : Loc.position; name_label : string; node : Jc_ast.expr_node;
    original_type : Jc_env.jc_type; region : Jc_env.region;
    typ : Jc_env.jc_type; .. > ->
  Jc_ast.expr list -> Jc_constructors.expr_with
module ExprAst :
  sig
    type t = Jc_ast.expr
    val subs : < node : Jc_ast.expr_node; .. > -> Jc_ast.expr list
  end
module IExpr :
  sig
    type t = ExprAst.t
    val subs : t -> t list
    val iter : (t -> unit) -> t -> unit
    val fold_left : ('a -> t -> 'a) -> 'a -> t -> 'a
    val fold_right : (t -> 'a -> 'a) -> t -> 'a -> 'a
    val iter_deep_left : ('a -> t -> 'a) -> 'a -> t -> unit
    val iter_deep_right : (t -> 'a -> 'a) -> t -> 'a -> unit
  end
val map_expr :
  ?before:(Jc_ast.expr -> Jc_ast.expr) ->
  ?after:(Jc_constructors.expr_with -> Jc_constructors.expr_with) ->
  Jc_ast.expr -> Jc_ast.expr
module NExprAst :
  sig
    type t = Jc_ast.nexpr
    val subs : < node : Jc_ast.nexpr_node; .. > -> Jc_ast.nexpr list
  end
module INExpr :
  sig
    type t = NExprAst.t
    val subs : t -> t list
    val iter : (t -> unit) -> t -> unit
    val fold_left : ('a -> t -> 'a) -> 'a -> t -> 'a
    val fold_right : (t -> 'a -> 'a) -> t -> 'a -> 'a
    val iter_deep_left : ('a -> t -> 'a) -> 'a -> t -> unit
    val iter_deep_right : (t -> 'a -> 'a) -> t -> 'a -> unit
  end
val replace_sub_pexpr :
  < loc : Loc.position; node : Jc_ast.pexpr_node; .. > ->
  Jc_ast.pexpr list -> Jc_constructors.pexpr_with
module PExprAst :
  sig
    type t = Jc_ast.pexpr
    val subs : < node : Jc_ast.pexpr_node; .. > -> Jc_ast.pexpr list
  end
module IPExpr :
  sig
    type t = PExprAst.t
    val subs : t -> t list
    val iter : (t -> unit) -> t -> unit
    val fold_left : ('a -> t -> 'a) -> 'a -> t -> 'a
    val fold_right : (t -> 'a -> 'a) -> t -> 'a -> 'a
    val iter_deep_left : ('a -> t -> 'a) -> 'a -> t -> unit
    val iter_deep_right : (t -> 'a -> 'a) -> t -> 'a -> unit
  end
val map_pexpr :
  ?before:(Jc_ast.pexpr -> Jc_ast.pexpr) ->
  ?after:(Jc_constructors.pexpr_with -> Jc_constructors.pexpr_with) ->
  Jc_ast.pexpr -> Jc_ast.pexpr
module TermAst :
  sig
    type t = Jc_ast.term
    val subs : < node : Jc_ast.term_node; .. > -> Jc_ast.term list
  end
module ITerm :
  sig
    type t = TermAst.t
    val subs : t -> t list
    val iter : (t -> unit) -> t -> unit
    val fold_left : ('a -> t -> 'a) -> 'a -> t -> 'a
    val fold_right : (t -> 'a -> 'a) -> t -> 'a -> 'a
    val iter_deep_left : ('a -> t -> 'a) -> 'a -> t -> unit
    val iter_deep_right : (t -> 'a -> 'a) -> t -> 'a -> unit
  end
val fold_sub_term :
  ('a -> 'b -> Jc_ast.term -> 'b) ->
  'a -> 'b -> < node : Jc_ast.term_node; .. > -> 'b
val fold_term : ('a -> Jc_ast.term -> 'a) -> 'a -> Jc_ast.term -> 'a
val fold_rec_term :
  ('a -> Jc_ast.term -> bool * 'a) -> 'a -> Jc_ast.term -> 'a
val map_term :
  (Jc_constructors.term_with -> Jc_ast.term) -> Jc_ast.term -> Jc_ast.term
val raw_sub_term : Jc_ast.term -> Jc_ast.term -> bool
val raw_strict_sub_term : Jc_ast.term -> Jc_ast.term -> bool
val iter_term_and_assertion :
  (ITerm.t -> unit) -> (Jc_ast.assertion -> 'a) -> Jc_ast.assertion -> unit
val iter_term_and_assertion_in_loop_annot :
  (ITerm.t -> unit) -> (Jc_ast.assertion -> 'a) -> Jc_ast.loop_annot -> unit
val iter_term_and_assertion_in_behavior :
  (ITerm.t -> unit) -> (Jc_ast.assertion -> 'a) -> Jc_ast.behavior -> unit
val iter_term_and_assertion_in_fun_spec :
  (ITerm.t -> unit) -> (Jc_ast.assertion -> 'a) -> Jc_ast.fun_spec -> unit
val fold_assertion :
  ('a -> Jc_ast.assertion -> 'a) -> 'a -> Jc_ast.assertion -> 'a
val fold_term_in_assertion :
  ('a -> Jc_ast.term -> 'a) -> 'a -> Jc_ast.assertion -> 'a
val fold_term_and_assertion :
  ('a -> Jc_ast.term -> 'a) ->
  ('a -> Jc_ast.assertion -> 'a) -> 'a -> Jc_ast.assertion -> 'a
val map_assertion :
  (Jc_constructors.assertion_with -> Jc_ast.assertion) ->
  Jc_ast.assertion -> Jc_ast.assertion
val map_term_in_assertion :
  (Jc_constructors.term_with -> Jc_ast.term) ->
  Jc_ast.assertion -> Jc_ast.assertion
val map_term_and_assertion :
  (Jc_constructors.assertion_with -> Jc_ast.assertion) ->
  (Jc_constructors.term_with -> Jc_ast.term) ->
  Jc_ast.assertion -> Jc_ast.assertion
val iter_pattern : (Jc_ast.pattern -> 'a) -> Jc_ast.pattern -> unit
val fold_pattern :
  (unit -> Jc_ast.pattern -> unit) -> unit -> Jc_ast.pattern -> unit