Quelle tac2typing_env.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 Names
open Tac2expr

module TVar : sig
  type t

  val equal : t -> t -> bool

  module Map : CSig.MapS with type key = t
end

type t

(** default strict:true *)
val empty_env : ?strict:bool -> unit -> t

val set_rec : (KerName.t * int) Id.Map.t -> t -> t

val reject_unbound_tvar : t -> t

val env_strict : t -> bool

val env_name : t -> TVar.t -> string

val fresh_id : t -> TVar.t

val get_alias : lident -> t -> TVar.t

val find_rec_var : Id.t -> t -> (KerName.t * int) option

type mix_var =
| GVar of TVar.t
| LVar of int

type mix_type_scheme = int * mix_var glb_typexpr

val mem_var : Id.t -> t -> bool

val find_var : Id.t -> t -> mix_type_scheme

val is_used_var : Id.t -> t -> bool

val bound_vars : t -> Id.Set.t

val get_variable0 : (Id.t -> bool) -> tacref or_relid -> tacref Locus.or_var

val get_variable : t -> tacref or_relid -> tacref Locus.or_var

(** View function, allows to ensure head normal forms *)
val kind : t -> TVar.t glb_typexpr -> TVar.t glb_typexpr

val pr_glbtype : t -> TVar.t glb_typexpr -> Pp.t

val eq_or_tuple : ('a -> 'b -> bool) -> 'a or_tuple -> 'b or_tuple -> bool

exception CannotUnify of TVar.t glb_typexpr * TVar.t glb_typexpr

(** unify0 raises CannotUnify, unify raises usererror *)
val unify0 : t -> TVar.t glb_typexpr -> TVar.t glb_typexpr -> unit

val unify : ?loc:Loc.t -> t -> TVar.t glb_typexpr -> TVar.t glb_typexpr -> unit

val unify_arrow : ?loc:Loc.t -> t
  -> TVar.t glb_typexpr
  -> (Loc.t option * TVar.t glb_typexpr) list
  -> TVar.t glb_typexpr

val abstract_var : t -> TVar.t glb_typexpr -> mix_type_scheme

val monomorphic : TVar.t glb_typexpr -> mix_type_scheme

val polymorphic : type_scheme -> mix_type_scheme

val push_name : Name.t -> mix_type_scheme -> t -> t

val push_ids : mix_type_scheme Id.Map.t -> t -> t

val subst_type : ('a -> 'b glb_typexpr) -> 'a glb_typexpr -> 'b glb_typexpr

val normalize : t ->
  int ref * int glb_typexpr TVar.Map.t ref ->
  TVar.t glb_typexpr ->
  int glb_typexpr

quality97%

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