package universo

You can search for identifiers within the package.

in-package search v0.2.0

package universo

universo
- Library universo.api
  - Universo_api
- Library universo.checking
  - Checking
    
    Checker
    
    B
    
    C
    
    F
    
    L
    
    M
    
    P
    
    S
    
    T
    
    U
    
    V
    
    MakeRE
    
    RE
    
    Typing
- Library universo.common
  - Common
    
    Constraints
    
    B
    
    F
    
    R
    
    S
    
    T
    
    U
    
    M
    
    Files
    
    B
    
    S
    
    P
    
    Processor
    
    Log
    
    D
    
    Logic
    
    B
    
    T
    
    LRA_REIFICATION
    
    LRA_SPECIFICATION
    
    MakeLraSpecif
    
    QFUF_SPECIFICATION
    
    Oracle
    
    M
    
    T
    
    U
    
    Util
    
    Universes
    
    B
    
    T
    
    C
- Library universo.elaboration
  - Elaboration
    
    Elaborate
    
    E
    
    F
    
    L
    
    M
    
    P
    
    R
    
    T
    
    Var
    
    B
    
    F
    
    T
    
    U
- Library universo.solving
  - Solving
    
    Solver
    
    Make
    
    MakeUF
    
    Utils
    
    B
    
    M
    
    LOGIC
    
    SMTSOLVER
    
    SOLVER
    
    Z3arith
    
    B
    
    L
    
    U
    
    ZA
    
    ZB
    
    ZI
    
    Make
    
    Z3cfg
    
    Z3LOGIC
    
    Make
    
    Syn
    
    Arith
    
    Z3syn
    
    B
    
    L
    
    O
    
    U
    
    Z
- Sources
  - universo.api
    
    universo_api.ml
  - universo.checking
    
    checker.ml
    
    checking.ml
  - universo.common
    
    common.ml
    
    constraints.ml
    
    files.ml
    
    log.ml
    
    logic.ml
    
    oracle.ml
    
    universes.ml
  - universo.elaboration
    
    elaborate.ml
    
    elaboration.ml
    
    var.ml
  - universo.solving
    
    solver.ml
    
    solving.ml
    
    utils.ml
    
    z3arith.ml
    
    z3cfg.ml
    
    z3syn.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.

package universo

Module Checking.CheckerSource

Module `Checking.Checker`Source