From 34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 18 Mar 2021 19:15:39 +0100 Subject: [recordops] complete API rewrite; the module is now called [structures] --- pretyping/structures.mli | 163 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 163 insertions(+) create mode 100644 pretyping/structures.mli (limited to 'pretyping/structures.mli') diff --git a/pretyping/structures.mli b/pretyping/structures.mli new file mode 100644 index 0000000000..a1cc38e8e0 --- /dev/null +++ b/pretyping/structures.mli @@ -0,0 +1,163 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Names.inductive -> projection list -> t + +val register : t -> unit +val subst : Mod_subst.substitution -> t -> t + +(** refreshes nparams, e.g. after section discharging *) +val rebuild : Environ.env -> t -> t + +(** [find isp] returns the Structure.t associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val find : Names.inductive -> t + +(** raise [Not_found] if not a structure projection *) +val find_from_projection : Names.Constant.t -> t + +(** [lookup_projections isp] returns the projections associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val find_projections : Names.inductive -> Names.Constant.t option list + +(** raise [Not_found] if not a projection *) +val projection_nparams : Names.Constant.t -> int + +val is_projection : Names.Constant.t -> bool + +end + +(** A canonical instance declares "canonical" conversion hints between + the effective components of a structure and the projections of the + structure *) +module Instance : sig + +type t + +(** Process a record instance, checkig it can be registered as canonical. + The record type must be declared as a canonical Structure.t beforehand. *) +val make : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t + +(** Register an instance as canonical *) +val register : warn:bool -> Environ.env -> Evd.evar_map -> t -> unit + +val subst : Mod_subst.substitution -> t -> t +val repr : t -> Names.GlobRef.t + +end + + +(** A ValuePattern.t characterizes the form of a component of canonical + instance and is used to query the data base of canonical instances *) +module ValuePattern : sig + +type t = + | Const_cs of Names.GlobRef.t + | Proj_cs of Names.Projection.Repr.t + | Prod_cs + | Sort_cs of Sorts.family + | Default_cs + +val equal : Environ.env -> t -> t -> bool +val print : t -> Pp.t + +(** Return the form of the component of a canonical structure *) +val of_constr : Environ.env -> Constr.t -> t * int option * Constr.t list + +end + + +(** The canonical solution of a problem (proj,val) is a global + [constant = fun abs : abstractions_ty => body] and + [body = RecodConstructor params canon_values] and the canonical value + corresponding to val is [val cvalue_arguments]. + It is possible that val is one of the [abs] abstractions, eg [Default_cs], + and in that case [cvalue_abstraction = Some i] *) + +module CanonicalSolution : sig + +type t = { + constant : EConstr.t; + + abstractions_ty : EConstr.t list; + body : EConstr.t; + + nparams : int; + params : EConstr.t list; + cvalue_abstraction : int option; + cvalue_arguments : EConstr.t list; +} + +(** [find (p,v)] returns a s such that p s = v. + The solution s gets a fresh universe instance and is decomposed into + bits for consumption by evarconv. Can raise [Not_found] on failure *) +val find : + Environ.env -> Evd.evar_map -> (Names.GlobRef.t * ValuePattern.t) -> + Evd.evar_map * t + +(** [is_open_canonical_projection env sigma t] is true if t is a FieldName + applied to term which is not a constructor. Used by evarconv not to + unfold too much and lose a projection too early *) +val is_open_canonical_projection : + Environ.env -> Evd.evar_map -> EConstr.t -> bool + +end + +(** Low level access to the Canonical Structure database *) +module CSTable : sig + +type entry = { + projection : Names.GlobRef.t; + value : ValuePattern.t; + solution : Names.GlobRef.t; +} + +(** [all] returns the list of tuples { p ; v ; s } + Note: p s = v *) +val entries : unit -> entry list + +(** [entries_for p] returns the list of canonical entries that have + p as their FieldName *) +val entries_for : projection:Names.GlobRef.t -> entry list + +end + +(** Some extra info for structures which are primitive records *) +module PrimitiveProjections : sig + +(** Sets up the mapping from constants to primitive projections *) +val register : Names.Projection.Repr.t -> Names.Constant.t -> unit + +val mem : Names.Constant.t -> bool + +val find_opt : Names.Constant.t -> Names.Projection.Repr.t option + +end -- cgit v1.2.3 From d9c80dadd353bd8b0eb90ce290048a2538f1a41a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Mar 2021 20:21:46 +0100 Subject: [doc] cleanup pretyping/structures.mli --- pretyping/structures.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/structures.mli') diff --git a/pretyping/structures.mli b/pretyping/structures.mli index a1cc38e8e0..05b21b1033 100644 --- a/pretyping/structures.mli +++ b/pretyping/structures.mli @@ -101,7 +101,6 @@ end corresponding to val is [val cvalue_arguments]. It is possible that val is one of the [abs] abstractions, eg [Default_cs], and in that case [cvalue_abstraction = Some i] *) - module CanonicalSolution : sig type t = { -- cgit v1.2.3