diff options
-rw-r--r-- | ltac/tacentries.ml | 132 | ||||
-rw-r--r-- | ltac/tacentries.mli | 2 | ||||
-rw-r--r-- | printing/pptactic.ml | 146 | ||||
-rw-r--r-- | printing/pptactic.mli | 5 | ||||
-rw-r--r-- | printing/pptacticsig.mli | 2 |
5 files changed, 154 insertions, 133 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2cc1b7b1c..f1b8eee5e 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -12,6 +12,7 @@ open Util open Names open Libobject open Genarg +open Extend open Pcoq open Egramml open Egramcoq @@ -19,7 +20,7 @@ open Vernacexpr open Libnames open Nameops -type 'a grammar_tactic_prod_item_expr = +type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t @@ -42,7 +43,6 @@ let coincide s pat off = !break let atactic n = - let open Extend in if n = 5 then Aentry (name_of_entry Tactic.binder_tactic) else Aentryl (name_of_entry Tactic.tactic_expr, n) @@ -51,7 +51,6 @@ type entry_name = EntryName : (** Quite ad-hoc *) let get_tacentry n m = - let open Extend in let check_lvl n = Int.equal m n && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) @@ -66,7 +65,6 @@ let get_separator = function | Some sep -> sep let rec parse_user_entry s sep = - let open Extend in let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then let entry = parse_user_entry (String.sub s 3 (l-8)) None in @@ -94,25 +92,14 @@ let arg_list = function Rawwit t -> Rawwit (ListArg t) let arg_opt = function Rawwit t -> Rawwit (OptArg t) let interp_entry_name interp symb = - let open Extend in let rec eval = function - | Ulist1 e -> - let EntryName (t, g) = eval e in - EntryName (arg_list t, Alist1 g) - | Ulist1sep (e, sep) -> - let EntryName (t, g) = eval e in - EntryName (arg_list t, Alist1sep (g, sep)) - | Ulist0 e -> - let EntryName (t, g) = eval e in - EntryName (arg_list t, Alist0 g) - | Ulist0sep (e, sep) -> - let EntryName (t, g) = eval e in - EntryName (arg_list t, Alist0sep (g, sep)) - | Uopt e -> - let EntryName (t, g) = eval e in - EntryName (arg_opt t, Aopt g) - | Uentry s -> interp s None - | Uentryl (s, n) -> interp s (Some n) + | Ulist1 e -> Ulist1 (eval e) + | Ulist1sep (e, sep) -> Ulist1sep (eval e, sep) + | Ulist0 e -> Ulist0 (eval e) + | Ulist0sep (e, sep) -> Ulist0sep (eval e, sep) + | Uopt e -> Uopt (eval e) + | Uentry s -> Uentry (interp s None) + | Uentryl (s, n) -> Uentryl (interp s (Some n), n) in eval symb @@ -134,15 +121,40 @@ let get_tactic_entry n = type tactic_grammar = { tacgram_level : int; - tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; + tacgram_prods : Pptactic.grammar_terminals; } (* Declaration of the tactic grammar rule *) let head_is_ident tg = match tg.tacgram_prods with -| GramTerminal _::_ -> true +| TacTerm _ :: _ -> true | _ -> false +let rec prod_item_of_symbol lev = function +| Extend.Ulist1 s -> + let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in + EntryName (Rawwit (ListArg typ), Alist1 e) +| Extend.Ulist0 s -> + let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in + EntryName (Rawwit (ListArg typ), Alist0 e) +| Extend.Ulist1sep (s, sep) -> + let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in + EntryName (Rawwit (ListArg typ), Alist1sep (e, sep)) +| Extend.Ulist0sep (s, sep) -> + let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in + EntryName (Rawwit (ListArg typ), Alist0sep (e, sep)) +| Extend.Uopt s -> + let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in + EntryName (Rawwit (OptArg typ), Aopt e) +| Extend.Uentry arg -> + let ArgT.Any tag = arg in + let wit = ExtraArg tag in + EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit))) +| Extend.Uentryl (s, n) -> + let ArgT.Any tag = s in + assert (coincide (ArgT.repr tag) "tactic" 0); + get_tacentry n lev + (** Tactic grammar extensions *) let add_tactic_entry (kn, ml, tg) = @@ -164,7 +176,14 @@ let add_tactic_entry (kn, ml, tg) = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then error "Notation for simple tactic must start with an identifier." in - let rules = make_rule mkact tg.tacgram_prods in + let map = function + | TacTerm s -> GramTerminal s + | TacNonTerm (loc, s, _) -> + let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in + GramNonTerminal (loc, typ, e) + in + let prods = List.map map tg.tacgram_prods in + let rules = make_rule mkact prods in synchronize_level_positions (); grammar_extend entry None (pos, [(None, None, List.rev [rules])]); 1 @@ -186,28 +205,27 @@ let register_tactic_notation_entry name entry = in entry_names := String.Map.add name entry !entry_names -let interp_prod_item lev = function - | TacTerm s -> GramTerminal s - | TacNonTerm (loc, (nt, sep), _) -> +let interp_prod_item = function + | TacTerm s -> TacTerm s + | TacNonTerm (loc, (nt, sep), id) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> - let ArgT.Any arg = - if String.Map.mem s !entry_names then - String.Map.find s !entry_names - else match ArgT.name s with - | None -> error ("Unknown entry "^s^".") - | Some arg -> arg - in - let wit = ExtraArg arg in - EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit))) + if String.Map.mem s !entry_names then String.Map.find s !entry_names + else begin match ArgT.name s with + | None -> error ("Unknown entry "^s^".") + | Some arg -> arg + end | Some n -> (** FIXME: do better someday *) assert (String.equal s "tactic"); - get_tacentry n lev + begin match Constrarg.wit_tactic with + | ExtraArg tag -> ArgT.Any tag + | _ -> assert false + end in - let EntryName (etyp, e) = interp_entry_name interp symbol in - GramNonTerminal (loc, etyp, e) + let symbol = interp_entry_name interp symbol in + TacNonTerm (loc, symbol, id) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -300,7 +318,7 @@ let add_glob_tactic_notation local n prods forml ids tac = let add_tactic_notation local n prods e = let ids = List.map_filter cons_production_parameter prods in - let prods = List.map (interp_prod_item n) prods in + let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in add_glob_tactic_notation local n prods false ids tac @@ -315,12 +333,13 @@ let extend_atomic_tactic name entries = let open Tacexpr in let map_prod prods = let (hd, rem) = match prods with - | GramTerminal s :: rem -> (s, rem) + | TacTerm s :: rem -> (s, rem) | _ -> assert false (** Not handled by the ML extension syntax *) in let empty_value = function - | GramTerminal s -> raise NonEmptyArgument - | GramNonTerminal (_, typ, e) -> + | TacTerm s -> raise NonEmptyArgument + | TacNonTerm (_, symb, _) -> + let EntryName (typ, e) = prod_item_of_symbol 0 symb in let Genarg.Rawwit wit = typ in let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in let default = epsilon_value inj e in @@ -342,33 +361,21 @@ let extend_atomic_tactic name entries = List.iteri add_atomic entries let add_ml_tactic_notation name prods = - let interp_prods = function - | TacTerm s -> None, GramTerminal s - | TacNonTerm (loc, symb, id) -> - let interp (ArgT.Any tag) lev = match lev with - | None -> - let wit = ExtraArg tag in - EntryName (Rawwit wit, Extend.Aentry (Pcoq.name_of_entry (Pcoq.genarg_grammar wit))) - | Some lev -> - assert (coincide (ArgT.repr tag) "tactic" 0); - EntryName (Rawwit Constrarg.wit_tactic, atactic lev) - in - let EntryName (etyp, e) = interp_entry_name interp symb in - Some id, GramNonTerminal (loc, etyp, e) - in - let prods = List.map (fun p -> List.map interp_prods p) prods in let len = List.length prods in let iter i prods = let open Tacexpr in - let (ids, prods) = List.split prods in - let ids = List.map_filter (fun x -> x) ids in + let get_id = function + | TacTerm s -> None + | TacNonTerm (_, _, id) -> Some id + in + let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in let tac = TacML (Loc.ghost, entry, List.map map ids) in add_glob_tactic_notation false 0 prods true ids tac in List.iteri iter (List.rev prods); - extend_atomic_tactic name (List.map (fun p -> List.map snd p) prods) + extend_atomic_tactic name prods (**********************************************************************) (** Ltac quotations *) @@ -376,7 +383,6 @@ let add_ml_tactic_notation name prods = let ltac_quotations = ref String.Set.empty let create_ltac_quotation name cast (e, l) = - let open Extend in let () = if String.Set.mem name !ltac_quotations then failwith ("Ltac quotation " ^ name ^ " already registered") diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 7586bff92..402cb2fc9 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -18,7 +18,7 @@ val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit (** {5 Tactic Notations} *) -type 'a grammar_tactic_prod_item_expr = +type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 9ab6895f3..44c832bd7 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -27,7 +27,11 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t + +type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { pptac_level : int; @@ -335,51 +339,23 @@ module Make try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) - let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) = - match wit with - | ListArg wit -> - let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - let ans = pr_sequence map x in - hov_if_not_empty 0 ans - | OptArg wit -> - let ans = match x with - | None -> mt () - | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) - in - hov_if_not_empty 0 ans - | PairArg (wit1, wit2) -> - let p, q = x in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in - hov_if_not_empty 0 ans - | ExtraArg s -> - try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) - with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) - let rec tacarg_using_rule_token pr_gen = function - | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | Egramml.GramNonTerminal _ :: l, a :: al -> - let r = tacarg_using_rule_token pr_gen (l,al) in - pr_gen a :: r - | [], [] -> [] - | _ -> failwith "Inconsistent arguments of extended tactic" - - let filter_arg = function - | Egramml.GramTerminal _ -> None - | Egramml.GramNonTerminal (_, Rawwit t, _) -> Some (ArgumentType t) + | [] -> [] + | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l + | TacNonTerm (_, (symb, arg), _) :: l -> + pr_gen symb arg :: tacarg_using_rule_token pr_gen l let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Egramml.GramTerminal s :: l, al) -> + | TacTerm s :: l -> (** First terminal token should be considered as the name of the tactic, so we tag it differently than the other terminal tokens. *) - primitive s :: (tacarg_using_rule_token pr_gen (l, al)) + primitive s :: tacarg_using_rule_token pr_gen l | _ -> tacarg_using_rule_token pr_gen l in pr_sequence (fun x -> x) l - let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = + let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ str "@" ++ int i @@ -390,31 +366,82 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_gen check pr_gen lev key l = + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in - let args = List.map_filter filter_arg pp.pptac_prods in - let () = if not (List.for_all2eq check args l) then raise Not_found in - let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + let rec pack prods args = match prods, args with + | [], [] -> [] + | TacTerm s :: prods, args -> TacTerm s :: pack prods args + | TacNonTerm (loc, symb, id) :: prods, arg :: args -> + TacNonTerm (loc, (symb, arg), id) :: pack prods args + | _ -> raise Not_found + in + let prods = pack pp.pptac_prods l in + let p = pr_tacarg_using_rule pr_gen prods in if pp.pptac_level > lev then surround p else p with Not_found -> - KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - - let check_type t arg = match arg with - | TacGeneric arg -> argument_type_eq t (genarg_tag arg) - | _ -> argument_type_eq t (ArgumentType wit_tactic) + let pr arg = str "_" in + KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg)) + let is_genarg tag wit = + let ArgT.Any tag = tag in + argument_type_eq (ArgumentType (ExtraArg tag)) wit + + let get_list : type l. l generic_argument -> l generic_argument list option = + function (GenArg (wit, arg)) -> match wit with + | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg) + | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg) + | _ -> None + + let get_opt : type l. l generic_argument -> l generic_argument option option = + function (GenArg (wit, arg)) -> match wit with + | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg) + | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg) + | _ -> None + + let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds = + fun prtac symb arg -> match symb with + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Ulist1 s | Extend.Ulist0 s -> + begin match get_list arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> pr_sequence (pr_any_arg prtac s) l + end + | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> + begin match get_list arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l + end + | Extend.Uopt s -> + begin match get_opt arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> pr_opt (pr_any_arg prtac s) l + end + | Extend.Uentry _ | Extend.Uentryl _ -> + str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + + let rec pr_targ prtac symb arg = match symb with + | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> + prtac (1, Any) arg + | Extend.Uentryl (_, l) -> prtac (l, Any) arg + | _ -> + match arg with + | TacGeneric arg -> + let pr l arg = prtac l (TacGeneric arg) in + pr_any_arg pr symb arg + | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + let pr_raw_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (pr_farg prtac) + pr_extend_gen (pr_farg prtac) let pr_glob_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (pr_farg prtac) + pr_extend_gen (pr_farg prtac) - let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen check_type (pr_farg prtac) - let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen check_type (pr_farg prtac) + let pr_raw_alias prc prlc prtac prpat lev key args = + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + let pr_glob_alias prc prlc prtac prpat lev key args = + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args (**********************************************************************) (* The tactic printer *) @@ -1278,10 +1305,6 @@ module Make (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) - let pr_top_generic env = pr_top_generic_rec - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern - let pr_raw_extend env = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr @@ -1289,20 +1312,11 @@ module Make (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) - let check_val_type t arg = - let ArgumentType t = t in -(* let t = Genarg.val_tag (Obj.magic t) in *) -(* let Val.Dyn (t', _) = arg in *) -(* match Genarg.Val.eq t t' with *) -(* | None -> false *) -(* | Some _ -> true *) - true (** FIXME *) - let pr_alias pr lev key args = - pr_alias_gen check_val_type pr lev key args + pr_alias_gen (fun _ arg -> pr arg) lev key args let pr_extend pr lev ml args = - pr_extend_gen check_val_type pr lev ml args + pr_extend_gen pr lev ml args let pr_atomic_tactic env = pr_atomic_tactic_level env ltop diff --git a/printing/pptactic.mli b/printing/pptactic.mli index b1e650b87..86e3ea548 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -17,6 +17,9 @@ open Constrexpr open Tacexpr open Ppextend +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> @@ -42,7 +45,7 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list +type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { pptac_level : int; diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index d49bef1fd..4ef2ea918 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -36,8 +36,6 @@ module type Pp = sig val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds - val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds - val pr_raw_extend: env -> int -> ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds |