diff options
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index ea960aa9..8fc430ae 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -22,14 +22,19 @@ open Library constructor (the name of which defaults to Build_S) *) type struc_typ = { - s_CONST : constructor; + s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (name * bool) list; s_PROJ : constant option list } -val declare_structure : +val declare_structure : inductive * constructor * (name * bool) list * constant option list -> unit +(* [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_structure : inductive -> struc_typ + (* [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise it fails with [Not_found] *) @@ -41,13 +46,22 @@ val find_projection_nparams : global_reference -> int (* raise [Not_found] if not a projection *) val find_projection : global_reference -> struc_typ +(* we keep an index (dnet) of record's arguments + fields + (=methods). Here is how to declare them: *) +val declare_method : + global_reference -> Evd.evar -> Evd.evar_map -> unit + (* and here is how to search for methods matched by a given term: *) +val methods_matching : constr -> + ((global_reference*Evd.evar*Evd.evar_map) * + (constr*existential_key)*Termops.subst) list + (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) (* structure *) type cs_pattern = Const_cs of global_reference - | Prod_cs + | Prod_cs | Sort_cs of sorts_family | Default_cs @@ -60,10 +74,11 @@ type obj_typ = { o_TCOMPS : constr list } (* ordered *) val cs_pattern_of_constr : constr -> cs_pattern * int * constr list - +val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds + val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ val declare_canonical_structure : global_reference -> unit val is_open_canonical_projection : Evd.evar_map -> (constr * constr list) -> bool -val canonical_projections : unit -> +val canonical_projections : unit -> ((global_reference * cs_pattern) * obj_typ) list |