Module Type.Conv

type ctx
val create : unit -> ctx
val copy : ctx -> ctx
val clear : ctx -> unit
val enter_bvar : ctx -> VarMap.key -> int option
val exit_bvar : handle:int CCOpt.t -> ctx -> VarMap.key -> unit
val find_bvar : ctx -> VarMap.key -> int option
val get_maxvar : ctx -> int
val incr_maxvar : ctx -> unit
val set_maxvar : ctx -> int -> unit
val of_simple_term : ctx -> TypedSTerm.t -> t option

convert a simple typed term into a type. The term is assumed to be closed.

returns

an error message if the term is not a type

parameter ctx

context used to map Var to HVar

val var_of_simple_term : ctx -> TypedSTerm.t Var.t -> t HVar.t

Convert a variable (and its type), and remember the binding.

val fresh_ty_var : ctx -> t HVar.t

Fresh type variable

val var_to_simple_var : ?⁠prefix:string -> ctx -> t HVar.t -> TypedSTerm.t Var.t
exception Error of TypedSTerm.t
val of_simple_term_exn : ctx -> TypedSTerm.t -> t
raises Invalid_argument

if conversion is impossible

val to_simple_term : ?⁠env:TypedSTerm.t Var.t DBEnv.t -> ctx -> t -> TypedSTerm.t

convert a type to a prolog term.

parameter env

the current environment for De Bruijn indices