package universo

  1. Overview
  2. Docs
module B = Kernel.Basic
module F = Common.Files
module L = Common.Log
module M = Api.Meta
module P = Api.Pp.Default
module S = Kernel.Signature
module T = Kernel.Term
module U = Common.Universes
module V = Elaboration.Var
type 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) Stdlib.Hashtbl.t;
    (*

    additional user constraints

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

    File were constraints are written

    *)
}
val global_env : t option Stdlib.ref

globel_env is a reference to the current type checking environment.

val get : 'a option -> 'b
val of_global_env : t -> C.t
module Typing : sig ... end
val check_user_constraints : (B.name, U.pred) Stdlib.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.

val 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.