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 --- dev/printers.mllib | 3 +- grammar/argextend.ml4 | 13 +- interp/genarg.ml | 292 ----------------------------------- interp/genarg.mli | 316 -------------------------------------- interp/genintern.ml | 82 ++++++++++ interp/genintern.mli | 43 ++++++ interp/interp.mllib | 4 +- interp/stdarg.ml | 36 ++--- lib/genarg.ml | 202 ++++++++++++++++++++++++ lib/genarg.mli | 250 ++++++++++++++++++++++++++++++ lib/lib.mllib | 1 + parsing/egramml.ml | 2 +- plugins/decl_mode/g_decl_mode.ml4 | 11 +- printing/genprint.ml | 53 +++++++ printing/genprint.mli | 28 ++++ printing/pptactic.ml | 6 +- printing/printing.mllib | 1 + tactics/geninterp.ml | 53 +++++++ tactics/geninterp.mli | 28 ++++ tactics/tacintern.ml | 4 +- tactics/tacintern.mli | 2 +- tactics/tacinterp.ml | 38 ++++- tactics/tacinterp.mli | 6 +- tactics/tacsubst.ml | 2 +- tactics/tactics.mllib | 1 + 25 files changed, 809 insertions(+), 668 deletions(-) delete mode 100644 interp/genarg.ml delete mode 100644 interp/genarg.mli create mode 100644 interp/genintern.ml create mode 100644 interp/genintern.mli create mode 100644 lib/genarg.ml create mode 100644 lib/genarg.mli create mode 100644 printing/genprint.ml create mode 100644 printing/genprint.mli create mode 100644 tactics/geninterp.ml create mode 100644 tactics/geninterp.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 80eaa6b850..3a8a2cc3d8 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -34,6 +34,7 @@ Predicate Rtree Heap Dnet +Genarg Names Univ @@ -120,11 +121,11 @@ Cases Pretyping Declaremods +Genprint Tok Lexer Ppextend Pputils -Genarg Stdarg Constrarg Constrexpr_ops diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index dffca2c622..fd18dfdf1f 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -186,21 +186,16 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = (Genarg.in_gen $make_globwit loc globtyp$ x)) >> end | Some f -> <:expr< $lid:f$>> in - let defs = [ - <:patt< Genarg.arg0_subst >>, subst; - <:patt< Genarg.arg0_glob >>, glob; - <:patt< Genarg.arg0_interp >>, interp; - ] in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< Genarg.rawwit $wit$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in declare_str_items loc - [ <:str_item< - value ($lid:"wit_"^s$) = - let arg = { (Genarg.default_arg0 $se$) with $list:defs$ } in - Genarg.make0 $default_value$ $se$ arg >>; + [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $default_value$ $se$ >>; + <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; + <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; + <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { diff --git a/interp/genarg.ml b/interp/genarg.ml deleted file mode 100644 index c0526d5085..0000000000 --- a/interp/genarg.ml +++ /dev/null @@ -1,292 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true -| IntroPatternArgType, IntroPatternArgType -> true -| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2 -| VarArgType, VarArgType -> true -| RefArgType, RefArgType -> true -| GenArgType, GenArgType -> true -| SortArgType, SortArgType -> true -| ConstrArgType, ConstrArgType -> true -| ConstrMayEvalArgType, ConstrMayEvalArgType -> true -| QuantHypArgType, QuantHypArgType -> true -| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2 -| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true -| BindingsArgType, BindingsArgType -> true -| RedExprArgType, RedExprArgType -> true -| List0ArgType arg1, List0ArgType arg2 -> argument_type_eq arg1 arg2 -| List1ArgType arg1, List1ArgType arg2 -> argument_type_eq arg1 arg2 -| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 -| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> - argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r -| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 -| _ -> false - -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 rlevel -type glevel -type tlevel - -type 'a generic_argument = argument_type * Obj.t -type raw_generic_argument = rlevel generic_argument -type glob_generic_argument = glevel generic_argument -type typed_generic_argument = tlevel generic_argument - -let rawwit t = t -let glbwit t = t -let topwit t = t - -let wit_list0 t = List0ArgType t - -let wit_list1 t = List1ArgType t - -let wit_opt t = OptArgType t - -let wit_pair t1 t2 = PairArgType (t1,t2) - -let in_gen t o = (t,Obj.repr o) -let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen" -let genarg_tag (s,_) = s - -let fold_list0 f = function - | (List0ArgType t, l) -> - List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) - | _ -> failwith "Genarg: not a list0" - -let fold_list1 f = function - | (List1ArgType t, l) -> - List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) - | _ -> failwith "Genarg: not a list1" - -let fold_opt f a = function - | (OptArgType t, l) -> - (match Obj.magic l with - | None -> a - | Some x -> f (in_gen t x)) - | _ -> failwith "Genarg: not a opt" - -let fold_pair f = function - | (PairArgType (t1,t2), l) -> - let (x1,x2) = Obj.magic l in - f (in_gen t1 x1) (in_gen t2 x2) - | _ -> failwith "Genarg: not a pair" - -let app_list0 f = function - | (List0ArgType t as u, l) -> - let o = Obj.magic l in - (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) - | _ -> failwith "Genarg: not a list0" - -let app_list1 f = function - | (List1ArgType t as u, l) -> - let o = Obj.magic l in - (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) - | _ -> failwith "Genarg: not a list1" - -let app_opt f = function - | (OptArgType t as u, l) -> - let o = Obj.magic l in - (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o)) - | _ -> failwith "Genarg: not an opt" - -let app_pair f1 f2 = function - | (PairArgType (t1,t2) as u, l) -> - let (o1,o2) = Obj.magic l in - let o1 = out_gen t1 (f1 (in_gen t1 o1)) in - let o2 = out_gen t2 (f2 (in_gen t2 o2)) in - (u, Obj.repr (o1,o2)) - | _ -> failwith "Genarg: not a pair" - -let has_type (t, v) u = argument_type_eq t u - -let unquote x = x - -type an_arg_of_this_type = Obj.t - -let in_generic t x = (t, Obj.repr x) - -type ('a,'b) abstract_argument_type = argument_type -type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type -type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type -type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type - -(** New interface for genargs. *) - -type glob_sign = { - ltacvars : Id.t list * Id.t list; - ltacrecvars : (Id.t * Nametab.ltac_constant) list; - gsigma : Evd.evar_map; - genv : Environ.env } - -module TacStore = Store.Make(struct end) - -type interp_sign = { - lfun : (Id.t * tlevel generic_argument) list; - extra : TacStore.t } - -type ('raw, 'glb, 'top) arg0 = { - arg0_rprint : 'raw -> std_ppcmds; - arg0_gprint : 'glb -> std_ppcmds; - arg0_tprint : 'top -> std_ppcmds; - arg0_glob : glob_sign -> 'raw -> glob_sign * 'glb; - arg0_subst : Mod_subst.substitution -> 'glb -> 'glb; - arg0_interp : interp_sign -> - Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top; -} - -let default_arg0 name = { - arg0_rprint = (fun _ -> str ""); - arg0_gprint = (fun _ -> str ""); - arg0_tprint = (fun _ -> str ""); - arg0_glob = (fun _ _ -> failwith ("undefined globalizer for " ^ name)); - arg0_subst = (fun _ _ -> failwith ("undefined substitutor for " ^ name)); - arg0_interp = (fun _ _ _ -> failwith ("undefined interpreter for " ^ name)); -} - -let default_uniform_arg0 name = { - arg0_rprint = (fun _ -> str ""); - arg0_gprint = (fun _ -> str ""); - arg0_tprint = (fun _ -> str ""); - arg0_glob = (fun ist x -> (ist, x)); - arg0_subst = (fun _ x -> x); - arg0_interp = (fun _ gl x -> (gl.Evd.sigma, x)); -} - -let arg0_map = ref (String.Map.empty : (Obj.t * Obj.t option) String.Map.t) -(** First component is the argument itself, second is the default raw - inhabitant. *) - -let make0 def name arg = - let () = - if String.Map.mem name !arg0_map then - Errors.anomaly (str "Genarg " ++ str name ++ str " already defined") - in - let arg = Obj.repr arg in - let def = Obj.magic def in - let () = arg0_map := String.Map.add name (arg, def) !arg0_map in - ExtraArgType name - -let get_obj name = - let (obj, _) = String.Map.find name !arg0_map in - (Obj.obj obj : (Obj.t, Obj.t, Obj.t) arg0) - -(** For now, the following functions are quite dummy and should only be applied - to an extra argument type, otherwise, they will badly fail. *) - -let arg_gen = function -| ExtraArgType name -> Obj.magic (get_obj name) -| _ -> assert false - -let rec raw_print (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - obj.arg0_rprint v -| _ -> assert false (* TODO *) - -let rec glb_print (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - obj.arg0_gprint v -| _ -> assert false (* TODO *) - -let rec top_print (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - obj.arg0_rprint v -| _ -> assert false (* TODO *) - -let rec globalize ist (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - let (ist, ans) = obj.arg0_glob ist v in - (ist, (tpe, ans)) -| _ -> assert false (* TODO *) - -let rec substitute subst (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - (tpe, obj.arg0_subst subst v) -| _ -> assert false (* TODO *) - -let rec interpret ist gl (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - let (ist, ans) = obj.arg0_interp ist gl v in - (ist, (tpe, ans)) -| _ -> assert false (* TODO *) - -(** Compatibility layer *) - -let create_arg v s = make0 v s (default_arg0 s) - -let default_empty_value t = - let rec aux = function - | List0ArgType _ -> Some (Obj.repr []) - | OptArgType _ -> Some (Obj.repr None) - | PairArgType(t1,t2) -> - (match aux t1, aux t2 with - | Some v1, Some v2 -> Some (Obj.repr (v1, v2)) - | _ -> None) - | ExtraArgType s -> - let (_, def) = String.Map.find s !arg0_map in - def - | _ -> None in - match aux t with - | Some v -> Some (Obj.obj v) - | None -> None - -(** Hackish part *) - -let arg0_names = ref (String.Map.empty : string String.Map.t) -(** We use this table to associate a name to a given witness, to use it with - the extension mechanism. This is REALLY ad-hoc, but I do not know how to - do so nicely either. *) - -let register_name0 t name = match t with -| ExtraArgType s -> - let () = assert (not (String.Map.mem s !arg0_names)) in - arg0_names := String.Map.add s name !arg0_names -| _ -> failwith "register_name0" - -let get_name0 name = - String.Map.find name !arg0_names diff --git a/interp/genarg.mli b/interp/genarg.mli deleted file mode 100644 index 629bd62a78..0000000000 --- a/interp/genarg.mli +++ /dev/null @@ -1,316 +0,0 @@ -(************************************************************************) -(* 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 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. FIXME: almost deprecated. *) - -(** {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 High-level creation} *) - -(** {5 Genarg environments} *) - -type glob_sign = { - ltacvars : Id.t list * Id.t list; - ltacrecvars : (Id.t * Nametab.ltac_constant) list; - gsigma : Evd.evar_map; - genv : Environ.env } - -module TacStore : Store.S - -type interp_sign = { - lfun : (Id.t * tlevel generic_argument) list; - extra : TacStore.t } - -(** {5 Generic arguments} *) - -type ('raw, 'glb, 'top) arg0 = { - arg0_rprint : 'raw -> std_ppcmds; - (** Printing at raw level function. *) - arg0_gprint : 'glb -> std_ppcmds; - (** Printing at glob level function. *) - arg0_tprint : 'top -> std_ppcmds; - (** Printing at top level function. *) - arg0_glob : glob_sign -> 'raw -> glob_sign * 'glb; - (** Globalization function. *) - arg0_subst : Mod_subst.substitution -> 'glb -> 'glb; - (** Substitution function. *) - arg0_interp : interp_sign -> - Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top; - (** Intepretation function. *) -} - -val make0 : 'raw option -> string -> ('raw, 'glb, 'top) arg0 -> - ('raw, 'glb, 'top) genarg_type -(** [make0 def name arg] create a generic argument named [name] with the - manipulation functions defined in [arg], and with a default empty value - [def]. FIXME: [def] is related to parsing and should be put elsewhere. *) - -val default_arg0 : string -> ('raw, 'glb, 'top) arg0 -(** A default [arg0] with a given name. Printing functions print a dummy value - and glob/subst/interp all fail. *) - -val default_uniform_arg0 : string -> ('a, 'a, 'a) arg0 -(** A default uniform [arg0] with a given name. Printing functions print a dummy - value and glob/subst/interp are all identity. *) - -val arg_gen : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) arg0 -(** Create the manipulation functions for any generic argument type. *) - -(** {5 Generic manipulation functions} - - Those functions are the counterparts of [arg0] fields, but they apply on any - generic argument. - - FIXME: only partially implemented for now. *) - -val raw_print : rlevel generic_argument -> std_ppcmds -val glb_print : glevel generic_argument -> std_ppcmds -val top_print : tlevel generic_argument -> std_ppcmds - -val globalize : glob_sign -> - rlevel generic_argument -> glob_sign * glevel generic_argument - -val substitute : Mod_subst.substitution -> - glevel generic_argument -> glevel generic_argument - -val interpret : interp_sign -> Goal.goal Evd.sigma -> - glevel generic_argument -> Evd.evar_map * tlevel 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} *) - -(** [in_generic] is used in combination with camlp4 [Gramext.action] magic - - [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument] - - where |a|_l is the interpretation of a at level l - - [in_generic] is not typable; we replace the second argument by an absurd - type (with no introduction rule) -*) -type an_arg_of_this_type - -val in_generic : - argument_type -> an_arg_of_this_type -> 'co generic_argument - -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. *) diff --git a/interp/genintern.ml b/interp/genintern.ml new file mode 100644 index 0000000000..00ea3a71bb --- /dev/null +++ b/interp/genintern.ml @@ -0,0 +1,82 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'raw -> glob_sign * 'glb +type 'glb subst_fun = substitution -> 'glb -> 'glb + +let arg0_intern_map = + ref (String.Map.empty : (Obj.t, Obj.t) intern_fun String.Map.t) +let arg0_subst_map = + ref (String.Map.empty : Obj.t subst_fun String.Map.t) + +let get_intern0 name = + try String.Map.find name !arg0_intern_map + with Not_found -> + Errors.anomaly (str "intern0 function not found: " ++ str name) + +let get_subst0 name = + try String.Map.find name !arg0_subst_map + with Not_found -> + Errors.anomaly (str "subst0 function not found: " ++ str name) + +(** For now, the following functions are quite dummy and should only be applied + to an extra argument type, otherwise, they will badly fail. *) + +let rec obj_intern t = match t with +| ExtraArgType s -> get_intern0 s +| _ -> assert false + +let intern t = Obj.magic (obj_intern (unquote (rawwit t))) + +let generic_intern ist v = + let t = genarg_tag v in + let (ist, ans) = obj_intern t ist (Unsafe.prj v) in + (ist, Unsafe.inj t ans) + +(** Substitution functions *) + +let rec obj_substitute t = match t with +| ExtraArgType s -> get_subst0 s +| _ -> assert false + +let substitute t = Obj.magic (obj_substitute (unquote (rawwit t))) + +let generic_substitute subs v = + let t = genarg_tag v in + let ans = obj_substitute t subs (Unsafe.prj v) in + Unsafe.inj t ans + +(** Registering functions *) + +let register_intern0 arg f = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_intern_map then + Errors.anomaly (str "intern0 function already registered: " ++ str s) + else + arg0_intern_map := String.Map.add s (Obj.magic f) !arg0_intern_map +| _ -> assert false + +let register_subst0 arg f = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_subst_map then + Errors.anomaly (str "subst0 function already registered: " ++ str s) + else + arg0_subst_map := String.Map.add s (Obj.magic f) !arg0_subst_map +| _ -> assert false diff --git a/interp/genintern.mli b/interp/genintern.mli new file mode 100644 index 0000000000..25050fe7c8 --- /dev/null +++ b/interp/genintern.mli @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'raw -> glob_sign * 'glb +(** The type of functions used for internalizing generic arguments. *) + +val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun + +val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun + +(** {5 Substitution functions} *) + +type 'glb subst_fun = substitution -> 'glb -> 'glb +(** The type of functions used for substituting generic arguments. *) + +val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun + +val generic_substitute : glob_generic_argument subst_fun + +(** Registering functions *) + +val register_intern0 : ('raw, 'glb, 'top) genarg_type -> + ('raw, 'glb) intern_fun -> unit + +val register_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb subst_fun -> unit diff --git a/interp/interp.mllib b/interp/interp.mllib index 77e2e5c00e..7f14fe42b4 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,11 +1,10 @@ +Genintern Constrexpr_ops Notation_ops Topconstr Ppextend Notation Dumpglob -Genarg -Stdarg Syntax_def Smartlocate Reserve @@ -17,4 +16,5 @@ Constrextern Coqlib Discharge Declare +Stdarg Constrarg diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 1216e06b1b..6f2ff6ec48 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -9,41 +9,23 @@ open Pp open Genarg -let def_uniform name pr = { (default_uniform_arg0 name) with - arg0_rprint = pr; - arg0_gprint = pr; - arg0_tprint = pr; -} - let wit_unit : unit uniform_genarg_type = - let pr_unit _ = str "()" in - let arg = def_uniform "unit" pr_unit in - make0 None "unit" arg + make0 None "unit" let wit_bool : bool uniform_genarg_type = - let pr_bool b = str (if b then "true" else "false") in - let arg = def_uniform "bool" pr_bool in - make0 None "bool" arg - -let () = register_name0 wit_bool "Stdarg.wit_bool" + make0 None "bool" let wit_int : int uniform_genarg_type = - let pr_int = int in - let arg = def_uniform "int" pr_int in - make0 None "int" arg - -let () = register_name0 wit_int "Stdarg.wit_int" + make0 None "int" let wit_string : string uniform_genarg_type = - let pr_string s = str "\"" ++ str s ++ str "\"" in - let arg = def_uniform "string" pr_string in - make0 None "string" arg - -let () = register_name0 wit_string "Stdarg.wit_string" + make0 None "string" let wit_pre_ident : string uniform_genarg_type = - let pr_pre_ident = str in - let arg = def_uniform "preident" pr_pre_ident in - make0 None "preident" arg + make0 None "preident" +let () = register_name0 wit_unit "Stdarg.wit_unit" +let () = register_name0 wit_bool "Stdarg.wit_bool" +let () = register_name0 wit_int "Stdarg.wit_int" +let () = register_name0 wit_string "Stdarg.wit_string" let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" diff --git a/lib/genarg.ml b/lib/genarg.ml new file mode 100644 index 0000000000..dbde4652c7 --- /dev/null +++ b/lib/genarg.ml @@ -0,0 +1,202 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true +| IntroPatternArgType, IntroPatternArgType -> true +| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2 +| VarArgType, VarArgType -> true +| RefArgType, RefArgType -> true +| GenArgType, GenArgType -> true +| SortArgType, SortArgType -> true +| ConstrArgType, ConstrArgType -> true +| ConstrMayEvalArgType, ConstrMayEvalArgType -> true +| QuantHypArgType, QuantHypArgType -> true +| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2 +| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true +| BindingsArgType, BindingsArgType -> true +| RedExprArgType, RedExprArgType -> true +| List0ArgType arg1, List0ArgType arg2 -> argument_type_eq arg1 arg2 +| List1ArgType arg1, List1ArgType arg2 -> argument_type_eq arg1 arg2 +| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 +| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> + argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r +| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 +| _ -> false + +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 rlevel +type glevel +type tlevel + +type 'a generic_argument = argument_type * Obj.t +type raw_generic_argument = rlevel generic_argument +type glob_generic_argument = glevel generic_argument +type typed_generic_argument = tlevel generic_argument + +let rawwit t = t +let glbwit t = t +let topwit t = t + +let wit_list0 t = List0ArgType t + +let wit_list1 t = List1ArgType t + +let wit_opt t = OptArgType t + +let wit_pair t1 t2 = PairArgType (t1,t2) + +let in_gen t o = (t,Obj.repr o) +let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen" +let genarg_tag (s,_) = s + +let fold_list0 f = function + | (List0ArgType t, l) -> + List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) + | _ -> failwith "Genarg: not a list0" + +let fold_list1 f = function + | (List1ArgType t, l) -> + List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) + | _ -> failwith "Genarg: not a list1" + +let fold_opt f a = function + | (OptArgType t, l) -> + (match Obj.magic l with + | None -> a + | Some x -> f (in_gen t x)) + | _ -> failwith "Genarg: not a opt" + +let fold_pair f = function + | (PairArgType (t1,t2), l) -> + let (x1,x2) = Obj.magic l in + f (in_gen t1 x1) (in_gen t2 x2) + | _ -> failwith "Genarg: not a pair" + +let app_list0 f = function + | (List0ArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not a list0" + +let app_list1 f = function + | (List1ArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not a list1" + +let app_opt f = function + | (OptArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not an opt" + +let app_pair f1 f2 = function + | (PairArgType (t1,t2) as u, l) -> + let (o1,o2) = Obj.magic l in + let o1 = out_gen t1 (f1 (in_gen t1 o1)) in + let o2 = out_gen t2 (f2 (in_gen t2 o2)) in + (u, Obj.repr (o1,o2)) + | _ -> failwith "Genarg: not a pair" + +let has_type (t, v) u = argument_type_eq t u + +let unquote x = x + +type an_arg_of_this_type = Obj.t + +let in_generic t x = (t, Obj.repr x) + +type ('a,'b) abstract_argument_type = argument_type +type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type +type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type +type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type + +(** Creating args *) + +let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty + +let create_arg opt name = + if String.Map.mem name !arg0_map then + Errors.anomaly (str "generic argument already declared: " ++ str name) + else + let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in + ExtraArgType name + +let make0 = create_arg + +let default_empty_value t = + let rec aux = function + | List0ArgType _ -> Some (Obj.repr []) + | OptArgType _ -> Some (Obj.repr None) + | PairArgType(t1, t2) -> + (match aux t1, aux t2 with + | Some v1, Some v2 -> Some (Obj.repr (v1, v2)) + | _ -> None) + | ExtraArgType s -> + String.Map.find s !arg0_map + | _ -> None in + match aux t with + | Some v -> Some (Obj.obj v) + | None -> None + +(** Hackish part *) + +let arg0_names = ref (String.Map.empty : string String.Map.t) +(** We use this table to associate a name to a given witness, to use it with + the extension mechanism. This is REALLY ad-hoc, but I do not know how to + do so nicely either. *) + +let register_name0 t name = match t with +| ExtraArgType s -> + let () = assert (not (String.Map.mem s !arg0_names)) in + arg0_names := String.Map.add s name !arg0_names +| _ -> failwith "register_name0" + +let get_name0 name = + String.Map.find name !arg0_names + +module Unsafe = +struct + +let inj tpe x = (tpe, x) +let prj (_, x) = x + +end diff --git a/lib/genarg.mli b/lib/genarg.mli new file mode 100644 index 0000000000..14133fff03 --- /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 diff --git a/lib/lib.mllib b/lib/lib.mllib index be27eed7d8..f28b49a4fe 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -16,3 +16,4 @@ Rtree Heap Dnet Unionfind +Genarg diff --git a/parsing/egramml.ml b/parsing/egramml.ml index a248047865..dc558e8416 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -23,7 +23,7 @@ let make_generic_action | None :: tl -> (* parse a non-binding item *) Gram.action (fun _ -> make env tl) | Some (p, t) :: tl -> (* non-terminal *) - Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in + Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in make [] (List.rev pil) (** Grammar extensions declared at ML level *) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index a90c565f10..8f570af7e2 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -105,12 +105,11 @@ let wit_proof_instr = let subst _ x = x in let glob ist v = (ist, Decl_interp.intern_proof_instr ist v) in let interp ist gl x = (Tacmach.project gl, interp_proof_instr ist gl x) in - let arg = { Genarg.default_arg0 name with - Genarg.arg0_subst = subst; - Genarg.arg0_glob = glob; - Genarg.arg0_interp = interp; - } in - Genarg.make0 None name arg + let arg = Genarg.make0 None name in + let () = Genintern.register_intern0 arg glob in + let () = Genintern.register_subst0 arg subst in + let () = Geninterp.register_interp0 arg interp in + arg let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr diff --git a/printing/genprint.ml b/printing/genprint.ml new file mode 100644 index 0000000000..5a1da2fd7d --- /dev/null +++ b/printing/genprint.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds; + glb : Obj.t -> std_ppcmds; + top : Obj.t -> std_ppcmds; +} + +let default_printer name = (); fun _ -> str "" + +let default_printer name = + let pr = default_printer name in + { raw = pr; glb = pr; top = pr; } + +let (arg0_printer_map : printer String.Map.t ref) = ref String.Map.empty + +let get_printer0 name = + try String.Map.find name !arg0_printer_map + with Not_found -> default_printer name + +let obj_printer t = match t with +| ExtraArgType s -> get_printer0 s +| _ -> assert false + +let raw_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).raw +let glb_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).glb +let top_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).top + +let generic_raw_print v = + (obj_printer (genarg_tag v)).raw (Unsafe.prj v) +let generic_glb_print v = + (obj_printer (genarg_tag v)).glb (Unsafe.prj v) +let generic_top_print v = + (obj_printer (genarg_tag v)).top (Unsafe.prj v) + +let register_print0 arg rpr gpr tpr = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_printer_map then + Errors.anomaly (str "interp0 function already registered: " ++ str s) + else + let pr = { raw = Obj.magic rpr; glb = Obj.magic gpr; top = Obj.magic tpr; } in + arg0_printer_map := String.Map.add s pr !arg0_printer_map +| _ -> assert false diff --git a/printing/genprint.mli b/printing/genprint.mli new file mode 100644 index 0000000000..8300f12bfc --- /dev/null +++ b/printing/genprint.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'raw -> std_ppcmds +(** Printer for raw level generic arguments. *) + +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds +(** Printer for glob level generic arguments. *) + +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds +(** Printer for top level generic arguments. *) + +val generic_raw_print : rlevel generic_argument -> std_ppcmds +val generic_glb_print : glevel generic_argument -> std_ppcmds +val generic_top_print : tlevel generic_argument -> std_ppcmds + +val register_print0 : ('raw, 'glb, 'top) genarg_type -> + ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2ff19c9601..47bc200361 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -177,7 +177,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi x) | ExtraArgType s -> try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genarg.raw_print x + with Not_found -> Genprint.generic_raw_print x let rec pr_glb_generic prc prlc prtac prpat x = @@ -219,7 +219,7 @@ let rec pr_glb_generic prc prlc prtac prpat x = x) | ExtraArgType s -> try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genarg.glb_print x + with Not_found -> Genprint.generic_glb_print x let rec pr_top_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with @@ -256,7 +256,7 @@ let rec pr_top_generic prc prlc prtac prpat x = x) | ExtraArgType s -> try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genarg.top_print x + with Not_found -> Genprint.generic_top_print x let rec tacarg_using_rule_token pr_gen = function | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al) diff --git a/printing/printing.mllib b/printing/printing.mllib index f5840bc3ea..9b3bffc8d6 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,3 +1,4 @@ +Genprint Pputils Ppconstr Printer diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml new file mode 100644 index 0000000000..deba015362 --- /dev/null +++ b/tactics/geninterp.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top + +let arg0_interp_map = + ref (String.Map.empty : (Obj.t, Obj.t) interp_fun String.Map.t) + +let get_interp0 name = + try String.Map.find name !arg0_interp_map + with Not_found -> + Errors.anomaly (str "interp0 function not found: " ++ str name) + +(** For now, the following functions are quite dummy and should only be applied + to an extra argument type, otherwise, they will badly fail. *) + +let rec obj_interp t = match t with +| ExtraArgType s -> get_interp0 s +| _ -> assert false + +let interp t = Obj.magic (obj_interp (unquote (rawwit t))) + +let generic_interp ist gl v = + let t = genarg_tag v in + let (sigma, ans) = obj_interp t ist gl (Unsafe.prj v) in + (sigma, Unsafe.inj t ans) + +(** Registering functions *) + +let register_interp0 arg f = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_interp_map then + Errors.anomaly (str "interp0 function already registered: " ++ str s) + else + arg0_interp_map := String.Map.add s (Obj.magic f) !arg0_interp_map +| _ -> assert false diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli new file mode 100644 index 0000000000..0f5e6bf0ff --- /dev/null +++ b/tactics/geninterp.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun + +val generic_interp : (glob_generic_argument, typed_generic_argument) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index d085704bbb..3e008657fe 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -53,7 +53,7 @@ let skip_metaid = function (** Generic arguments *) -type glob_sign = Genarg.glob_sign = { +type glob_sign = Genintern.glob_sign = { ltacvars : Id.t list * Id.t list; (* ltac variables and the subset of vars introduced by Intro/Let/... *) ltacrecvars : (Id.t * ltac_constant) list; @@ -798,7 +798,7 @@ and intern_genarg ist x = in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist (out_gen (rawwit (wit_tactic n)) x)) | None -> - snd (Genarg.globalize ist x) + snd (Genintern.generic_intern ist x) (** Other entry points *) diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index ca33cf21ec..3fa59ed3b9 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -23,7 +23,7 @@ open Nametab (** Globalization of tactic expressions : Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) -type glob_sign = Genarg.glob_sign = { +type glob_sign = Genintern.glob_sign = { ltacvars : Id.t list * Id.t list; ltacrecvars : (Id.t * ltac_constant) list; gsigma : Evd.evar_map; diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a13a8faf2e..e0fe2cde41 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -87,7 +87,7 @@ let catch_error call_trace tac g = raise located_exc end -module TacStore = Genarg.TacStore +module TacStore = Geninterp.TacStore let f_avoid_ids : Id.t list TacStore.field = TacStore.field () (* ids inherited from the call context (needed to get fresh ids) *) @@ -95,7 +95,7 @@ let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () (* Signature for interpretation: val_interp and interpretation functions *) -type interp_sign = Genarg.interp_sign = { +type interp_sign = Geninterp.interp_sign = { lfun : (Id.t * value) list; extra : TacStore.t } @@ -1437,7 +1437,7 @@ and interp_genarg ist gl x = in_gen (topwit (wit_tactic n)) (TacArg(dloc,valueIn (of_tacvalue f))) | None -> - let (sigma,v) = interpret ist gl x in + let (sigma,v) = Geninterp.generic_interp ist gl x in evdref:=sigma; v in @@ -1966,7 +1966,7 @@ and interp_atomic ist gl tac = | List0ArgType _ -> app_list0 f x | List1ArgType _ -> app_list1 f x | ExtraArgType _ -> - let (sigma, v) = Genarg.interpret ist { gl with sigma = !evdref } x in + let (sigma, v) = Geninterp.generic_interp ist { gl with sigma = !evdref } x in evdref := sigma; v | QuantHypArgType | RedExprArgType @@ -2021,6 +2021,36 @@ let hide_interp t ot gl = | None -> t gl | Some t' -> (tclTHEN t t') gl +(***************************************************************************) +(** Register standard arguments *) + +let def_intern ist x = (ist, x) +let def_subst _ x = x +let def_interp ist gl x = (gl.Evd.sigma, x) + +let declare_uniform t pr = + Genintern.register_intern0 t def_intern; + Genintern.register_subst0 t def_subst; + Geninterp.register_interp0 t def_interp; + Genprint.register_print0 t pr pr pr + +let () = + let pr_unit _ = str "()" in + declare_uniform wit_unit pr_unit + +let () = + declare_uniform wit_int int + +let () = + let pr_bool b = if b then str "true" else str "false" in + declare_uniform wit_bool pr_bool + +let () = + let pr_string s = str "\"" ++ str s ++ str "\"" in + declare_uniform wit_string pr_string + +let () = + declare_uniform wit_pre_ident str (***************************************************************************) (* Other entry points *) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 254bb9fdd8..6affc21a47 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -33,11 +33,11 @@ end type value = Value.t module TacStore : Store.S with - type t = Genarg.TacStore.t - and type 'a field = 'a Genarg.TacStore.field + type t = Geninterp.TacStore.t + and type 'a field = 'a Geninterp.TacStore.field (** Signature for interpretation: val\_interp and interpretation functions *) -type interp_sign = Genarg.interp_sign = { +type interp_sign = Geninterp.interp_sign = { lfun : (Id.t * value) list; extra : TacStore.t } diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index f1ada93649..dcdaf9dbc1 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -329,6 +329,6 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen (glbwit (Extrawit.wit_tactic n)) (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x)) | None -> - Genarg.substitute subst x + Genintern.generic_substitute subst x let _ = Hook.set Auto.extern_subst_tactic subst_tactic diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index c08cc66dad..0b97e08527 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Geninterp Dn Termdn Btermdn -- cgit v1.2.3