diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 21:04:00 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 21:04:00 +0000 |
commit | bd7da353ea503423206e329af7a56174cb39f435 (patch) | |
tree | 275cce39ed6fb899660155a43ab0987c4f83025b | |
parent | 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 (diff) |
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
-rw-r--r-- | dev/printers.mllib | 3 | ||||
-rw-r--r-- | grammar/argextend.ml4 | 13 | ||||
-rw-r--r-- | interp/genintern.ml | 82 | ||||
-rw-r--r-- | interp/genintern.mli | 43 | ||||
-rw-r--r-- | interp/interp.mllib | 4 | ||||
-rw-r--r-- | interp/stdarg.ml | 36 | ||||
-rw-r--r-- | lib/genarg.ml (renamed from interp/genarg.ml) | 134 | ||||
-rw-r--r-- | lib/genarg.mli (renamed from interp/genarg.mli) | 116 | ||||
-rw-r--r-- | lib/lib.mllib | 1 | ||||
-rw-r--r-- | parsing/egramml.ml | 2 | ||||
-rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 11 | ||||
-rw-r--r-- | printing/genprint.ml | 53 | ||||
-rw-r--r-- | printing/genprint.mli | 28 | ||||
-rw-r--r-- | printing/pptactic.ml | 6 | ||||
-rw-r--r-- | printing/printing.mllib | 1 | ||||
-rw-r--r-- | tactics/geninterp.ml | 53 | ||||
-rw-r--r-- | tactics/geninterp.mli | 28 | ||||
-rw-r--r-- | tactics/tacintern.ml | 4 | ||||
-rw-r--r-- | tactics/tacintern.mli | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 38 | ||||
-rw-r--r-- | tactics/tacinterp.mli | 6 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 2 | ||||
-rw-r--r-- | tactics/tactics.mllib | 1 |
23 files changed, 404 insertions, 263 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 80eaa6b85..3a8a2cc3d 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 dffca2c62..fd18dfdf1 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/genintern.ml b/interp/genintern.ml new file mode 100644 index 000000000..00ea3a71b --- /dev/null +++ b/interp/genintern.ml @@ -0,0 +1,82 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Names +open Mod_subst +open Genarg + +type glob_sign = { + ltacvars : Id.t list * Id.t list; + ltacrecvars : (Id.t * Nametab.ltac_constant) list; + gsigma : Evd.evar_map; + genv : Environ.env } + +type ('raw, 'glb) intern_fun = glob_sign -> '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 000000000..25050fe7c --- /dev/null +++ b/interp/genintern.mli @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Mod_subst +open Genarg + +type glob_sign = { + ltacvars : Id.t list * Id.t list; + ltacrecvars : (Id.t * Nametab.ltac_constant) list; + gsigma : Evd.evar_map; + genv : Environ.env } + +(** {5 Internalization functions} *) + +type ('raw, 'glb) intern_fun = glob_sign -> '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 77e2e5c00..7f14fe42b 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 1216e06b1..6f2ff6ec4 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/interp/genarg.ml b/lib/genarg.ml index c0526d508..dbde4652c 100644 --- a/interp/genarg.ml +++ b/lib/genarg.ml @@ -8,7 +8,6 @@ open Pp open Util -open Names type argument_type = (* Basic types *) @@ -150,126 +149,29 @@ 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 "<abstract>"); - arg0_gprint = (fun _ -> str "<abstract>"); - arg0_tprint = (fun _ -> str "<abstract>"); - 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 "<abstract>"); - arg0_gprint = (fun _ -> str "<abstract>"); - arg0_tprint = (fun _ -> str "<abstract>"); - 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) +(** 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) -> + | 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 + String.Map.find s !arg0_map | _ -> None in match aux t with | Some v -> Some (Obj.obj v) @@ -290,3 +192,11 @@ let register_name0 t name = match t with 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/interp/genarg.mli b/lib/genarg.mli index 629bd62a7..14133fff0 100644 --- a/interp/genarg.mli +++ b/lib/genarg.mli @@ -6,10 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc -open Pp -open Names - (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. @@ -79,9 +75,12 @@ type ('raw, 'glob, 'top) genarg_type 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 +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. FIXME: almost deprecated. *) + 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} *) @@ -177,77 +176,6 @@ val app_pair : ('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 = @@ -291,20 +219,6 @@ val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, '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 @@ -314,3 +228,23 @@ val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit 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 be27eed7d..f28b49a4f 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 a24804786..dc558e841 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 a90c565f1..8f570af7e 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 000000000..5a1da2fd7 --- /dev/null +++ b/printing/genprint.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Genarg + +type printer = { + raw : Obj.t -> std_ppcmds; + glb : Obj.t -> std_ppcmds; + top : Obj.t -> std_ppcmds; +} + +let default_printer name = (); fun _ -> str "<genarg:" ++ str name ++ 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 000000000..8300f12bf --- /dev/null +++ b/printing/genprint.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Entry point for generic printers *) + +open Pp +open Genarg + +val raw_print : ('raw, 'glb, 'top) genarg_type -> '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 2ff19c960..47bc20036 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 f5840bc3e..9b3bffc8d 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 000000000..deba01536 --- /dev/null +++ b/tactics/geninterp.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Names +open Genarg + +module TacStore = Store.Make(struct end) + +type interp_sign = { + lfun : (Id.t * tlevel generic_argument) list; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> + 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 000000000..0f5e6bf0f --- /dev/null +++ b/tactics/geninterp.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Interpretation functions for generic arguments. *) + +open Names +open Genarg + +module TacStore : Store.S + +type interp_sign = { + lfun : (Id.t * tlevel generic_argument) list; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> + 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 d085704bb..3e008657f 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 ca33cf21e..3fa59ed3b 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 a13a8faf2..e0fe2cde4 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 254bb9fdd..6affc21a4 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 f1ada9364..dcdaf9dbc 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 c08cc66da..0b97e0852 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Geninterp Dn Termdn Btermdn |