From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- parsing/cLexer.ml4 | 732 ++++++++++++++++++++++++++++++++++++++++ parsing/cLexer.mli | 32 ++ parsing/compat.ml4 | 332 +++++++++++------- parsing/egramcoq.ml | 743 ++++++++++++++++++++++------------------ parsing/egramcoq.mli | 46 +-- parsing/egramml.ml | 75 +++-- parsing/egramml.mli | 18 +- parsing/g_constr.ml4 | 63 ++-- parsing/g_ltac.ml4 | 260 -------------- parsing/g_prim.ml4 | 6 +- parsing/g_proofs.ml4 | 16 +- parsing/g_tactic.ml4 | 162 +++------ parsing/g_vernac.ml4 | 337 ++++++++++--------- parsing/highparsing.mllib | 2 - parsing/lexer.ml4 | 695 -------------------------------------- parsing/lexer.mli | 38 --- parsing/parsing.mllib | 2 +- parsing/pcoq.ml | 527 +++++++++++++++++++++++++++++ parsing/pcoq.ml4 | 836 ---------------------------------------------- parsing/pcoq.mli | 141 +++----- parsing/tok.ml | 27 +- parsing/tok.mli | 2 +- 22 files changed, 2321 insertions(+), 2771 deletions(-) create mode 100644 parsing/cLexer.ml4 create mode 100644 parsing/cLexer.mli delete mode 100644 parsing/g_ltac.ml4 delete mode 100644 parsing/lexer.ml4 delete mode 100644 parsing/lexer.mli create mode 100644 parsing/pcoq.ml delete mode 100644 parsing/pcoq.ml4 (limited to 'parsing') diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 new file mode 100644 index 00000000..aec6a326 --- /dev/null +++ b/parsing/cLexer.ml4 @@ -0,0 +1,732 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* char -> int = compare end +module CharMap = Map.Make (CharOrd) + +type ttree = { + node : string option; + branch : ttree CharMap.t } + +let empty_ttree = { node = None; branch = CharMap.empty } + +let ttree_add ttree str = + let rec insert tt i = + if i == String.length str then + {node = Some str; branch = tt.branch} + else + let c = str.[i] in + let br = + match try Some (CharMap.find c tt.branch) with Not_found -> None with + | Some tt' -> + CharMap.add c (insert tt' (i + 1)) (CharMap.remove c tt.branch) + | None -> + let tt' = {node = None; branch = CharMap.empty} in + CharMap.add c (insert tt' (i + 1)) tt.branch + in + { node = tt.node; branch = br } + in + insert ttree 0 + +(* Search a string in a dictionary: raises [Not_found] + if the word is not present. *) + +let ttree_find ttree str = + let rec proc_rec tt i = + if i == String.length str then tt + else proc_rec (CharMap.find str.[i] tt.branch) (i+1) + in + proc_rec ttree 0 + +(* Removes a string from a dictionary: returns an equal dictionary + if the word not present. *) +let ttree_remove ttree str = + let rec remove tt i = + if i == String.length str then + {node = None; branch = tt.branch} + else + let c = str.[i] in + let br = + match try Some (CharMap.find c tt.branch) with Not_found -> None with + | Some tt' -> + CharMap.add c (remove tt' (i + 1)) (CharMap.remove c tt.branch) + | None -> tt.branch + in + { node = tt.node; branch = br } + in + remove ttree 0 + +let ttree_elements ttree = + let rec elts tt accu = + let accu = match tt.node with + | None -> accu + | Some s -> CString.Set.add s accu + in + CharMap.fold (fun _ tt accu -> elts tt accu) tt.branch accu + in + elts ttree CString.Set.empty + +(* Errors occurring while lexing (explained as "Lexer error: ...") *) + +module Error = struct + + type t = + | Illegal_character + | Unterminated_comment + | Unterminated_string + | Undefined_token + | Bad_token of string + | UnsupportedUnicode of int + + exception E of t + + let to_string x = + "Syntax Error: Lexer: " ^ + (match x with + | Illegal_character -> "Illegal character" + | Unterminated_comment -> "Unterminated comment" + | Unterminated_string -> "Unterminated string" + | Undefined_token -> "Undefined token" + | Bad_token tok -> Format.sprintf "Bad token %S" tok + | UnsupportedUnicode x -> + Printf.sprintf "Unsupported Unicode character (0x%x)" x) + + (* Require to fix the Camlp4 signature *) + let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x)) + +end +open Error + +let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str) + +let bad_token str = raise (Error.E (Bad_token str)) + +(* Lexer conventions on tokens *) + +type token_kind = + | Utf8Token of (Unicode.status * int) + | AsciiChar + | EmptyStream + +let error_utf8 loc cs = + let bp = Stream.count cs in + Stream.junk cs; (* consume the char to avoid read it and fail again *) + let loc = set_loc_pos loc bp (bp+1) in + err loc Illegal_character + +let utf8_char_size loc cs = function + (* Utf8 leading byte *) + | '\x00'..'\x7F' -> 1 + | '\xC0'..'\xDF' -> 2 + | '\xE0'..'\xEF' -> 3 + | '\xF0'..'\xF7' -> 4 + | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 loc cs + +let njunk n = Util.repeat n Stream.junk + +let check_utf8_trailing_byte loc cs c = + if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 loc cs + +(* Recognize utf8 blocks (of length less than 4 bytes) *) +(* but don't certify full utf8 compliance (e.g. no emptyness check) *) +let lookup_utf8_tail loc c cs = + let c1 = Char.code c in + if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 loc cs + else + let n, unicode = + if Int.equal (c1 land 0x20) 0 then + match Stream.npeek 2 cs with + | [_;c2] -> + check_utf8_trailing_byte loc cs c2; + 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F) + | _ -> error_utf8 loc cs + else if Int.equal (c1 land 0x10) 0 then + match Stream.npeek 3 cs with + | [_;c2;c3] -> + check_utf8_trailing_byte loc cs c2; + check_utf8_trailing_byte loc cs c3; + 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + + (Char.code c3 land 0x3F) + | _ -> error_utf8 loc cs + else match Stream.npeek 4 cs with + | [_;c2;c3;c4] -> + check_utf8_trailing_byte loc cs c2; + check_utf8_trailing_byte loc cs c3; + check_utf8_trailing_byte loc cs c4; + 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + + (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) + | _ -> error_utf8 loc cs + in + Utf8Token (Unicode.classify unicode, n) + +let lookup_utf8 loc cs = + match Stream.peek cs with + | Some ('\x00'..'\x7F') -> AsciiChar + | Some ('\x80'..'\xFF' as c) -> lookup_utf8_tail loc c cs + | None -> EmptyStream + +let unlocated f x = f x + (** FIXME: should we still unloc the exception? *) +(* try f x with Loc.Exc_located (_, exc) -> raise exc *) + +let check_keyword str = + let rec loop_symb = parser + | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str + | [< s >] -> + match unlocated lookup_utf8 Compat.CompatLoc.ghost s with + | Utf8Token (_,n) -> njunk n s; loop_symb s + | AsciiChar -> Stream.junk s; loop_symb s + | EmptyStream -> () + in + loop_symb (Stream.of_string str) + +let check_ident str = + let rec loop_id intail = parser + | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> + loop_id true s + | [< ' ('0'..'9' | ''') when intail; s >] -> + loop_id true s + | [< s >] -> + match unlocated lookup_utf8 Compat.CompatLoc.ghost s with + | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s + | Utf8Token (Unicode.IdentPart, n) when intail -> + njunk n s; + loop_id true s + | EmptyStream -> () + | Utf8Token _ | AsciiChar -> bad_token str + in + loop_id false (Stream.of_string str) + +let is_ident str = + try let _ = check_ident str in true with Error.E _ -> false + +(* Keyword and symbol dictionary *) +let token_tree = ref empty_ttree + +let is_keyword s = + try match (ttree_find !token_tree s).node with None -> false | Some _ -> true + with Not_found -> false + +let add_keyword str = + if not (is_keyword str) then + begin + check_keyword str; + token_tree := ttree_add !token_tree str + end + +let remove_keyword str = + token_tree := ttree_remove !token_tree str + +let keywords () = ttree_elements !token_tree + +(* Freeze and unfreeze the state of the lexer *) +type frozen_t = ttree + +let freeze () = !token_tree +let unfreeze tt = (token_tree := tt) + +(* The string buffering machinery *) + +let buff = ref (String.create 80) + +let store len x = + if len >= String.length !buff then + buff := !buff ^ String.create (String.length !buff); + !buff.[len] <- x; + succ len + +let rec nstore n len cs = + if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len + +let get_buff len = String.sub !buff 0 len + +(* The classical lexer: idents, numbers, quoted strings, comments *) + +let warn_unrecognized_unicode = + CWarnings.create ~name:"unrecognized-unicode" ~category:"parsing" + (fun (u,id) -> + strbrk (Printf.sprintf "Not considering unicode character \"%s\" of unknown \ + lexical status as part of identifier \"%s\"." u id)) + +let rec ident_tail loc len = parser + | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> + ident_tail loc (store len c) s + | [< s >] -> + match lookup_utf8 loc s with + | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> + ident_tail loc (nstore n len s) s + | Utf8Token (Unicode.Unknown, n) -> + let id = get_buff len in + let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in + warn_unrecognized_unicode ~loc:!@loc (u,id); len + | _ -> len + +let rec number len = parser + | [< ' ('0'..'9' as c); s >] -> number (store len c) s + | [< >] -> len + +let warn_comment_terminator_in_string = + CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing" + (fun () -> + (strbrk + "Not interpreting \"*)\" as the end of current \ + non-terminated comment because it occurs in a \ + non-terminated string of the comment.")) + +(* If the string being lexed is in a comment, [comm_level] is Some i with i the + current level of comments nesting. Otherwise, [comm_level] is None. *) +let rec string loc ~comm_level bp len = parser + | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> + if esc then string loc ~comm_level bp (store len '"') s else (loc, len) + | [< ''('; s >] -> + (parser + | [< ''*'; s >] -> + string loc + (Option.map succ comm_level) + bp (store (store len '(') '*') + s + | [< >] -> + string loc comm_level bp (store len '(') s) s + | [< ''*'; s >] -> + (parser + | [< '')'; s >] -> + let () = match comm_level with + | Some 0 -> + warn_comment_terminator_in_string ~loc:!@loc () + | _ -> () + in + let comm_level = Option.map pred comm_level in + string loc comm_level bp (store (store len '*') ')') s + | [< >] -> + string loc comm_level bp (store len '*') s) s + | [< ''\n' as c; s >] ep -> + (* If we are parsing a comment, the string if not part of a token so we + update the first line of the location. Otherwise, we update the last + line. *) + let loc = + if Option.has_some comm_level then bump_loc_line loc ep + else bump_loc_line_last loc ep + in + string loc comm_level bp (store len c) s + | [< 'c; s >] -> string loc comm_level bp (store len c) s + | [< _ = Stream.empty >] ep -> + let loc = set_loc_pos loc bp ep in + err loc Unterminated_string + +(* Hook for exporting comment into xml theory files *) +let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () + +(* To associate locations to a file name *) +let current_file = ref None + +(* Utilities for comments in beautify *) +let comment_begin = ref None +let comm_loc bp = match !comment_begin with +| None -> comment_begin := Some bp +| _ -> () + +let comments = ref [] +let current_comment = Buffer.create 8192 +let between_commands = ref true + +let rec split_comments comacc acc pos = function + [] -> comments := List.rev acc; comacc + | ((b,e),c as com)::coms -> + (* Take all comments that terminates before pos, or begin exactly + at pos (used to print comments attached after an expression) *) + if e<=pos || pos=b then split_comments (c::comacc) acc pos coms + else split_comments comacc (com::acc) pos coms + +let extract_comments pos = split_comments [] [] pos !comments + +(* The state of the lexer visible from outside *) +type lexer_state = int option * string * bool * ((int * int) * string) list * string option + +let init_lexer_state f = (None,"",true,[],f) +let set_lexer_state (o,s,b,c,f) = + comment_begin := o; + Buffer.clear current_comment; Buffer.add_string current_comment s; + between_commands := b; + comments := c; + current_file := f +let release_lexer_state () = + (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) +let drop_lexer_state () = + set_lexer_state (init_lexer_state None) + +let real_push_char c = Buffer.add_char current_comment c + +(* Add a char if it is between two commands, if it is a newline or + if the last char is not a space itself. *) +let push_char c = + if + !between_commands || List.mem c ['\n';'\r'] || + (List.mem c [' ';'\t']&& + (Int.equal (Buffer.length current_comment) 0 || + not (let s = Buffer.contents current_comment in + List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r']))) + then + real_push_char c + +let push_string s = Buffer.add_string current_comment s + +let null_comment s = + let rec null i = + i<0 || (List.mem s.[i] [' ';'\t';'\n';'\r'] && null (i-1)) in + null (String.length s - 1) + +let comment_stop ep = + let current_s = Buffer.contents current_comment in + if !Flags.xml_export && Buffer.length current_comment > 0 && + (!between_commands || not(null_comment current_s)) then + Hook.get f_xml_output_comment current_s; + (if !Flags.beautify && Buffer.length current_comment > 0 && + (!between_commands || not(null_comment current_s)) then + let bp = match !comment_begin with + Some bp -> bp + | None -> + Feedback.msg_notice + (str "No begin location for comment '" + ++ str current_s ++str"' ending at " + ++ int ep); + ep-1 in + comments := ((bp,ep),current_s) :: !comments); + Buffer.clear current_comment; + comment_begin := None; + between_commands := false + +let rec comment loc bp = parser bp2 + | [< ''('; + loc = (parser + | [< ''*'; s >] -> push_string "(*"; comment loc bp s + | [< >] -> push_string "("; loc ); + s >] -> comment loc bp s + | [< ''*'; + loc = parser + | [< '')' >] -> push_string "*)"; loc + | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc + | [< ''"'; s >] -> + let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in + push_string "\""; push_string (get_buff len); push_string "\""; + comment loc bp s + | [< _ = Stream.empty >] ep -> + let loc = set_loc_pos loc bp ep in + err loc Unterminated_comment + | [< ''\n' as z; s >] ep -> real_push_char z; comment (bump_loc_line loc ep) bp s + | [< 'z; s >] -> real_push_char z; comment loc bp s + +(* Parse a special token, using the [token_tree] *) + +(* Peek as much utf-8 lexemes as possible *) +(* and retain the longest valid special token obtained *) +let rec progress_further loc last nj tt cs = + try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) + with Failure _ -> last + +and update_longest_valid_token loc last nj tt cs = + match tt.node with + | Some _ as last' -> + stream_njunk nj cs; + progress_further loc last' 0 tt cs + | None -> + progress_further loc last nj tt cs + +(* nj is the number of char peeked since last valid token *) +(* n the number of char in utf8 block *) +and progress_utf8 loc last nj n c tt cs = + try + let tt = CharMap.find c tt.branch in + if Int.equal n 1 then + update_longest_valid_token loc last (nj+n) tt cs + else + match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with + | l when Int.equal (List.length l) (n - 1) -> + List.iter (check_utf8_trailing_byte loc cs) l; + let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in + update_longest_valid_token loc last (nj+n) tt cs + | _ -> + error_utf8 loc cs + with Not_found -> + last + +and progress_from_byte loc last nj tt cs c = + progress_utf8 loc last nj (utf8_char_size loc cs c) c tt cs + +let find_keyword loc id s = + let tt = ttree_find !token_tree id in + match progress_further loc tt.node 0 tt s with + | None -> raise Not_found + | Some c -> KEYWORD c + +let process_sequence loc bp c cs = + let rec aux n cs = + match Stream.peek cs with + | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs + | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) + in + aux 1 cs + +(* Must be a special token *) +let process_chars loc bp c cs = + let t = progress_from_byte loc None (-1) !token_tree cs c in + let ep = Stream.count cs in + match t with + | Some t -> (KEYWORD t, set_loc_pos loc bp ep) + | None -> + let ep' = bp + utf8_char_size loc cs c in + njunk (ep' - ep) cs; + let loc = set_loc_pos loc bp ep' in + err loc Undefined_token + +(* Parse what follows a dot *) + +let parse_after_dot loc c bp = + parser + | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d); s >] -> + let field = get_buff len in + (try find_keyword loc ("."^field) s with Not_found -> FIELD field) + | [< s >] -> + match lookup_utf8 loc s with + | Utf8Token (Unicode.Letter, n) -> + let len = ident_tail loc (nstore n 0 s) s in + let field = get_buff len in + (try find_keyword loc ("."^field) s with Not_found -> FIELD field) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s) + +(* Parse what follows a question mark *) + +let parse_after_qmark loc bp s = + match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK + | None -> KEYWORD "?" + | _ -> + match lookup_utf8 loc s with + | Utf8Token (Unicode.Letter, _) -> LEFTQMARK + | AsciiChar | Utf8Token _ | EmptyStream -> + fst (process_chars loc bp '?' s) + +let blank_or_eof cs = + match Stream.peek cs with + | None -> true + | Some (' ' | '\t' | '\n' |'\r') -> true + | _ -> false + +(* Parse a token in a char stream *) + +let rec next_token loc = parser bp + | [< ''\n' as c; s >] ep -> + comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s + | [< '' ' | '\t' | '\r' as c; s >] -> + comm_loc bp; push_char c; next_token loc s + | [< ''.' as c; t = parse_after_dot loc c bp; s >] ep -> + comment_stop bp; + (* We enforce that "." should either be part of a larger keyword, + for instance ".(", or followed by a blank or eof. *) + let () = match t with + | KEYWORD ("." | "...") -> + if not (blank_or_eof s) then + err (set_loc_pos loc bp (ep+1)) Undefined_token; + between_commands := true; + | _ -> () + in + (t, set_loc_pos loc bp ep) + | [< ' ('-'|'+'|'*' as c); s >] -> + let t,new_between_commands = + if !between_commands then process_sequence loc bp c s, true + else process_chars loc bp c s,false + in + comment_stop bp; between_commands := new_between_commands; t + | [< ''?'; s >] ep -> + let t = parse_after_qmark loc bp s in + comment_stop bp; (t, set_loc_pos loc bp ep) + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); + len = ident_tail loc (store 0 c); s >] ep -> + let id = get_buff len in + comment_stop bp; + (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> + comment_stop bp; + (INT (get_buff len), set_loc_pos loc bp ep) + | [< ''\"'; (loc,len) = string loc None bp 0 >] ep -> + comment_stop bp; + (STRING (get_buff len), set_loc_pos loc bp ep) + | [< ' ('(' as c); + t = parser + | [< ''*'; s >] -> + comm_loc bp; + push_string "(*"; + let loc = comment loc bp s in next_token loc s + | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> + t + | [< ' ('{' | '}' as c); s >] ep -> + let t,new_between_commands = + if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true + else process_chars loc bp c s, false + in + comment_stop bp; between_commands := new_between_commands; t + | [< s >] -> + match lookup_utf8 loc s with + | Utf8Token (Unicode.Letter, n) -> + let len = ident_tail loc (nstore n 0 s) s in + let id = get_buff len in + let ep = Stream.count s in + comment_stop bp; + (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) -> + let t = process_chars loc bp (Stream.next s) s in + comment_stop bp; t + | EmptyStream -> + comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) + +(* (* Debug: uncomment this for tracing tokens seen by coq...*) +let next_token loc s = + let (t,loc as r) = next_token loc s in + Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t); + r *) + +(* Location table system for creating tables associating a token count + to its location in a char stream (the source) *) + +let locerr () = invalid_arg "Lexer: location function" + +let loct_create () = Hashtbl.create 207 + +let loct_func loct i = + try Hashtbl.find loct i with Not_found -> locerr () + +let loct_add loct i loc = Hashtbl.add loct i loc + +(** {6 The lexer of Coq} *) + +(** Note: removing a token. + We do nothing because [remove_token] is called only when removing a grammar + rule with [Grammar.delete_rule]. The latter command is called only when + unfreezing the state of the grammar entries (see GRAMMAR summary, file + env/metasyntax.ml). Therefore, instead of removing tokens one by one, + we unfreeze the state of the lexer. This restores the behaviour of the + lexer. B.B. *) + +IFDEF CAMLP5 THEN + +type te = Tok.t + +(** Names of tokens, for this lexer, used in Grammar error messages *) + +let token_text = function + | ("", t) -> "'" ^ t ^ "'" + | ("IDENT", "") -> "identifier" + | ("IDENT", t) -> "'" ^ t ^ "'" + | ("INT", "") -> "integer" + | ("INT", s) -> "'" ^ s ^ "'" + | ("STRING", "") -> "string" + | ("EOI", "") -> "end of input" + | (con, "") -> con + | (con, prm) -> con ^ " \"" ^ prm ^ "\"" + +let func cs = + let loct = loct_create () in + let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in + let ts = + Stream.from + (fun i -> + let (tok, loc) = next_token !cur_loc cs in + cur_loc := Compat.after loc; + loct_add loct i loc; Some tok) + in + (ts, loct_func loct) + +let lexer = { + Token.tok_func = func; + Token.tok_using = + (fun pat -> match Tok.of_pattern pat with + | KEYWORD s -> add_keyword s + | _ -> ()); + Token.tok_removing = (fun _ -> ()); + Token.tok_match = Tok.match_pattern; + Token.tok_comm = None; + Token.tok_text = token_text } + +ELSE (* official camlp4 for ocaml >= 3.10 *) + +module M_ = Camlp4.ErrorHandler.Register (Error) + +module Loc = Compat.CompatLoc +module Token = struct + include Tok (* Cf. tok.ml *) + module Loc = Compat.CompatLoc + module Error = Camlp4.Struct.EmptyError + module Filter = struct + type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t + type t = unit + let mk _is_kwd = () + let keyword_added () kwd _ = add_keyword kwd + let keyword_removed () _ = () + let filter () x = x + let define_filter () _ = () + end +end + +let mk () = + let loct = loct_create () in + let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in + let rec self init_loc (* FIXME *) = + parser i + [< (tok, loc) = next_token !cur_loc; s >] -> + cur_loc := Compat.set_loc_file loc !current_file; + loct_add loct i loc; + [< '(tok, loc); self init_loc s >] + | [< >] -> [< >] + in + self + +END + +(** Terminal symbols interpretation *) + +let is_ident_not_keyword s = + is_ident s && not (is_keyword s) + +let is_number s = + let rec aux i = + Int.equal (String.length s) i || + match s.[i] with '0'..'9' -> aux (i+1) | _ -> false + in aux 0 + +let strip s = + let len = + let rec loop i len = + if Int.equal i (String.length s) then len + else if s.[i] == ' ' then loop (i + 1) len + else loop (i + 1) (len + 1) + in + loop 0 0 + in + if len == String.length s then s + else + let s' = String.create len in + let rec loop i i' = + if i == String.length s then s' + else if s.[i] == ' ' then loop (i + 1) i' + else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end + in + loop 0 0 + +let terminal s = + let s = strip s in + let () = match s with "" -> failwith "empty token." | _ -> () in + if is_ident_not_keyword s then IDENT s + else if is_number s then INT s + else KEYWORD s diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli new file mode 100644 index 00000000..e0fdf8cb --- /dev/null +++ b/parsing/cLexer.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val remove_keyword : string -> unit +val is_keyword : string -> bool +val keywords : unit -> CString.Set.t + +val check_ident : string -> unit +val is_ident : string -> bool +val check_keyword : string -> unit + +type frozen_t +val freeze : unit -> frozen_t +val unfreeze : frozen_t -> unit + +val xml_output_comment : (string -> unit) Hook.t + +(* Retrieve the comments lexed at a given location of the stream + currently being processeed *) +val extract_comments : int -> string list + +val terminal : string -> Tok.t + +(** The lexer of Coq: *) + +include Compat.LexerSig diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index d1d55c81..befa0d01 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -10,6 +10,10 @@ (** Locations *) +let file_loc_of_file = function +| None -> "" +| Some f -> f + IFDEF CAMLP5 THEN module CompatLoc = struct @@ -20,23 +24,49 @@ end exception Exc_located = Ploc.Exc -IFDEF CAMLP5_6_00 THEN -let ploc_make_loc fname lnb pos bpep = Ploc.make_loc fname lnb pos bpep "" -let ploc_file_name = Ploc.file_name -ELSE -let ploc_make_loc fname lnb pos bpep = Ploc.make lnb pos bpep -let ploc_file_name _ = "" -END - -let of_coqloc loc = - let (fname, lnb, pos, bp, ep) = Loc.represent loc in - ploc_make_loc fname lnb pos (bp,ep) - let to_coqloc loc = - Loc.create (ploc_file_name loc) (Ploc.line_nb loc) - (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc) + { Loc.fname = Ploc.file_name loc; + Loc.line_nb = Ploc.line_nb loc; + Loc.bol_pos = Ploc.bol_pos loc; + Loc.bp = Ploc.first_pos loc; + Loc.ep = Ploc.last_pos loc; + Loc.line_nb_last = Ploc.line_nb_last loc; + Loc.bol_pos_last = Ploc.bol_pos_last loc; } + +let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) "" + +(* Update a loc without allocating an intermediate pair *) +let set_loc_pos loc bp ep = + Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp) + +(* Increase line number by 1 and update position of beginning of line *) +let bump_loc_line loc bol_pos = + Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos + (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + +(* Same as [bump_loc_line], but for the last line in location *) +(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop, + so we have to resort to a hack merging two locations. *) +(* Warning: [bump_loc_line_last] changes the end position. You may need to call + [set_loc_pos] to fix it. *) +let bump_loc_line_last loc bol_pos = + let loc' = + Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos + (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc) + in + Ploc.encl loc loc' -let make_loc = Ploc.make_unlined +let set_loc_file loc fname = + Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc) + (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + +(* For some reason, the [Ploc.after] function of Camlp5 does not update line + numbers, so we define our own function that does it. *) +let after loc = + let line_nb = Ploc.line_nb_last loc in + let bol_pos = Ploc.bol_pos_last loc in + Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos + (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc) ELSE @@ -44,16 +74,39 @@ module CompatLoc = Camlp4.PreCast.Loc exception Exc_located = CompatLoc.Exc_located -let of_coqloc loc = - let (fname, lnb, pos, bp, ep) = Loc.represent loc in - CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false) - let to_coqloc loc = - Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc) - (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc) + { Loc.fname = CompatLoc.file_name loc; + Loc.line_nb = CompatLoc.start_line loc; + Loc.bol_pos = CompatLoc.start_bol loc; + Loc.bp = CompatLoc.start_off loc; + Loc.ep = CompatLoc.stop_off loc; + Loc.line_nb_last = CompatLoc.stop_line loc; + Loc.bol_pos_last = CompatLoc.stop_bol loc; } + +let make_loc fname line_nb bol_pos start stop = + CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false) + +open CompatLoc + +let set_loc_pos loc bp ep = + of_tuple (file_name loc, start_line loc, start_bol loc, bp, + stop_line loc, stop_bol loc, ep, is_ghost loc) + +let bump_loc_line loc bol_pos = + of_tuple (file_name loc, start_line loc + 1, bol_pos, start_off loc, + start_line loc + 1, bol_pos, stop_off loc, is_ghost loc) -let make_loc (start, stop) = - CompatLoc.of_tuple ("", 0, 0, start, 0, 0, stop, false) +let bump_loc_line_last loc bol_pos = + of_tuple (file_name loc, start_line loc, start_bol loc, start_off loc, + stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc) + +let set_loc_file loc fname = + of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc, + stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) + +let after loc = + of_tuple (file_name loc, stop_line loc, stop_bol loc, stop_off loc, + stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) END @@ -65,6 +118,7 @@ IFDEF CAMLP5 THEN module PcamlSig = struct end module Token = Token +module CompatGramext = struct include Gramext type assoc = g_assoc end ELSE @@ -73,69 +127,11 @@ module Ast = Camlp4.PreCast.Ast module Pcaml = Camlp4.PreCast.Syntax module MLast = Ast module Token = struct exception Error of string end +module CompatGramext = Camlp4.Sig.Grammar END - -(** Grammar auxiliary types *) - -IFDEF CAMLP5 THEN - -let to_coq_assoc = function -| Gramext.RightA -> Extend.RightA -| Gramext.LeftA -> Extend.LeftA -| Gramext.NonA -> Extend.NonA - -let of_coq_assoc = function -| Extend.RightA -> Gramext.RightA -| Extend.LeftA -> Gramext.LeftA -| Extend.NonA -> Gramext.NonA - -let of_coq_position = function -| Extend.First -> Gramext.First -| Extend.Last -> Gramext.Last -| Extend.Before s -> Gramext.Before s -| Extend.After s -> Gramext.After s -| Extend.Level s -> Gramext.Level s - -let to_coq_position = function -| Gramext.First -> Extend.First -| Gramext.Last -> Extend.Last -| Gramext.Before s -> Extend.Before s -| Gramext.After s -> Extend.After s -| Gramext.Level s -> Extend.Level s -| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *) - -ELSE - -let to_coq_assoc = function -| PcamlSig.Grammar.RightA -> Extend.RightA -| PcamlSig.Grammar.LeftA -> Extend.LeftA -| PcamlSig.Grammar.NonA -> Extend.NonA - -let of_coq_assoc = function -| Extend.RightA -> PcamlSig.Grammar.RightA -| Extend.LeftA -> PcamlSig.Grammar.LeftA -| Extend.NonA -> PcamlSig.Grammar.NonA - -let of_coq_position = function -| Extend.First -> PcamlSig.Grammar.First -| Extend.Last -> PcamlSig.Grammar.Last -| Extend.Before s -> PcamlSig.Grammar.Before s -| Extend.After s -> PcamlSig.Grammar.After s -| Extend.Level s -> PcamlSig.Grammar.Level s - -let to_coq_position = function -| PcamlSig.Grammar.First -> Extend.First -| PcamlSig.Grammar.Last -> Extend.Last -| PcamlSig.Grammar.Before s -> Extend.Before s -| PcamlSig.Grammar.After s -> Extend.After s -| PcamlSig.Grammar.Level s -> Extend.Level s - -END - - -(** Signature of Lexer *) +(** Signature of CLexer *) IFDEF CAMLP5 THEN @@ -146,12 +142,23 @@ module type LexerSig = sig exception E of t val to_string : t -> string end + type lexer_state + val init_lexer_state : string option -> lexer_state + val set_lexer_state : lexer_state -> unit + val release_lexer_state : unit -> lexer_state + val drop_lexer_state : unit -> unit end ELSE -module type LexerSig = - Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t +module type LexerSig = sig + include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t + type lexer_state + val init_lexer_state : string option -> lexer_state + val set_lexer_state : lexer_state -> unit + val release_lexer_state : unit -> lexer_state + val drop_lexer_state : unit -> unit +end END @@ -170,10 +177,13 @@ module type GrammarSig = sig string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list + type coq_parsable + val parsable : ?file:string -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> parsable -> 'a + val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit + val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a end @@ -189,16 +199,37 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list + type coq_parsable = parsable * L.lexer_state ref + let parsable ?file c = + let state = ref (L.init_lexer_state file) in + L.set_lexer_state !state; + let a = parsable c in + state := L.release_lexer_state (); + (a,state) let action = Gramext.action let entry_create = Entry.create - let entry_parse e p = - try Entry.parse e p - with Exc_located (loc,e) -> Loc.raise (to_coqloc loc) e -IFDEF CAMLP5_6_02_1 THEN + let entry_parse e (p,state) = + L.set_lexer_state !state; + try + let c = Entry.parse e p in + state := L.release_lexer_state (); + c + with Exc_located (loc,e) -> + L.drop_lexer_state (); + let loc' = Loc.get_loc (Exninfo.info e) in + let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in + Loc.raise loc e + let with_parsable (p,state) f x = + L.set_lexer_state !state; + try + let a = f x in + state := L.release_lexer_state (); + a + with e -> + L.drop_lexer_state (); + raise e + let entry_print ft x = Entry.print ft x -ELSE - let entry_print _ x = Entry.print x -END let srules' = Gramext.srules let parse_tokens_after_filter = Entry.parse_token end @@ -210,12 +241,13 @@ module type GrammarSig = sig with module Loc = CompatLoc and type Token.t = Tok.t type 'a entry = 'a Entry.t type action = Action.t - type parsable - val parsable : char Stream.t -> parsable + type coq_parsable + val parsable : ?file:string -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> parsable -> 'a + val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit + val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b val srules' : production_rule list -> symbol end @@ -225,19 +257,96 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct include Camlp4.Struct.Grammar.Static.Make (L) type 'a entry = 'a Entry.t type action = Action.t - type parsable = char Stream.t - let parsable s = s + type coq_parsable = char Stream.t * L.lexer_state ref + let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state) let action = Action.mk let entry_create = Entry.mk - let entry_parse e s = - try parse e (*FIXME*)CompatLoc.ghost s - with Exc_located (loc,e) -> raise_coq_loc loc e + let entry_parse e (s,state) = + L.set_lexer_state !state; + try + let c = parse e (*FIXME*)CompatLoc.ghost s in + state := L.release_lexer_state (); + c + with Exc_located (loc,e) -> + L.drop_lexer_state (); + raise_coq_loc loc e;; + let with_parsable (p,state) f x = + L.set_lexer_state !state; + try + let a = f x in + state := L.release_lexer_state (); + a + with e -> + L.drop_lexer_state (); + Pervasives.raise e;; let entry_print ft x = Entry.print ft x let srules' = srules (entry_create "dummy") end END +(** Some definitions are grammar-specific in Camlp4, so we use a functor to + depend on it while taking a dummy argument in Camlp5. *) + +module GramextMake (G : GrammarSig) : +sig + val stoken : Tok.t -> G.symbol + val sself : G.symbol + val snext : G.symbol + val slist0 : G.symbol -> G.symbol + val slist0sep : G.symbol * G.symbol -> G.symbol + val slist1 : G.symbol -> G.symbol + val slist1sep : G.symbol * G.symbol -> G.symbol + val sopt : G.symbol -> G.symbol + val snterml : G.internal_entry * string -> G.symbol + val snterm : G.internal_entry -> G.symbol + val snterml_level : G.symbol -> string +end = +struct + +IFDEF CAMLP5 THEN + let stoken tok = + let pattern = match tok with + | Tok.KEYWORD s -> "", s + | Tok.IDENT s -> "IDENT", s + | Tok.PATTERNIDENT s -> "PATTERNIDENT", s + | Tok.FIELD s -> "FIELD", s + | Tok.INT s -> "INT", s + | Tok.STRING s -> "STRING", s + | Tok.LEFTQMARK -> "LEFTQMARK", "" + | Tok.BULLET s -> "BULLET", s + | Tok.EOI -> "EOI", "" + in + Gramext.Stoken pattern +ELSE + module Gramext = G + let stoken tok = match tok with + | Tok.KEYWORD s -> Gramext.Skeyword s + | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok) +END + + IFDEF CAMLP5 THEN + let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) + let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) + ELSE + let slist0sep (x, y) = Gramext.Slist0sep (x, y) + let slist1sep (x, y) = Gramext.Slist1sep (x, y) + END + + let snterml (x, y) = Gramext.Snterml (x, y) + let snterm x = Gramext.Snterm x + let sself = Gramext.Sself + let snext = Gramext.Snext + let slist0 x = Gramext.Slist0 x + let slist1 x = Gramext.Slist1 x + let sopt x = Gramext.Sopt x + + let snterml_level = function + | Gramext.Snterml (_, l) -> l + | _ -> failwith "snterml_level" + +end + (** Misc functional adjustments *) @@ -303,23 +412,10 @@ let make_fun loc cl = END -(** Explicit antiquotation $anti:... $ *) - -IFDEF CAMLP5 THEN -let expl_anti loc e = <:expr< $anti:e$ >> -ELSE -let expl_anti _loc e = e (* FIXME: understand someday if we can do better *) -END - -(** Qualified names in OCaml *) - IFDEF CAMLP5 THEN -let qualified_name loc path name = - let fold dir accu = <:expr< $uid:dir$.$accu$ >> in - List.fold_right fold path <:expr< $lid:name$ >> +let warning_verbose = Gramext.warning_verbose ELSE -let qualified_name loc path name = - let fold dir accu = Ast.IdAcc (loc, Ast.IdUid (loc, dir), accu) in - let path = List.fold_right fold path (Ast.IdLid (loc, name)) in - Ast.ExId (loc, path) +(* TODO: this is a workaround, since there isn't such + [warning_verbose] in new camlp4. *) +let warning_verbose = ref true END diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index b0bbdd81..a292c746 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -6,17 +6,145 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat -open Errors +open CErrors open Util open Pcoq -open Extend open Constrexpr +open Notation open Notation_term +open Extend open Libnames -open Tacexpr open Names -open Egramml + +(**********************************************************************) +(* This determines (depending on the associativity of the current + level and on the expected associativity) if a reference to constr_n is + a reference to the current level (to be translated into "SELF" on the + left border and into "constr LEVEL n" elsewhere), to the level below + (to be translated into "NEXT") or to an below wrt associativity (to be + translated in camlp4 into "constr" without level) or to another level + (to be translated into "constr LEVEL n") + + The boolean is true if the entry was existing _and_ empty; this to + circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the + converse of the extension mechanism *) + +let constr_level = string_of_int + +let default_levels = + [200,Extend.RightA,false; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 10,Extend.RightA,false; + 9,Extend.RightA,false; + 8,Extend.RightA,true; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_pattern_levels = + [200,Extend.RightA,true; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 11,Extend.LeftA,false; + 10,Extend.RightA,false; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_constr_levels = (default_levels, default_pattern_levels) + +(* At a same level, LeftA takes precedence over RightA and NoneA *) +(* In case, several associativity exists for a level, we make two levels, *) +(* first LeftA, then RightA and NoneA together *) + +let admissible_assoc = function + | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false + | Extend.RightA, Some Extend.LeftA -> false + | _ -> true + +let create_assoc = function + | None -> Extend.RightA + | Some a -> a + +let error_level_assoc p current expected = + let open Pp in + let pr_assoc = function + | Extend.LeftA -> str "left" + | Extend.RightA -> str "right" + | Extend.NonA -> str "non" in + errorlabstrm "" + (str "Level " ++ int p ++ str " is already declared " ++ + pr_assoc current ++ str " associative while it is now expected to be " ++ + pr_assoc expected ++ str " associative.") + +let create_pos = function + | None -> Extend.First + | Some lev -> Extend.After (constr_level lev) + +type gram_level = + gram_position option * gram_assoc option * string option * + (** for reinitialization: *) gram_reinit option + +let find_position_gen current ensure assoc lev = + match lev with + | None -> + current, (None, None, None, None) + | Some n -> + let after = ref None in + let init = ref None in + let rec add_level q = function + | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l + | (p,a,reinit)::l when Int.equal p n -> + if reinit then + let a' = create_assoc assoc in + (init := Some (a',create_pos q); (p,a',false)::l) + else if admissible_assoc (a,assoc) then + raise Exit + else + error_level_assoc p a (Option.get assoc) + | l -> after := q; (n,create_assoc assoc,ensure)::l + in + try + let updated = add_level None current in + let assoc = create_assoc assoc in + begin match !init with + | None -> + (* Create the entry *) + updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) + | _ -> + (* The reinit flag has been updated *) + updated, (Some (Extend.Level (constr_level n)), None, None, !init) + end + with + (* Nothing has changed *) + Exit -> + (* Just inherit the existing associativity and name (None) *) + current, (Some (Extend.Level (constr_level n)), None, None, None) + +let rec list_mem_assoc_triple x = function + | [] -> false + | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l + +let register_empty_levels accu forpat levels = + let rec filter accu = function + | [] -> ([], accu) + | n :: rem -> + let rem, accu = filter accu rem in + let (clev, plev) = accu in + let levels = if forpat then plev else clev in + if not (list_mem_assoc_triple n levels) then + let nlev, ans = find_position_gen levels true None (Some n) in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + ans :: rem, nlev + else rem, accu + in + filter accu levels + +let find_position accu forpat assoc level = + let (clev, plev) = accu in + let levels = if forpat then plev else clev in + let nlev, ans = find_position_gen levels false assoc level in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + (ans, nlev) (**************************************************************************) (* @@ -45,6 +173,146 @@ open Egramml (**********************************************************************) (** Declare Notations grammar rules *) +(**********************************************************************) +(* Binding constr entry keys to entries *) + +(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp4_assoc = function + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA + +let assoc_eq al ar = match al, ar with +| NonA, NonA +| RightA, RightA +| LeftA, LeftA -> true +| _, _ -> false + +(* [adjust_level assoc from prod] where [assoc] and [from] are the name + and associativity of the level where to add the rule; the meaning of + the result is + + None = SELF + Some None = NEXT + Some (Some (n,cur)) = constr LEVEL n + s.t. if [cur] is set then [n] is the same as the [from] level *) +let adjust_level assoc from = function +(* Associativity is None means force the level *) + | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) +(* Compute production name on the right side *) + (* If NonA or LeftA on the right-hand side, set to NEXT *) + | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> + Some None + (* If RightA on the right-hand side, set to the explicit (current) level *) + | (NumLevel n,BorderProd (Right,Some RightA)) -> + Some (Some (n,true)) +(* Compute production name on the left side *) + (* If NonA on the left-hand side, adopt the current assoc ?? *) + | (NumLevel n,BorderProd (Left,Some NonA)) -> None + (* If the expected assoc is the current one, set to SELF *) + | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> + None + (* Otherwise, force the level, n or n-1, according to expected assoc *) + | (NumLevel n,BorderProd (Left,Some a)) -> + begin match a with + | LeftA -> Some (Some (n, true)) + | _ -> Some None + end + (* None means NEXT *) + | (NextLevel,_) -> Some None +(* Compute production name elsewhere *) + | (NumLevel n,InternalProd) -> + if from = n + 1 then Some None else Some (Some (n, Int.equal n from)) + +type _ target = +| ForConstr : constr_expr target +| ForPattern : cases_pattern_expr target + +type prod_info = production_level * production_position + +type (_, _) entry = +| TTName : ('self, Name.t Loc.located) entry +| TTReference : ('self, reference) entry +| TTBigint : ('self, Bigint.bigint) entry +| TTBinder : ('self, local_binder list) entry +| TTConstr : prod_info * 'r target -> ('r, 'r) entry +| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry +| TTBinderListT : ('self, local_binder list) entry +| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry + +type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry + +(* This computes the name of the level where to add a new rule *) +let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = + fun forpat level -> match forpat with + | ForConstr -> + if level = 200 then Constr.binder_constr, None + else Constr.operconstr, Some level + | ForPattern -> Constr.pattern, Some level + +let target_entry : type s. s target -> s Gram.entry = function +| ForConstr -> Constr.operconstr +| ForPattern -> Constr.pattern + +let is_self from e = match e with +| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false +| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n +| _ -> false + +let is_binder_level from e = match e with +| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 +| _ -> false + +let make_sep_rules tkl = + let rec mkrule : Tok.t list -> unit rules = function + | [] -> Rules ({ norec_rule = Stop }, ignore) + | tkn :: rem -> + let Rules ({ norec_rule = r }, f) = mkrule rem in + let r = { norec_rule = Next (r, Atoken tkn) } in + Rules (r, fun _ -> f) + in + let r = mkrule (List.rev tkl) in + Arules [r] + +let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat -> + if is_binder_level from p then Aentryl (target_entry forpat, 200) + else if is_self from p then Aself + else + let g = target_entry forpat in + let lev = adjust_level assoc from p in + begin match lev with + | None -> Aentry g + | Some None -> Anext + | Some (Some (lev, cur)) -> Aentryl (g, lev) + end + +let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with +| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat +| TTConstrList (typ', [], forpat) -> + Alist1 (symbol_of_target typ' assoc from forpat) +| TTConstrList (typ', tkl, forpat) -> + Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) +| TTBinderListF [] -> Alist1 (Aentry Constr.binder) +| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) +| TTName -> Aentry Prim.name +| TTBinder -> Aentry Constr.binder +| TTBinderListT -> Aentry Constr.open_binders +| TTBigint -> Aentry Prim.bigint +| TTReference -> Aentry Constr.global + +let interp_entry forpat e = match e with +| ETName -> TTAny TTName +| ETReference -> TTAny TTReference +| ETBigint -> TTAny TTBigint +| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") +| ETBinder false -> TTAny TTBinder +| ETConstr p -> TTAny (TTConstr (p, forpat)) +| ETPattern -> assert false (** not used *) +| ETOther _ -> assert false (** not used *) +| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETBinderList (true, []) -> TTAny TTBinderListT +| ETBinderList (true, _) -> assert false +| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) + let constr_expr_of_name (loc,na) = match na with | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None) | Name id -> CRef (Ident (loc,id), None) @@ -53,333 +321,158 @@ let cases_pattern_expr_of_name (loc,na) = match na with | Anonymous -> CPatAtom (loc,None) | Name id -> CPatAtom (loc,Some (Ident (loc,id))) -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - -let make_constr_action - (f : Loc.t -> constr_notation_substitution -> constr_expr) pil = - let rec make (constrs,constrlists,binders as fullsubst) = function - | [] -> - Gram.action (fun (loc:CompatLoc.t) -> f (!@loc) fullsubst) - | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> - (* parse a non-binding item *) - Gram.action (fun _ -> make fullsubst tl) - | GramConstrNonTerminal (typ, Some _) :: tl -> - (* parse a binding non-terminal *) - (match typ with - | (ETConstr _| ETOther _) -> - Gram.action (fun (v:constr_expr) -> - make (v :: constrs, constrlists, binders) tl) - | ETReference -> - Gram.action (fun (v:reference) -> - make (CRef (v,None) :: constrs, constrlists, binders) tl) - | ETName -> - Gram.action (fun (na:Loc.t * Name.t) -> - make (constr_expr_of_name na :: constrs, constrlists, binders) tl) - | ETBigint -> - Gram.action (fun (v:Bigint.bigint) -> - make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl) - | ETConstrList (_,n) -> - Gram.action (fun (v:constr_expr list) -> - make (constrs, v::constrlists, binders) tl) - | ETBinder _ | ETBinderList (true,_) -> - Gram.action (fun (v:local_binder list) -> - make (constrs, constrlists, v::binders) tl) - | ETBinderList (false,_) -> - Gram.action (fun (v:local_binder list list) -> - make (constrs, constrlists, List.flatten v::binders) tl) - | ETPattern -> - failwith "Unexpected entry of type cases pattern") - | GramConstrListMark (n,b) :: tl -> - (* Rebuild expansions of ConstrList *) - let heads,constrs = List.chop n constrs in - let constrlists = - if b then (heads@List.hd constrlists)::List.tl constrlists - else heads::constrlists - in make (constrs, constrlists, binders) tl - in - make ([],[],[]) (List.rev pil) - -let check_cases_pattern_env loc (env,envlist,hasbinders) = - if hasbinders then Topconstr.error_invalid_pattern_notation loc - else (env,envlist) - -let make_cases_pattern_action - (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = - let rec make (env,envlist,hasbinders as fullenv) = function - | [] -> - Gram.action - (fun (loc:CompatLoc.t) -> - let loc = !@loc in - f loc (check_cases_pattern_env loc fullenv)) - | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> - (* parse a non-binding item *) - Gram.action (fun _ -> make fullenv tl) - | GramConstrNonTerminal (typ, Some _) :: tl -> - (* parse a binding non-terminal *) - (match typ with - | ETConstr _ -> (* pattern non-terminal *) - Gram.action (fun (v:cases_pattern_expr) -> - make (v::env, envlist, hasbinders) tl) - | ETReference -> - Gram.action (fun (v:reference) -> - make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl) - | ETName -> - Gram.action (fun (na:Loc.t * Name.t) -> - make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl) - | ETBigint -> - Gram.action (fun (v:Bigint.bigint) -> - make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl) - | ETConstrList (_,_) -> - Gram.action (fun (vl:cases_pattern_expr list) -> - make (env, vl :: envlist, hasbinders) tl) - | ETBinder _ | ETBinderList (true,_) -> - Gram.action (fun (v:local_binder list) -> - make (env, envlist, hasbinders) tl) - | ETBinderList (false,_) -> - Gram.action (fun (v:local_binder list list) -> - make (env, envlist, true) tl) - | (ETPattern | ETOther _) -> - anomaly (Pp.str "Unexpected entry of type cases pattern or other")) - | GramConstrListMark (n,b) :: tl -> - (* Rebuild expansions of ConstrList *) - let heads,env = List.chop n env in - if b then - make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl - else - make (env,heads::envlist,hasbinders) tl - in - make ([],[],false) (List.rev pil) - -let rec make_constr_prod_item assoc from forpat = function - | GramConstrTerminal tok :: l -> - gram_token_of_token tok :: make_constr_prod_item assoc from forpat l - | GramConstrNonTerminal (nt, ovar) :: l -> - symbol_of_constr_prod_entry_key assoc from forpat nt - :: make_constr_prod_item assoc from forpat l - | GramConstrListMark _ :: l -> - make_constr_prod_item assoc from forpat l - | [] -> - [] - -let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = - let entry = - if forpat then weaken_entry Constr.pattern - else weaken_entry Constr.operconstr in - grammar_extend entry reinit (pos,[(name, p4assoc, [])]) - -let pure_sublevels level symbs = - let filter s = - try - let i = level_of_snterml s in - begin match level with - | Some j when Int.equal i j -> None - | _ -> Some i - end - with Failure _ -> None - in - List.map_filter filter symbs - -let extend_constr (entry,level) (n,assoc) mkact forpat rules = - List.fold_left (fun nb pt -> - let symbs = make_constr_prod_item assoc n forpat pt in - let pure_sublevels = pure_sublevels level symbs in - let needed_levels = register_empty_levels forpat pure_sublevels in - let map_level (pos, ass1, name, ass2) = - (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in - let needed_levels = List.map map_level needed_levels in - let pos,p4assoc,name,reinit = find_position forpat assoc level in - let nb_decls = List.length needed_levels + 1 in - List.iter (prepare_empty_levels forpat) needed_levels; - grammar_extend entry reinit (Option.map of_coq_position pos, - [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]); - nb_decls) 0 rules - -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - -let extend_constr_constr_notation ng = - let level = ng.notgram_level in - let mkact loc env = CNotation (loc, ng.notgram_notation, env) in - let e = interp_constr_entry_key false (ETConstr (level, ())) in - let ext = (ETConstr (level, ()), ng.notgram_assoc) in - extend_constr e ext (make_constr_action mkact) false ng.notgram_prods - -let extend_constr_pat_notation ng = - let level = ng.notgram_level in - let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in - let e = interp_constr_entry_key true (ETConstr (level, ())) in - let ext = ETConstr (level, ()), ng.notgram_assoc in - extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods - -let extend_constr_notation ng = - (* Add the notation in constr *) - let nb = extend_constr_constr_notation ng in - (* Add the notation in cases_pattern *) - let nb' = extend_constr_pat_notation ng in - nb + nb' - -(**********************************************************************) -(** Grammar declaration for Tactic Notation (Coq level) *) - -let get_tactic_entry n = - if Int.equal n 0 then - weaken_entry Tactic.simple_tactic, None - else if Int.equal n 5 then - weaken_entry Tactic.binder_tactic, None - else if 1<=n && n<5 then - weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) - else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") - -(**********************************************************************) -(** State of the grammar extensions *) - -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : grammar_prod_item list; +type 'r env = { + constrs : 'r list; + constrlists : 'r list list; + binders : (local_binder list * bool) list; } -type all_grammar_command = - | Notation of Notation.level * notation_grammar - | TacticGrammar of KerName.t * tactic_grammar - | MLTacticGrammar of ml_tactic_name * grammar_prod_item list list - -(** ML Tactic grammar extensions *) - -let add_ml_tactic_entry name prods = - let entry = weaken_entry Tactic.simple_tactic in - let mkact loc l : raw_tactic_expr = Tacexpr.TacML (loc, name, List.map snd l) in - let rules = List.map (make_rule mkact) prods in - synchronize_level_positions (); - grammar_extend entry None (None ,[(None, None, List.rev rules)]); - 1 - -(* Declaration of the tactic grammar rule *) - -let head_is_ident tg = match tg.tacgram_prods with -| GramTerminal _::_ -> true -| _ -> false - -(** Tactic grammar extensions *) - -let add_tactic_entry kn tg = - let entry, pos = get_tactic_entry tg.tacgram_level in - let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in - let () = - 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 - synchronize_level_positions (); - grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]); - 1 - -let (grammar_state : (int * all_grammar_command) list ref) = ref [] - -let extend_grammar gram = - let nb = match gram with - | Notation (_,a) -> extend_constr_notation a - | TacticGrammar (kn, g) -> add_tactic_entry kn g - | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr +let push_constr subst v = { subst with constrs = v :: subst.constrs } + +let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> +match e with +| TTConstr _ -> push_constr subst v +| TTName -> + begin match forpat with + | ForConstr -> push_constr subst (constr_expr_of_name v) + | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) + end +| TTBinder -> { subst with binders = (v, true) :: subst.binders } +| TTBinderListT -> { subst with binders = (v, true) :: subst.binders } +| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } +| TTBigint -> + begin match forpat with + | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v)) + | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v)) + end +| TTReference -> + begin match forpat with + | ForConstr -> push_constr subst (CRef (v, None)) + | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v)) + end +| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } + +type (_, _) ty_symbol = +| TyTerm : Tok.t -> ('s, string) ty_symbol +| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol + +type ('self, _, 'r) ty_rule = +| TyStop : ('self, 'r, 'r) ty_rule +| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule +| TyMark : int * bool * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule + +type 'r gen_eval = Loc.t -> 'r env -> 'r + +let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function +| TyStop -> + fun f env loc -> f loc env +| TyNext (rem, TyTerm _) -> + fun f env _ -> ty_eval rem f env +| TyNext (rem, TyNonTerm (_, _, _, false)) -> + fun f env _ -> ty_eval rem f env +| TyNext (rem, TyNonTerm (forpat, e, _, true)) -> + fun f env v -> + ty_eval rem f (push_item forpat e env v) +| TyMark (n, b, rem) -> + fun f env -> + let heads, constrs = List.chop n env.constrs in + let constrlists = + if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists + else heads :: env.constrlists + in + ty_eval rem f { env with constrs; constrlists; } + +let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function +| TyStop -> Stop +| TyMark (_, _, r) -> ty_erase r +| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) +| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) + +type ('self, 'r) any_ty_rule = +| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule + +let make_ty_rule assoc from forpat prods = + let rec make_ty_rule = function + | [] -> AnyTyRule TyStop + | GramConstrTerminal tok :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyNext (r, TyTerm tok)) + | GramConstrNonTerminal (e, var) :: rem -> + let AnyTyRule r = make_ty_rule rem in + let TTAny e = interp_entry forpat e in + let s = symbol_of_entry assoc from e in + let bind = match var with None -> false | Some _ -> true in + AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind))) + | GramConstrListMark (n, b) :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyMark (n, b, r)) in - grammar_state := (nb,gram) :: !grammar_state + make_ty_rule (List.rev prods) -let extend_constr_grammar pr ntn = - extend_grammar (Notation (pr, ntn)) +let target_to_bool : type r. r target -> bool = function +| ForConstr -> false +| ForPattern -> true -let extend_tactic_grammar kn ntn = - extend_grammar (TacticGrammar (kn, ntn)) +let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = + let empty = (pos, [(name, p4assoc, [])]) in + if forpat then ExtendRule (Constr.pattern, reinit, empty) + else ExtendRule (Constr.operconstr, reinit, empty) + +let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with +| Stop -> [] +| Next (rem, Aentryl (_, i)) -> + let rem = pure_sublevels level rem in + begin match level with + | Some j when Int.equal i j -> rem + | _ -> i :: rem + end +| Next (rem, _) -> pure_sublevels level rem + +let make_act : type r. r target -> _ -> r gen_eval = function +| ForConstr -> fun notation loc env -> + let env = (env.constrs, env.constrlists, List.map fst env.binders) in + CNotation (loc, notation , env) +| ForPattern -> fun notation loc env -> + let invalid = List.exists (fun (_, b) -> not b) env.binders in + let () = if invalid then Topconstr.error_invalid_pattern_notation loc in + let env = (env.constrs, env.constrlists) in + CPatNotation (loc, notation, env, []) + +let extend_constr state forpat ng = + let n = ng.notgram_level in + let assoc = ng.notgram_assoc in + let (entry, level) = interp_constr_entry_key forpat n in + let fold (accu, state) pt = + let AnyTyRule r = make_ty_rule assoc n forpat pt in + let symbs = ty_erase r in + let pure_sublevels = pure_sublevels level symbs in + let isforpat = target_to_bool forpat in + let needed_levels, state = register_empty_levels state isforpat pure_sublevels in + let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in + let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in + let empty = { constrs = []; constrlists = []; binders = [] } in + let act = ty_eval r (make_act forpat ng.notgram_notation) empty in + let rule = (name, p4assoc, [Rule (symbs, act)]) in + let r = ExtendRule (entry, reinit, (pos, [rule])) in + (accu @ empty_rules @ [r], state) + in + List.fold_left fold ([], state) ng.notgram_prods -let extend_ml_tactic_grammar name ntn = - extend_grammar (MLTacticGrammar (name, ntn)) +let constr_levels = GramState.field () -let recover_constr_grammar ntn prec = - let filter = function - | _, Notation (prec', ng) when - Notation.level_eq prec prec' && - String.equal ntn ng.notgram_notation -> Some ng - | _ -> None +let extend_constr_notation (_, ng) state = + let levels = match GramState.get state constr_levels with + | None -> default_constr_levels + | Some lev -> lev in - match List.map_filter filter !grammar_state with - | [x] -> x - | _ -> assert false - -(* Summary functions: the state of the lexer is included in that of the parser. - Because the grammar affects the set of keywords when adding or removing - grammar rules. *) -type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t - -let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ()) - -(* We compare the current state of the grammar and the state to unfreeze, - by computing the longest common suffixes *) -let factorize_grams l1 l2 = - if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 - -let number_of_entries gcl = - List.fold_left (fun n (p,_) -> n + p) 0 gcl - -let unfreeze (grams, lex) = - let (undo, redo, common) = factorize_grams !grammar_state grams in - let n = number_of_entries undo in - remove_grammars n; - remove_levels n; - grammar_state := common; - Lexer.unfreeze lex; - List.iter extend_grammar (List.rev_map snd redo) - -(** No need to provide an init function : the grammar state is - statically available, and already empty initially, while - the lexer state should not be resetted, since it contains - keywords declared in g_*.ml4 *) - -let _ = - Summary.declare_summary "GRAMMAR_LEXER" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = Summary.nop } - -let with_grammar_rule_protection f x = - let fs = freeze false in - try let a = f x in unfreeze fs; a - with reraise -> - let reraise = Errors.push reraise in - let () = unfreeze fs in - iraise reraise - -(**********************************************************************) -(** Ltac quotations *) + (* Add the notation in constr *) + let (r, levels) = extend_constr levels ForConstr ng in + (* Add the notation in cases_pattern *) + let (r', levels) = extend_constr levels ForPattern ng in + let state = GramState.set state constr_levels levels in + (r @ r', state) -let ltac_quotations = ref String.Set.empty +let constr_grammar : (Notation.level * notation_grammar) grammar_command = + create_grammar_command "Notation" extend_constr_notation -let create_ltac_quotation name cast wit e = - let () = - if String.Set.mem name !ltac_quotations then - failwith ("Ltac quotation " ^ name ^ " already registered") - in - let () = ltac_quotations := String.Set.add name !ltac_quotations in -(* let level = Some "1" in *) - let level = None in - let assoc = Some (of_coq_assoc Extend.RightA) in - let rule = [ - gram_token_of_string name; - gram_token_of_string ":"; - symbol_of_prod_entry_key (Agram (Gram.Entry.name e)); - ] in - let action v _ _ loc = - let loc = !@loc in - let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in - TacArg (loc, arg) - in - let gram = (level, assoc, [rule, Gram.action action]) in - maybe_uncurry (Gram.extend Tactic.tactic_expr) (None, [gram]) +let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 964bd541..6dda3817 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -19,51 +19,7 @@ open Egramml (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) -(** For constr notations *) - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : grammar_prod_item list; -} - (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> notation_grammar -> unit +val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit (** Add a term notation rule to the parsing system. *) - -val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit -(** Add a tactic notation rule to the parsing system. This produces a TacAlias - tactic with the provided kernel name. *) - -val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit -(** Add a ML tactic notation rule to the parsing system. This produces a - TacML tactic with the provided string as name. *) - -val recover_constr_grammar : notation -> Notation.level -> notation_grammar -(** For a declared grammar, returns the rule + the ordered entry types - of variables in the rule (for use in the interpretation) *) - -val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b - -(** {5 Adding tactic quotations} *) - -val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) -> - ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit -(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is, - Ltac grammar now accepts arguments of the form ["name" ":" ], and - generates a generic argument using [f] on the entry parsed by [e]. *) diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 3896970c..97a3e89a 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -7,41 +7,60 @@ (************************************************************************) open Util -open Compat -open Names +open Extend open Pcoq open Genarg open Vernacexpr -(** Making generic actions in type generic_argument *) - -let make_generic_action - (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil = - let rec make env = function - | [] -> - Gram.action (fun loc -> f (to_coqloc loc) env) - | None :: tl -> (* parse a non-binding item *) - Gram.action (fun _ -> make env tl) - | Some (p, t) :: tl -> (* non-terminal *) - Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in - make [] (List.rev pil) - (** Grammar extensions declared at ML level *) -type grammar_prod_item = +type 's grammar_prod_item = | GramTerminal of string - | GramNonTerminal of - Loc.t * argument_type * prod_entry_key * Id.t option + | GramNonTerminal : + Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item + +type 'a ty_arg = ('a -> raw_generic_argument) + +type ('self, _, 'r) ty_rule = +| TyStop : ('self, 'r, 'r) ty_rule +| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option -> + ('self, 'b -> 'a, 'r) ty_rule + +type ('self, 'r) any_ty_rule = +| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule + +let rec ty_rule_of_gram = function +| [] -> AnyTyRule TyStop +| GramTerminal s :: rem -> + let AnyTyRule rem = ty_rule_of_gram rem in + let tok = Atoken (CLexer.terminal s) in + let r = TyNext (rem, tok, None) in + AnyTyRule r +| GramNonTerminal (_, t, tok) :: rem -> + let AnyTyRule rem = ty_rule_of_gram rem in + let inj = Some (fun obj -> Genarg.in_gen t obj) in + let r = TyNext (rem, tok, inj) in + AnyTyRule r + +let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function +| TyStop -> Extend.Stop +| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok) + +type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r -let make_prod_item = function - | GramTerminal s -> (gram_token_of_string s, None) - | GramNonTerminal (_,t,e,po) -> - (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po) +let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function +| TyStop -> fun f loc -> f loc [] +| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f +| TyNext (rem, tok, Some inj) -> fun f x -> + let f loc args = f loc (inj x :: args) in + ty_eval rem f -let make_rule mkact pt = - let (symbs,ntl) = List.split (List.map make_prod_item pt) in - let act = make_generic_action mkact ntl in - (symbs, act) +let make_rule f prod = + let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in + let symb = ty_erase ty_rule in + let f loc l = f loc (List.rev l) in + let act = ty_eval ty_rule f in + Extend.Rule (symb, act) (** Vernac grammar extensions *) @@ -58,6 +77,6 @@ let get_extend_vernac_rule (s, i) = let extend_vernac_command_grammar s nt gl = let nt = Option.default Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; - let mkact loc l = VernacExtend (s,List.map snd l) in + let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in - maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)]) + grammar_extend nt None (None, [None, None, rules]) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index f71c368a..1ad94720 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -6,24 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Vernacexpr + (** Mapping of grammar productions to camlp4 actions. *) (** This is the part specific to vernac extensions. For the Coq-level Notation and Tactic Notation, see Egramcoq. *) -type grammar_prod_item = +type 's grammar_prod_item = | GramTerminal of string - | GramNonTerminal of Loc.t * Genarg.argument_type * - Pcoq.prod_entry_key * Names.Id.t option + | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type * + ('s, 'a) Extend.symbol -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> - grammar_prod_item list -> unit + Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> + vernac_expr grammar_prod_item list -> unit -val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list +val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list (** Utility function reused in Egramcoq : *) val make_rule : - (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) -> - grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action + (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> + 'a grammar_prod_item list -> 'a Extend.production_rule diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5edb7b80..7f3a3d10 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -29,7 +29,7 @@ let constr_kw = "Prop"; "Set"; "Type"; ".("; "_"; ".."; "`{"; "`("; "{|"; "|}" ] -let _ = List.iter Lexer.add_keyword constr_kw +let _ = List.iter CLexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c @@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> - Errors.user_err_loc + CErrors.user_err_loc (aloc,"Constr:mk_cofixb", Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with @@ -127,15 +127,12 @@ let name_colon = let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr sort global + GLOBAL: binder_constr lconstr constr operconstr universe_level sort global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: - [ [ id = Prim.ident -> id - - (* This is used in quotations and Syntax *) - | id = METAIDENT -> Id.of_string id ] ] + [ [ id = Prim.ident -> id ] ] ; Prim.name: [ [ "_" -> (!@loc, Anonymous) ] ] @@ -218,16 +215,13 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> + | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; record_declaration: - [ [ fs = record_fields -> CRecord (!@loc, None, fs) -(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) -(* CRecord (!@loc, Some c, fs) *) - ] ] + [ [ fs = record_fields -> CRecord (!@loc, fs) ] ] ; record_fields: @@ -267,14 +261,14 @@ GEXTEND Gram CLetTuple (!@loc,lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)]) + CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)]) + CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)]) + CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -304,10 +298,10 @@ GEXTEND Gram | -> [] ] ] ; instance: - [ [ "@{"; l = LIST1 level; "}" -> Some l + [ [ "@{"; l = LIST1 universe_level; "}" -> Some l | -> None ] ] ; - level: + universe_level: [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None @@ -338,11 +332,10 @@ GEXTEND Gram br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ] ; case_item: - [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] - ; - pred_pattern: - [ [ ona = OPT ["as"; id=name -> id]; - ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ] + [ [ c=operconstr LEVEL "100"; + ona = OPT ["as"; id=name -> id]; + ty = OPT ["in"; t=pattern -> t] -> + (c,ona,ty) ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] @@ -386,14 +379,17 @@ GEXTEND Gram | "10" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with - | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp) + | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp) + | CPatCstr (_, r, None, l2) -> CErrors.user_err_loc + (cases_pattern_expr_loc p, "compound_pattern", + Pp.str "Nested applications not supported.") | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) - | _ -> Errors.user_err_loc + | _ -> CErrors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Such pattern cannot have arguments.")) - |"@"; r = Prim.reference; lp = LIST1 NEXT -> - CPatCstr (!@loc, r, lp, []) ] + |"@"; r = Prim.reference; lp = LIST0 NEXT -> + CPatCstr (!@loc, r, Some lp, []) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ] | "0" @@ -405,6 +401,14 @@ GEXTEND Gram CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> CPatNotation(!@loc,"( _ )",([p],[]),[]) | _ -> p) + | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> + let p = + match p with + CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> + CPatNotation(!@loc,"( _ )",([p],[]),[]) + | _ -> p + in + CPatCast (!@loc, p, ty) | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (!@loc, String s) ] ] ; @@ -480,6 +484,13 @@ GEXTEND Gram List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + | "'"; p = pattern LEVEL "0" -> + let (p, ty) = + match p with + | CPatCast (_, p, ty) -> (p, Some ty) + | _ -> (p, None) + in + [LocalPattern (!@loc, p, ty)] ] ] ; typeclass_constraint: diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 deleted file mode 100644 index 959b0e89..00000000 --- a/parsing/g_ltac.ml4 +++ /dev/null @@ -1,260 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* a - | e -> Tacexp (e:raw_tactic_expr) - -let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () -let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat - -(* Tactics grammar rules *) - -GEXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - constr_may_eval constr_eval; - - tactic_then_last: - [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> - Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) - | -> [||] - ] ] - ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last) - | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l)) - | ".."; l = tactic_then_last -> ([], Some (TacId [], l)) - | ta = tactic_expr -> ([ta], None) - | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last) - | -> ([TacId []], None) - ] ] - ; - tactic_then_locality: (* [true] for the local variant [TacThens] and [false] - for [TacExtend] *) - [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] - ; - tactic_expr: - [ "5" RIGHTA - [ te = binder_tactic -> te ] - | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) - | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> - match l , tail with - | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) - | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) - | false , None -> TacThen (ta0,TacDispatch first) - | true , None -> TacThens (ta0,first) ] - | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> TacTry ta - | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) - | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta) - | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta - | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "once"; ta = tactic_expr -> TacOnce ta - | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta - | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta -(*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) - | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (tc,Some s) ] -(*End of To do*) - | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] - | "1" RIGHTA - [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchGoal (b,false,mrl) - | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; - mrl = match_context_list; "end" -> - TacMatchGoal (b,true,mrl) - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> - TacMatch (b,c,mrl) - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacFirst l - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacSolve l - | IDENT "idtac"; l = LIST0 message_token -> TacId l - | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; - l = LIST0 message_token -> TacFail (g,n,l) - | st = simple_tactic -> st - | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(!@loc,ConstrMayEval(ConstrTerm c)) - | a = tactic_top_or_arg -> TacArg(!@loc,a) - | r = reference; la = LIST0 tactic_arg -> - TacArg(!@loc,TacCall (!@loc,r,la)) ] - | "0" - [ "("; a = tactic_expr; ")" -> a - | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> - begin match tail with - | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) - | None -> TacDispatch tf - end - | a = tactic_atom -> TacArg (!@loc,a) ] ] - ; - failkw: - [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] - ; - (* binder_tactic: level 5 of tactic_expr *) - binder_tactic: - [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> - TacFun (it,body) - | "let"; isrec = [IDENT "rec" -> true | -> false]; - llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) - | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] - ; - (* Tactic arguments *) - tactic_arg: - [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | "ltac:"; n = natural -> TacGeneric (genarg_of_int n) - | a = tactic_top_or_arg -> a - | r = reference -> Reference r - | c = Constr.constr -> ConstrMayEval (ConstrTerm c) - (* Unambigous entries: tolerated w/o "ltac:" modifier *) - | id = METAIDENT -> MetaIdArg (!@loc,true,id) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] - ; - (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_top_or_arg: - [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacGeneric (genarg_of_ipattern ipat) - | c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l - | IDENT "type_term"; c=uconstr -> TacPretype c - | IDENT "numgoals" -> TacNumgoals ] ] - ; - (* If a qualid is given, use its short name. TODO: have the shortest - non ambiguous name where dots are replaced by "_"? Probably too - verbose most of the time. *) - fresh_id: - [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ] - ; - constr_eval: - [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrEval (rtc,c) - | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrContext (id,c) - | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrTypeOf c ] ] - ; - constr_may_eval: (* For extensions *) - [ [ c = constr_eval -> c - | c = Constr.constr -> ConstrTerm c ] ] - ; - tactic_atom: - [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id) - | n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (!@loc,r,[]) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] - ; - match_key: - [ [ "match" -> Once - | "lazymatch" -> Select - | "multimatch" -> General ] ] - ; - input_fun: - [ [ "_" -> None - | l = ident -> Some l ] ] - ; - let_clause: - [ [ id = identref; ":="; te = tactic_expr -> - (id, arg_of_expr te) - | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (id, arg_of_expr (TacFun(args,te))) ] ] - ; - match_pattern: - [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - msg_warning (strbrk "appcontext is deprecated"); - Subterm (true,oid, pc) - | pc = Constr.lconstr_pattern -> Term pc ] ] - ; - match_hyps: - [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) - | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) - | na = name; ":="; mpv = match_pattern -> - let t, ty = - match mpv with - | Term t -> (match t with - | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) - | _ -> mpv, None) - | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty) - ] ] - ; - match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "_"; "=>"; te = tactic_expr -> All te ] ] - ; - match_context_list: - [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] - ; - match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) - | "_"; "=>"; te = tactic_expr -> All te ] ] - ; - match_list: - [ [ mrl = LIST1 match_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] - ; - message_token: - [ [ id = identref -> MsgIdent id - | s = STRING -> MsgString s - | n = integer -> MsgInt n ] ] - ; - - ltac_def_kind: - [ [ ":=" -> false - | "::=" -> true ] ] - ; - - (* Definitions for tactics *) - tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, body) ] ] - ; - tactic: - [ [ tac = tactic_expr -> tac ] ] - ; - END diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 5297c163..b90e06cd 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -15,7 +15,7 @@ open Pcoq open Pcoq.Prim let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] -let _ = List.iter Lexer.add_keyword prim_kw +let _ = List.iter CLexer.add_keyword prim_kw let local_make_qualid l id = make_qualid (DirPath.make l) id @@ -28,7 +28,7 @@ let my_int_of_string loc s = if n > 1024 * 2048 then raise Exit; n with Failure _ | Exit -> - Errors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") + CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") GEXTEND Gram GLOBAL: @@ -93,7 +93,7 @@ GEXTEND Gram ; ne_string: [ [ s = STRING -> - if s="" then Errors.user_err_loc(!@loc, "", Pp.str"Empty string."); s + if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s ] ] ; ne_lstring: diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 422384f3..70c5d5d8 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -88,7 +88,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) @@ -103,10 +103,9 @@ GEXTEND Gram (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ]; - dbnames = opt_hintbases -> + info = hint_info; dbnames = opt_hintbases -> VernacHints (false,dbnames, - HintsResolve (List.map (fun x -> (pri, true, x)) lc)) + HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] @@ -116,9 +115,8 @@ GEXTEND Gram | c = constr -> HintsConstr c ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ] -> - HintsResolve (List.map (fun x -> (pri, true, x)) lc) + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> + HintsResolve (List.map (fun x -> (info, true, x)) lc) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) @@ -134,6 +132,8 @@ GEXTEND Gram | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] ; mode: - [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ] + [ [ l = LIST1 [ "+" -> ModeInput + | "!" -> ModeNoHeadEvar + | "-" -> ModeOutput ] -> l ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 2a00a176..3152afb2 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Tacexpr open Genredexpr @@ -22,10 +22,10 @@ open Decl_kinds open Pcoq -let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta] +let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter Lexer.add_keyword tactic_kw +let _ = List.iter CLexer.add_keyword tactic_kw let err () = raise Stream.Failure @@ -111,8 +111,8 @@ let check_for_coloneq = | KEYWORD "(" -> skip_binders 2 | _ -> err ()) -let lookup_at_as_coma = - Gram.Entry.of_parser "lookup_at_as_coma" +let lookup_at_as_comma = + Gram.Entry.of_parser "lookup_at_as_comma" (fun strm -> match get_tok (stream_nth 0 strm) with | KEYWORD (","|"at"|"as") -> () @@ -141,11 +141,11 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = (id,CProdN(loc,bl,ty)) (* Functions overloaded by quotifier *) -let induction_arg_of_constr (c,lbind as clbind) = match lbind with +let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | NoBindings -> begin try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c)) - with e when Errors.noncritical e -> ElimOnConstr clbind + with e when CErrors.noncritical e -> ElimOnConstr clbind end | _ -> ElimOnConstr clbind @@ -211,12 +211,16 @@ let merge_occurrences loc cl = function in (Some p, ans) +let warn_deprecated_eqn_syntax = + CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated" + (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg)) + (* Auxiliary grammar rules *) GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis bindings red_expr int_or_var open_constr uconstr - simple_intropattern clause_dft_concl hypident; + simple_intropattern in_clause clause_dft_concl hypident destruction_arg; int_or_var: [ [ n = integer -> ArgArg n @@ -231,16 +235,16 @@ GEXTEND Gram [ [ id = identref -> id ] ] ; open_constr: - [ [ c = constr -> ((),c) ] ] + [ [ c = constr -> c ] ] ; uconstr: [ [ c = constr -> c ] ] ; - induction_arg: + destruction_arg: [ [ n = natural -> (None,ElimOnAnonHyp n) | test_lpar_id_rpar; c = constr_with_bindings -> - (Some false,induction_arg_of_constr c) - | c = constr_with_bindings -> (None,induction_arg_of_constr c) + (Some false,destruction_arg_of_constr c) + | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c ] ] ; constr_with_bindings_arg: @@ -281,19 +285,23 @@ GEXTEND Gram intropatterns: [ [ l = LIST0 nonsimple_intropattern -> l ]] ; + ne_intropatterns: + [ [ l = LIST1 nonsimple_intropattern -> l ]] + ; or_and_intropattern: - [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> tc - | "()" -> [[]] - | "("; si = simple_intropattern; ")" -> [[si]] + [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc + | "()" -> IntroAndPattern [] + | "("; si = simple_intropattern; ")" -> IntroAndPattern [si] | "("; si = simple_intropattern; ","; - tc = LIST1 simple_intropattern SEP "," ; ")" -> [si::tc] + tc = LIST1 simple_intropattern SEP "," ; ")" -> + IntroAndPattern (si::tc) | "("; si = simple_intropattern; "&"; tc = LIST1 simple_intropattern SEP "&" ; ")" -> (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function - | ([]|[_]|[_;_]) as l -> [l] - | t::q -> [[t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (pairify q)))]] - in pairify (si::tc) ] ] + | ([]|[_]|[_;_]) as l -> l + | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] + in IntroAndPattern (pairify (si::tc)) ] ] ; equality_intropattern: [ [ "->" -> IntroRewrite true @@ -334,20 +342,20 @@ GEXTEND Gram ExplicitBindings bl | bl = LIST1 constr -> ImplicitBindings bl ] ] ; - opt_bindings: - [ [ bl = LIST1 bindings SEP "," -> bl | -> [NoBindings] ] ] - ; constr_with_bindings: [ [ c = constr; l = with_bindings -> (c, l) ] ] ; with_bindings: [ [ "with"; bl = bindings -> bl | -> NoBindings ] ] ; - red_flag: - [ [ IDENT "beta" -> FBeta - | IDENT "iota" -> FIota - | IDENT "zeta" -> FZeta - | IDENT "delta"; d = delta_flag -> d + red_flags: + [ [ IDENT "beta" -> [FBeta] + | IDENT "iota" -> [FMatch;FFix;FCofix] + | IDENT "match" -> [FMatch] + | IDENT "fix" -> [FFix] + | IDENT "cofix" -> [FCofix] + | IDENT "zeta" -> [FZeta] + | IDENT "delta"; d = delta_flag -> [d] ] ] ; delta_flag: @@ -357,7 +365,7 @@ GEXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flag -> Redops.make_red_flag s + [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s) | d = delta_flag -> all_with d ] ] ; @@ -450,15 +458,6 @@ GEXTEND Gram [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ] ; - hintbases: - [ [ "with"; "*" -> None - | "with"; l = LIST1 [ x = IDENT -> x] -> Some l - | -> Some [] ] ] - ; - auto_using: - [ [ "using"; l = LIST1 constr SEP "," -> l - | -> [] ] ] - ; eliminator: [ [ "using"; el = constr_with_bindings -> el ] ] ; @@ -477,42 +476,35 @@ GEXTEND Gram eqn_ipat: [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat) | IDENT "_eqn"; ":"; pat = naming_intropattern -> - let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in - msg_warning (strbrk msg); Some (!@loc, pat) + let loc = !@loc in + warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat) | IDENT "_eqn" -> - let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in - msg_warning (strbrk msg); Some (!@loc, IntroAnonymous) + let loc = !@loc in + warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous) | -> None ] ] ; as_name: [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac - | -> TacId [] ] ] - ; - opt_by_tactic: [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac | -> None ] ] ; - rename : - [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] - ; rewriter : - [ [ "!"; c = constr_with_bindings -> (RepeatPlus,(None,c)) + [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings -> (Precisely n,(None,c)) + | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c) | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c) | n = natural; c = constr_with_bindings_arg -> (Precisely n,c) - | c = constr_with_bindings -> (Precisely 1, (None,c)) + | c = constr_with_bindings_arg -> (Precisely 1, c) ] ] ; oriented_rewriter : [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; induction_clause: - [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat; cl = opt_clause - -> (c,(eq,pat),cl) ] ] + [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; + cl = opt_clause -> (c,(eq,pat),cl) ] ] ; induction_clause_list: [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator; @@ -523,23 +515,15 @@ GEXTEND Gram | _,_,Some _ -> err () | _,_,None -> (ic,el) ]] ; - move_location: - [ [ IDENT "after"; id = id_or_meta -> MoveAfter id - | IDENT "before"; id = id_or_meta -> MoveBefore id - | "at"; IDENT "top" -> MoveFirst - | "at"; IDENT "bottom" -> MoveLast ] ] - ; simple_tactic: [ [ (* Basic tactics *) - IDENT "intros"; pl = intropatterns -> TacAtom (!@loc, TacIntroPattern pl) - | IDENT "intro"; id = ident; hto = move_location -> - TacAtom (!@loc, TacIntroMove (Some id, hto)) - | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto)) - | IDENT "intro"; id = ident -> TacAtom (!@loc, TacIntroMove (Some id, MoveLast)) - | IDENT "intro" -> TacAtom (!@loc, TacIntroMove (None, MoveLast)) - - | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c) + IDENT "intros"; pl = ne_intropatterns -> + TacAtom (!@loc, TacIntroPattern (false,pl)) + | IDENT "intros" -> + TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false])) + | IDENT "eintros"; pl = ne_intropatterns -> + TacAtom (!@loc, TacIntroPattern (true,pl)) | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp)) @@ -557,12 +541,8 @@ GEXTEND Gram TacAtom (!@loc, TacElim (true,cl,el)) | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl) | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl) - | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n)) - | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n)) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd)) - | "cofix" -> TacAtom (!@loc, TacCofix None) - | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id)) | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd)) @@ -605,60 +585,26 @@ GEXTEND Gram | IDENT "generalize"; c = constr; l = LIST1 constr -> let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l))) - | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; + | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) - | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c) (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> TacAtom (!@loc, TacInductionDestruct (true,false,ic)) | IDENT "einduction"; ic = induction_clause_list -> TacAtom (!@loc, TacInductionDestruct(true,true,ic)) - | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; - h2 = quantified_hypothesis -> TacAtom (!@loc, TacDoubleInduction (h1,h2)) | IDENT "destruct"; icl = induction_clause_list -> TacAtom (!@loc, TacInductionDestruct(false,false,icl)) | IDENT "edestruct"; icl = induction_clause_list -> TacAtom (!@loc, TacInductionDestruct(false,true,icl)) - (* Automation tactic *) - | IDENT "trivial"; lems = auto_using; db = hintbases -> - TacAtom (!@loc, TacTrivial (Off, lems, db)) - | IDENT "info_trivial"; lems = auto_using; db = hintbases -> - TacAtom (!@loc, TacTrivial (Info, lems, db)) - | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases -> - TacAtom (!@loc, TacTrivial (Debug, lems, db)) - | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases -> - TacAtom (!@loc, TacAuto (Off, n, lems, db)) - | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases -> - TacAtom (!@loc, TacAuto (Info, n, lems, db)) - | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases -> - TacAtom (!@loc, TacAuto (Debug, n, lems, db)) - - (* Context management *) - | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l)) - | IDENT "clear"; l = LIST0 id_or_meta -> - let is_empty = match l with [] -> true | _ -> false in - TacAtom (!@loc, TacClear (is_empty, l)) - | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l) - | IDENT "move"; hfrom = id_or_meta; hto = move_location -> - TacAtom (!@loc, TacMove (hfrom,hto)) - | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) - - (* Constructors *) - | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll)) - | IDENT "eexists"; bll = opt_bindings -> - TacAtom (!@loc, TacSplit (true,bll)) - (* Equivalence relations *) - | IDENT "symmetry"; "in"; cl = in_clause -> TacAtom (!@loc, TacSymmetry cl) - (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t)) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 839f768b..e61be53a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -8,7 +8,7 @@ open Pp open Compat -open Errors +open CErrors open Util open Names open Constrexpr @@ -20,22 +20,19 @@ open Misctypes open Tok (* necessary for camlp4 *) open Pcoq -open Pcoq.Tactic open Pcoq.Prim open Pcoq.Constr open Pcoq.Vernac_ open Pcoq.Module let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter Lexer.add_keyword vernac_kw +let _ = List.iter CLexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) let query_command = Gram.entry_create "vernac:query_command" -let tactic_mode = Gram.entry_create "vernac:tactic_command" -let noedit_mode = Gram.entry_create "vernac:noedit_command" let subprf = Gram.entry_create "vernac:subprf" let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" @@ -48,21 +45,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -let command_entry = ref noedit_mode -let set_command_entry e = command_entry := e -let get_command_entry () = !command_entry - - -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let set_tactic_mode () = set_command_entry tactic_mode -let set_noedit_mode () = set_command_entry noedit_mode -let _ = Proof_global.register_proof_mode {Proof_global. - name = "Classic" ; - set = set_tactic_mode ; - reset = set_noedit_mode - } - let make_bullet s = let n = String.length s in match s.[0] with @@ -71,26 +53,11 @@ let make_bullet s = | '*' -> Star n | _ -> assert false -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" - (fun strm -> - match get_tok (stream_nth 0 strm) with - | KEYWORD "[" -> - (match get_tok (stream_nth 1 strm) with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - -let default_command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) - GEXTEND Gram - GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; vernac: FIRST - [ [ IDENT "Time"; l = vernac_list -> VernacTime l - | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l) + [ [ IDENT "Time"; c = located_vernac -> VernacTime c + | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v @@ -128,28 +95,13 @@ GEXTEND Gram | c = subprf -> c ] ] ; - vernac_list: - [ [ c = located_vernac -> [c] ] ] - ; vernac_aux: LAST - [ [ prfcom = default_command_entry -> prfcom ] ] + [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: [ [ c = subgoal_command -> c None] ] ; - selector: - [ [ n=natural; ":" -> SelectNth n - | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id - | IDENT "all" ; ":" -> SelectAll - | IDENT "par" ; ":" -> SelectAllParallel ] ] - ; - - tactic_mode: - [ [ gln = OPT selector; - tac = subgoal_command -> tac gln ] ] - ; - subprf: [ [ s = BULLET -> VernacBullet (make_bullet s) | "{" -> VernacSubproof None @@ -164,35 +116,37 @@ GEXTEND Gram | None -> c None | _ -> VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) - end - | info = OPT [IDENT "Info";n=natural -> n]; - tac = Tactic.tactic; - use_dft_tac = [ "." -> false | "..." -> true ] -> - (fun g -> - let g = Option.default (Proof_global.get_default_goal_selector ()) g in - VernacSolve(g,info,tac,use_dft_tac)) ] ] + end ] ] ; located_vernac: [ [ v = vernac -> !@loc, v ] ] ; END -let test_plurial_form = function +let warn_plural_command = + CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled + (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) + +let test_plural_form loc kwd = function | [(_,([_],_))] -> - Flags.if_verbose msg_warning - (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") + warn_plural_command ~loc:!@loc kwd | _ -> () -let test_plurial_form_types = function +let test_plural_form_types loc kwd = function | [([_],_)] -> - Flags.if_verbose msg_warning - (strbrk "Keywords Implicit Types expect more than one type") + warn_plural_command ~loc:!@loc kwd | _ -> () +let fresh_var env c = + Namegen.next_ident_away (Id.of_string "pat") + (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c)) + +let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var + (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition; + record_field decl_notation rec_definition pidentref; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -203,8 +157,8 @@ GEXTEND Gram VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) - | stre = assumptions_token; nl = inline; bl = assum_list -> - test_plurial_form bl; + | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> + test_plural_form loc kwd bl; VernacAssumption (stre, nl, bl) | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) @@ -257,11 +211,11 @@ GEXTEND Gram | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) - | IDENT "Variables" -> (Some Discharge, Definitional) - | IDENT "Axioms" -> (None, Logical) - | IDENT "Parameters" -> (None, Definitional) - | IDENT "Conjectures" -> (None, Conjectural) ] ] + [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical)) + | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional)) + | IDENT "Axioms" -> ("Axioms", (None, Logical)) + | IDENT "Parameters" -> ("Parameters", (None, Definitional)) + | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) @@ -272,8 +226,8 @@ GEXTEND Gram [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] ; univ_constraint: - [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = identref -> (l, ord, r) ] ] + [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = universe_level -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) @@ -289,11 +243,19 @@ GEXTEND Gram (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> + let (bl, c) = expand_pattern_binders mkCLambdaN bl c in (match c with CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> - DefineBody (bl, red, c, Some t) + let ((bl, c), tyo) = + if List.exists (function LocalPattern _ -> true | _ -> false) bl + then + let c = CCast (!@loc, c, CastConv t) in + (expand_pattern_binders mkCLambdaN bl c, None) + else ((bl, c), Some t) + in + DefineBody (bl, red, c, tyo) | bl = binders; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; @@ -462,6 +424,10 @@ let starredidentreflist_to_expr l = | [] -> SsEmpty | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x +let warn_deprecated_include_type = + CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" + (fun () -> strbrk "Include Type is deprecated; use Include instead") + (* Modules and Sections *) GEXTEND Gram GLOBAL: gallina_ext module_expr module_type section_subset_expr; @@ -501,9 +467,8 @@ GEXTEND Gram | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - Flags.if_verbose - msg_warning (strbrk "Include Type is deprecated; use Include instead"); - VernacInclude(e::l) ] ] + warn_deprecated_include_type ~loc:!@loc (); + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -607,9 +572,23 @@ GEXTEND Gram ; END +let warn_deprecated_arguments_scope = + CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" + (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") + +let warn_deprecated_implicit_arguments = + CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" + (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") + +let warn_deprecated_arguments_syntax = + CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated" + (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only " + ++ strbrk "in the first arguments list. The syntax allowing" + ++ strbrk " them to appear in other lists is deprecated.") + (* Extensions: implicits, coercions, etc. *) GEXTEND Gram - GLOBAL: gallina_ext instance_name; + GLOBAL: gallina_ext instance_name hint_info; gallina_ext: [ [ (* Transparent and Opaque *) @@ -662,81 +641,69 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; + info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) | IDENT "Existing"; IDENT "Instance"; id = global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances ([id], pri) + info = hint_info -> + VernacDeclareInstances [id, info] + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances (ids, pri) + pri = OPT [ "|"; i = natural -> i ] -> + let info = { hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is (* Arguments *) | IDENT "Arguments"; qid = smart_global; - impl = LIST1 [ l = LIST0 - [ item = argument_spec -> - let id, r, s = item in [`Id (id,r,s,false,false)] - | "/" -> [`Slash] - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items - ] -> l ] SEP ","; + args = LIST0 argument_spec_block; + more_implicits = OPT + [ ","; impl = LIST1 + [ impl = LIST0 more_implicits_block -> + let warn_deprecated = List.exists fst impl in + if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc (); + List.flatten (List.map snd impl)] + SEP "," -> impl + ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in - let impl = List.map List.flatten impl in - let rec aux n (narg, impl) = function - | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl - | `Slash :: tl -> aux (n+1) (n, impl) tl - | [] -> narg, impl in - let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in - let nargs, rest = List.hd nargs, List.tl nargs in - if List.exists (fun arg -> not (Int.equal arg nargs)) rest then - error "All arguments lists must have the same length"; - let err_incompat x y = - error ("Options \""^x^"\" and \""^y^"\" are incompatible") in - if nargs > 0 && List.mem `ReductionNeverUnfold mods then - err_incompat "simpl never" "/"; - if List.mem `ReductionNeverUnfold mods && - List.mem `ReductionDontExposeCase mods then - err_incompat "simpl never" "simpl nomatch"; - VernacArguments (qid, impl, nargs, mods) - + let slash_position = ref None in + let rec parse_args i = function + | [] -> [] + | `Id x :: args -> x :: parse_args (i+1) args + | `Slash :: args -> + if Option.is_empty !slash_position then + (slash_position := Some i; parse_args i args) + else + error "The \"/\" modifier can occur only once" + in + let args = parse_args 0 (List.flatten args) in + let more_implicits = Option.default [] more_implicits in + VernacArguments (qid, args, more_implicits, !slash_position, mods) + + (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + warn_deprecated_arguments_scope ~loc:!@loc (); VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - Flags.if_verbose - msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); - VernacDeclareImplicits (qid,pos) + warn_deprecated_implicit_arguments ~loc:!@loc (); + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plurial_form_types bl; + test_plural_form_types loc "Implicit Types" bl; VernacReserve bl | IDENT "Generalizable"; @@ -775,6 +742,55 @@ GEXTEND Gram snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s ] ]; + (* List of arguments implicit status, scope, modifiers *) + argument_spec_block: [ + [ item = argument_spec -> + let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = NotImplicit}] + | "/" -> [`Slash] + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = NotImplicit}) items + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = Implicit}) items + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = MaximallyImplicit}) items + ] + ]; + name_or_bang: [ + [ b = OPT "!"; id = name -> + not (Option.is_empty b), id + ] + ]; + (* Same as [argument_spec_block], but with only implicit status and names *) + more_implicits_block: [ + [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)]) + | "/" -> (true (* Should warn about deprecated syntax *), []) + | "["; items = LIST1 name_or_bang; "]" -> + (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items) + | "{"; items = LIST1 name_or_bang; "}" -> + (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items) + ] + ]; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque @@ -783,10 +799,15 @@ GEXTEND Gram | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: - [ [ name = identref; sup = OPT binders -> - (let (loc,id) = name in (loc, Name id)), + [ [ name = pidentref; sup = OPT binders -> + (let ((loc,id),l) = name in ((loc, Name id),l)), (Option.default [] sup) - | -> (!@loc, Anonymous), [] ] ] + | -> ((!@loc, Anonymous), None), [] ] ] + ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { hint_priority = i; hint_pattern = pat } + | -> { hint_priority = None; hint_pattern = None } ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] @@ -804,17 +825,13 @@ GEXTEND Gram GLOBAL: command query_command class_rawexpr; command: - [ [ IDENT "Ltac"; - l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition (true, l) - - | IDENT "Comments"; l = LIST0 comment -> VernacComments l + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) + info = hint_info -> + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) (* System directory *) | IDENT "Pwd" -> VernacChdir None @@ -870,7 +887,20 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (table,v) + begin match v with + | StringValue s -> + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + VernacSetAppendOption (table, s) + else + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) + | _ -> VernacSetOption (table, v) + end | "Set"; table = option_table -> VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_table -> @@ -943,7 +973,6 @@ GEXTEND Gram | IDENT "Classes" -> PrintClasses | IDENT "TypeClasses" -> PrintTypeClasses | IDENT "Instances"; qid = smart_global -> PrintInstances qid - | IDENT "Ltac"; qid = global -> PrintLtac qid | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) @@ -954,7 +983,6 @@ GEXTEND Gram | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s - | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s @@ -1083,7 +1111,7 @@ GEXTEND Gram VernacDelimiters (sc, None) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; - refl = LIST1 smart_global -> VernacBindScope (sc,refl) + refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) | IDENT "Infix"; local = obsolete_locality; op = ne_lstring; ":="; p = constr; @@ -1102,10 +1130,6 @@ GEXTEND Gram | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> VernacNotationAddFormat (n,s,fmt) - | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; - pil = LIST1 production_item; ":="; t = Tactic.tactic - -> VernacTacticNotation (n,pil,t) - | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; @@ -1131,9 +1155,6 @@ GEXTEND Gram obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; - tactic_level: - [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] - ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] @@ -1143,10 +1164,10 @@ GEXTEND Gram | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA - | IDENT "only"; IDENT "parsing" -> - SetOnlyParsing Flags.Current + | IDENT "only"; IDENT "printing" -> SetOnlyPrinting + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetOnlyParsing (Coqinit.get_compat_version s) + SetCompatVersion (Coqinit.get_compat_version s) | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; s2 = OPT [s = STRING -> (!@loc,s)] -> begin match s1, s2 with @@ -1165,10 +1186,4 @@ GEXTEND Gram | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; - production_item: - [ [ s = ne_string -> TacTerm s - | nt = IDENT; - po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; - ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] - ; END diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 13ed8046..8df519b5 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -3,5 +3,3 @@ G_vernac G_prim G_proofs G_tactic -G_ltac -G_obligations diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 deleted file mode 100644 index 5d96873f..00000000 --- a/parsing/lexer.ml4 +++ /dev/null @@ -1,695 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* char -> int = compare end -module CharMap = Map.Make (CharOrd) - -type ttree = { - node : string option; - branch : ttree CharMap.t } - -let empty_ttree = { node = None; branch = CharMap.empty } - -let ttree_add ttree str = - let rec insert tt i = - if i == String.length str then - {node = Some str; branch = tt.branch} - else - let c = str.[i] in - let br = - match try Some (CharMap.find c tt.branch) with Not_found -> None with - | Some tt' -> - CharMap.add c (insert tt' (i + 1)) (CharMap.remove c tt.branch) - | None -> - let tt' = {node = None; branch = CharMap.empty} in - CharMap.add c (insert tt' (i + 1)) tt.branch - in - { node = tt.node; branch = br } - in - insert ttree 0 - -(* Search a string in a dictionary: raises [Not_found] - if the word is not present. *) - -let ttree_find ttree str = - let rec proc_rec tt i = - if i == String.length str then tt - else proc_rec (CharMap.find str.[i] tt.branch) (i+1) - in - proc_rec ttree 0 - -(* Removes a string from a dictionary: returns an equal dictionary - if the word not present. *) -let ttree_remove ttree str = - let rec remove tt i = - if i == String.length str then - {node = None; branch = tt.branch} - else - let c = str.[i] in - let br = - match try Some (CharMap.find c tt.branch) with Not_found -> None with - | Some tt' -> - CharMap.add c (remove tt' (i + 1)) (CharMap.remove c tt.branch) - | None -> tt.branch - in - { node = tt.node; branch = br } - in - remove ttree 0 - - -(* Errors occurring while lexing (explained as "Lexer error: ...") *) - -module Error = struct - - type t = - | Illegal_character - | Unterminated_comment - | Unterminated_string - | Undefined_token - | Bad_token of string - | UnsupportedUnicode of int - - exception E of t - - let to_string x = - "Syntax Error: Lexer: " ^ - (match x with - | Illegal_character -> "Illegal character" - | Unterminated_comment -> "Unterminated comment" - | Unterminated_string -> "Unterminated string" - | Undefined_token -> "Undefined token" - | Bad_token tok -> Format.sprintf "Bad token %S" tok - | UnsupportedUnicode x -> - Printf.sprintf "Unsupported Unicode character (0x%x)" x) - - (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) - -end -open Error - -let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str) - -let bad_token str = raise (Error.E (Bad_token str)) - -(* Lexer conventions on tokens *) - -type token_kind = - | Utf8Token of (Unicode.status * int) - | AsciiChar - | EmptyStream - -let error_unsupported_unicode_character n unicode cs = - let bp = Stream.count cs in - err (bp,bp+n) (UnsupportedUnicode unicode) - -let error_utf8 cs = - let bp = Stream.count cs in - Stream.junk cs; (* consume the char to avoid read it and fail again *) - err (bp, bp+1) Illegal_character - -let utf8_char_size cs = function - (* Utf8 leading byte *) - | '\x00'..'\x7F' -> 1 - | '\xC0'..'\xDF' -> 2 - | '\xE0'..'\xEF' -> 3 - | '\xF0'..'\xF7' -> 4 - | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs - -let njunk n = Util.repeat n Stream.junk - -let check_utf8_trailing_byte cs c = - if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs - -(* Recognize utf8 blocks (of length less than 4 bytes) *) -(* but don't certify full utf8 compliance (e.g. no emptyness check) *) -let lookup_utf8_tail c cs = - let c1 = Char.code c in - if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs - else - let n, unicode = - if Int.equal (c1 land 0x20) 0 then - match Stream.npeek 2 cs with - | [_;c2] -> - check_utf8_trailing_byte cs c2; - 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F) - | _ -> error_utf8 cs - else if Int.equal (c1 land 0x10) 0 then - match Stream.npeek 3 cs with - | [_;c2;c3] -> - check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + - (Char.code c3 land 0x3F) - | _ -> error_utf8 cs - else match Stream.npeek 4 cs with - | [_;c2;c3;c4] -> - check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - check_utf8_trailing_byte cs c4; - 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + - (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) - | _ -> error_utf8 cs - in - try Unicode.classify unicode, n - with Unicode.Unsupported -> - njunk n cs; error_unsupported_unicode_character n unicode cs - -let lookup_utf8 cs = - match Stream.peek cs with - | Some ('\x00'..'\x7F') -> AsciiChar - | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs) - | None -> EmptyStream - -let unlocated f x = f x - (** FIXME: should we still unloc the exception? *) -(* try f x with Loc.Exc_located (_, exc) -> raise exc *) - -let check_keyword str = - let rec loop_symb = parser - | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str - | [< s >] -> - match unlocated lookup_utf8 s with - | Utf8Token (_,n) -> njunk n s; loop_symb s - | AsciiChar -> Stream.junk s; loop_symb s - | EmptyStream -> () - in - loop_symb (Stream.of_string str) - -let check_keyword_to_add s = - try check_keyword s - with Error.E (UnsupportedUnicode unicode) -> - Flags.if_verbose msg_warning - (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ - which will not be parsable." s unicode)) - -let check_ident str = - let rec loop_id intail = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> - loop_id true s - | [< ' ('0'..'9' | ''') when intail; s >] -> - loop_id true s - | [< s >] -> - match unlocated lookup_utf8 s with - | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s - | Utf8Token (Unicode.IdentPart, n) when intail -> - njunk n s; - loop_id true s - | EmptyStream -> () - | Utf8Token _ | AsciiChar -> bad_token str - in - loop_id false (Stream.of_string str) - -let is_ident str = - try let _ = check_ident str in true with Error.E _ -> false - -(* Keyword and symbol dictionary *) -let token_tree = ref empty_ttree - -let is_keyword s = - try match (ttree_find !token_tree s).node with None -> false | Some _ -> true - with Not_found -> false - -let add_keyword str = - if not (is_keyword str) then - begin - check_keyword_to_add str; - token_tree := ttree_add !token_tree str - end - -let remove_keyword str = - token_tree := ttree_remove !token_tree str - -(* Freeze and unfreeze the state of the lexer *) -type frozen_t = ttree - -let freeze () = !token_tree -let unfreeze tt = (token_tree := tt) - -(* The string buffering machinery *) - -let buff = ref (String.create 80) - -let store len x = - if len >= String.length !buff then - buff := !buff ^ String.create (String.length !buff); - !buff.[len] <- x; - succ len - -let rec nstore n len cs = - if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len - -let get_buff len = String.sub !buff 0 len - -(* The classical lexer: idents, numbers, quoted strings, comments *) - -let rec ident_tail len = parser - | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> - ident_tail (store len c) s - | [< s >] -> - match lookup_utf8 s with - | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> - ident_tail (nstore n len s) s - | _ -> len - -let rec number len = parser - | [< ' ('0'..'9' as c); s >] -> number (store len c) s - | [< >] -> len - -let rec string in_comments bp len = parser - | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> - if esc then string in_comments bp (store len '"') s else len - | [< ''('; s >] -> - (parser - | [< ''*'; s >] -> - string - (Option.map succ in_comments) - bp (store (store len '(') '*') - s - | [< >] -> - string in_comments bp (store len '(') s) s - | [< ''*'; s >] -> - (parser - | [< '')'; s >] -> - let () = match in_comments with - | Some 0 -> - msg_warning - (strbrk - "Not interpreting \"*)\" as the end of current \ - non-terminated comment because it occurs in a \ - non-terminated string of the comment.") - | _ -> () - in - let in_comments = Option.map pred in_comments in - string in_comments bp (store (store len '*') ')') s - | [< >] -> - string in_comments bp (store len '*') s) s - | [< 'c; s >] -> string in_comments bp (store len c) s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string - -(* Hook for exporting comment into xml theory files *) -let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () - -(* Utilities for comments in beautify *) -let comment_begin = ref None -let comm_loc bp = match !comment_begin with -| None -> comment_begin := Some bp -| _ -> () - -let current = Buffer.create 8192 -let between_com = ref true - -type com_state = int option * string * bool -let restore_com_state (o,s,b) = - comment_begin := o; - Buffer.clear current; Buffer.add_string current s; - between_com := b -let dflt_com = (None,"",true) -let com_state () = - let s = (!comment_begin, Buffer.contents current, !between_com) in - restore_com_state dflt_com; s - -let real_push_char c = Buffer.add_char current c - -(* Add a char if it is between two commands, if it is a newline or - if the last char is not a space itself. *) -let push_char c = - if - !between_com || List.mem c ['\n';'\r'] || - (List.mem c [' ';'\t']&& - (Int.equal (Buffer.length current) 0 || - not (let s = Buffer.contents current in - List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r']))) - then - real_push_char c - -let push_string s = Buffer.add_string current s - -let null_comment s = - let rec null i = - i<0 || (List.mem s.[i] [' ';'\t';'\n';'\r'] && null (i-1)) in - null (String.length s - 1) - -let comment_stop ep = - let current_s = Buffer.contents current in - if !Flags.xml_export && Buffer.length current > 0 && - (!between_com || not(null_comment current_s)) then - Hook.get f_xml_output_comment current_s; - (if Flags.do_beautify() && Buffer.length current > 0 && - (!between_com || not(null_comment current_s)) then - let bp = match !comment_begin with - Some bp -> bp - | None -> - msgerrnl(str "No begin location for comment '" - ++ str current_s ++str"' ending at " - ++ int ep); - ep-1 in - Pp.comments := ((bp,ep),current_s) :: !Pp.comments); - Buffer.clear current; - comment_begin := None; - between_com := false - -(* Does not unescape!!! *) -let rec comm_string bp = parser - | [< ''"' >] -> push_string "\"" - | [< ''\\'; _ = - (parser [< ' ('"' | '\\' as c) >] -> - let () = match c with - | '"' -> real_push_char c - | _ -> () - in - real_push_char c - | [< >] -> real_push_char '\\'); s >] - -> comm_string bp s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string - | [< 'c; s >] -> real_push_char c; comm_string bp s - -let rec comment bp = parser bp2 - | [< ''('; - _ = (parser - | [< ''*'; s >] -> push_string "(*"; comment bp s - | [< >] -> push_string "(" ); - s >] -> comment bp s - | [< ''*'; - _ = parser - | [< '')' >] -> push_string "*)"; - | [< s >] -> real_push_char '*'; comment bp s >] -> () - | [< ''"'; s >] -> - if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) - else ignore (string (Some 0) bp2 0 s); - comment bp s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment - | [< 'z; s >] -> real_push_char z; comment bp s - -(* Parse a special token, using the [token_tree] *) - -(* Peek as much utf-8 lexemes as possible *) -(* and retain the longest valid special token obtained *) -let rec progress_further last nj tt cs = - try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) - with Failure _ -> last - -and update_longest_valid_token last nj tt cs = - match tt.node with - | Some _ as last' -> - stream_njunk nj cs; - progress_further last' 0 tt cs - | None -> - progress_further last nj tt cs - -(* nj is the number of char peeked since last valid token *) -(* n the number of char in utf8 block *) -and progress_utf8 last nj n c tt cs = - try - let tt = CharMap.find c tt.branch in - if Int.equal n 1 then - update_longest_valid_token last (nj+n) tt cs - else - match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with - | l when Int.equal (List.length l) (n - 1) -> - List.iter (check_utf8_trailing_byte cs) l; - let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in - update_longest_valid_token last (nj+n) tt cs - | _ -> - error_utf8 cs - with Not_found -> - last - -and progress_from_byte last nj tt cs c = - progress_utf8 last nj (utf8_char_size cs c) c tt cs - -let find_keyword id s = - let tt = ttree_find !token_tree id in - match progress_further tt.node 0 tt s with - | None -> raise Not_found - | Some c -> KEYWORD c - -let process_sequence bp c cs = - let rec aux n cs = - match Stream.peek cs with - | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - | _ -> BULLET (String.make n c), (bp, Stream.count cs) - in - aux 1 cs - -(* Must be a special token *) -let process_chars bp c cs = - let t = progress_from_byte None (-1) !token_tree cs c in - let ep = Stream.count cs in - match t with - | Some t -> (KEYWORD t, (bp, ep)) - | None -> - let ep' = bp + utf8_char_size cs c in - njunk (ep' - ep) cs; - err (bp, ep') Undefined_token - -let token_of_special c s = match c with - | '$' -> METAIDENT s - | '.' -> FIELD s - | _ -> assert false - -(* Parse what follows a dot / a dollar *) - -let parse_after_special c bp = - parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] -> - token_of_special c (get_buff len) - | [< s >] -> - match lookup_utf8 s with - | Utf8Token (Unicode.Letter, n) -> - token_of_special c (get_buff (ident_tail (nstore n 0 s) s)) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) - -(* Parse what follows a question mark *) - -let parse_after_qmark bp s = - match Stream.peek s with - | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK - | None -> KEYWORD "?" - | _ -> - match lookup_utf8 s with - | Utf8Token (Unicode.Letter, _) -> LEFTQMARK - | AsciiChar | Utf8Token _ | EmptyStream -> - fst (process_chars bp '?' s) - -let blank_or_eof cs = - match Stream.peek cs with - | None -> true - | Some (' ' | '\t' | '\n' |'\r') -> true - | _ -> false - -(* Parse a token in a char stream *) - -let rec next_token = parser bp - | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> - comm_loc bp; push_char c; next_token s - | [< ''$' as c; t = parse_after_special c bp >] ep -> - comment_stop bp; (t, (ep, bp)) - | [< ''.' as c; t = parse_after_special c bp; s >] ep -> - comment_stop bp; - (* We enforce that "." should either be part of a larger keyword, - for instance ".(", or followed by a blank or eof. *) - let () = match t with - | KEYWORD ("." | "...") -> - if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; - between_com := true; - | _ -> () - in - (t, (bp,ep)) - | [< ' ('-'|'+'|'*' as c); s >] -> - let t,new_between_com = - if !between_com then process_sequence bp c s,true - else process_chars bp c s,false - in - comment_stop bp; between_com := new_between_com; t - | [< ''?'; s >] ep -> - let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c); s >] ep -> - let id = get_buff len in - comment_stop bp; - (try find_keyword id s with Not_found -> IDENT id), (bp, ep) - | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> - comment_stop bp; - (INT (get_buff len), (bp, ep)) - | [< ''\"'; len = string None bp 0 >] ep -> - comment_stop bp; - (STRING (get_buff len), (bp, ep)) - | [< ' ('(' as c); - t = parser - | [< ''*'; s >] -> - comm_loc bp; - push_string "(*"; - comment bp s; - next_token s - | [< t = process_chars bp c >] -> comment_stop bp; t >] -> - t - | [< s >] -> - match lookup_utf8 s with - | Utf8Token (Unicode.Letter, n) -> - let len = ident_tail (nstore n 0 s) s in - let id = get_buff len in - let ep = Stream.count s in - comment_stop bp; - (try find_keyword id s with Not_found -> IDENT id), (bp, ep) - | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) -> - let t = process_chars bp (Stream.next s) s in - let new_between_com = match t with - (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in - comment_stop bp; between_com := new_between_com; t - | EmptyStream -> - comment_stop bp; (EOI, (bp, bp + 1)) - -(* (* Debug: uncomment this for tracing tokens seen by coq...*) -let next_token s = - let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t); - (t,(bp,ep)) -*) - -(* Location table system for creating tables associating a token count - to its location in a char stream (the source) *) - -let locerr () = invalid_arg "Lexer: location function" - -let loct_create () = Hashtbl.create 207 - -let loct_func loct i = - try Hashtbl.find loct i with Not_found -> locerr () - -let loct_add loct i loc = Hashtbl.add loct i loc - -let current_location_table = ref (loct_create ()) - -type location_table = (int, CompatLoc.t) Hashtbl.t -let location_table () = !current_location_table -let restore_location_table t = current_location_table := t - -(** {6 The lexer of Coq} *) - -(** Note: removing a token. - We do nothing because [remove_token] is called only when removing a grammar - rule with [Grammar.delete_rule]. The latter command is called only when - unfreezing the state of the grammar entries (see GRAMMAR summary, file - env/metasyntax.ml). Therefore, instead of removing tokens one by one, - we unfreeze the state of the lexer. This restores the behaviour of the - lexer. B.B. *) - -IFDEF CAMLP5 THEN - -type te = Tok.t - -(** Names of tokens, for this lexer, used in Grammar error messages *) - -let token_text = function - | ("", t) -> "'" ^ t ^ "'" - | ("IDENT", "") -> "identifier" - | ("IDENT", t) -> "'" ^ t ^ "'" - | ("INT", "") -> "integer" - | ("INT", s) -> "'" ^ s ^ "'" - | ("STRING", "") -> "string" - | ("EOI", "") -> "end of input" - | (con, "") -> con - | (con, prm) -> con ^ " \"" ^ prm ^ "\"" - -let func cs = - let loct = loct_create () in - let ts = - Stream.from - (fun i -> - let (tok, loc) = next_token cs in - loct_add loct i (make_loc loc); Some tok) - in - current_location_table := loct; - (ts, loct_func loct) - -let lexer = { - Token.tok_func = func; - Token.tok_using = - (fun pat -> match Tok.of_pattern pat with - | KEYWORD s -> add_keyword s - | _ -> ()); - Token.tok_removing = (fun _ -> ()); - Token.tok_match = Tok.match_pattern; - Token.tok_comm = None; - Token.tok_text = token_text } - -ELSE (* official camlp4 for ocaml >= 3.10 *) - -module M_ = Camlp4.ErrorHandler.Register (Error) - -module Loc = CompatLoc -module Token = struct - include Tok (* Cf. tok.ml *) - module Loc = CompatLoc - module Error = Camlp4.Struct.EmptyError - module Filter = struct - type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t - type t = unit - let mk _is_kwd = () - let keyword_added () kwd _ = add_keyword kwd - let keyword_removed () _ = () - let filter () x = x - let define_filter () _ = () - end -end - -let mk () _init_loc(*FIXME*) cs = - let loct = loct_create () in - let rec self = - parser i - [< (tok, loc) = next_token; s >] -> - let loc = make_loc loc in - loct_add loct i loc; - [< '(tok, loc); self s >] - | [< >] -> [< >] - in current_location_table := loct; self cs - -END - -(** Terminal symbols interpretation *) - -let is_ident_not_keyword s = - is_ident s && not (is_keyword s) - -let is_number s = - let rec aux i = - Int.equal (String.length s) i || - match s.[i] with '0'..'9' -> aux (i+1) | _ -> false - in aux 0 - -let strip s = - let len = - let rec loop i len = - if Int.equal i (String.length s) then len - else if s.[i] == ' ' then loop (i + 1) len - else loop (i + 1) (len + 1) - in - loop 0 0 - in - if len == String.length s then s - else - let s' = String.create len in - let rec loop i i' = - if i == String.length s then s' - else if s.[i] == ' ' then loop (i + 1) i' - else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end - in - loop 0 0 - -let terminal s = - let s = strip s in - let () = match s with "" -> Errors.error "empty token." | _ -> () in - if is_ident_not_keyword s then IDENT s - else if is_number s then INT s - else KEYWORD s diff --git a/parsing/lexer.mli b/parsing/lexer.mli deleted file mode 100644 index 24b0ec84..00000000 --- a/parsing/lexer.mli +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -val remove_keyword : string -> unit -val is_keyword : string -> bool - -(* val location_function : int -> Loc.t *) - -(** for coqdoc *) -type location_table -val location_table : unit -> location_table -val restore_location_table : location_table -> unit - -val check_ident : string -> unit -val is_ident : string -> bool -val check_keyword : string -> unit - -type frozen_t -val freeze : unit -> frozen_t -val unfreeze : frozen_t -> unit - -type com_state -val com_state: unit -> com_state -val restore_com_state: com_state -> unit - -val xml_output_comment : (string -> unit) Hook.t - -val terminal : string -> Tok.t - -(** The lexer of Coq: *) - -include Compat.LexerSig diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index a0cb8319..0e1c79c9 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,6 +1,6 @@ Tok Compat -Lexer +CLexer Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml new file mode 100644 index 00000000..7dc02190 --- /dev/null +++ b/parsing/pcoq.ml @@ -0,0 +1,527 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* CompatGramext.RightA +| Extend.LeftA -> CompatGramext.LeftA +| Extend.NonA -> CompatGramext.NonA + +let of_coq_position = function +| Extend.First -> CompatGramext.First +| Extend.Last -> CompatGramext.Last +| Extend.Before s -> CompatGramext.Before s +| Extend.After s -> CompatGramext.After s +| Extend.Level s -> CompatGramext.Level s + +module Symbols = GramextMake(G) + +let camlp4_verbosity silent f x = + let a = !warning_verbose in + warning_verbose := silent; + f x; + warning_verbose := a + +let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x + +(** Grammar extensions *) + +(** NB: [extend_statment = + gram_position option * single_extend_statment list] + and [single_extend_statment = + string option * gram_assoc option * production_rule list] + and [production_rule = symbol list * action] + + In [single_extend_statement], first two parameters are name and + assoc iff a level is created *) + +(** Binding general entry keys to symbol *) + +let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function +| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc)) +| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) + +let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function + | Atoken t -> Symbols.stoken t + | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) + | Aself -> Symbols.sself + | Anext -> Symbols.snext + | Aentry e -> + Symbols.snterm (G.Entry.obj e) + | Aentryl (e, n) -> + Symbols.snterml (G.Entry.obj e, string_of_int n) + | Arules rs -> + G.srules' (List.map symbol_of_rules rs) + +and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function +| Stop -> fun accu -> accu +| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) + +and symbol_of_rules : type a. a Extend.rules -> _ = function +| Rules (r, act) -> + let symb = symbol_of_rule r.norec_rule [] in + let act = of_coq_action r.norec_rule act in + (symb, act) + +let of_coq_production_rule : type a. a Extend.production_rule -> _ = function +| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) + +let of_coq_single_extend_statement (lvl, assoc, rule) = + (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + +let of_coq_extend_statement (pos, st) = + (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + +(** Type of reinitialization data *) +type gram_reinit = gram_assoc * gram_position + +type extend_rule = +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule + +type ext_kind = + | ByGrammar of extend_rule + | ByEXTEND of (unit -> unit) * (unit -> unit) + +(** The list of extensions *) + +let camlp4_state = ref [] + +(** Deletion *) + +let grammar_delete e reinit (pos,rls) = + List.iter + (fun (n,ass,lev) -> + List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) + (List.rev rls); + match reinit with + | Some (a,ext) -> + let a = of_coq_assoc a in + let ext = of_coq_position ext in + let lev = match pos with + | Some (CompatGramext.Level n) -> n + | _ -> assert false + in + maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) + | None -> () + +(** Extension *) + +let grammar_extend e reinit ext = + let ext = of_coq_extend_statement ext in + let undo () = grammar_delete e reinit ext in + let redo () = camlp4_verbosity false (maybe_uncurry (G.extend e)) ext in + camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + redo () + +let grammar_extend_sync e reinit ext = + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; + camlp4_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + +(** The apparent parser of Coq; encapsulate G to keep track + of the extensions. *) + +module Gram = + struct + include G + let extend e = + maybe_curry + (fun ext -> + camlp4_state := + (ByEXTEND ((fun () -> grammar_delete e None ext), + (fun () -> maybe_uncurry (G.extend e) ext))) + :: !camlp4_state; + maybe_uncurry (G.extend e) ext) + let delete_rule e pil = + (* spiwack: if you use load an ML module which contains GDELETE_RULE + in a section, God kills a kitty. As it would corrupt remove_grammars. + There does not seem to be a good way to undo a delete rule. As deleting + takes fewer arguments than extending. The production rule isn't returned + by delete_rule. If we could retrieve the necessary information, then + ByEXTEND provides just the framework we need to allow this in section. + I'm not entirely sure it makes sense, but at least it would be more correct. + *) + G.delete_rule e pil + end + +(** Remove extensions + + [n] is the number of extended entries (not the number of Grammar commands!) + to remove. *) + +let rec remove_grammars n = + if n>0 then + (match !camlp4_state with + | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") + | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> + grammar_delete g reinit (of_coq_extend_statement ext); + camlp4_state := t; + remove_grammars (n-1) + | ByEXTEND (undo,redo)::t -> + undo(); + camlp4_state := t; + remove_grammars n; + redo(); + camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) + +let make_rule r = [None, None, r] + +(** An entry that checks we reached the end of the input. *) + +let eoi_entry en = + let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in + let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in + let act = Gram.action (fun _ x loc -> x) in + maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + e + +let map_entry f en = + let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in + let symbs = [Symbols.snterm (Gram.Entry.obj en)] in + let act = Gram.action (fun x loc -> f x) in + maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + e + +(* Parse a string, does NOT check if the entire string was read + (use eoi_entry) *) + +let parse_string f x = + let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) + +type gram_universe = string + +let utables : (string, unit) Hashtbl.t = + Hashtbl.create 97 + +let create_universe u = + let () = Hashtbl.add utables u () in + u + +let uprim = create_universe "prim" +let uconstr = create_universe "constr" +let utactic = create_universe "tactic" +let uvernac = create_universe "vernac" + +let get_univ u = + if Hashtbl.mem utables u then u + else raise Not_found + +let new_entry u s = + let ename = u ^ ":" ^ s in + let e = Gram.entry_create ename in + e + +let make_gen_entry u s = new_entry u s + +module GrammarObj = +struct + type ('r, _, _) obj = 'r Gram.entry + let name = "grammar" + let default _ = None +end + +module Grammar = Register(GrammarObj) + +let register_grammar = Grammar.register0 +let genarg_grammar = Grammar.obj + +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = + let e = new_entry u s in + let Rawwit t = etyp in + let () = Grammar.register0 t e in + e + +(* Initial grammar entries *) + +module Prim = + struct + let gec_gen n = make_gen_entry uprim n + + (* Entries that can be referred via the string -> Gram.entry table *) + (* Typically for tactic or vernac extensions *) + let preident = gec_gen "preident" + let ident = gec_gen "ident" + let natural = gec_gen "natural" + let integer = gec_gen "integer" + let bigint = Gram.entry_create "Prim.bigint" + let string = gec_gen "string" + let reference = make_gen_entry uprim "reference" + let by_notation = Gram.entry_create "by_notation" + let smart_global = Gram.entry_create "smart_global" + + (* parsed like ident but interpreted as a term *) + let var = gec_gen "var" + + let name = Gram.entry_create "Prim.name" + let identref = Gram.entry_create "Prim.identref" + let pidentref = Gram.entry_create "Prim.pidentref" + 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" + + let qualid = Gram.entry_create "Prim.qualid" + let fullyqualid = Gram.entry_create "Prim.fullyqualid" + let dirpath = Gram.entry_create "Prim.dirpath" + + let ne_string = Gram.entry_create "Prim.ne_string" + let ne_lstring = Gram.entry_create "Prim.ne_lstring" + + end + +module Constr = + struct + let gec_constr = make_gen_entry uconstr + + (* Entries that can be referred via the string -> Gram.entry table *) + let constr = gec_constr "constr" + let operconstr = gec_constr "operconstr" + let constr_eoi = eoi_entry constr + let lconstr = gec_constr "lconstr" + let binder_constr = gec_constr "binder_constr" + let ident = make_gen_entry uconstr "ident" + let global = make_gen_entry uconstr "global" + let universe_level = make_gen_entry uconstr "universe_level" + let sort = make_gen_entry uconstr "sort" + let pattern = Gram.entry_create "constr:pattern" + let constr_pattern = gec_constr "constr_pattern" + let lconstr_pattern = gec_constr "lconstr_pattern" + let closed_binder = Gram.entry_create "constr:closed_binder" + let binder = Gram.entry_create "constr:binder" + let binders = Gram.entry_create "constr:binders" + let open_binders = Gram.entry_create "constr:open_binders" + let binders_fixannot = Gram.entry_create "constr:binders_fixannot" + let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint" + let record_declaration = Gram.entry_create "constr:record_declaration" + let appl_arg = Gram.entry_create "constr:appl_arg" + end + +module Module = + struct + let module_expr = Gram.entry_create "module_expr" + let module_type = Gram.entry_create "module_type" + end + +module Tactic = + struct + (* Main entry for extensions *) + let simple_tactic = Gram.entry_create "tactic:simple_tactic" + + (* Entries that can be referred via the string -> Gram.entry table *) + (* Typically for tactic user extensions *) + let open_constr = + make_gen_entry utactic "open_constr" + let constr_with_bindings = + make_gen_entry utactic "constr_with_bindings" + let bindings = + make_gen_entry utactic "bindings" + let hypident = Gram.entry_create "hypident" + let constr_may_eval = make_gen_entry utactic "constr_may_eval" + let constr_eval = make_gen_entry utactic "constr_eval" + let uconstr = + make_gen_entry utactic "uconstr" + let quantified_hypothesis = + make_gen_entry utactic "quantified_hypothesis" + let destruction_arg = make_gen_entry utactic "destruction_arg" + let int_or_var = make_gen_entry utactic "int_or_var" + let red_expr = make_gen_entry utactic "red_expr" + let simple_intropattern = + make_gen_entry utactic "simple_intropattern" + let in_clause = make_gen_entry utactic "in_clause" + let clause_dft_concl = + make_gen_entry utactic "clause" + + + (* Main entries for ltac *) + let tactic_arg = Gram.entry_create "tactic:tactic_arg" + let tactic_expr = make_gen_entry utactic "tactic_expr" + let binder_tactic = make_gen_entry utactic "binder_tactic" + + let tactic = make_gen_entry utactic "tactic" + + (* Main entry for quotations *) + let tactic_eoi = eoi_entry tactic + + end + +module Vernac_ = + struct + let gec_vernac s = Gram.entry_create ("vernac:" ^ s) + + (* The different kinds of vernacular commands *) + let gallina = gec_vernac "gallina" + let gallina_ext = gec_vernac "gallina_ext" + let command = gec_vernac "command" + let syntax = gec_vernac "syntax_command" + let vernac = gec_vernac "Vernac.vernac" + let vernac_eoi = eoi_entry vernac + let rec_definition = gec_vernac "Vernac.rec_definition" + let hint_info = gec_vernac "hint_info" + (* Main vernac entry *) + let main_entry = Gram.entry_create "vernac" + let noedit_mode = gec_vernac "noedit_command" + + let () = + let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in + let act_eoi = Gram.action (fun _ loc -> None) in + let rule = [ + ([ Symbols.stoken Tok.EOI ], act_eoi); + ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac ); + ] in + maybe_uncurry (Gram.extend main_entry) (None, make_rule rule) + + let command_entry_ref = ref noedit_mode + let command_entry = + Gram.Entry.of_parser "command_entry" + (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) + + end + +let main_entry = Vernac_.main_entry + +let set_command_entry e = Vernac_.command_entry_ref := e +let get_command_entry () = !Vernac_.command_entry_ref + +let epsilon_value f e = + let r = Rule (Next (Stop, e), fun x _ -> f x) in + let ext = of_coq_extend_statement (None, [None, None, [r]]) in + let entry = G.entry_create "epsilon" in + let () = maybe_uncurry (G.extend entry) ext in + try Some (parse_string entry "") with _ -> None + +(** Synchronized grammar extensions *) + +module GramState = Store.Make(struct end) + +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t + +module GrammarCommand = Dyn.Make(struct end) +module GrammarInterp = struct type 'a t = 'a grammar_extension end +module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) + +let grammar_interp = ref GrammarInterpMap.empty + +let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref [] + +type 'a grammar_command = 'a GrammarCommand.tag + +let create_grammar_command name interp : _ grammar_command = + let obj = GrammarCommand.create name in + let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in + obj + +let extend_grammar_command tag g = + let modify = GrammarInterpMap.find tag !grammar_interp in + let grammar_state = match !grammar_stack with + | [] -> GramState.empty + | (_, _, st) :: _ -> st + in + let (rules, st) = modify g grammar_state in + let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in + let () = List.iter iter rules in + let nb = List.length rules in + grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack + +let recover_grammar_command (type a) (tag : a grammar_command) : a list = + let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) -> + match GrammarCommand.eq tag tag' with + | None -> None + | Some Refl -> Some v + in + List.map_filter filter !grammar_stack + +let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g + +(* Summary functions: the state of the lexer is included in that of the parser. + Because the grammar affects the set of keywords when adding or removing + grammar rules. *) +type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t + +let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ()) + +(* We compare the current state of the grammar and the state to unfreeze, + by computing the longest common suffixes *) +let factorize_grams l1 l2 = + if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 + +let number_of_entries gcl = + List.fold_left (fun n (p,_,_) -> n + p) 0 gcl + +let unfreeze (grams, lex) = + let (undo, redo, common) = factorize_grams !grammar_stack grams in + let n = number_of_entries undo in + remove_grammars n; + grammar_stack := common; + CLexer.unfreeze lex; + List.iter extend_dyn_grammar (List.rev_map pi2 redo) + +(** No need to provide an init function : the grammar state is + statically available, and already empty initially, while + the lexer state should not be resetted, since it contains + keywords declared in g_*.ml4 *) + +let _ = + Summary.declare_summary "GRAMMAR_LEXER" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = Summary.nop } + +let with_grammar_rule_protection f x = + let fs = freeze false in + try let a = f x in unfreeze fs; a + with reraise -> + let reraise = CErrors.push reraise in + let () = unfreeze fs in + iraise reraise + +(** Registering grammar of generic arguments *) + +let () = + let open Stdarg in + let open Constrarg in +(* Grammar.register0 wit_unit; *) +(* Grammar.register0 wit_bool; *) + Grammar.register0 wit_int (Prim.integer); + Grammar.register0 wit_string (Prim.string); + Grammar.register0 wit_pre_ident (Prim.preident); + Grammar.register0 wit_int_or_var (Tactic.int_or_var); + Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern); + Grammar.register0 wit_ident (Prim.ident); + Grammar.register0 wit_var (Prim.var); + Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis); + Grammar.register0 wit_constr (Constr.constr); + Grammar.register0 wit_uconstr (Tactic.uconstr); + Grammar.register0 wit_open_constr (Tactic.open_constr); + Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings); + Grammar.register0 wit_bindings (Tactic.bindings); +(* Grammar.register0 wit_hyp_location_flag; *) + Grammar.register0 wit_red_expr (Tactic.red_expr); + Grammar.register0 wit_tactic (Tactic.tactic); + Grammar.register0 wit_ltac (Tactic.tactic); + Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); + Grammar.register0 wit_destruction_arg (Tactic.destruction_arg); + () diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 deleted file mode 100644 index 32dbeaa4..00000000 --- a/parsing/pcoq.ml4 +++ /dev/null @@ -1,836 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*