diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 55 | ||||
| -rw-r--r-- | interp/genarg.mli | 176 |
2 files changed, 91 insertions, 140 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index a029a3b31..5d61de508 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -74,6 +74,11 @@ type open_glob_constr = unit * glob_constr_and_expr type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern +type ('raw, 'glob, 'top) genarg_type = argument_type + +type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type +(** Alias for concision *) + (* Dynamics but tagged by a type expression *) type 'a generic_argument = argument_type * Obj.t @@ -82,88 +87,50 @@ type rlevel type glevel type tlevel -let rawwit_bool = BoolArgType -let globwit_bool = BoolArgType +let rawwit t = t +let glbwit t = t +let topwit t = t + let wit_bool = BoolArgType -let rawwit_int = IntArgType -let globwit_int = IntArgType let wit_int = IntArgType -let rawwit_int_or_var = IntOrVarArgType -let globwit_int_or_var = IntOrVarArgType let wit_int_or_var = IntOrVarArgType -let rawwit_string = StringArgType -let globwit_string = StringArgType let wit_string = StringArgType -let rawwit_pre_ident = PreIdentArgType -let globwit_pre_ident = PreIdentArgType let wit_pre_ident = PreIdentArgType -let rawwit_intro_pattern = IntroPatternArgType -let globwit_intro_pattern = IntroPatternArgType let wit_intro_pattern = IntroPatternArgType -let rawwit_ident_gen b = IdentArgType b -let globwit_ident_gen b = IdentArgType b let wit_ident_gen b = IdentArgType b -let rawwit_ident = rawwit_ident_gen true -let globwit_ident = globwit_ident_gen true let wit_ident = wit_ident_gen true -let rawwit_pattern_ident = rawwit_ident_gen false -let globwit_pattern_ident = globwit_ident_gen false let wit_pattern_ident = wit_ident_gen false -let rawwit_var = VarArgType -let globwit_var = VarArgType let wit_var = VarArgType -let rawwit_ref = RefArgType -let globwit_ref = RefArgType let wit_ref = RefArgType -let rawwit_quant_hyp = QuantHypArgType -let globwit_quant_hyp = QuantHypArgType let wit_quant_hyp = QuantHypArgType -let rawwit_sort = SortArgType -let globwit_sort = SortArgType let wit_sort = SortArgType -let rawwit_constr = ConstrArgType -let globwit_constr = ConstrArgType let wit_constr = ConstrArgType -let rawwit_constr_may_eval = ConstrMayEvalArgType -let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType -let rawwit_open_constr_gen b = OpenConstrArgType b -let globwit_open_constr_gen b = OpenConstrArgType b let wit_open_constr_gen b = OpenConstrArgType b -let rawwit_open_constr = rawwit_open_constr_gen false -let globwit_open_constr = globwit_open_constr_gen false let wit_open_constr = wit_open_constr_gen false -let rawwit_casted_open_constr = rawwit_open_constr_gen true -let globwit_casted_open_constr = globwit_open_constr_gen true let wit_casted_open_constr = wit_open_constr_gen true -let rawwit_constr_with_bindings = ConstrWithBindingsArgType -let globwit_constr_with_bindings = ConstrWithBindingsArgType let wit_constr_with_bindings = ConstrWithBindingsArgType -let rawwit_bindings = BindingsArgType -let globwit_bindings = BindingsArgType let wit_bindings = BindingsArgType -let rawwit_red_expr = RedExprArgType -let globwit_red_expr = RedExprArgType let wit_red_expr = RedExprArgType let wit_list0 t = List0ArgType t @@ -242,9 +209,7 @@ let create_arg v s = Errors.anomaly ~label:"Genarg.create" (str ("already declared generic argument " ^ s)); let t = ExtraArgType s in dyntab := (s,Option.map (in_gen t) v) :: !dyntab; - (t,t,t) - -let exists_argtype s = List.mem_assoc s !dyntab + t let default_empty_argtype_value s = List.assoc s !dyntab diff --git a/interp/genarg.mli b/interp/genarg.mli index 7bcb5aa11..0f6ffddd9 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -92,120 +92,116 @@ ExtraArgType of string '_a '_b {% \end{%}verbatim{% }%} *) -(** 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 -*) +(** {5 Base type combinators} *) -type rlevel -type glevel -type tlevel +type ('raw, 'glob, 'top) genarg_type +(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized + one, and ['top] the internalized one. *) + +type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type +(** Alias for concision when the three types agree. *) + +val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type +(** Create a new generic type of argument: force to associate + unique ML types at each of the three levels. *) + +(** {6 Type constructors} *) + +val wit_bool : bool uniform_genarg_type + +val wit_int : int uniform_genarg_type -type ('a,'co) abstract_argument_type +val wit_int_or_var : int or_var uniform_genarg_type -val rawwit_bool : (bool,rlevel) abstract_argument_type -val globwit_bool : (bool,glevel) abstract_argument_type -val wit_bool : (bool,tlevel) abstract_argument_type +val wit_string : string uniform_genarg_type -val rawwit_int : (int,rlevel) abstract_argument_type -val globwit_int : (int,glevel) abstract_argument_type -val wit_int : (int,tlevel) abstract_argument_type +val wit_pre_ident : string uniform_genarg_type -val rawwit_int_or_var : (int or_var,rlevel) abstract_argument_type -val globwit_int_or_var : (int or_var,glevel) abstract_argument_type -val wit_int_or_var : (int or_var,tlevel) abstract_argument_type +val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type -val rawwit_string : (string,rlevel) abstract_argument_type -val globwit_string : (string,glevel) abstract_argument_type +val wit_ident : Id.t uniform_genarg_type -val wit_string : (string,tlevel) abstract_argument_type +val wit_pattern_ident : Id.t uniform_genarg_type -val rawwit_pre_ident : (string,rlevel) abstract_argument_type -val globwit_pre_ident : (string,glevel) abstract_argument_type -val wit_pre_ident : (string,tlevel) abstract_argument_type +val wit_ident_gen : bool -> Id.t uniform_genarg_type -val rawwit_intro_pattern : (intro_pattern_expr located,rlevel) abstract_argument_type -val globwit_intro_pattern : (intro_pattern_expr located,glevel) abstract_argument_type -val wit_intro_pattern : (intro_pattern_expr located,tlevel) abstract_argument_type +val wit_var : (Id.t located, Id.t located, Id.t) genarg_type -val rawwit_ident : (Id.t,rlevel) abstract_argument_type -val globwit_ident : (Id.t,glevel) abstract_argument_type -val wit_ident : (Id.t,tlevel) abstract_argument_type +val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type -val rawwit_pattern_ident : (Id.t,rlevel) abstract_argument_type -val globwit_pattern_ident : (Id.t,glevel) abstract_argument_type -val wit_pattern_ident : (Id.t,tlevel) abstract_argument_type +val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val rawwit_ident_gen : bool -> (Id.t,rlevel) abstract_argument_type -val globwit_ident_gen : bool -> (Id.t,glevel) abstract_argument_type -val wit_ident_gen : bool -> (Id.t,tlevel) abstract_argument_type +val wit_sort : (glob_sort, glob_sort, sorts) genarg_type -val rawwit_var : (Id.t located,rlevel) abstract_argument_type -val globwit_var : (Id.t located,glevel) abstract_argument_type -val wit_var : (Id.t,tlevel) abstract_argument_type +val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val rawwit_ref : (reference,rlevel) abstract_argument_type -val globwit_ref : (global_reference located or_var,glevel) abstract_argument_type -val wit_ref : (global_reference,tlevel) abstract_argument_type +val wit_constr_may_eval : + ((constr_expr,reference or_by_notation,constr_expr) may_eval, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, + constr) genarg_type -val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type -val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type -val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type +val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type -val rawwit_sort : (glob_sort,rlevel) abstract_argument_type -val globwit_sort : (glob_sort,glevel) abstract_argument_type -val wit_sort : (sorts,tlevel) abstract_argument_type +val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type -val rawwit_constr : (constr_expr,rlevel) abstract_argument_type -val globwit_constr : (glob_constr_and_expr,glevel) abstract_argument_type -val wit_constr : (constr,tlevel) abstract_argument_type +val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_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 : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,glevel) abstract_argument_type -val wit_constr_may_eval : (constr,tlevel) abstract_argument_type +val wit_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings sigma) genarg_type -val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type -val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type +val wit_bindings : + (constr_expr bindings, + glob_constr_and_expr bindings, + constr bindings sigma) genarg_type -val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type -val wit_open_constr : (open_constr,tlevel) abstract_argument_type +val wit_red_expr : + ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type -val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type -val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type +val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type -val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type -val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type -val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type +(** {5 Specialized types} *) -val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type -val globwit_bindings : (glob_constr_and_expr bindings,glevel) abstract_argument_type -val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type +(** 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 +*) + +type rlevel +type glevel +type tlevel -val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type -val globwit_red_expr : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_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 +type ('a, 'co) abstract_argument_type +(** Type at level ['co] represented by an OCaml value of type ['a]. *) -val wit_list0 : - ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type +val rawwit : ('a, 'b, 'c) genarg_type -> ('a, 'co) abstract_argument_type +(** Projection on the raw type constructor. *) -val wit_list1 : - ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type +val glbwit : ('a, 'b, 'c) genarg_type -> ('b, 'co) abstract_argument_type +(** Projection on the globalized type constructor. *) -val wit_opt : - ('a,'co) abstract_argument_type -> ('a option,'co) abstract_argument_type +val topwit : ('a, 'b, 'c) genarg_type -> ('c, 'co) abstract_argument_type +(** Projection on the internalized type constructor. *) -val wit_pair : - ('a,'co) abstract_argument_type -> - ('b,'co) abstract_argument_type -> - ('a * 'b,'co) abstract_argument_type +(** {5 Generic arguments} *) -(** ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) type 'a generic_argument +(** A inhabitant of ['level generic_argument] is a inhabitant of some type at + level ['level], together with the representation of this type. *) + +(** {6 Manipulation of generic arguments} + +Those functions fail if they are applied to an argument which has not the right +dynamic type. *) val fold_list0 : ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c @@ -237,16 +233,6 @@ val app_pair : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument -(** create a new generic type of argument: force to associate - unique ML types at each of the three levels *) -val create_arg : 'rawa option -> - string -> - ('a,tlevel) abstract_argument_type - * ('globa,glevel) abstract_argument_type - * ('rawa,rlevel) abstract_argument_type - -val exists_argtype : string -> bool - type argument_type = (** Basic types *) | BoolArgType @@ -298,4 +284,4 @@ type an_arg_of_this_type val in_generic : argument_type -> an_arg_of_this_type -> 'co generic_argument -val default_empty_value : ('a,rlevel) abstract_argument_type -> 'a option +val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option |