From dfac5aa2285de5b89f08ada3c30c0a1594737440 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Sep 2016 18:02:52 +0200 Subject: Making Vernacexpr independent from Tacexpr. --- ide/texmacspp.ml | 2 +- intf/genredexpr.mli | 14 +++++++++++++- intf/tacexpr.mli | 6 +++++- intf/vernacexpr.mli | 17 ++++++----------- ltac/g_ltac.ml4 | 8 ++++---- ltac/tacentries.ml | 4 ++-- ltac/tacentries.mli | 2 +- ltac/tacintern.ml | 6 ++++-- parsing/g_proofs.ml4 | 8 +++++--- printing/ppvernac.ml | 6 +++--- tactics/hints.mli | 2 +- toplevel/vernacentries.ml | 2 ++ 12 files changed, 47 insertions(+), 30 deletions(-) diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 53a29008a..458e84835 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -742,7 +742,7 @@ let rec tmpp v loc = | VernacShow _ as x -> xmlTODO loc x | VernacCheckGuard as x -> xmlTODO loc x | VernacProof (tac,using) -> - let tac = Option.map (xmlRawTactic "closingtactic") tac in + let tac = None (** FIXME *) in let using = Option.map (xmlSectionSubsetDescr "using") using in xmlProof loc (Option.List.(cons tac (cons using []))) | VernacProofMode name -> xmlProofMode loc name diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 2df79673a..16f0c0c92 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -8,6 +8,8 @@ (** Reduction expressions *) +open Names + (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = @@ -50,5 +52,15 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of (Loc.t * Names.Id.t) * 'a + | ConstrContext of (Loc.t * Id.t) * 'a | ConstrTypeOf of 'a + +open Libnames +open Constrexpr +open Misctypes + +type r_trm = constr_expr +type r_pat = constr_pattern_expr +type r_cst = reference or_by_notation + +type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 5b5957bef..946d124a4 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -34,7 +34,7 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) -type goal_selector = +type goal_selector = Vernacexpr.goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -401,3 +401,7 @@ type ltac_call_kind = | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map type ltac_trace = (Loc.t * ltac_call_kind) list + +type tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ed44704df..5713b2ee6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -8,7 +8,6 @@ open Loc open Names -open Tacexpr open Misctypes open Constrexpr open Decl_kinds @@ -27,7 +26,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation to print a goal that is out of focus (or already solved) it doesn't make sense to apply a tactic to it. Hence it the types may look very similar, they do not seem to mean the same thing. *) -type goal_selector = Tacexpr.goal_selector = +type goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -130,7 +129,7 @@ type hints_expr = | HintsTransparency of reference list * bool | HintsMode of reference * hint_mode list | HintsConstructors of reference list - | HintsExtern of int * constr_expr option * raw_tactic_expr + | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument type search_restriction = | SearchInside of reference list @@ -171,7 +170,7 @@ type sort_expr = glob_sort type definition_expr = | ProveBody of local_binder list * constr_expr - | DefineBody of local_binder list * raw_red_expr option * constr_expr + | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type fixpoint_expr = @@ -432,9 +431,9 @@ type vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of raw_red_expr option * int option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * raw_red_expr + | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable | VernacSearch of searchable * int option * search_restriction | VernacLocate of locatable @@ -460,7 +459,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_expr option + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn @@ -473,10 +472,6 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and tacdef_body = - | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) - (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later vernac_type: if it is starts, ends, continues a proof or diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index c67af33e2..42276ad3f 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -287,15 +287,15 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, TacFun (it, body)) + Tacexpr.TacticDefinition (id, TacFun (it, body)) | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, body) + if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, body) + Tacexpr.TacticDefinition (id, body) ] ] ; tactic: diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2fed0e14f..2d7b7bf13 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -425,7 +425,7 @@ let warn_unusable_identifier = let register_ltac local tacl = let map tactic_body = match tactic_body with - | TacticDefinition ((loc,id), body) -> + | Tacexpr.TacticDefinition ((loc,id), body) -> let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then @@ -441,7 +441,7 @@ let register_ltac local tacl = in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 27df819ee..969c118fb 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -13,7 +13,7 @@ open Tacexpr (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index cd791398d..b6ff32ac3 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -796,11 +796,13 @@ let () = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let f l = + (** FIXME: use generic internalization *) + let f l tac = + let tac = out_gen (rawwit Constrarg.wit_ltac) tac in let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check - (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars }) + (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars }) tac in Hook.set Hints.extern_intern_tac f diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1e3c4b880..6ce7ca023 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -26,6 +26,8 @@ let hint_proof_using e = function | None -> None | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) +let in_tac tac = Genarg.in_gen (Genarg.rawwit Constrarg.wit_ltac) tac + (* Proof commands *) GEXTEND Gram GLOBAL: command; @@ -41,9 +43,9 @@ GEXTEND Gram | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; "with"; ta = tactic; l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l) + VernacProof (Some (in_tac ta),hint_proof_using G_vernac.section_subset_expr l) | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = tactic -> ta ] -> + ta = OPT [ "with"; ta = tactic -> in_tac ta ] -> VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None @@ -127,7 +129,7 @@ GEXTEND Gram | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; tac = tactic -> - HintsExtern (n,c,tac) ] ] + HintsExtern (n,c, in_tac tac) ] ] ; constr_body: [ [ ":="; c = lconstr -> c diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 40ce28dc0..d4de05da8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -195,7 +195,7 @@ module Make | HintsExtern (n,c,tac) -> let pat = match c with None -> mt () | Some pat -> pr_pat pat in keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ - spc() ++ pr_raw_tactic tac + spc() ++ pr_raw_generic (Global.env ()) tac in hov 2 (keyword "Hint "++ pph ++ opth) @@ -1179,12 +1179,12 @@ module Make return (keyword "Proof " ++ spc () ++ keyword "using" ++ spc() ++ pr_using e) | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) + return (keyword "Proof with" ++ spc() ++ pr_raw_generic (Global.env ()) te) | VernacProof (Some te, Some e) -> return ( keyword "Proof" ++ spc () ++ keyword "using" ++ spc() ++ pr_using e ++ spc() ++ - keyword "with" ++ spc() ++pr_raw_tactic te + keyword "with" ++ spc() ++ pr_raw_generic (Global.env ()) te ) | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) diff --git a/tactics/hints.mli b/tactics/hints.mli index 6f5ee8ba5..6d5342e00 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -210,7 +210,7 @@ val run_hint : hint -> val repr_hint : hint -> (raw_hint * clausenv) hint_ast val extern_intern_tac : - (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t + (patvar list -> Genarg.raw_generic_argument -> Tacexpr.glob_tactic_expr) Hook.t (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6e632999c..56ddd4d3c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -844,6 +844,8 @@ let focus_command_cond = Proof.no_cond command_focus let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = + (** FIXME *) + let tac = Genarg.out_gen (Genarg.rawwit Constrarg.wit_ltac) tac in if not (refining ()) then error "Unknown command of the non proof-editing mode."; match tac with -- cgit v1.2.3