package universo

You can search for identifiers within the package.

in-package search v0.2.0

package universo

universo.api
- Universo_api
universo.checking
- Checking
  - Checker
    
    MakeRE
    
    Conv
    
    RE
    
    Typing
universo.common
- Common
  - Constraints
  - Files
  - Log
  - Logic
    
    LRA_REIFICATION
    
    LRA_SPECIFICATION
    
    MakeLraSpecif
    
    Lra
    
    QFUF_SPECIFICATION
  - Oracle
    
    Util
  - Universes
    
    C
universo.elaboration
- Elaboration
  - Elaborate
  - Var
universo.solving
- Solving
  - Solver
    
    Make
    
    S
    
    MakeUF
    
    S
  - Utils
    
    LOGIC
    
    SMTSOLVER
    
    SOLVER
  - Z3arith
    
    Make
    
    Spec
  - Z3cfg
    
    Arith
    
    S
    
    Make
    
    ZL
    
    Syn
    
    Z3LOGIC
  - Z3syn

Legend:
Library
Module
Module type
Parameter
Class
Class type

module B = Kernel.Basic

module C = Common.Constraints

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 = {

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
*)

}

val global_env : t option ref

globel_env is a reference to the current type checking environment.

val get : 'a option -> 'a

val of_global_env : t -> C.t

module MakeRE (Conv : Kernel.Reduction.ConvChecker) : Kernel.Reduction.S

module RE : Kernel.Reduction.S

module Typing : sig ... end

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.

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.