package universo

You can search for identifiers within the package.

in-package search v0.2.0

A tool for Dedukti to play with universes

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

D

dedukti-dev@inria.fr

Maintainers

D

dedukti-dev@inria.fr

Sources

v2.7.tar.gz

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/universo.checking/Checking/Checker/index.html

Module `Checking.Checker`Source

module B = Kernel.Basic

Sourcemodule C = Common.Constraints

Sourcemodule F = Common.Files

Sourcemodule L = Common.Log

Sourcemodule M = Api.Meta

Sourcemodule P = Api.Pp.Default

module S = Kernel.Signature

module T = Kernel.Term

Sourcemodule U = Common.Universes

Sourcemodule V = Elaboration.Var

Sourcetype t = {

env : Api.Env.t;
(*
The current environement used for type checking
*)
in_path : F.path;
(*
path of the original file that should be typed checked
*)
meta_out : M.cfg;
(*
Meta configuration to translate back universes of Universo to the original theory universes
*)
constraints : (B.name, U.pred) Hashtbl.t;
(*
additional user constraints
*)
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

Source

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