Module type TermInner.UTIL_REPR

module type UTIL_REPR = sig .. end

type t_

val head_sym : t_ -> TermInner.id

Search for a head symbol
Raises Not_found if not an application/const

val to_seq : t_ -> t_ Sequence.t

Iterate on sub-terms

val to_seq_vars : t_ -> t_ Var.t Sequence.t

Iterate on variables

val to_seq_consts : t_ -> ID.t Sequence.t

IDs occurring as Const

module VarSet: CCSet.S  with type elt = t_ Var.t

val to_seq_free_vars : ?bound:VarSet.t ->
       t_ -> t_ Var.t Sequence.t

Iterate on free variables.

val free_vars : ?bound:VarSet.t ->
       t_ -> VarSet.t

free_vars t computes the set of free variables of t.

bound : variables bound on the path

val is_var : t_ -> bool

val is_const : t_ -> bool

val is_closed : t_ -> bool

is_closed t means to_seq_free_vars t = empty

val is_undefined : t_ -> bool

val free_meta_vars : ?init:t_ MetaVar.t ID.Map.t ->
       t_ -> t_ MetaVar.t ID.Map.t

The free type meta-variables in t

val bind_unfold : TermInner.Binder.t ->
       t_ ->
       t_ Var.t list * t_

bind_unfold binder (bind binder x1...xn. t) returns x1...xn, t

val fun_unfold : t_ ->
       t_ Var.t list * t_

fun_unfold (fun x y z. t) = [x;y;z], t. Special case of TermInner.UTIL_REPR.bind_unfold

val get_ty_arg : t_ -> int -> t_ option

get_ty_arg ty n gets the n-th argument of ty, if ty is a function type with at least n arguments.

val ty_unfold : t_ ->
       t_ Var.t list * t_ list *
       t_

ty_unfold ty decomposes ty into a list of quantified type variables, a list of parameters, and a return type (which is not an arrow).

ty_unfold (forall a b, a -> b -> c -> d) will return ([a;b], [a;b;c], d)

val ty_is_Type : t_ -> bool

t == Type?

val ty_returns_Type : t_ -> bool

t == forall ... -> ... -> ... -> Type?

val ty_returns_Prop : t_ -> bool

val ty_returns : t_ -> t_

follow forall/arrows to get return type.

val ty_is_Kind : t_ -> bool

type == Kind?

val ty_is_Prop : t_ -> bool

t == Prop?

val ty_is_unitype : t_ -> bool

val ty_num_param : t_ -> int

Number of type variables that must be bound in the type.