Module Typing

module Typing: sig .. end

Typing parse trees


Typing parse trees

val debug_parse_only : Debug.flag
val debug_type_only : Debug.flag
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 : 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