diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 65 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 24 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 79 | ||||
| -rw-r--r-- | grammar/q_util.mli | 4 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 30 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 49 |
6 files changed, 107 insertions, 144 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 46c68ecc3..5bf7b65d7 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -10,10 +10,8 @@ open Genarg open Q_util -open Egramml open Compat open Extend -open Pcoq let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> @@ -23,12 +21,7 @@ let qualified_name loc s = let (name, path) = CList.sep_last path in qualified_name loc path name -let mk_extraarg loc s = - try - let name = Genarg.get_name0 s in - qualified_name loc name - with Not_found -> - <:expr< $lid:"wit_"^s$ >> +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$ >> @@ -41,28 +34,19 @@ 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 has_extraarg l = - let check = function - | ExtNonTerminal(ExtraArgType _, _, _) -> true - | _ -> false - in - List.exists check l - let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (t, _, p) :: tl -> - <:expr< - (fun $lid:p$ -> - let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) - >> + | 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< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g + | ExtNonTerminal (_, g, _) -> + let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in + mlexpr_of_prod_entry_key base g let rec make_prod = function | [] -> <:expr< Extend.Stop >> @@ -71,6 +55,27 @@ let rec make_prod = function 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$ >> -> CString.equal s 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 declare_tactic_argument loc s (typ, pr, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr = match typ with | `Uniform typ -> @@ -136,8 +141,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$) = @@ -146,10 +149,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + make_extend loc s cl wit; <:str_item< do { - Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; Egramcoq.create_ltac_quotation $se$ @@ -160,8 +161,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in let pr_rules = match pr with | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in @@ -169,17 +168,14 @@ let declare_vernac_argument loc s pr cl = [ <:str_item< value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + make_extend loc s cl wit; <:str_item< do { - Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); 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 Pcoq open Pcaml open PcamlSig (* necessary for camlp4 *) @@ -236,10 +232,7 @@ EXTEND | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in ExtNonTerminal (type_of_user_symbol e, e, s) - | s = STRING -> - if String.length s > 0 && Util.is_letter s.[0] then - Lexer.add_keyword s; - ExtTerminal s + | s = STRING -> ExtTerminal s ] ] ; entry_name: diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 6a265bf4a..ae18925ea 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,46 +1,22 @@ Coq_config -Hook -Terminal Hashset Hashcons -CSet CMap Int -Dyn -HMap Option Store Exninfo -Backtrace -Pp_control -Flags Loc CList CString -Serialize -Stateid -Feedback -Pp -CArray -CStack -Util -Ppstyle -Errors Segmenttree Unicodetable Unicode -Genarg - -Stdarg -Constrarg Tok Compat -Lexer -Entry -Pcoq Q_util Argextend diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 1848bf85f..4160d03c5 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -47,44 +47,63 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> -let repr_entry e = - let entry u = - let _ = Pcoq.get_entry u e in - Some (Entry.univ_name u, e) - in - try entry Pcoq.uprim with Not_found -> - try entry Pcoq.uconstr with Not_found -> - try entry Pcoq.utactic with Not_found -> None - -let rec mlexpr_of_prod_entry_key = function - | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> - | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> - | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> - | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Extend.Uentry e -> - begin match repr_entry e with - | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> - | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >> - end +let rec mlexpr_of_prod_entry_key f = function + | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >> + | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (CString.equal e "tactic"); if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> -let type_entry u e = - let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in - Genarg.unquote t - let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s -> Genarg.ListArgType (type_of_user_symbol s) | Uopt s -> Genarg.OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> - try type_entry Pcoq.uprim e with Not_found -> - try type_entry Pcoq.uconstr e with Not_found -> - try type_entry Pcoq.utactic e with Not_found -> - Genarg.ExtraArgType e +| Uentry e | Uentryl (e, _) -> Genarg.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 := Int.equal 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 > 5 && coincide s "_mods" (l-5) then + let entry = parse_user_entry (String.sub s 0 (l-1)) "" in + Umodifiers entry + else if Int.equal 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.mli b/grammar/q_util.mli index 837ec6fb0..5f292baf3 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -28,6 +28,8 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr val mlexpr_of_ident : string -> MLast.expr -val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr +val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type + +val parse_user_entry : string -> string -> Extend.user_symbol diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index c35fa00d2..1951b8b45 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -10,14 +10,8 @@ (** Implementation of the TACTIC EXTEND macro. *) -open Util -open Pp -open Names -open Genarg open Q_util open Argextend -open Pcoq -open Egramml open Compat let dloc = <:expr< Loc.ghost >> @@ -39,14 +33,6 @@ let rec mlexpr_of_argtype loc = function <:expr< Genarg.PairArgType $t1$ $t2$ >> | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> -let rec make_when loc = function - | [] -> <:expr< True >> - | ExtNonTerminal (t, _, p) :: l -> - let l = make_when loc l 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$ >> | ExtNonTerminal (t, _, p) :: l -> @@ -64,29 +50,21 @@ let rec extract_signature = function | _::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 None, make_let false e pt) let make_fun_clauses loc s l = - check_unicity s l; let map c = Compat.make_fun loc [make_clause c] in mlexpr_of_list map l let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (nt, g, id) -> + let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ - $mlexpr_of_prod_entry_key g$ >> + $mlexpr_of_prod_entry_key base g$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl @@ -125,7 +103,7 @@ let declare_tactic loc s c cl = match cl 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]. *) - if List.is_empty rem then + if CList.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 @@ -200,7 +178,7 @@ EXTEND let e = parse_user_entry e sep in ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> - if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); + let () = if CString.is_empty s then failwith "Empty terminal." in ExtTerminal s ] ] ; diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 3bb1e0907..453907689 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -10,13 +10,9 @@ (** Implementation of the VERNAC EXTEND macro. *) -open Pp -open Util open Q_util open Argextend open Tacextend -open Pcoq -open Egramml open Compat type rule = { @@ -42,7 +38,7 @@ let rec make_let e = function let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let e pt) (* To avoid warnings *) @@ -58,34 +54,34 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr c) pt)), + vala None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr cg) pt)), + vala None, <:expr< fun () -> $cg$ $str:s$ >>) - | None, None -> msg_warning - (strbrk("Vernac entry \""^s^"\" misses a classifier. "^ + | 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: ")++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ - "new vernacular command does not alter the system state;"))++fnl()++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ + "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;"))++fnl()++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ + "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;")) ++fnl()++ - str"- "++hov 0 ( - strbrk"Add a specific classifier in each clause using the syntax:" - ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++ - strbrk("Specific classifiers have precedence over global "^ - "classifiers. Only one classifier is called.")++fnl()); + "\""^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 (Some (make_when loc pt)), + vala None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = @@ -164,8 +160,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - if String.is_empty s then - Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty."); + let () = if CString.is_empty 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 ; "]" ; |