Module Checker.Check

the module holding the second and third phases of the borrow checker.

module L = Location
module T = Type
module CC = ComputeConstraint
module Error : sig ... end
type grave = Error.loc_invalid_reason L.Map.t
type state = {
overwrites : T.typ IR.VarMap.t;
constrs : L.ConstrSet.t;
scope : IR.variable list;
grave : grave;
}
type context = {
blocks : (IR.label, grave) Stdlib.Hashtbl.t;
ti : Typecheck.type_info;
ci : CC.constraint_info;
}
val make_context : Typecheck.type_info -> CC.constraint_info -> context
val top_level_borrows : context -> state -> (L.location * Syntax.mutability * Type.L.abstract_loc) Stdlib.Seq.t
val take_access : context -> state -> mut:Syntax.mutability -> L.location -> Error.loc_invalid_reason -> state
val invalidate_loc : context -> state -> L.location -> Error.loc_invalid_reason -> state
val loc_is_readable : 'a L.Map.t -> L.Map.key -> 'a Stdlib.Seq.t
val loc_is_writable : 'a L.Map.t -> L.Map.key -> 'a Stdlib.Seq.t
val typ_is_valid : state -> Type.typ -> Error.loc_invalid_reason Stdlib.Seq.t
val error : Error.error -> 'a
val process_value : context -> state -> IR.value -> state
val check_value : Error.loc_invalid_reason L.Map.t -> IR.value -> unit
val process_expr : context -> state -> IR.expr -> state
val process_expr : context -> state -> IR.expr -> state
val check_expr : Error.loc_invalid_reason L.Map.t -> IR.expr -> unit
val merge_grave_to_block : context -> IR.label -> Error.loc_invalid_reason L.Map.t -> unit
val block_info_to_state : context -> CC.block_info -> grave -> state
val check_program_1 : context -> state -> IR.program -> unit
val check_block : context -> IR.block -> unit
val check_program_2 : context -> Error.loc_invalid_reason L.Map.t -> IR.program -> unit
val check_function : context -> IR.function_def -> unit