Module Checking.CheckerSource

module B = Kernel.Basic
Sourcemodule L = Common.Log
Sourcemodule M = Api.Meta
module S = Kernel.Signature
module T = Kernel.Term
Sourcetype t = {
  1. env : Api.Env.t;
    (*

    The current environement used for type checking

    *)
  2. in_path : F.path;
    (*

    path of the original file that should be typed checked

    *)
  3. meta_out : M.cfg;
    (*

    Meta configuration to translate back universes of Universo to the original theory universes

    *)
  4. constraints : (B.name, U.pred) Hashtbl.t;
    (*

    additional user constraints

    *)
  5. out_file : F.cout F.t;
    (*

    File were constraints are written

    *)
}
Sourceval global_env : t option ref

globel_env is a reference to the current type checking environment.

Sourceval get : 'a option -> 'a
Sourceval of_global_env : t -> C.t
Sourcemodule MakeRE (Conv : Kernel.Reduction.ConvChecker) : Kernel.Reduction.S
module RE : Kernel.Reduction.S
module Typing : sig ... end
Sourceval check_user_constraints : (B.name, U.pred) Hashtbl.t -> B.name -> T.term -> unit

check_user_constraints table name t checks whether the user has added constraints on the onstant name and if so, add this constraint. In t, every universo variable (md.var) are replaced by the sort associated to the constant name.

Sourceval mk_entry : t -> Api.Env.t -> Parsers.Entry.entry -> unit

mk_entry env e type checks the entry e in the same way then dkcheck does. However, the convertibility tests is hacked so that we can add constraints dynamically while type checking the term. This is really close to what is done with typical ambiguity in Coq.