Quelle hConstr.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Constr

type t
(** Hashconsed constr in an implicit environment,
    keeping variables which have different types and bodies separate.

    For instance the [x] subterms in [fun x : bool => x] and [fun x : nat => x] are different
    (and have different hashes modulo accidental collision)
    and the [x] subterms in [fun (y:nat) (x:bool) => x] and [fun (x:bool) (y:nat) => x] are different
    (one is [Rel 1], the other is [Rel 2])
    but the [x] subterms in [fun (y:nat) (x:bool) => x] and [fun (y:bool) (x:bool) => x] are shared.

    This allows using it as a cache key while typechecking.

    Hashconsing information of subterms is also kept. *)

val self : t -> constr

val kind : t -> (t,t,Sorts.t,UVars.Instance.t,Sorts.relevance) kind_of_term

val refcount : t -> int
(** How many times this term appeared as a subterm of the argument to [of_constr]. *)

val of_constr : Environ.env -> constr -> t

(* May not be used on Rel! (subterms can be rels) *)
val of_kind_nohashcons : (t,t,Sorts.t,UVars.Instance.t,Sorts.relevance) kind_of_term -> t
(** Build a [t] without hashconsing. Its refcount may be 1 even if
    an identical term was already seen.

    May not be used to build [Rel].

    This is intended for the reconstruction of the inductive type when checking CaseInvert. *)

module Tbl : sig
  (** Imperative tables indexed by [HConstr.t].
      The interfaces exposed are the same as [Hashtbl]
      but are not guaranteed to be implemented by [Hashtbl]. *)

  type key = t

  type 'a t

  val find_opt : 'a t -> key -> 'a option

  val add : 'a t -> key -> 'a -> unit

  val create : unit -> 'a t
end

val hcons : t -> int * Constr.t

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.