Module Recordops

Operations concerning records and canonical structures

Records
type proj_kind = {
pk_name : Names.Name.t;
pk_true_proj : bool;
pk_canonical : bool;
}
type struc_typ = {
s_CONST : Names.constructor;
s_EXPECTEDPARAM : int;
s_PROJKIND : proj_kind list;
s_PROJ : Names.Constant.t option list;
}
type struc_tuple = Names.constructor * proj_kind list * Names.Constant.t option list
val register_structure : Environ.env -> struc_tuple -> unit
val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
val lookup_structure : Names.inductive -> struc_typ

lookup_structure isp returns the struc_typ associated to the inductive path isp if it corresponds to a structure, otherwise it fails with Not_found

val lookup_projections : Names.inductive -> Names.Constant.t option list

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_projection_nparams : Names.GlobRef.t -> int

raise Not_found if not a projection

val find_projection : Names.GlobRef.t -> struc_typ

raise Not_found if not a projection

val is_projection : Names.Constant.t -> bool
val register_primitive_projection : Names.Projection.Repr.t -> Names.Constant.t -> unit

Sets up the mapping from constants to primitive projections

val is_primitive_projection : Names.Constant.t -> bool
val find_primitive_projection : Names.Constant.t -> Names.Projection.Repr.t option
Canonical structures
type cs_pattern =
| Const_cs of Names.GlobRef.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs

A cs_pattern characterizes the form of a component of canonical structure

type obj_typ = {
o_DEF : Constr.constr;
o_CTX : Univ.AUContext.t;
o_INJ : int option;

position of trivial argument

o_TABS : Constr.constr list;

ordered

o_TPARAMS : Constr.constr list;

ordered

o_NPARAMS : int;
o_TCOMPS : Constr.constr list;
}

ordered

val cs_pattern_of_constr : Environ.env -> Constr.constr -> cs_pattern * int option * Constr.constr list

Return the form of the component of a canonical structure

val pr_cs_pattern : cs_pattern -> Pp.t
val lookup_canonical_conversion : (Names.GlobRef.t * cs_pattern) -> Constr.constr * obj_typ
val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> (Names.Constant.t * Names.inductive) -> unit
val subst_canonical_structure : Mod_subst.substitution -> (Names.Constant.t * Names.inductive) -> Names.Constant.t * Names.inductive
val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool
val canonical_projections : unit -> ((Names.GlobRef.t * cs_pattern) * obj_typ) list
val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Names.Constant.t * Names.inductive