package coq

  1. Overview
  2. Docs
On This Page
  1. Serialization
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module implements the handling of opaque proof terms. Opaque proof terms are special since:

  • they can be lazily computed and substituted
  • they are stored in an optionally loaded segment of .vo files An opaque proof terms holds an index into an opaque table.
type 'a delayed_universes =
  1. | PrivateMonomorphic of 'a
  2. | PrivatePolymorphic of int * Univ.ContextSet.t
    (*

    Number of surrounding bound universes + local constraints

    *)
type opaquetab
type opaque
val empty_opaquetab : opaquetab

From a proofterm to some opaque.

type cooking_info = {
  1. modlist : work_list;
  2. abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t;
}
type opaque_proofterm = Constr.t * unit delayed_universes
type opaque_handle
type indirect_accessor = {
  1. access_proof : Names.DirPath.t -> opaque_handle -> opaque_proofterm option;
  2. access_discharge : cooking_info list -> opaque_proofterm -> opaque_proofterm;
}

Opaque terms are indexed by their library dirpath and an integer index. The two functions above activate this indirect storage, by telling how to retrieve terms.

From a opaque back to a constr. This might use the indirect opaque accessor given as an argument.

val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
val subst_opaque : Mod_subst.substitution -> opaque -> opaque
val discharge_opaque : cooking_info -> opaque -> opaque
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
Serialization
type opaque_disk
val dump : ?except:Future.UUIDSet.t -> opaquetab -> opaque_disk * opaque_handle Future.UUIDMap.t
val get_opaque_disk : opaque_handle -> opaque_disk -> opaque_proofterm option
val set_opaque_disk : opaque_handle -> opaque_proofterm -> opaque_disk -> unit
val repr_handle : opaque_handle -> int

Only used for pretty-printing

OCaml

Innovation. Community. Security.