diff options
Diffstat (limited to 'interp/genarg.mli')
| -rw-r--r-- | interp/genarg.mli | 52 |
1 files changed, 29 insertions, 23 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index 86b19de7..fab5ff33 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: genarg.mli 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) open Util open Names open Term open Libnames open Rawterm +open Pattern open Topconstr open Term open Evd @@ -21,7 +22,9 @@ type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = | AN of 'a - | ByNotation of loc * string * Notation.delimiters option + | ByNotation of (loc * string * Notation.delimiters option) + +val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) (* in the environment by the effective calls to Intro, Inversion, etc *) @@ -31,6 +34,8 @@ type rawconstr_and_expr = rawconstr * constr_expr option type open_constr_expr = unit * constr_expr type open_rawconstr = unit * rawconstr_and_expr +type rawconstr_pattern_and_expr = rawconstr_and_expr * constr_pattern + type 'a with_ebindings = 'a * open_constr bindings type intro_pattern_expr = @@ -39,6 +44,7 @@ type intro_pattern_expr = | IntroRewrite of bool | IntroIdentifier of identifier | IntroFresh of identifier + | IntroForthcoming of bool | IntroAnonymous and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list @@ -72,7 +78,7 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds effective use \end{verbatim} -To distinguish between the uninterpreted (raw), globalized and +To distinguish between the uninterpreted (raw), globalized and interpreted worlds, we annotate the type [generic_argument] by a phantom argument which is either [constr_expr], [rawconstr] or [constr]. @@ -104,16 +110,16 @@ ExtraArgType of string '_a '_b \end{verbatim} *) -(* All of [rlevel], [glevel] and [tlevel] must be non convertible +(* All of [rlevel], [glevel] and [tlevel] must be non convertible to ensure the injectivity of the type inference from type ['co generic_argument] to [('a,'co) abstract_argument_type]; this guarantees that, for 'co fixed, the type of - out_gen is monomorphic over 'a, hence type-safe + out_gen is monomorphic over 'a, hence type-safe *) -type rlevel = constr_expr -type glevel = rawconstr_and_expr -type tlevel = open_constr +type rlevel +type glevel +type tlevel type ('a,'co) abstract_argument_type @@ -174,8 +180,8 @@ val rawwit_constr : (constr_expr,rlevel) abstract_argument_type val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type val wit_constr : (constr,tlevel) abstract_argument_type -val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation) may_eval,rlevel) abstract_argument_type -val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type +val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation,constr_expr) may_eval,rlevel) abstract_argument_type +val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) may_eval,glevel) abstract_argument_type val wit_constr_may_eval : (constr,tlevel) abstract_argument_type val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type @@ -192,15 +198,15 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type -val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type +val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type -val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type +val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type -val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type -val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type -val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type +val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type +val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type +val wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type val wit_list0 : ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type @@ -219,29 +225,29 @@ val wit_pair : (* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) type 'a generic_argument -val fold_list0 : +val fold_list0 : ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c -val fold_list1 : +val fold_list1 : ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c val fold_opt : ('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c val fold_pair : - ('a generic_argument -> 'a generic_argument -> 'c) -> + ('a generic_argument -> 'a generic_argument -> 'c) -> 'a generic_argument -> 'c (* [app_list0] fails if applied to an argument not of tag [List0 t] for some [t]; it's the responsability of the caller to ensure it *) -val app_list0 : ('a generic_argument -> 'b generic_argument) -> +val app_list0 : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument -val app_list1 : ('a generic_argument -> 'b generic_argument) -> +val app_list1 : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument -val app_opt : ('a generic_argument -> 'b generic_argument) -> +val app_opt : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument val app_pair : @@ -291,7 +297,7 @@ val unquote : ('a,'co) abstract_argument_type -> argument_type val in_gen : ('a,'co) abstract_argument_type -> 'a -> 'co generic_argument val out_gen : - ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a + ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a (* [in_generic] is used in combination with camlp4 [Gramext.action] magic @@ -305,5 +311,5 @@ val out_gen : *) type an_arg_of_this_type -val in_generic : +val in_generic : argument_type -> an_arg_of_this_type -> 'co generic_argument |