Quelle evarconv.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 EConstr
open Environ
open Reductionops
open Evd
open Locus

(** {4 Unification for type inference. } *)

type unify_flags = Evarsolve.unify_flags

(** The default subterm transparent state is no unfoldings *)
val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags

type unify_fun = unify_flags ->
  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result

val conv_fun : unify_fun -> Evarsolve.unifier

exception UnableToUnify of evar_map * Pretype_errors.unification_error

(** {6 Main unification algorithm for type inference. } *)

(** There are two variants for unification: one that delays constraints outside its capabilities
    ([unify_delay]) and another that tries to solve such remaining constraints using
    heuristics ([unify]). *)

(** These functions allow to pass arbitrary flags to the unifier and can delay constraints.
    In case the flags are not specified, they default to
    [default_flags_of TransparentState.full] currently.

    In case of success, the two terms are hence unifiable only if the remaining constraints
    can be solved or [check_problems_are_solved] is true.

    @raises UnableToUnify in case the two terms do not unify *)

val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map

(** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining
    constraints. In case of success the two terms are unified without condition.

    The with_ho option tells if higher-order unification should be tried to resolve the
    constraints.

    @raises a PretypeError if it cannot unify *)
val unify : ?flags:unify_flags -> ?with_ho:bool ->
  env -> evar_map -> conv_pb -> constr -> constr -> evar_map

(** {6 Unification heuristics. } *)

(** Try heuristics to solve pending unification problems and to solve
   evars with candidates.

   The with_ho option tells if higher-order unification should be tried
   to resolve the constraints.

    @raises a PretypeError if it fails to resolve some problem *)

val solve_unif_constraints_with_heuristics :
  env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map

(** Check all pending unification problems relative to a set of evars
    are solved and raise a PretypeError otherwise *)

val check_problems_are_solved : ?evars:Evar.Set.t -> env -> evar_map -> unit

(** Hook for the canonical structure resolution *)

type hook = Environ.env -> Evd.evar_map -> ((Names.Constant.t * EConstr.EInstance.t) * EConstr.t list option * EConstr.t) -> (EConstr.t * EConstr.t list) -> (Evd.evar_map * Structures.CanonicalSolution.t) option

val all_hooks : hook CString.Map.t ref

val register_hook : name:CString.Map.key -> ?override:bool -> hook -> unit

val active_hooks : string list ref

val deactivate_hook : name:Util.String.t -> unit

val activate_hook : name:CString.Map.key -> unit

val apply_hooks : hook

(** Check if a canonical structure is applicable. *)

val decompose_proj : ?metas:(Constr.metavariable -> types option) -> env -> evar_map -> state -> (Names.Constant.t * EConstr.EInstance.t) *
            (EConstr.t list option * EConstr.t * Reductionops.Stack.t)
val check_conv_record : env -> evar_map ->
  (Names.Constant.t * EConstr.EInstance.t) *
            (EConstr.t list option * EConstr.t * Reductionops.Stack.t) ->
  state ->
  evar_map * (constr * constr)
  * constr * constr list * (EConstr.t list * EConstr.t list option) *
    (EConstr.t list * EConstr.t list) *
    (Stack.t * Stack.t) * constr *
    (int option * constr)

(** Compares two constants/inductives/constructors unifying their universes.
   It required the number of arguments applied to the c/i/c in order to decided
   the kind of check it must perform. *)
val compare_heads : env -> evar_map ->
  nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result

(** Try to solve problems of the form ?x[args] = c by second-order
    matching, using typing to select occurrences *)

type occurrence_match_test =
  env -> evar_map -> constr -> constr -> bool * evar_map

(** When given the choice of abstracting an occurrence or leaving it,
    force abstration. *)

type occurrence_selection =
  | AtOccurrences of occurrences
  | Unspecified of Abstraction.abstraction

(** By default, unspecified, not preferring abstraction.
    This provides the most general solutions. *)
val default_occurrence_selection : occurrence_selection

type occurrences_selection =
  occurrence_match_test * occurrence_selection list

val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test

(** [default_occurrence_selection n]
    Gives the default test and occurrences for [n] arguments *)
val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) ->
  TransparentState.t -> int -> occurrences_selection

val second_order_matching : unify_flags -> env -> evar_map ->
  EConstr.existential -> occurrences_selection -> constr -> evar_map * bool

(** Declare function to enforce evars resolution by using typing constraints *)

val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit

(** Override default [evar_conv_x] algorithm. *)
val set_evar_conv : unify_fun -> unit

(** The default unification algorithm with evars and universes. *)
val evar_conv_x : unify_fun

val evar_unify : Evarsolve.unifier

(**/**)
(* For debugging *)
module Cs_keys_cache : sig type t end

val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
  env -> evar_map -> conv_pb ->
  Cs_keys_cache.t ->
  bool option -> state -> state ->
      Evarsolve.unification_result

val occur_rigidly : Evarsolve.unify_flags ->
  'a -> Evd.evar_map -> Evar.t * 'b -> EConstr.t -> bool
(**/**)

(** {6 Functions to deal with impossible cases } *)
val coq_unit_judge : env -> evar_map -> evar_map * EConstr.unsafe_judgment

quality100%

¤ Dauer der Verarbeitung: 0.20 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.