From bd7da353ea503423206e329af7a56174cb39f435 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 21 Jun 2013 21:04:00 +0000 Subject: Splitted up Genarg in four different levels: 1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/genarg.mli | 250 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 250 insertions(+) create mode 100644 lib/genarg.mli (limited to 'lib/genarg.mli') diff --git a/lib/genarg.mli b/lib/genarg.mli new file mode 100644 index 000000000..14133fff0 --- /dev/null +++ b/lib/genarg.mli @@ -0,0 +1,250 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raw_object ---> raw_object generic_argument -------+ + encapsulation decaps| + | + V + raw_object + | + globalization | + V + glob_object + | + encaps | + in_glob | + V + glob_object generic_argument + | + out in out_glob | + object <--- object generic_argument <--- object <--- glob_object <---+ + | decaps encaps interp decaps + | + V +effective use +{% \end{%}verbatim{% }%} + +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], [glob_constr] or +[constr]. + +Transformation for each type : +{% \begin{%}verbatim{% }%} +tag raw open type cooked closed type + +BoolArgType bool bool +IntArgType int int +IntOrVarArgType int or_var int +StringArgType string (parsed w/ "") string +PreIdentArgType string (parsed w/o "") (vernac only) +IdentArgType true identifier identifier +IdentArgType false identifier (pattern_ident) identifier +IntroPatternArgType intro_pattern_expr intro_pattern_expr +VarArgType identifier located identifier +RefArgType reference global_reference +QuantHypArgType quantified_hypothesis quantified_hypothesis +ConstrArgType constr_expr constr +ConstrMayEvalArgType constr_expr may_eval constr +OpenConstrArgType open_constr_expr open_constr +ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings +BindingsArgType constr_expr bindings constr bindings +List0ArgType of argument_type +List1ArgType of argument_type +OptArgType of argument_type +ExtraArgType of string '_a '_b +{% \end{%}verbatim{% }%} +*) + +(** {5 Generic types} *) + +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 make0 : '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. *) + +val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type +(** Alias for [make0]. *) + +(** {5 Specialized types} *) + +(** 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 + +type ('a, 'co) abstract_argument_type +(** Type at level ['co] represented by an OCaml value of type ['a]. *) + +type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type +(** Specialized type at raw level. *) + +type 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type +(** Specialized type at globalized level. *) + +type 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type +(** Specialized type at internalized level. *) + +(** {6 Projections} *) + +val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type +(** Projection on the raw type constructor. *) + +val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type +(** Projection on the globalized type constructor. *) + +val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type +(** Projection on the internalized type constructor. *) + +(** {5 Generic arguments} *) + +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. *) + +type raw_generic_argument = rlevel generic_argument +type glob_generic_argument = glevel generic_argument +type typed_generic_argument = tlevel generic_argument + +(** {6 Constructors} *) + +val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument +(** [in_gen t x] embeds an argument of type [t] into a generic argument. *) + +val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a +(** [out_gen t x] recovers an argument of type [t] from a generic argument. It + fails if [x] has not the right dynamic type. *) + +val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool +(** [has_type v t] tells whether [v] has type [t]. If true, it ensures that + [out_gen t v] will not raise a dynamic type exception. *) + +(** {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 + +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 -> '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) -> +'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) -> +'a generic_argument -> 'b generic_argument + +val app_pair : + ('a generic_argument -> 'b generic_argument) -> + ('a generic_argument -> 'b generic_argument) + -> 'a generic_argument -> 'b generic_argument + +(** {6 Type reification} *) + +type argument_type = + (** Basic types *) + | IntOrVarArgType + | IntroPatternArgType + | IdentArgType of bool + | VarArgType + | RefArgType + (** Specific types *) + | GenArgType + | SortArgType + | ConstrArgType + | ConstrMayEvalArgType + | QuantHypArgType + | OpenConstrArgType of bool + | ConstrWithBindingsArgType + | BindingsArgType + | RedExprArgType + | List0ArgType of argument_type + | List1ArgType of argument_type + | OptArgType of argument_type + | PairArgType of argument_type * argument_type + | ExtraArgType of string + +val argument_type_eq : argument_type -> argument_type -> bool + +val genarg_tag : 'a generic_argument -> argument_type + +val unquote : ('a, 'co) abstract_argument_type -> argument_type + +(** {5 Basic generic type constructors} *) + +(** {6 Parameterized types} *) + +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 + +(** {5 Magic used by the parser} *) + +val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option + +val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit +(** Used by the extension to give a name to types. The string should be the + absolute path of the argument witness, e.g. + [register_name0 wit_toto "MyArg.wit_toto"]. *) + +val get_name0 : string -> string +(** Return the absolute path of a given witness. *) + +(** {5 Unsafe loophole} *) + +module Unsafe : +sig + +(** Unsafe magic functions. Not for kids. This is provided here as a loophole to + escape this module. Do NOT use outside of the dedicated areas. NOT. EVER. *) + +val inj : argument_type -> Obj.t -> 'lev generic_argument +(** Injects an object as generic argument. !!!BEWARE!!! only do this as + [inj tpe x] where: + + 1. [tpe] is the reification of a [('a, 'b, 'c) genarg_type]; + 2. [x] has type ['a], ['b] or ['c] according to the return level ['lev]. *) + +val prj : 'lev generic_argument -> Obj.t +(** Recover the contents of a generic argument. *) + +end -- cgit v1.2.3