From d0a9edabf59a858625d11516cdb230d223a77aeb Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 31 May 2016 12:14:55 +0200 Subject: Yet another Makefile reform : a unique phase without nasty make tricks We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy) --- grammar/argextend.ml4 | 256 ----------------------------------------------- grammar/argextend.mlp | 254 ++++++++++++++++++++++++++++++++++++++++++++++ grammar/gramCompat.ml4 | 86 ---------------- grammar/gramCompat.mlp | 86 ++++++++++++++++ grammar/q_constr.ml4 | 114 --------------------- grammar/q_constr.mlp | 112 +++++++++++++++++++++ grammar/q_util.ml4 | 118 ---------------------- grammar/q_util.mlp | 118 ++++++++++++++++++++++ grammar/tacextend.ml4 | 184 ---------------------------------- grammar/tacextend.mlp | 182 +++++++++++++++++++++++++++++++++ grammar/vernacextend.ml4 | 200 ------------------------------------ grammar/vernacextend.mlp | 198 ++++++++++++++++++++++++++++++++++++ 12 files changed, 950 insertions(+), 958 deletions(-) delete mode 100644 grammar/argextend.ml4 create mode 100644 grammar/argextend.mlp delete mode 100644 grammar/gramCompat.ml4 create mode 100644 grammar/gramCompat.mlp delete mode 100644 grammar/q_constr.ml4 create mode 100644 grammar/q_constr.mlp delete mode 100644 grammar/q_util.ml4 create mode 100644 grammar/q_util.mlp delete mode 100644 grammar/tacextend.ml4 create mode 100644 grammar/tacextend.mlp delete mode 100644 grammar/vernacextend.ml4 create mode 100644 grammar/vernacextend.mlp (limited to 'grammar') diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 deleted file mode 100644 index 8e06adce9..000000000 --- a/grammar/argextend.ml4 +++ /dev/null @@ -1,256 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > - -let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> - -let rec make_wit loc = function - | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> mk_extraarg loc s - -let is_self s = function -| ExtraArgType s' -> s = s' -| _ -> false - -let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> -let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> -let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> - -let make_act loc act pil = - let rec make = function - | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> - | ExtTerminal _ :: tl -> - <:expr< (fun _ -> $make tl$) >> in - make (List.rev pil) - -let make_prod_item = function - | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (g, _) -> - let base s = <:expr< $lid:s$ >> in - mlexpr_of_prod_entry_key base g - -let rec make_prod = function -| [] -> <:expr< Extend.Stop >> -| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> - -let make_rule loc (prods,act) = - <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> - -let is_ident x = function -| <:expr< $lid:s$ >> -> (s : string) = x -| _ -> false - -let make_extend loc s cl wit = match cl with -| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act -> - (** Special handling of identity arguments by not redeclaring an entry *) - <:str_item< - value $lid:s$ = - let () = Pcoq.register_grammar $wit$ $lid:e$ in - $lid:e$ - >> -| _ -> - let se = mlexpr_of_string s in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in - <:str_item< - value $lid:s$ = - let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in - let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in - $lid:s$ >> - -let warning_redundant prefix s = - Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s - -let get_type prefix s = function -| None -> None -| Some typ -> - if is_self s typ then - let () = warning_redundant prefix s in None - else Some typ - -let check_type prefix s = function -| None -> () -| Some _ -> warning_redundant prefix s - -let declare_tactic_argument loc s (typ, f, g, h) cl = - let se = mlexpr_of_string s in - let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with - | `Uniform (typ, pr) -> - let typ = get_type "" s typ in - typ, pr, typ, pr, typ, pr - | `Specialized (a, rpr, c, gpr, e, tpr) -> - (** Check that we actually need the TYPED AS arguments *) - let rawtyp = get_type "RAW_" s a in - let glbtyp = get_type "GLOB_" s c in - let toptyp = get_type "" s e in - let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in - let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in - rawtyp, rpr, glbtyp, gpr, toptyp, tpr - in - let glob = match g with - | None -> - begin match rawtyp with - | None -> <:expr< fun ist v -> (ist, v) >> - | Some rawtyp -> - <:expr< fun ist v -> - let ans = out_gen $make_globwit loc rawtyp$ - (Tacintern.intern_genarg ist - (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in - (ist, ans) >> - end - | Some f -> - <:expr< fun ist v -> (ist, $lid:f$ ist v) >> - in - let interp = match f with - | None -> - begin match globtyp with - | None -> - let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in - <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> - | Some globtyp -> - <:expr< fun ist x -> - Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> - end - | Some f -> - (** Compatibility layer, TODO: remove me *) - let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in - <:expr< - let f = $lid:f$ in - fun ist v -> Ftactic.nf_s_enter { Proofview.Goal.s_enter = fun gl -> - let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in - let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in - Sigma.Unsafe.of_pair (Ftactic.return v, sigma) - } - >> in - let subst = match h with - | None -> - begin match globtyp with - | None -> <:expr< fun s v -> v >> - | Some globtyp -> - <:expr< fun s x -> - out_gen $make_globwit loc globtyp$ - (Tacsubst.subst_genarg s - (Genarg.in_gen $make_globwit loc globtyp$ x)) >> - end - | Some f -> <:expr< $lid:f$>> in - let dyn = match typ with - | None -> <:expr< None >> - | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> - in - let wit = <:expr< $lid:"wit_"^s$ >> in - declare_str_items loc - [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; - <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; - <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; - <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; - make_extend loc s cl wit; - <:str_item< do { - Pptactic.declare_extra_genarg_pprule - $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; - Tacentries.create_ltac_quotation $se$ - (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v)) - ($lid:s$, None) - } >> ] - -let declare_vernac_argument loc s pr cl = - let se = mlexpr_of_string s in - let wit = <:expr< $lid:"wit_"^s$ >> in - let pr_rules = match pr with - | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> - | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in - declare_str_items loc - [ <:str_item< - value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = - Genarg.create_arg $se$ >>; - make_extend loc s cl wit; - <:str_item< do { - Pptactic.declare_extra_genarg_pprule $wit$ - $pr_rules$ - (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) - (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } - >> ] - -open Pcaml -open PcamlSig (* necessary for camlp4 *) - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "ARGUMENT"; "EXTEND"; s = entry_name; - header = argextend_header; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - declare_tactic_argument loc s header l - | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name; - pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - declare_vernac_argument loc s pr l ] ] - ; - argextend_specialized: - [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ]; - "RAW_PRINTED"; "BY"; rawpr = LIDENT; - globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ]; - "GLOB_PRINTED"; "BY"; globpr = LIDENT -> - (rawtyp, rawpr, globtyp, globpr) ] ] - ; - argextend_header: - [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; - "PRINTED"; "BY"; pr = LIDENT; - f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; - g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; - h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; - special = OPT argextend_specialized -> - let repr = match special with - | None -> `Uniform (typ, pr) - | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) - in - (repr, f, g, h) ] ] - ; - argtype: - [ "2" - [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] - | "1" - [ e = argtype; LIDENT "list" -> ListArgType e - | e = argtype; LIDENT "option" -> OptArgType e ] - | "0" - [ e = LIDENT -> - let e = parse_user_entry e "" in - type_of_user_symbol e - | "("; e = argtype; ")" -> e ] ] - ; - argrule: - [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] - ; - genarg: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, s) - | s = STRING -> ExtTerminal s - ] ] - ; - entry_name: - [ [ s = LIDENT -> s - | UIDENT -> failwith "Argument entry names must be lowercase" - ] ] - ; - END diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp new file mode 100644 index 000000000..eaaa7f025 --- /dev/null +++ b/grammar/argextend.mlp @@ -0,0 +1,254 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > + +let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> + +let rec make_wit loc = function + | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> + | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> + | PairArgType (t1,t2) -> + <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> + | ExtraArgType s -> mk_extraarg loc s + +let is_self s = function +| ExtraArgType s' -> s = s' +| _ -> false + +let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> +let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> +let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> + +let make_act loc act pil = + let rec make = function + | [] -> <:expr< (fun loc -> $act$) >> + | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtTerminal _ :: tl -> + <:expr< (fun _ -> $make tl$) >> in + make (List.rev pil) + +let make_prod_item = function + | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> + | ExtNonTerminal (g, _) -> + let base s = <:expr< $lid:s$ >> in + mlexpr_of_prod_entry_key base g + +let rec make_prod = function +| [] -> <:expr< Extend.Stop >> +| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> + +let make_rule loc (prods,act) = + <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> + +let is_ident x = function +| <:expr< $lid:s$ >> -> (s : string) = x +| _ -> false + +let make_extend loc s cl wit = match cl with +| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act -> + (** Special handling of identity arguments by not redeclaring an entry *) + <:str_item< + value $lid:s$ = + let () = Pcoq.register_grammar $wit$ $lid:e$ in + $lid:e$ + >> +| _ -> + let se = mlexpr_of_string s in + let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in + <:str_item< + value $lid:s$ = + let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + $lid:s$ >> + +let warning_redundant prefix s = + Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s + +let get_type prefix s = function +| None -> None +| Some typ -> + if is_self s typ then + let () = warning_redundant prefix s in None + else Some typ + +let check_type prefix s = function +| None -> () +| Some _ -> warning_redundant prefix s + +let declare_tactic_argument loc s (typ, f, g, h) cl = + let se = mlexpr_of_string s in + let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with + | `Uniform (typ, pr) -> + let typ = get_type "" s typ in + typ, pr, typ, pr, typ, pr + | `Specialized (a, rpr, c, gpr, e, tpr) -> + (** Check that we actually need the TYPED AS arguments *) + let rawtyp = get_type "RAW_" s a in + let glbtyp = get_type "GLOB_" s c in + let toptyp = get_type "" s e in + let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in + let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in + rawtyp, rpr, glbtyp, gpr, toptyp, tpr + in + let glob = match g with + | None -> + begin match rawtyp with + | None -> <:expr< fun ist v -> (ist, v) >> + | Some rawtyp -> + <:expr< fun ist v -> + let ans = out_gen $make_globwit loc rawtyp$ + (Tacintern.intern_genarg ist + (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in + (ist, ans) >> + end + | Some f -> + <:expr< fun ist v -> (ist, $lid:f$ ist v) >> + in + let interp = match f with + | None -> + begin match globtyp with + | None -> + let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in + <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> + | Some globtyp -> + <:expr< fun ist x -> + Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> + end + | Some f -> + (** Compatibility layer, TODO: remove me *) + let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in + <:expr< + let f = $lid:f$ in + fun ist v -> Ftactic.nf_s_enter { Proofview.Goal.s_enter = fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in + Sigma.Unsafe.of_pair (Ftactic.return v, sigma) + } + >> in + let subst = match h with + | None -> + begin match globtyp with + | None -> <:expr< fun s v -> v >> + | Some globtyp -> + <:expr< fun s x -> + out_gen $make_globwit loc globtyp$ + (Tacsubst.subst_genarg s + (Genarg.in_gen $make_globwit loc globtyp$ x)) >> + end + | Some f -> <:expr< $lid:f$>> in + let dyn = match typ with + | None -> <:expr< None >> + | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> + in + let wit = <:expr< $lid:"wit_"^s$ >> in + declare_str_items loc + [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; + <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; + <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; + <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; + <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; + make_extend loc s cl wit; + <:str_item< do { + Pptactic.declare_extra_genarg_pprule + $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; + Tacentries.create_ltac_quotation $se$ + (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v)) + ($lid:s$, None) + } >> ] + +let declare_vernac_argument loc s pr cl = + let se = mlexpr_of_string s in + let wit = <:expr< $lid:"wit_"^s$ >> in + let pr_rules = match pr with + | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> + | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in + declare_str_items loc + [ <:str_item< + value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = + Genarg.create_arg $se$ >>; + make_extend loc s cl wit; + <:str_item< do { + Pptactic.declare_extra_genarg_pprule $wit$ + $pr_rules$ + (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) + (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } + >> ] + +open Pcaml +open PcamlSig (* necessary for camlp4 *) + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "ARGUMENT"; "EXTEND"; s = entry_name; + header = argextend_header; + OPT "|"; l = LIST1 argrule SEP "|"; + "END" -> + declare_tactic_argument loc s header l + | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name; + pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; + OPT "|"; l = LIST1 argrule SEP "|"; + "END" -> + declare_vernac_argument loc s pr l ] ] + ; + argextend_specialized: + [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ]; + "RAW_PRINTED"; "BY"; rawpr = LIDENT; + globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ]; + "GLOB_PRINTED"; "BY"; globpr = LIDENT -> + (rawtyp, rawpr, globtyp, globpr) ] ] + ; + argextend_header: + [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; + "PRINTED"; "BY"; pr = LIDENT; + f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; + special = OPT argextend_specialized -> + let repr = match special with + | None -> `Uniform (typ, pr) + | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) + in + (repr, f, g, h) ] ] + ; + argtype: + [ "2" + [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] + | "1" + [ e = argtype; LIDENT "list" -> ListArgType e + | e = argtype; LIDENT "option" -> OptArgType e ] + | "0" + [ e = LIDENT -> + let e = parse_user_entry e "" in + type_of_user_symbol e + | "("; e = argtype; ")" -> e ] ] + ; + argrule: + [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] + ; + genarg: + [ [ e = LIDENT; "("; s = LIDENT; ")" -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) + | s = STRING -> ExtTerminal s + ] ] + ; + entry_name: + [ [ s = LIDENT -> s + | UIDENT -> failwith "Argument entry names must be lowercase" + ] ] + ; + END diff --git a/grammar/gramCompat.ml4 b/grammar/gramCompat.ml4 deleted file mode 100644 index 6246da7bb..000000000 --- a/grammar/gramCompat.ml4 +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > *) -ELSE - Ast.stSem_of_list l -END - -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) - -IFDEF CAMLP5 THEN - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - -ELSE - -let make_fun loc cl = - let mk_when = function - | Some w -> w - | None -> Ast.ExNil loc - in - let mk_clause (patt,optwhen,expr) = - (* correspond to <:match_case< ... when ... -> ... >> *) - Ast.McArr (loc, patt, mk_when optwhen, expr) in - let init = mk_clause (default_patt loc) in - let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in - let l = List.fold_right add_clause cl init in - Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *) - -END diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp new file mode 100644 index 000000000..6246da7bb --- /dev/null +++ b/grammar/gramCompat.mlp @@ -0,0 +1,86 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > *) +ELSE + Ast.stSem_of_list l +END + +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) + +IFDEF CAMLP5 THEN + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) + +ELSE + +let make_fun loc cl = + let mk_when = function + | Some w -> w + | None -> Ast.ExNil loc + in + let mk_clause (patt,optwhen,expr) = + (* correspond to <:match_case< ... when ... -> ... >> *) + Ast.McArr (loc, patt, mk_when optwhen, expr) in + let init = mk_clause (default_patt loc) in + let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in + let l = List.fold_right add_clause cl init in + Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *) + +END diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 deleted file mode 100644 index af90f5f2a..000000000 --- a/grammar/q_constr.ml4 +++ /dev/null @@ -1,114 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > - -let apply_ref f l = - <:expr< - Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$) - >> - -EXTEND - GLOBAL: expr; - expr: - [ [ "PATTERN"; "["; c = constr; "]" -> - <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] - ; - ident: - [ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ] - ; - name: - [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] - ; - string: - [ [ s = UIDENT -> s | s = LIDENT -> s ] ] - ; - constr: - [ "200" RIGHTA - [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> - | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> - | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> - <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> - (* fix todo *) - ] - | "100" RIGHTA - [ c1 = constr; ":"; c2 = SELF -> - <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] - | "90" RIGHTA - [ c1 = constr; "->"; c2 = SELF -> - <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] - | "75" RIGHTA - [ "~"; c = constr -> - apply_ref <:expr< coq_not_ref >> [c] ] - | "70" RIGHTA - [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT -> - apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ] - | "10" LEFTA - [ f = constr; args = LIST1 NEXT -> - let args = mlexpr_of_list (fun x -> x) args in - <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ] - | "0" - [ id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),Misctypes.IntroAnonymous,None) >> - | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> - | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> - apply_ref <:expr< coq_sumbool_ref >> [c1;c2] - | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$, None) >> - | c = match_constr -> c - | "("; c = constr LEVEL "200"; ")" -> c ] ] - ; - match_constr: - [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; - "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> - let br = mlexpr_of_list (fun x -> x) br in - <:expr< Glob_term.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> - ] ] - ; - match_type: - [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; - "return"; ty = constr LEVEL "100" -> - let nal = mlexpr_of_list (fun x -> x) nal in - <:expr< Some $ty$ >>, - <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> - | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ] - ; - eqn: - [ [ (lid,pl) = pattern; "=>"; rhs = constr -> - let lid = mlexpr_of_list (fun x -> x) lid in - <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> - ] ] - ; - pattern: - [ [ "%"; e = string; lip = LIST0 patvar -> - let lp = mlexpr_of_list (fun (_,x) -> x) lip in - let lid = List.flatten (List.map fst lip) in - lid, <:expr< Glob_term.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> - | p = patvar -> p - | "("; p = pattern; ")" -> p ] ] - ; - patvar: - [ [ "_" -> [], <:expr< Glob_term.PatVar ($dloc$,Anonymous) >> - | id = ident -> [id], <:expr< Glob_term.PatVar ($dloc$,Name $id$) >> - ] ] - ; - END;; - -(* Example -open Coqlib -let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] -*) diff --git a/grammar/q_constr.mlp b/grammar/q_constr.mlp new file mode 100644 index 000000000..8e1587ec3 --- /dev/null +++ b/grammar/q_constr.mlp @@ -0,0 +1,112 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > + +let apply_ref f l = + <:expr< + Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$) + >> + +EXTEND + GLOBAL: expr; + expr: + [ [ "PATTERN"; "["; c = constr; "]" -> + <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] + ; + ident: + [ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ] + ; + name: + [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] + ; + string: + [ [ s = UIDENT -> s | s = LIDENT -> s ] ] + ; + constr: + [ "200" RIGHTA + [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> + <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> + | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> + <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> + | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> + <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> + (* fix todo *) + ] + | "100" RIGHTA + [ c1 = constr; ":"; c2 = SELF -> + <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] + | "90" RIGHTA + [ c1 = constr; "->"; c2 = SELF -> + <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] + | "75" RIGHTA + [ "~"; c = constr -> + apply_ref <:expr< coq_not_ref >> [c] ] + | "70" RIGHTA + [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT -> + apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ] + | "10" LEFTA + [ f = constr; args = LIST1 NEXT -> + let args = mlexpr_of_list (fun x -> x) args in + <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ] + | "0" + [ id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),Misctypes.IntroAnonymous,None) >> + | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> + | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> + apply_ref <:expr< coq_sumbool_ref >> [c1;c2] + | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$, None) >> + | c = match_constr -> c + | "("; c = constr LEVEL "200"; ")" -> c ] ] + ; + match_constr: + [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; + "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> + let br = mlexpr_of_list (fun x -> x) br in + <:expr< Glob_term.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> + ] ] + ; + match_type: + [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; + "return"; ty = constr LEVEL "100" -> + let nal = mlexpr_of_list (fun x -> x) nal in + <:expr< Some $ty$ >>, + <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> + | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ] + ; + eqn: + [ [ (lid,pl) = pattern; "=>"; rhs = constr -> + let lid = mlexpr_of_list (fun x -> x) lid in + <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> + ] ] + ; + pattern: + [ [ "%"; e = string; lip = LIST0 patvar -> + let lp = mlexpr_of_list (fun (_,x) -> x) lip in + let lid = List.flatten (List.map fst lip) in + lid, <:expr< Glob_term.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> + | p = patvar -> p + | "("; p = pattern; ")" -> p ] ] + ; + patvar: + [ [ "_" -> [], <:expr< Glob_term.PatVar ($dloc$,Anonymous) >> + | id = ident -> [id], <:expr< Glob_term.PatVar ($dloc$,Name $id$) >> + ] ] + ; + END;; + +(* Example +open Coqlib +let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] +*) diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 deleted file mode 100644 index 2d5c40894..000000000 --- a/grammar/q_util.ml4 +++ /dev/null @@ -1,118 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let e1 = f e1 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< [$e1$ :: $e2$] >>) - l (let loc = CompatLoc.ghost in <:expr< [] >>) - -let mlexpr_of_pair m1 m2 (a1,a2) = - let e1 = m1 a1 and e2 = m2 a2 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< ($e1$, $e2$) >> - -(* We don't give location for tactic quotation! *) -let loc = CompatLoc.ghost - - -let mlexpr_of_bool = function - | true -> <:expr< True >> - | false -> <:expr< False >> - -let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> - -let mlexpr_of_string s = <:expr< $str:s$ >> - -let mlexpr_of_option f = function - | None -> <:expr< None >> - | Some e -> <:expr< Some $f e$ >> - -let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> - -let rec mlexpr_of_prod_entry_key f = function - | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Extend.Aentry $f e$ >> - | Uentryl (e, l) -> - (** Keep in sync with Pcoq! *) - assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> - else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> - -let rec type_of_user_symbol = function -| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> - ListArgType (type_of_user_symbol s) -| Uopt s -> - OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> ExtraArgType e - -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := c = d; - incr i - done; - !break - -let rec parse_user_entry s sep = - 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)) "" in - Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) "" in - Ulist1sep (entry, sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) "" in - Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) "" in - Ulist0sep (entry, sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) "" in - Uopt entry - else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in - Uentryl ("tactic", n) - else - let s = match s with "hyp" -> "var" | _ -> s in - Uentry s diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp new file mode 100644 index 000000000..2d5c40894 --- /dev/null +++ b/grammar/q_util.mlp @@ -0,0 +1,118 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let e1 = f e1 in + let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + <:expr< [$e1$ :: $e2$] >>) + l (let loc = CompatLoc.ghost in <:expr< [] >>) + +let mlexpr_of_pair m1 m2 (a1,a2) = + let e1 = m1 a1 and e2 = m2 a2 in + let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + <:expr< ($e1$, $e2$) >> + +(* We don't give location for tactic quotation! *) +let loc = CompatLoc.ghost + + +let mlexpr_of_bool = function + | true -> <:expr< True >> + | false -> <:expr< False >> + +let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> + +let mlexpr_of_string s = <:expr< $str:s$ >> + +let mlexpr_of_option f = function + | None -> <:expr< None >> + | Some e -> <:expr< Some $f e$ >> + +let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> + +let rec mlexpr_of_prod_entry_key f = function + | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Uentry e -> <:expr< Extend.Aentry $f e$ >> + | Uentryl (e, l) -> + (** Keep in sync with Pcoq! *) + assert (e = "tactic"); + if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> + else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + +let rec type_of_user_symbol = function +| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> + ListArgType (type_of_user_symbol s) +| Uopt s -> + OptArgType (type_of_user_symbol s) +| Uentry e | Uentryl (e, _) -> ExtraArgType e + +let coincide s pat off = + let len = String.length pat in + let break = ref true in + let i = ref 0 in + while !break && !i < len do + let c = Char.code s.[off + !i] in + let d = Char.code pat.[!i] in + break := c = d; + incr i + done; + !break + +let rec parse_user_entry s sep = + 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)) "" in + Ulist1 entry + else if l > 12 && coincide s "ne_" 0 && + coincide s "_list_sep" (l-9) then + let entry = parse_user_entry (String.sub s 3 (l-12)) "" in + Ulist1sep (entry, sep) + else if l > 5 && coincide s "_list" (l-5) then + let entry = parse_user_entry (String.sub s 0 (l-5)) "" in + Ulist0 entry + else if l > 9 && coincide s "_list_sep" (l-9) then + let entry = parse_user_entry (String.sub s 0 (l-9)) "" in + Ulist0sep (entry, sep) + else if l > 4 && coincide s "_opt" (l-4) then + let entry = parse_user_entry (String.sub s 0 (l-4)) "" in + Uopt entry + else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then + let n = Char.code s.[6] - 48 in + Uentryl ("tactic", n) + else + let s = match s with "hyp" -> "var" | _ -> s in + Uentry s diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 deleted file mode 100644 index 8593bad5d..000000000 --- a/grammar/tacextend.ml4 +++ /dev/null @@ -1,184 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > - -let plugin_name = <:expr< __coq_plugin_name >> - -let mlexpr_of_ident id = - (** Workaround for badly-designed generic arguments lacking a closure *) - let id = "$" ^ id in - <:expr< Names.Id.of_string_soft $str:id$ >> - -let rec make_patt = function - | [] -> <:patt< [] >> - | ExtNonTerminal (_, p) :: l -> - <:patt< [ $lid:p$ :: $make_patt l$ ] >> - | _::l -> make_patt l - -let rec make_let raw e = function - | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, p) :: l -> - let t = type_of_user_symbol g in - let 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< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in - <:expr< let $lid:p$ = $v$ in $e$ >> - | _::l -> make_let raw e l - -let make_clause (pt,_,e) = - (make_patt pt, - vala None, - make_let false e pt) - -let make_fun_clauses loc s l = - let map c = GramCompat.make_fun loc [make_clause c] in - mlexpr_of_list map l - -let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> - -let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> -| Uentry e -> - let arg = get_argt <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> -| Uentryl (e, l) -> - assert (e = "tactic"); - let arg = get_argt <:expr< Constrarg.wit_tactic >> in - <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> - -let make_prod_item = function - | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> - | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> - -let mlexpr_of_clause cl = - mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl - -(** Special treatment of constr entries *) -let is_constr_gram = function -| ExtTerminal _ -> false -| ExtNonTerminal (Uentry "constr", _) -> true -| _ -> false - -let make_var = function - | ExtNonTerminal (_, p) -> Some p - | _ -> assert false - -let declare_tactic loc s c cl = match cl with -| [(ExtTerminal 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 = List.map make_var 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 ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in - let name = mlexpr_of_string name in - let tac = match rem with - | [] -> - (** 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]. *) - <:expr< fun _ $lid:"ist"$ -> $tac$ >> - | _ -> - let f = GramCompat.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$, $ml$, [])) >> 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 gl = mlexpr_of_clause cl in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in - declare_str_items loc - [ <:str_item< do { - try do { - Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); - 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)) ]; } >> - ] - -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 - | ExtNonTerminal _ :: _ -> - (* En attendant la syntaxe de tacticielles *) - failwith "Tactic syntax must start with an identifier" - | _ -> (l,c,e)) - ] ] - ; - tacargs: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, s) - | s = STRING -> - let () = if s = "" then failwith "Empty terminal." in - ExtTerminal s - ] ] - ; - tac_name: - [ [ s = LIDENT -> s - | s = UIDENT -> s - ] ] - ; - END diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp new file mode 100644 index 000000000..1d52a85a5 --- /dev/null +++ b/grammar/tacextend.mlp @@ -0,0 +1,182 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > + +let plugin_name = <:expr< __coq_plugin_name >> + +let mlexpr_of_ident id = + (** Workaround for badly-designed generic arguments lacking a closure *) + let id = "$" ^ id in + <:expr< Names.Id.of_string_soft $str:id$ >> + +let rec make_patt = function + | [] -> <:patt< [] >> + | ExtNonTerminal (_, p) :: l -> + <:patt< [ $lid:p$ :: $make_patt l$ ] >> + | _::l -> make_patt l + +let rec make_let raw e = function + | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g in + let 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< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in + <:expr< let $lid:p$ = $v$ in $e$ >> + | _::l -> make_let raw e l + +let make_clause (pt,_,e) = + (make_patt pt, + vala None, + make_let false e pt) + +let make_fun_clauses loc s l = + let map c = GramCompat.make_fun loc [make_clause c] in + mlexpr_of_list map l + +let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> + +let rec mlexpr_of_symbol = function +| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Uentry e -> + let arg = get_argt <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let arg = get_argt <:expr< Constrarg.wit_tactic >> in + <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> + +let make_prod_item = function + | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> + | ExtNonTerminal (g, id) -> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> + +let mlexpr_of_clause cl = + mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl + +(** Special treatment of constr entries *) +let is_constr_gram = function +| ExtTerminal _ -> false +| ExtNonTerminal (Uentry "constr", _) -> true +| _ -> false + +let make_var = function + | ExtNonTerminal (_, p) -> Some p + | _ -> assert false + +let declare_tactic loc s c cl = match cl with +| [(ExtTerminal 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 = List.map make_var 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 ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in + let name = mlexpr_of_string name in + let tac = match rem with + | [] -> + (** 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]. *) + <:expr< fun _ $lid:"ist"$ -> $tac$ >> + | _ -> + let f = GramCompat.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$, $ml$, [])) >> 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 gl = mlexpr_of_clause cl in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in + declare_str_items loc + [ <:str_item< do { + try do { + Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); + 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)) ]; } >> + ] + +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 + | ExtNonTerminal _ :: _ -> + (* En attendant la syntaxe de tacticielles *) + failwith "Tactic syntax must start with an identifier" + | _ -> (l,c,e)) + ] ] + ; + tacargs: + [ [ e = LIDENT; "("; s = LIDENT; ")" -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) + | s = STRING -> + let () = if s = "" then failwith "Empty terminal." in + ExtTerminal s + ] ] + ; + tac_name: + [ [ s = LIDENT -> s + | s = UIDENT -> s + ] ] + ; + END diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 deleted file mode 100644 index 1611de39c..000000000 --- a/grammar/vernacextend.ml4 +++ /dev/null @@ -1,200 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* e - | ExtNonTerminal (g, p) :: l -> - let t = type_of_user_symbol g in - let loc = MLast.loc_of_expr e in - let e = make_let e l in - <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> - | _::l -> make_let e l - -let make_clause { r_patt = pt; r_branch = e; } = - (make_patt pt, - vala None, - make_let e pt) - -(* To avoid warnings *) -let mk_ignore c pt = - let fold accu = function - | ExtNonTerminal (_, p) -> p :: accu - | _ -> accu - in - let names = List.fold_left fold [] pt in - let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in - let names = List.fold_left fold <:expr< () >> names in - <:expr< do { let _ = $names$ in $c$ } >> - -let make_clause_classifier cg s { r_patt = pt; r_class = c; } = - match c ,cg with - | Some c, _ -> - (make_patt pt, - vala None, - make_let (mk_ignore c pt) pt) - | None, Some cg -> - (make_patt pt, - vala None, - <:expr< fun () -> $cg$ $str:s$ >>) - | None, None -> prerr_endline - (("Vernac entry \""^s^"\" misses a classifier. "^ - "A classifier is a function that returns an expression "^ - "of type vernac_classification (see Vernacexpr). You can: ") ^ - "- " ^ ( - ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ - "new vernacular command does not alter the system state;"))^ "\n" ^ - "- " ^ ( - ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ - "new vernacular command alters the system state but not the "^ - "parser nor it starts a proof or ends one;"))^ "\n" ^ - "- " ^ ( - ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ - "a global function f. The function f will be called passing "^ - "\""^s^"\" as the only argument;")) ^ "\n" ^ - "- " ^ ( - "Add a specific classifier in each clause using the syntax:" - ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^ - ("Specific classifiers have precedence over global "^ - "classifiers. Only one classifier is called.") ^ "\n"); - (make_patt pt, - vala None, - <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) - -let make_fun_clauses loc s l = - let map c = - let depr = match c.r_depr with - | None -> false - | Some () -> true - in - let cl = GramCompat.make_fun loc [make_clause c] in - <:expr< ($mlexpr_of_bool depr$, $cl$)>> - in - mlexpr_of_list map l - -let make_fun_classifiers loc s c l = - let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in - mlexpr_of_list (fun x -> x) cl - -let make_prod_item = function - | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | ExtNonTerminal (g, id) -> - let nt = type_of_user_symbol g in - let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in - <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ - $mlexpr_of_prod_entry_key base g$ >> - -let mlexpr_of_clause cl = - let mkexpr { r_head = a; r_patt = b; } = match a with - | None -> mlexpr_of_list make_prod_item b - | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) - in - mlexpr_of_list mkexpr cl - -let declare_command loc s c nt cl = - let se = mlexpr_of_string s in - let gl = mlexpr_of_clause cl in - let funcl = make_fun_clauses loc s cl in - let classl = make_fun_classifiers loc s c cl in - declare_str_items loc - [ <:str_item< do { - try do { - CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; - CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } - with [ e when Errors.noncritical e -> - Pp.msg_warning - (Pp.app - (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) - (Errors.print e)) ]; - CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; - } >> ] - -open Pcaml -open PcamlSig (* necessary for camlp4 *) - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s c <:expr> l - | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s c <:expr> l - | "DECLARE"; "PLUGIN"; name = STRING -> - declare_str_items loc [ - <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Mltop.add_known_module $str:name$ >>; - ] - ] ] - ; - classification: - [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> - | "CLASSIFIED"; "AS"; "SIDEFF" -> - <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> - | "CLASSIFIED"; "AS"; "QUERY" -> - <:expr< fun _ -> Vernac_classifier.classify_as_query >> - ] ] - ; - deprecation: - [ [ "DEPRECATED" -> () ] ] - ; - (* spiwack: comment-by-guessing: it seems that the isolated string (which - otherwise could have been another argument) is not passed to the - VernacExtend interpreter function to discriminate between the clauses. *) - rule: - [ [ "["; s = STRING; l = LIST0 args; "]"; - d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun () -> $e$ >> in - { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } - | "[" ; "-" ; l = LIST1 args ; "]" ; - d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun () -> $e$ >> in - { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } - ] ] - ; - classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ] - ; - args: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, s) - | s = STRING -> - ExtTerminal s - ] ] - ; - END -;; diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp new file mode 100644 index 000000000..fa8610fb9 --- /dev/null +++ b/grammar/vernacextend.mlp @@ -0,0 +1,198 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* e + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g in + let loc = MLast.loc_of_expr e in + let e = make_let e l in + <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> + | _::l -> make_let e l + +let make_clause { r_patt = pt; r_branch = e; } = + (make_patt pt, + vala None, + make_let e pt) + +(* To avoid warnings *) +let mk_ignore c pt = + let fold accu = function + | ExtNonTerminal (_, p) -> p :: accu + | _ -> accu + in + let names = List.fold_left fold [] pt in + let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in + let names = List.fold_left fold <:expr< () >> names in + <:expr< do { let _ = $names$ in $c$ } >> + +let make_clause_classifier cg s { r_patt = pt; r_class = c; } = + match c ,cg with + | Some c, _ -> + (make_patt pt, + vala None, + make_let (mk_ignore c pt) pt) + | None, Some cg -> + (make_patt pt, + vala None, + <:expr< fun () -> $cg$ $str:s$ >>) + | None, None -> prerr_endline + (("Vernac entry \""^s^"\" misses a classifier. "^ + "A classifier is a function that returns an expression "^ + "of type vernac_classification (see Vernacexpr). You can: ") ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ + "new vernacular command does not alter the system state;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ + "new vernacular command alters the system state but not the "^ + "parser nor it starts a proof or ends one;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ + "a global function f. The function f will be called passing "^ + "\""^s^"\" as the only argument;")) ^ "\n" ^ + "- " ^ ( + "Add a specific classifier in each clause using the syntax:" + ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^ + ("Specific classifiers have precedence over global "^ + "classifiers. Only one classifier is called.") ^ "\n"); + (make_patt pt, + vala None, + <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + +let make_fun_clauses loc s l = + let map c = + let depr = match c.r_depr with + | None -> false + | Some () -> true + in + let cl = GramCompat.make_fun loc [make_clause c] in + <:expr< ($mlexpr_of_bool depr$, $cl$)>> + in + mlexpr_of_list map l + +let make_fun_classifiers loc s c l = + let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in + mlexpr_of_list (fun x -> x) cl + +let make_prod_item = function + | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtNonTerminal (g, id) -> + let nt = type_of_user_symbol g in + let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in + <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ + $mlexpr_of_prod_entry_key base g$ >> + +let mlexpr_of_clause cl = + let mkexpr { r_head = a; r_patt = b; } = match a with + | None -> mlexpr_of_list make_prod_item b + | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) + in + mlexpr_of_list mkexpr cl + +let declare_command loc s c nt cl = + let se = mlexpr_of_string s in + let gl = mlexpr_of_clause cl in + let funcl = make_fun_clauses loc s cl in + let classl = make_fun_classifiers loc s c cl in + declare_str_items loc + [ <:str_item< do { + try do { + CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; + CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } + with [ e when Errors.noncritical e -> + Pp.msg_warning + (Pp.app + (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) + (Errors.print e)) ]; + CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; + } >> ] + +open Pcaml +open PcamlSig (* necessary for camlp4 *) + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification; + OPT "|"; l = LIST1 rule SEP "|"; + "END" -> + declare_command loc s c <:expr> l + | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; + OPT "|"; l = LIST1 rule SEP "|"; + "END" -> + declare_command loc s c <:expr> l + | "DECLARE"; "PLUGIN"; name = STRING -> + declare_str_items loc [ + <:str_item< value __coq_plugin_name = $str:name$ >>; + <:str_item< value _ = Mltop.add_known_module $str:name$ >>; + ] + ] ] + ; + classification: + [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> + | "CLASSIFIED"; "AS"; "SIDEFF" -> + <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> + | "CLASSIFIED"; "AS"; "QUERY" -> + <:expr< fun _ -> Vernac_classifier.classify_as_query >> + ] ] + ; + deprecation: + [ [ "DEPRECATED" -> () ] ] + ; + (* spiwack: comment-by-guessing: it seems that the isolated string (which + otherwise could have been another argument) is not passed to the + VernacExtend interpreter function to discriminate between the clauses. *) + rule: + [ [ "["; s = STRING; l = LIST0 args; "]"; + d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> + let () = if s = "" then failwith "Command name is empty." in + let b = <:expr< fun () -> $e$ >> in + { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + | "[" ; "-" ; l = LIST1 args ; "]" ; + d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> + let b = <:expr< fun () -> $e$ >> in + { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + ] ] + ; + classifier: + [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ] + ; + args: + [ [ e = LIDENT; "("; s = LIDENT; ")" -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) + | s = STRING -> + ExtTerminal s + ] ] + ; + END +;; -- cgit v1.2.3