diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 14:42:51 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 14:51:20 +0100 |
commit | 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 (patch) | |
tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 | |
parent | 92a6a72ec4680d0f241e8b1ddd7b87f7ad11f65e (diff) |
Removing the registering of default values for generic arguments.
-rw-r--r-- | grammar/argextend.ml4 | 81 | ||||
-rw-r--r-- | interp/constrarg.ml | 34 | ||||
-rw-r--r-- | interp/stdarg.ml | 10 | ||||
-rw-r--r-- | lib/genarg.ml | 16 | ||||
-rw-r--r-- | lib/genarg.mli | 6 | ||||
-rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
-rw-r--r-- | tactics/g_rewrite.ml4 | 2 | ||||
-rw-r--r-- | tactics/taccoerce.ml | 4 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | tactics/tauto.ml | 2 | ||||
-rw-r--r-- | toplevel/g_obligations.ml4 | 2 |
13 files changed, 38 insertions, 129 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index be4097f13..46c68ecc3 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -48,82 +48,6 @@ let has_extraarg l = in List.exists check l -let rec is_possibly_empty = function -| Uopt _ -> true -| Ulist0 _ -> true -| Ulist0sep _ -> true -| Umodifiers _ -> true -| Ulist1 t -> is_possibly_empty t -| Ulist1sep (t, _) -> is_possibly_empty t -| _ -> false - -let rec get_empty_entry = function -| Uopt _ -> <:expr< None >> -| Ulist0 _ -> <:expr< [] >> -| Ulist0sep _ -> <:expr< [] >> -| Umodifiers _ -> <:expr< [] >> -| Ulist1 t -> <:expr< [$get_empty_entry t$] >> -| Ulist1sep (t, _) -> <:expr< [$get_empty_entry t$] >> -| _ -> assert false - -let statically_known_possibly_empty s (prods,_) = - List.for_all (function - | ExtNonTerminal(t, e, _) -> - begin match t with - | ExtraArgType s' -> - (* For ExtraArg we don't know (we'll have to test dynamically) *) - (* unless it is a recursive call *) - s <> s' - | _ -> - is_possibly_empty e - end - | ExtTerminal _ -> - (* This consumes a token for sure *) false) - prods - -let possibly_empty_subentries loc (prods,act) = - let bind_name s v e = - <:expr< let $lid:s$ = $v$ in $e$ >> - in - let rec aux = function - | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >> - | ExtNonTerminal(_, e, s) :: tl when is_possibly_empty e -> - bind_name s (get_empty_entry e) (aux tl) - | ExtNonTerminal(t, _, s) :: tl -> - let t = match t with - | ExtraArgType _ as t -> t - | _ -> assert false - in - (* We check at runtime if extraarg s parses "epsilon" *) - <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with - [ None -> raise Exit - | Some v -> v ] in $aux tl$ >> - | _ -> assert false (* already filtered out *) in - if has_extraarg prods then - (* Needs a dynamic check; catch all exceptions if ever some rhs raises *) - (* an exception rather than returning a value; *) - (* declares loc because some code can refer to it; *) - (* ensures loc is used to avoid "unused variable" warning *) - (true, <:expr< try Some $aux prods$ - with [ Exit -> None ] >>) - else - (* Static optimisation *) - (false, aux prods) - -let make_possibly_empty_subentries loc s cl = - let cl = List.filter (statically_known_possibly_empty s) cl in - if cl = [] then - <:expr< None >> - else - let rec aux = function - | (true, e) :: l -> - <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >> - | (false, e) :: _ -> - <:expr< Some $e$ >> - | [] -> - <:expr< None >> in - aux (List.map (possibly_empty_subentries loc) cl) - let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> @@ -214,12 +138,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = 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 dyn = $dyn$ in - Genarg.make0 ?dyn $default_value$ $se$ >>; + Genarg.make0 ?dyn $se$ >>; <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; @@ -245,7 +168,7 @@ let declare_vernac_argument loc s pr cl = declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = - Genarg.create_arg None $se$ >>; + Genarg.create_arg $se$ >>; <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a48d68375..ead4e3969 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -20,48 +20,48 @@ let loc_of_or_by_notation f = function | ByNotation (loc,s,_) -> loc let wit_int_or_var = - Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var" + Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = - Genarg.make0 None "intropattern" + Genarg.make0 "intropattern" let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - Genarg.make0 None "tactic" + Genarg.make0 "tactic" let wit_ident = - Genarg.make0 None "ident" + Genarg.make0 "ident" let wit_var = - Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var" + Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var" -let wit_ref = Genarg.make0 None "ref" +let wit_ref = Genarg.make0 "ref" -let wit_quant_hyp = Genarg.make0 None "quant_hyp" +let wit_quant_hyp = Genarg.make0 "quant_hyp" let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = - Genarg.make0 None "sort" + Genarg.make0 "sort" let wit_constr = - Genarg.make0 None "constr" + Genarg.make0 "constr" let wit_constr_may_eval = - Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval" + Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval" -let wit_uconstr = Genarg.make0 None "uconstr" +let wit_uconstr = Genarg.make0 "uconstr" -let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr" +let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings" +let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings" -let wit_bindings = Genarg.make0 None "bindings" +let wit_bindings = Genarg.make0 "bindings" let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = - Genarg.make0 None "hyp_location_flag" + Genarg.make0 "hyp_location_flag" -let wit_red_expr = Genarg.make0 None "redexpr" +let wit_red_expr = Genarg.make0 "redexpr" let wit_clause_dft_concl = - Genarg.make0 None "clause_dft_concl" + Genarg.make0 "clause_dft_concl" (** Register location *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 9c3ed9413..56b995e53 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -9,19 +9,19 @@ open Genarg let wit_unit : unit uniform_genarg_type = - make0 None "unit" + make0 "unit" let wit_bool : bool uniform_genarg_type = - make0 None "bool" + make0 "bool" let wit_int : int uniform_genarg_type = - make0 None "int" + make0 "int" let wit_string : string uniform_genarg_type = - make0 None "string" + make0 "string" let wit_pre_ident : string uniform_genarg_type = - make0 None "preident" + make0 "preident" let () = register_name0 wit_unit "Stdarg.wit_unit" let () = register_name0 wit_bool "Stdarg.wit_bool" diff --git a/lib/genarg.ml b/lib/genarg.ml index c7273ac93..7aada461f 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -246,7 +246,6 @@ struct end type ('raw, 'glb, 'top) load = { - nil : 'raw option; dyn : 'top Val.tag; } @@ -254,30 +253,19 @@ module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end) let arg0_map = ref LoadMap.empty -let create_arg opt ?dyn name = +let create_arg ?dyn name = match ArgT.name name with | Some _ -> Errors.anomaly (str "generic argument already declared: " ++ str name) | None -> let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in - let obj = LoadMap.Pack { nil = opt; dyn; } in + let obj = LoadMap.Pack { dyn; } in let name = ArgT.create name in let () = arg0_map := LoadMap.add name obj !arg0_map in ExtraArg name let make0 = create_arg -let rec default_empty_value : type a b c. (a, b, c) genarg_type -> a option = function -| ListArg _ -> Some [] -| OptArg _ -> Some None -| PairArg (t1, t2) -> - begin match default_empty_value t1, default_empty_value t2 with - | Some v1, Some v2 -> Some (v1, v2) - | _ -> None - end -| ExtraArg s -> - match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.nil - let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function | ListArg t -> Val.List (val_tag t) | OptArg t -> Val.Opt (val_tag t) diff --git a/lib/genarg.mli b/lib/genarg.mli index ce0536cf4..d509649f2 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -110,11 +110,11 @@ end type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision when the three types agree. *) -val make0 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type +val make0 : ?dyn:'top Val.tag -> 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 -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type +val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type (** Alias for [make0]. *) (** {5 Specialized types} *) @@ -250,8 +250,6 @@ val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, '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. diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index b62cfd6ad..2d096a108 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -87,7 +87,7 @@ let vernac_proof_instr instr = (* Only declared at raw level, because only used in vernac commands. *) let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = - Genarg.make0 None "proof_instr" + Genarg.make0 "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode will replace the normal parser entry for tactics with this one. *) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 97b9e95e1..61ada5cc8 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -146,7 +146,7 @@ module Tactic = Pcoq.Tactic type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = - Genarg.create_arg None "function_rec_definition_loc" + Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 85b9d6a08..ae8b83b95 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -931,9 +931,9 @@ type cmp = type 'i test = | Test of cmp * 'i * 'i -let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 None "cmp" +let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = - Genarg.make0 None "tactest" + Genarg.make0 "tactest" let pr_cmp = function | Eq -> Pp.str"=" diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 6b6dc7b21..8b012aa88 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -184,7 +184,7 @@ END type binders_argtype = local_binder list let wit_binders = - (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type) + (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 0cd3e0944..358f6d646 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -18,11 +18,11 @@ open Constrarg exception CannotCoerceTo of string let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) = - Genarg.create_arg None "constr_context" + Genarg.create_arg "constr_context" (* includes idents known to be bound and references *) let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = - Genarg.create_arg None "constr_under_binders" + Genarg.create_arg "constr_under_binders" let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 32f7c3c61..36faba113 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -109,7 +109,7 @@ type tacvalue = | VRec of value Id.Map.t ref * glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - Genarg.create_arg None "tacvalue" + Genarg.create_arg "tacvalue" let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v diff --git a/tactics/tauto.ml b/tactics/tauto.ml index d3e0b1f44..a86fdb98a 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -55,7 +55,7 @@ type tauto_flags = { } let wit_tauto_flags : tauto_flags uniform_genarg_type = - Genarg.create_arg None "tauto_flags" + Genarg.create_arg "tauto_flags" let assoc_flags ist = let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index d620febbc..32ccf21d2 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -32,7 +32,7 @@ let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Spec type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = - Genarg.create_arg None "withtac" + Genarg.create_arg "withtac" let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac) |