summaryrefslogtreecommitdiff
path: root/grammar/tacextend.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/tacextend.ml4')
-rw-r--r--grammar/tacextend.ml4281
1 files changed, 281 insertions, 0 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
new file mode 100644
index 00000000..0421ad7c
--- /dev/null
+++ b/grammar/tacextend.ml4
@@ -0,0 +1,281 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
+open Util
+open Pp
+open Names
+open Genarg
+open Q_util
+open Q_coqast
+open Argextend
+open Pcoq
+open Egramml
+open Compat
+
+let dloc = <:expr< Loc.ghost >>
+
+let plugin_name = <:expr< __coq_plugin_name >>
+
+let rec make_patt = function
+ | [] -> <:patt< [] >>
+ | GramNonTerminal(loc',_,_,Some p)::l ->
+ let p = Names.Id.to_string p in
+ <:patt< [ $lid:p$ :: $make_patt l$ ] >>
+ | _::l -> make_patt l
+
+let rec make_when loc = function
+ | [] -> <:expr< True >>
+ | GramNonTerminal(loc',t,_,Some p)::l ->
+ let loc' = of_coqloc loc' in
+ let p = Names.Id.to_string p in
+ let l = make_when loc l in
+ let loc = CompatLoc.merge loc' loc in
+ let t = mlexpr_of_argtype loc' t in
+ <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
+ | _::l -> make_when loc l
+
+let rec make_let raw e = function
+ | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
+ | GramNonTerminal(loc,t,_,Some p)::l ->
+ let loc = of_coqloc loc in
+ let p = Names.Id.to_string p in
+ let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
+ let e = make_let raw e l in
+ let v =
+ if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
+ else <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in
+ <:expr< let $lid:p$ = $v$ in $e$ >>
+ | _::l -> make_let raw e l
+
+let rec extract_signature = function
+ | [] -> []
+ | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
+ | _::l -> extract_signature l
+
+
+
+let check_unicity s l =
+ let l' = List.map (fun (l,_,_) -> extract_signature l) l in
+ if not (Util.List.distinct l') then
+ Pp.msg_warning
+ (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^
+ "non-terminals in the same order: put them in distinct tactic entries"))
+
+let make_clause (pt,_,e) =
+ (make_patt pt,
+ vala (Some (make_when (MLast.loc_of_expr e) pt)),
+ make_let false e pt)
+
+let make_fun_clauses loc s l =
+ check_unicity s l;
+ Compat.make_fun loc (List.map make_clause l)
+
+let rec make_args = function
+ | [] -> <:expr< [] >>
+ | GramNonTerminal(loc,t,_,Some p)::l ->
+ let loc = of_coqloc loc in
+ let p = Names.Id.to_string p in
+ <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
+ | _::l -> make_args l
+
+let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
+ | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
+ | GramNonTerminal (loc,nt,_,sopt) ->
+ let loc = of_coqloc loc in <:expr< None >>
+
+let make_prod_item = function
+ | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+ | GramNonTerminal (loc,nt,g,sopt) ->
+ let loc = of_coqloc loc in
+ <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
+ $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
+
+let mlexpr_of_clause =
+ mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a)
+
+let rec make_tags loc = function
+ | [] -> <:expr< [] >>
+ | GramNonTerminal(loc',t,_,Some p)::l ->
+ let loc' = of_coqloc loc' in
+ let l = make_tags loc l in
+ let loc = CompatLoc.merge loc' loc in
+ let t = mlexpr_of_argtype loc' t in
+ <:expr< [ $t$ :: $l$ ] >>
+ | _::l -> make_tags loc l
+
+let make_one_printing_rule se (pt,_,e) =
+ let level = mlexpr_of_int 0 in (* only level 0 supported here *)
+ let loc = MLast.loc_of_expr e in
+ let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
+ <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$;
+ pptac_prods = ($level$, $prods$) }) >>
+
+let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
+
+let make_empty_check = function
+| GramNonTerminal(_, t, e, _)->
+ let is_extra = match t with ExtraArgType _ -> true | _ -> false in
+ if is_possibly_empty e || is_extra then
+ (* This possibly parses epsilon *)
+ let wit = make_wit loc t in
+ let rawwit = make_rawwit loc t in
+ <:expr<
+ match Genarg.default_empty_value $wit$ with
+ [ None -> raise Exit
+ | Some v ->
+ Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
+ (Genarg.in_gen $rawwit$ v) ] >>
+ else
+ (* This does not parse epsilon (this Exit is static time) *)
+ raise Exit
+| GramTerminal _ ->
+ (* Idem *)
+ raise Exit
+
+let rec possibly_empty_subentries loc = function
+ | [] -> []
+ | (s,prodsl) :: l ->
+ let rec aux = function
+ | [] -> (false,<:expr< None >>)
+ | prods :: rest ->
+ try
+ let l = List.map make_empty_check prods in
+ if has_extraarg prods then
+ (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$
+ with [ Exit -> $snd (aux rest)$ ] >>)
+ else
+ (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>)
+ with Exit -> aux rest in
+ let (nonempty,v) = aux prodsl in
+ if nonempty then (s,v) :: possibly_empty_subentries loc l
+ else possibly_empty_subentries loc l
+
+let possibly_atomic loc prods =
+ let l = List.map_filter (function
+ | GramTerminal s :: l, _, _ -> Some (s,l)
+ | _ -> None) prods
+ in
+ possibly_empty_subentries loc (List.factorize_left String.equal l)
+
+(** Special treatment of constr entries *)
+let is_constr_gram = function
+| GramTerminal _ -> false
+| GramNonTerminal (_, _, e, _) ->
+ match e with
+ | Aentry ("constr", "constr") -> true
+ | _ -> false
+
+let make_vars len =
+ (** We choose names unlikely to be written by a human, even though that
+ does not matter at all. *)
+ List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i)))
+
+let declare_tactic loc s c cl = match cl with
+| [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
+ (** 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 = make_vars (List.length rem) in
+ let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
+ let entry = mlexpr_of_string s in
+ let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
+ let name = mlexpr_of_string name in
+ let tac =
+ (** Special handling of tactics without arguments: such tactics do not do
+ a Proofview.Goal.nf_enter to compute their arguments. It matters for some
+ whole-prof tactics like [shelve_unifiable]. *)
+ if List.is_empty rem then
+ <:expr< fun _ $lid:"ist"$ -> $tac$ >>
+ else
+ let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+ <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
+ in
+ (** Arguments are not passed directly to the ML tactic in the TacML node,
+ the ML tactic retrieves its arguments in the [ist] environment instead.
+ This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+ let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in
+ let name = <:expr< Names.Id.of_string $name$ >> in
+ declare_str_items loc
+ [ <:str_item< do {
+ let obj () = Tacenv.register_ltac True False $name$ $body$ in
+ try do {
+ Tacenv.register_ml_tactic $se$ $tac$;
+ Mltop.declare_cache_obj obj $plugin_name$; }
+ with [ e when Errors.noncritical e ->
+ Pp.msg_warning
+ (Pp.app
+ (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
+ (Errors.print e)) ]; } >>
+ ]
+| _ ->
+ (** Otherwise we add parsing and printing rules to generate a call to a
+ TacML tactic. *)
+ let entry = mlexpr_of_string s in
+ let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
+ let pp = make_printing_rule se cl in
+ let gl = mlexpr_of_clause cl in
+ let atom =
+ mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
+ (possibly_atomic loc cl) in
+ let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ $atom$ >> in
+ declare_str_items loc
+ [ <:str_item< do {
+ try do {
+ Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
+ Mltop.declare_cache_obj $obj$ $plugin_name$;
+ List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; }
+ with [ e when Errors.noncritical e ->
+ Pp.msg_warning
+ (Pp.app
+ (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
+ (Errors.print e)) ]; } >>
+ ]
+
+open Pcaml
+open PcamlSig (* necessary for camlp4 *)
+
+EXTEND
+ GLOBAL: str_item;
+ str_item:
+ [ [ "TACTIC"; "EXTEND"; s = tac_name;
+ c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
+ OPT "|"; l = LIST1 tacrule SEP "|";
+ "END" ->
+ declare_tactic loc s c l ] ]
+ ;
+ tacrule:
+ [ [ "["; l = LIST1 tacargs; "]";
+ c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
+ "->"; "["; e = Pcaml.expr; "]" ->
+ (match l with
+ | GramNonTerminal _ :: _ ->
+ (* En attendant la syntaxe de tacticielles *)
+ failwith "Tactic syntax must start with an identifier"
+ | _ -> (l,c,e))
+ ] ]
+ ;
+ tacargs:
+ [ [ e = LIDENT; "("; s = LIDENT; ")" ->
+ let t, g = interp_entry_name false None e "" in
+ GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+ let t, g = interp_entry_name false None e sep in
+ GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ | s = STRING ->
+ if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
+ GramTerminal s
+ ] ]
+ ;
+ tac_name:
+ [ [ s = LIDENT -> s
+ | s = UIDENT -> s
+ ] ]
+ ;
+ END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 04:43:52 +0000