diff options
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 54 |
1 files changed, 40 insertions, 14 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index bd118bbce5..8eb88f70d8 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -17,18 +17,32 @@ open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) -val constr_loc : constr_expr -> Loc.t +(** {6 Equalities on [constr_expr] related types} *) -val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t -val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t +val explicitation_eq : explicitation -> explicitation -> bool +(** Equality on [explicitation]. *) -val local_binders_loc : local_binder list -> Loc.t +val constr_expr_eq : constr_expr -> constr_expr -> bool +(** Equality on [constr_expr]. This is a syntactical one, which is oblivious to + some parsing details, including locations. *) + +val local_binder_eq : local_binder -> local_binder -> bool +(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool +(** Equality on [binding_kind] *) val binder_kind_eq : binder_kind -> binder_kind -> bool +(** Equality on [binder_kind] *) -val default_binder_kind : binder_kind +(** {6 Retrieving locations} *) + +val constr_loc : constr_expr -> Loc.t +val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t +val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t +val local_binders_loc : local_binder list -> Loc.t + +(** {6 Constructors}*) val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr @@ -38,24 +52,36 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr -val coerce_reference_to_id : reference -> identifier -val coerce_to_id : constr_expr -> identifier located -val coerce_to_name : constr_expr -> name located - val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr -(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *) val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr +(** Same as [abstract_constr_expr], with location *) + val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr +(** Same as [prod_constr_expr], with location *) -(** For binders parsing *) +(** {6 Destructors}*) -(** With let binders *) -val names_of_local_assums : local_binder list -> name located list +val coerce_reference_to_id : reference -> identifier +(** FIXME: nothing to do here *) + +val coerce_to_id : constr_expr -> identifier located +(** Destruct terms of the form [CRef (Ident _)]. *) + +val coerce_to_name : constr_expr -> name located +(** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) + +(** {6 Binder manipulation} *) + +val default_binder_kind : binder_kind -(** Does not take let binders into account *) val names_of_local_binders : local_binder list -> name located list +(** Retrieve a list of binding names from a list of binders. *) + +val names_of_local_assums : local_binder list -> name located list +(** Same as [names_of_local_binders], but does not take the [let] bindings into + account. *) val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit) -> Glob_term.glob_constr -> raw_cases_pattern_expr |