From 389aa51f37fda1a7a8490d1b4042b881aba730df Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Jul 2018 16:30:16 +0200 Subject: Pass unnamed arguments to ML macros. This was imposing a bit of useless burden on the API for no good reason. --- plugins/ltac/tacentries.ml | 48 ++++++++++++++++----------------------------- plugins/ltac/tacentries.mli | 5 +---- 2 files changed, 18 insertions(+), 35 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 636cb8ebf8..a77a9c2f45 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -187,7 +187,7 @@ let add_tactic_entry (kn, ml, tg) state = | TacTerm s -> GramTerminal s | TacNonTerm (loc, (s, ido)) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e)) + GramNonTerminal (Loc.tag ?loc @@ (typ, e)) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -556,18 +556,14 @@ let () = ] in register_grammars_by_name "tactic" entries -let get_identifier id = +let get_identifier i = (** Workaround for badly-designed generic arguments lacking a closure *) - Names.Id.of_string_soft ("$" ^ id) - + Names.Id.of_string_soft (Printf.sprintf "$%i" i) type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig -| TyArg : - ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig -| TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig +| TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml @@ -581,18 +577,16 @@ let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.a | TUentry a -> Uentry (Genarg.ArgT.Any a) | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i) -let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list = - fun sign -> match sign with +let rec clause_of_sign : type a. int -> a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list = + fun i sign -> match sign with | TyNil -> [] - | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' - | TyArg (a, id, sig') -> - let id = get_identifier id in - TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig' - | TyAnonArg (a, sig') -> - TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig' + | TyIdent (s, sig') -> TacTerm s :: clause_of_sign i sig' + | TyArg (a, sig') -> + let id = Some (get_identifier i) in + TacNonTerm (None, (untype_user_symbol a, id)) :: clause_of_sign (i + 1) sig' let clause_of_ty_ml = function - | TyML (t,_) -> clause_of_sign t + | TyML (t,_) -> clause_of_sign 1 t let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = fun sign tac -> @@ -603,7 +597,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i | _ :: _ -> assert false end | TyIdent (s, sig') -> eval_sign sig' tac - | TyArg (a, _, sig') -> + | TyArg (a, sig') -> let f = eval_sign sig' in begin fun tac vals ist -> match vals with | [] -> assert false @@ -611,7 +605,6 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in f (tac v') vals ist end tac - | TyAnonArg (a, sig') -> eval_sign sig' tac let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function | TyML (t,tac) -> eval_sign t tac @@ -623,14 +616,12 @@ let is_constr_entry = function let rec only_constr : type a. a ty_sig -> bool = function | TyNil -> true | TyIdent(_,_) -> false -| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false -| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false +| TyArg (u, s) -> if is_constr_entry u then only_constr s else false -let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function +let rec mk_sign_vars : type a. int -> a ty_sig -> Name.t list = fun i tu -> match tu with | TyNil -> [] -| TyIdent (_,s) -> mk_sign_vars s -| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s -| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s +| TyIdent (_,s) -> mk_sign_vars i s +| TyArg (_, s) -> Name (get_identifier i) :: mk_sign_vars (i + 1) s let dummy_id = Id.of_string "_" @@ -661,12 +652,7 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) - (* - let patt = make_patt rem in - let vars = List.map make_var rem in - let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in - *) - let vars = mk_sign_vars s in + let vars = mk_sign_vars 1 s in let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in let tac = match s with | TyNil -> eval ml_tac diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 138a584e01..0b2b426018 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -73,10 +73,7 @@ val print_located_tactic : Libnames.qualid -> unit type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig -| TyArg : - ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig -| TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig +| TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml -- cgit v1.2.3 From 278f64296af13865ed50c966f1a4c1ab4357423e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Jul 2018 18:05:46 +0200 Subject: Port g_derive to coqpp. Unluckily this is the only file that contains a VERNAC EXTEND and no ARGUMENT EXTEND, which are not handled yet. --- plugins/derive/g_derive.ml4 | 20 -------------------- plugins/derive/g_derive.mlg | 28 ++++++++++++++++++++++++++++ 2 files changed, 28 insertions(+), 20 deletions(-) delete mode 100644 plugins/derive/g_derive.ml4 create mode 100644 plugins/derive/g_derive.mlg (limited to 'plugins') diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 deleted file mode 100644 index a59324149c..0000000000 --- a/plugins/derive/g_derive.ml4 +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - [ Derive.start_deriving f suchthat lemma ] -END diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg new file mode 100644 index 0000000000..2e059c7f95 --- /dev/null +++ b/plugins/derive/g_derive.mlg @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + { let () = Derive.start_deriving f suchthat lemma in st } +END -- cgit v1.2.3 From bc240341d9f0f7466c82e8ee9f3f325cda6fc3bf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 13 Sep 2018 15:54:08 +0200 Subject: Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one. --- plugins/derive/g_derive.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 2e059c7f95..18316bf2cd 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuara VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { let () = Derive.start_deriving f suchthat lemma in st } + { Derive.start_deriving f suchthat lemma } END -- cgit v1.2.3