diff options
author | 2007-09-28 22:36:35 +0000 | |
---|---|---|
committer | 2007-09-28 22:36:35 +0000 | |
commit | 83015147aac453effee4d5b1b6363b31c56edd84 (patch) | |
tree | 9790716a80165743ebe63ef3e43a8f2df8640ca1 /parsing | |
parent | 38a70c48e843dd5da4120ed14148663cba094851 (diff) |
Creation of a new token PATTERNIDENT (?ident) for intro patterns, so
that "intros ? a ? b" behaves as expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10155 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 8 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
-rw-r--r-- | parsing/lexer.ml4 | 14 | ||||
-rw-r--r-- | parsing/pcoq.ml4 | 2 | ||||
-rw-r--r-- | parsing/pcoq.mli | 2 |
6 files changed, 22 insertions, 10 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 10d7f46b5..04e0f84ca 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -157,7 +157,7 @@ GEXTEND Gram | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) - | "@"; "?"; (locid,id) = identref; args=LIST1 identref -> + | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> let args = List.map (fun x -> CRef (Ident x), None) args in CApp(loc,(None,CPatVar(locid,(true,id))),args) ] | "9" @@ -222,7 +222,7 @@ GEXTEND Gram | n=INT -> CPrim (loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (loc, String s) | "_" -> CHole loc - | "?"; id=ident -> CPatVar(loc,(false,id)) ] ] + | id=pattern_ident -> CPatVar(loc,(false,id)) ] ] ; fix_constr: [ [ fx1=single_fix -> mk_single_fix fx1 diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index d2d5ad36a..8501b3436 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -27,13 +27,19 @@ GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath - ne_string string; + ne_string string pattern_ident pattern_identref; preident: [ [ s = IDENT -> s ] ] ; ident: [ [ s = IDENT -> id_of_string s ] ] ; + pattern_ident: + [ [ s = PATTERNIDENT -> id_of_string s ] ] + ; + pattern_identref: + [ [ id = pattern_ident -> (loc, id) ] ] + ; var: (* as identref, but interpret as a term identifier in ltac *) [ [ id = ident -> (loc,id) ] ] ; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ff23fb225..a4f5a4f42 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -188,7 +188,7 @@ GEXTEND Gram | t::q -> IntroOrAndPattern [[t;pairify q]] in pairify tc | "_" -> IntroWildcard - | "?"; prefix = ident -> IntroFresh prefix + | prefix = pattern_ident -> IntroFresh prefix | "?" -> IntroAnonymous | id = ident -> IntroIdentifier id ] ] diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 043a0c08a..cfa62fa5a 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -272,7 +272,7 @@ let add_keyword str = (* Adding a new token (keyword or special token). *) let add_token (con, str) = match con with | "" -> add_keyword str - | "METAIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI" + | "METAIDENT" | "PATTERNIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI" -> () | _ -> raise (Token.Error ("\ @@ -463,14 +463,16 @@ let process_chars bp c cs = | Some t -> (("", t), (bp, ep)) | None -> err (bp, ep) Undefined_token -(* Parse what follows a dot *) -let parse_after_dot bp c = parser +(* Parse what follows a dot/question mark *) +let parse_after_dot bp c = + let constructor = if c = '?' then "PATTERNIDENT" else "FIELD" in + parser | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> - ("FIELD", get_buff len) + (constructor, get_buff len) | [< s >] -> match lookup_utf8 s with | Some (Utf8Letter n) -> - ("FIELD", get_buff (ident_tail (nstore n 0 s) s)) + (constructor, get_buff (ident_tail (nstore n 0 s) s)) | Some (Utf8IdentPart _ | AsciiChar | Utf8Symbol) | None -> fst (process_chars bp c s) @@ -481,7 +483,7 @@ let rec next_token = parser bp | [< ''$'; len = ident_tail (store 0 '$') >] ep -> comment_stop bp; (("METAIDENT", get_buff len), (bp,ep)) - | [< ''.' as c; t = parse_after_dot bp c >] ep -> + | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep -> comment_stop bp; if Options.do_translate() & t=("",".") then between_com := true; (t, (bp,ep)) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index b0e573eb9..d72a49046 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -399,6 +399,8 @@ module Prim = let name = Gram.Entry.create "Prim.name" let identref = Gram.Entry.create "Prim.identref" + let pattern_ident = Gram.Entry.create "pattern_ident" + let pattern_identref = Gram.Entry.create "pattern_identref" (* A synonym of ident - maybe ident will be located one day *) let base_ident = Gram.Entry.create "Prim.base_ident" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f0d10dcb0..651554486 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -132,6 +132,8 @@ module Prim : val ident : identifier Gram.Entry.e val name : name located Gram.Entry.e val identref : identifier located Gram.Entry.e + val pattern_ident : identifier Gram.Entry.e + val pattern_identref : identifier located Gram.Entry.e val base_ident : identifier Gram.Entry.e val natural : int Gram.Entry.e val bigint : Bigint.bigint Gram.Entry.e |