From a3b4bde65a350bf3dc54ccec8f7608355c6a008a Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Jun 2013 19:48:50 +0000 Subject: Proof-of-concept: moved four easy-to-handle generic arguments to their own file, Stdarg. This required a little trick to correctly handle wit_* naming. We use a dynamic table to remember exactly where those arguments come from. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/printers.mllib | 1 + dev/top_printers.ml | 4 ---- grammar/argextend.ml4 | 20 ++++++++++---------- grammar/grammar.mllib | 1 + grammar/q_coqast.ml4 | 4 ---- interp/genarg.ml | 32 ++++++++++++++++---------------- interp/genarg.mli | 20 ++++++++------------ interp/interp.mllib | 1 + interp/stdarg.ml | 44 ++++++++++++++++++++++++++++++++++++++++++++ interp/stdarg.mli | 19 +++++++++++++++++++ parsing/pcoq.ml4 | 1 + printing/pptactic.ml | 18 +++--------------- tactics/taccoerce.ml | 1 + tactics/tacintern.ml | 6 ------ tactics/tacinterp.ml | 29 ++++++++--------------------- tactics/tacsubst.ml | 4 ---- 16 files changed, 113 insertions(+), 92 deletions(-) create mode 100644 interp/stdarg.ml create mode 100644 interp/stdarg.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 76fbbfdd51..c16b4abbac 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -125,6 +125,7 @@ Lexer Ppextend Pputils Genarg +Stdarg Constrexpr_ops Notation_ops Topconstr diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4857b16cc1..939e9422ac 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -351,11 +351,7 @@ let pploc x = let (l,r) = Loc.unloc x in (* extendable tactic arguments *) let rec pr_argument_type = function (* Basic types *) - | BoolArgType -> str"bool" - | IntArgType -> str"int" | IntOrVarArgType -> str"int-or-var" - | StringArgType -> str"string" - | PreIdentArgType -> str"pre-ident" | IntroPatternArgType -> str"intro-pattern" | IdentArgType true -> str"ident" | IdentArgType false -> str"pattern_ident" diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index b5830e7896..4ea5f35c11 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -18,20 +18,20 @@ let default_loc = <:expr< Loc.ghost >> let mk_extraarg s = if Extrawit.tactic_genarg_level s = None then - <:expr< $lid:"wit_"^s$ >> + try + let name = Genarg.get_name0 s in + <:expr< $lid:name$ >> + with Not_found -> + <:expr< $lid:"wit_"^s$ >> else - <:expr< - let module WIT = struct - open Extrawit; - value wit = $lid:"wit_"^s$; - end in WIT.wit >> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"wit_"^s$; + end in WIT.wit >> let rec make_wit loc = function - | BoolArgType -> <:expr< Genarg.wit_bool >> - | IntArgType -> <:expr< Genarg.wit_int >> | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> - | StringArgType -> <:expr< Genarg.wit_string >> - | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.wit_var >> diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 818d220b81..a97b8a2a63 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -27,6 +27,7 @@ Unicode Names Libnames Genarg +Stdarg Tok Lexer Extrawit diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 0f5be6efb7..65aeef11e1 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -201,15 +201,11 @@ let mlexpr_of_red_expr = function <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> let rec mlexpr_of_argtype loc = function - | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> - | Genarg.IntArgType -> <:expr< Genarg.IntArgType >> | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> - | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> - | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> diff --git a/interp/genarg.ml b/interp/genarg.ml index 18408c8f50..83038c8ba0 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -15,11 +15,7 @@ open Misctypes type argument_type = (* Basic types *) - | BoolArgType - | IntArgType | IntOrVarArgType - | StringArgType - | PreIdentArgType | IntroPatternArgType | IdentArgType of bool | VarArgType @@ -41,11 +37,7 @@ type argument_type = | ExtraArgType of string let rec argument_type_eq arg1 arg2 = match arg1, arg2 with -| BoolArgType, BoolArgType -> true -| IntArgType, IntArgType -> true | IntOrVarArgType, IntOrVarArgType -> true -| StringArgType, StringArgType -> true -| PreIdentArgType, PreIdentArgType -> true | IntroPatternArgType, IntroPatternArgType -> true | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2 | VarArgType, VarArgType -> true @@ -97,16 +89,8 @@ let rawwit t = t let glbwit t = t let topwit t = t -let wit_bool = BoolArgType - -let wit_int = IntArgType - let wit_int_or_var = IntOrVarArgType -let wit_string = StringArgType - -let wit_pre_ident = PreIdentArgType - let wit_intro_pattern = IntroPatternArgType let wit_ident_gen b = IdentArgType b @@ -339,3 +323,19 @@ let default_empty_value t = 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 index 20311be66b..bbd783047c 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -274,11 +274,7 @@ val interpret : interp_sign -> Goal.goal Evd.sigma -> type argument_type = (** Basic types *) - | BoolArgType - | IntArgType | IntOrVarArgType - | StringArgType - | PreIdentArgType | IntroPatternArgType | IdentArgType of bool | VarArgType @@ -311,16 +307,8 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type open Evd -val wit_bool : bool uniform_genarg_type - -val wit_int : int uniform_genarg_type - val wit_int_or_var : int or_var uniform_genarg_type -val wit_string : string uniform_genarg_type - -val wit_pre_ident : string uniform_genarg_type - val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type val wit_ident : Id.t uniform_genarg_type @@ -392,3 +380,11 @@ 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/interp.mllib b/interp/interp.mllib index 6d7e921119..86440bc297 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -5,6 +5,7 @@ Ppextend Notation Dumpglob Genarg +Stdarg Syntax_def Smartlocate Reserve diff --git a/interp/stdarg.ml b/interp/stdarg.ml new file mode 100644 index 0000000000..cfc65bde8b --- /dev/null +++ b/interp/stdarg.ml @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* str (if out_gen (rawwit wit_bool) x then "true" else "false") - | IntArgType -> int (out_gen (rawwit wit_int) x) | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) - | StringArgType -> str "\"" ++ str (out_gen (rawwit wit_string) x) ++ str "\"" - | PreIdentArgType -> str (out_gen (rawwit wit_pre_ident) x) | IntroPatternArgType -> pr_intro_pattern (out_gen (rawwit wit_intro_pattern) x) | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) @@ -180,16 +176,12 @@ 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 -> str "[no printer for " ++ str s ++ str "]" + with Not_found -> Genarg.raw_print x let rec pr_glob_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with - | BoolArgType -> str (if out_gen (glbwit wit_bool) x then "true" else "false") - | IntArgType -> int (out_gen (glbwit wit_int) x) | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) - | StringArgType -> str "\"" ++ str (out_gen (glbwit wit_string) x) ++ str "\"" - | PreIdentArgType -> str (out_gen (glbwit wit_pre_ident) x) | IntroPatternArgType -> pr_intro_pattern (out_gen (glbwit wit_intro_pattern) x) | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) @@ -226,15 +218,11 @@ let rec pr_glob_generic prc prlc prtac prpat x = x) | ExtraArgType s -> try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str "[no printer for " ++ str s ++ str "]" + with Not_found -> Genarg.glb_print x let rec pr_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with - | BoolArgType -> str (if out_gen (topwit wit_bool) x then "true" else "false") - | IntArgType -> int (out_gen (topwit wit_int) x) | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) - | StringArgType -> str "\"" ++ str (out_gen (topwit wit_string) x) ++ str "\"" - | PreIdentArgType -> str (out_gen (topwit wit_pre_ident) x) | IntroPatternArgType -> pr_intro_pattern (out_gen (topwit wit_intro_pattern) x) | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x) | VarArgType -> pr_id (out_gen (topwit wit_var) x) @@ -267,7 +255,7 @@ let rec pr_generic prc prlc prtac prpat x = x) | ExtraArgType s -> try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str "[no printer for " ++ str s ++ str "]" + with Not_found -> Genarg.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/tactics/taccoerce.ml b/tactics/taccoerce.ml index d5b3986aff..89774ba213 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -14,6 +14,7 @@ open Term open Pattern open Misctypes open Genarg +open Stdarg exception CannotCoerceTo of string diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 5abba699e3..456779732e 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -747,15 +747,9 @@ and intern_match_rule onlytac ist = function and intern_genarg ist x = match genarg_tag x with - | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (rawwit wit_bool) x) - | IntArgType -> in_gen (glbwit wit_int) (out_gen (rawwit wit_int) x) | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (intern_or_var ist (out_gen (rawwit wit_int_or_var) x)) - | StringArgType -> - in_gen (glbwit wit_string) (out_gen (rawwit wit_string) x) - | PreIdentArgType -> - in_gen (glbwit wit_pre_ident) (out_gen (rawwit wit_pre_ident) x) | IntroPatternArgType -> let lf = ref ([],[]) in (* how to know which names are bound by the intropattern *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d9dc233b92..06a3ad2600 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -33,6 +33,7 @@ open Termops open Tacexpr open Hiddentac open Genarg +open Stdarg open Printer open Pretyping open Extrawit @@ -1358,15 +1359,9 @@ and interp_genarg ist gl x = let rec interp_genarg ist gl x = let gl = { gl with sigma = !evdref } in match genarg_tag x with - | BoolArgType -> in_gen (topwit wit_bool) (out_gen (glbwit wit_bool) x) - | IntArgType -> in_gen (topwit wit_int) (out_gen (glbwit wit_int) x) | IntOrVarArgType -> in_gen (topwit wit_int_or_var) (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x))) - | StringArgType -> - in_gen (topwit wit_string) (out_gen (glbwit wit_string) x) - | PreIdentArgType -> - in_gen (topwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x) | IntroPatternArgType -> in_gen (topwit wit_intro_pattern) (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x)) @@ -1876,12 +1871,8 @@ and interp_atomic ist gl tac = | TacAlias (loc,s,l,(_,body)) -> fun gl -> let evdref = ref gl.sigma in let rec f x = match genarg_tag x with - | IntArgType -> - in_gen (topwit wit_int) (out_gen (glbwit wit_int) x) | IntOrVarArgType -> mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x) - | PreIdentArgType -> - failwith "pre-identifiers cannot be bound" | IntroPatternArgType -> let ipat = interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x) in in_gen (topwit wit_intro_pattern) ipat @@ -1929,10 +1920,6 @@ and interp_atomic ist gl tac = let wit = glbwit (wit_list0 wit_var) in let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in in_gen (topwit (wit_list0 wit_genarg)) ans - | List0ArgType IntArgType -> - let wit = glbwit (wit_list0 wit_int) in - let ans = List.map (fun x -> in_gen (topwit wit_int) x) (out_gen wit x) in - in_gen (topwit (wit_list0 wit_genarg)) ans | List0ArgType IntOrVarArgType -> let wit = glbwit (wit_list0 wit_int_or_var) in let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in @@ -1961,10 +1948,6 @@ and interp_atomic ist gl tac = let wit = glbwit (wit_list1 wit_var) in let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in in_gen (topwit (wit_list1 wit_genarg)) ans - | List1ArgType IntArgType -> - let wit = glbwit (wit_list1 wit_int) in - let ans = List.map (fun x -> in_gen (topwit wit_int) x) (out_gen wit x) in - in_gen (topwit (wit_list1 wit_genarg)) ans | List1ArgType IntOrVarArgType -> let wit = glbwit (wit_list1 wit_int_or_var) in let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in @@ -1979,12 +1962,16 @@ and interp_atomic ist gl tac = let mk_ipat x = interp_intro_pattern ist gl x in let ans = List.map mk_ipat (out_gen wit x) in in_gen (topwit (wit_list1 wit_intro_pattern)) ans - | StringArgType | BoolArgType + | List0ArgType _ -> app_list0 f x + | List1ArgType _ -> app_list1 f x + | ExtraArgType _ -> + let (sigma, v) = Genarg.interpret ist { gl with sigma = !evdref } x in + evdref := sigma; + v | QuantHypArgType | RedExprArgType | OpenConstrArgType _ | ConstrWithBindingsArgType - | ExtraArgType _ | BindingsArgType + | BindingsArgType | OptArgType _ | PairArgType _ - | List0ArgType _ | List1ArgType _ -> error "This argument type is not supported in tactic notations." in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index f33e3ccec6..ba80d6d6cd 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -286,11 +286,7 @@ and subst_match_rule subst = function and subst_genarg subst (x:glob_generic_argument) = match genarg_tag x with - | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (glbwit wit_bool) x) - | IntArgType -> in_gen (glbwit wit_int) (out_gen (glbwit wit_int) x) | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x) - | StringArgType -> in_gen (glbwit wit_string) (out_gen (glbwit wit_string) x) - | PreIdentArgType -> in_gen (glbwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x) | IntroPatternArgType -> in_gen (glbwit wit_intro_pattern) (out_gen (glbwit wit_intro_pattern) x) | IdentArgType b -> -- cgit v1.2.3