Quelle record.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 Vernacexpr
open Constrexpr
open Structures

module Data : sig
  type coercion_flags = {
    coe_local : bool;
    coe_reversible : bool;
  }
  type instance_flags = {
    inst_locality : Hints.hint_locality;
    inst_priority : int option;
  }
  type projection_flags = {
    pf_coercion: coercion_flags option;
    pf_instance: instance_flags option;
    pf_canonical: bool;
  }
  type t = {
    is_coercion : Vernacexpr.coercion_flag;
    proj_flags : projection_flags list;
  }
end

module Ast : sig
  type t =
    { name : Names.lident
    ; is_coercion : coercion_flag
    ; binders: local_binder_expr list
    ; cfs : (local_decl_expr * Data.projection_flags * notation_declaration list) list
    ; idbuild : lident
    ; sort : constr_expr option
    ; default_inhabitant_id : Id.t option
    }
end

val definition_structure
  : flags:ComInductive.flags
  -> cumul_univ_decl_expr option
  -> inductive_kind
  -> primitive_proj:bool
  -> Ast.t list
  -> GlobRef.t list

module RecordEntry : sig

  type one_ind_info = {
    (* inhabitant_id not redundant with the entry in non prim record case *)
    inhabitant_id : Id.t;
    default_dep_elim : DeclareInd.default_dep_elim;
    (* implfs includes the param and principal argument info *)
    implfs : Impargs.manual_implicits list;
    fieldlocs : Loc.t option list;
  }

  type t = {
    global_univs : Univ.ContextSet.t;
    ubinders : UState.named_universes_entry;
    mie : Entries.mutual_inductive_entry;
    ind_infos : one_ind_info list;
    param_impls : Impargs.manual_implicits;
  }

end

(** A record is an inductive [mie] with extra metadata *)
module Record_decl : sig
  type t = {
    entry : RecordEntry.t;
    records : Data.t list;
    projections_kind : Decls.definition_object_kind;
    indlocs : DeclareInd.indlocs;
  }
end

(** Ast.t list at the constr level *)
val interp_structure
  : flags:ComInductive.flags
  -> cumul_univ_decl_expr option
  -> inductive_kind
  -> primitive_proj:bool
  -> Ast.t list
  -> Record_decl.t

val declare_existing_class : GlobRef.t -> unit

val canonical_inhabitant_id : isclass:bool -> Id.t -> Id.t

(* Implementation internals, consult Rocq developers before using;
   current user Elpi, see https://github.com/LPCIC/coq-elpi/pull/151 *)
module Internal : sig
  val declare_projections
    : Names.inductive
    -> kind:Decls.definition_object_kind
    -> inhabitant_id:Names.Id.t
    -> Data.projection_flags list
    -> ?fieldlocs:Loc.t option list
    -> Impargs.manual_implicits list
    -> Structure.projection list

  val declare_structure_entry : Structure.t -> unit

end

quality100%

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