Module Recordops

Operations concerning records and canonical structures

Records
type struc_typ = {
s_CONST : Names.constructor;
s_EXPECTEDPARAM : int;
s_PROJKIND : (Names.Name.t * bool) list;
s_PROJ : Names.Constant.t option list;
}
type struc_tuple = Names.constructor * (Names.Name.t * bool) list * Names.Constant.t option list
val declare_structure : struc_tuple -> unit
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 declare_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 declare_canonical_structure : Names.GlobRef.t -> unit
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