Module Typing

module Typing: sig .. end

Typing parse trees

val debug_parse_only : Debug.flag

val debug_type_only : Debug.flag

val warn_useless_at : Loc.warning_id

val type_mlw_file : Env.env ->
       string list -> string -> Ptree.mlw_file -> Pmodule.pmodule Wstdlib.Mstr.t

Incremental typing of parsed modules

val open_file : Env.env -> Env.pathname -> unit

val close_file : unit -> Pmodule.pmodule Wstdlib.Mstr.t

val discard_file : unit -> unit

val open_module : ?intf:Ptree.qualid -> Ptree.ident -> unit

val close_module : Loc.position -> unit

val open_scope : Loc.position -> Ptree.ident -> unit

val close_scope : Loc.position -> import:bool -> unit

val add_decl : Loc.position -> Ptree.decl -> unit

Typing terms and formulas in isolation

val string_list_of_qualid : Ptree.qualid -> string list

val print_qualid : Stdlib.Format.formatter -> Ptree.qualid -> unit

val type_term_in_namespace : Theory.namespace -> Decl.known_map -> Coercion.t -> Ptree.term -> Term.term

val type_fmla_in_namespace : Theory.namespace -> Decl.known_map -> Coercion.t -> Ptree.term -> Term.term

val type_expr_in_muc : Pmodule.pmodule_uc -> ?denv:Dexpr.denv -> Ptree.expr -> Expr.expr

module Unsafe: sig .. end

exported for Coma

val ty_of_pty : Theory.theory_uc -> Ptree.pty -> Ty.ty

val type_term_in_denv : Theory.namespace ->
       Decl.known_map -> Coercion.t -> Dterm.denv -> Ptree.term -> Term.term

val check_term_in_denv : Theory.namespace ->
       Decl.known_map ->
       Coercion.t -> Dterm.denv -> Ptree.term -> Ty.ty -> Term.term

val type_fmla_in_denv : Theory.namespace ->
       Decl.known_map -> Coercion.t -> Dterm.denv -> Ptree.term -> Term.term