Module Logtk__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 -> Logtk.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 -> Logtk.TypedSTerm.t Logtk.Var.t -> t Logtk.HVar.t

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

val fresh_ty_var : ctx -> t Logtk.HVar.t

Fresh type variable

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

if conversion is impossible

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

convert a type to a prolog term.

parameter env

the current environment for De Bruijn indices