1 files changed, 162 insertions, 0 deletions
diff --git a/pretyping/structures.mli b/pretyping/structures.mli
new file mode 100644
index 0000000000..05b21b1033
--- /dev/null
+++ b/pretyping/structures.mli
@@ -0,0 +1,162 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq 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)         *)
+(************************************************************************)
+
+
+(** A structure S is a non recursive inductive type with a single
+   constructor *)
+module Structure : sig
+
+(** A projection to a structure field *)
+type projection = {
+  proj_name : Names.Name.t;            (** field name *)
+  proj_true : bool;                    (** false for primitive records *)
+  proj_canonical : bool;               (** false = not to be used for CS inference *)
+  proj_body : Names.Constant.t option; (** the projection function *)
+}
+
+type t = {
+  name : Names.inductive;
+  projections : projection list;
+  nparams : int;
+}
+
+val make : Environ.env -> 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