diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | .merlin | 2 | ||||
| -rw-r--r-- | Makefile.build | 5 | ||||
| -rw-r--r-- | configure.ml | 20 | ||||
| -rw-r--r-- | grammar/argextend.mlp | 7 | ||||
| -rw-r--r-- | grammar/compat5.mlp | 23 | ||||
| -rw-r--r-- | grammar/compat5b.mlp | 23 | ||||
| -rw-r--r-- | grammar/gramCompat.mlp | 86 | ||||
| -rw-r--r-- | grammar/q_util.mli | 2 | ||||
| -rw-r--r-- | grammar/q_util.mlp | 10 | ||||
| -rw-r--r-- | grammar/tacextend.mlp | 17 | ||||
| -rw-r--r-- | grammar/vernacextend.mlp | 14 | ||||
| -rw-r--r-- | intf/extend.mli | 2 | ||||
| -rw-r--r-- | parsing/cLexer.ml4 | 108 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 48 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 421 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 17 | ||||
| -rw-r--r-- | parsing/g_prim.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/parsing.mllib | 1 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 228 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 72 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 5 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.ml4 | 35 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 8 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 4 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 2 |
29 files changed, 439 insertions, 729 deletions
diff --git a/.gitignore b/.gitignore index 64c49b008..371136fc7 100644 --- a/.gitignore +++ b/.gitignore @@ -121,7 +121,6 @@ ide/xml_lexer.ml g_*.ml ide/project_file.ml -parsing/compat.ml parsing/cLexer.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml @@ -44,4 +44,4 @@ B tools/coqdoc S dev B dev -PKG threads.posix +PKG threads.posix camlp5 diff --git a/Makefile.build b/Makefile.build index 01cc4d878..eeb648ba1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -272,11 +272,10 @@ endif ## Explicit dependencies for grammar stuff -GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi -GRAMCMO := grammar/gramCompat.cmo grammar/q_util.cmo \ +GRAMBASEDEPS := grammar/q_util.cmi +GRAMCMO := grammar/q_util.cmo \ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo -grammar/q_util.cmi : grammar/gramCompat.cmo grammar/argextend.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo diff --git a/configure.ml b/configure.ml index dfc6724a2..cc63fde70 100644 --- a/configure.ml +++ b/configure.ml @@ -310,10 +310,8 @@ let args_options = Arg.align [ "<dir> Specifies the ocamlfind command to use"; "-lablgtkdir", arg_string_option Prefs.lablgtkdir, "<dir> Specifies the path to the Lablgtk library"; - "-usecamlp5", Arg.Set Prefs.usecamlp5, - " Specifies to use camlp5 instead of camlp4"; - "-usecamlp4", Arg.Clear Prefs.usecamlp5, - " Specifies to use camlp4 instead of camlp5"; + "-usecamlp5", Arg.Unit (fun () -> ()), + " Deprecated"; "-camlp5dir", Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s), "<dir> Specifies where is the Camlp5 library and tells to use it"; @@ -561,7 +559,6 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with dir, camlp5o with Not_found -> let () = printf "No Camlp5 installation found." in - let () = printf "Looking for Camlp4 instead...\n" in raise NoCamlp5 let check_camlp5_version camlp5o = @@ -580,18 +577,7 @@ let config_camlpX () = let camlp5_version = check_camlp5_version camlp5o in "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version with NoCamlp5 -> - (* We now try to use Camlp4, either by explicit choice or - by lack of proper Camlp5 installation *) - let camlp4mod = "camlp4lib" in - let camlp4libdir = camllib/"camlp4" in - if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then - die "No Camlp4 installation found.\n"; - try - let camlp4orf = which_camlpX "camlp4orf" in - let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in - let camlp4_version = List.nth (string_split ' ' version_line) 2 in - "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version - with _ -> die "No Camlp4 installation found.\n" + die "No Camlp5 installation found.\n" let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX () diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index d0ab5d803..aaf3afe43 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -7,11 +7,13 @@ (************************************************************************) open Q_util -open GramCompat -let loc = CompatLoc.ghost +let loc = Ploc.dummy let default_loc = <:expr< Loc.ghost >> +let declare_str_items loc l = + MLast.StDcl (loc, Ploc.VaVal l) (* correspond to <:str_item< declare $list:l'$ end >> *) + let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function @@ -185,7 +187,6 @@ let declare_vernac_argument loc s pr cl = >> ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/grammar/compat5.mlp b/grammar/compat5.mlp deleted file mode 100644 index 8473a1fb7..000000000 --- a/grammar/compat5.mlp +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Adding a bit of camlp5 syntax to camlp4 for compatibility: - - GEXTEND ... becomes EXTEND ... -*) - -open Camlp4.PreCast - -let rec my_token_filter = parser - | [< '(KEYWORD "GEXTEND", loc); s >] -> - [< '(KEYWORD "EXTEND", loc); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) diff --git a/grammar/compat5b.mlp b/grammar/compat5b.mlp deleted file mode 100644 index 46802a825..000000000 --- a/grammar/compat5b.mlp +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Adding a bit of camlp5 syntax to camlp4 for compatibility: - - EXTEND ... becomes EXTEND Gram ... -*) - -open Camlp4.PreCast - -let rec my_token_filter = parser - | [< '(KEYWORD "EXTEND",_ as t); s >] -> - [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp deleted file mode 100644 index 6246da7bb..000000000 --- a/grammar/gramCompat.mlp +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Compatibility file depending on ocaml/camlp4 version *) - -(** Misc module emulation *) - -IFDEF CAMLP5 THEN - -module CompatLoc = struct - include Ploc - let ghost = dummy - let merge = encl -end - -ELSE - -module CompatLoc = Camlp4.PreCast.Loc - -END - -IFDEF CAMLP5 THEN - -module PcamlSig = struct end - -ELSE - -module PcamlSig = Camlp4.Sig -module Ast = Camlp4.PreCast.Ast -module Pcaml = Camlp4.PreCast.Syntax -module MLast = Ast - -END - -(** Compatibility with camlp5 strict mode *) -IFDEF CAMLP5 THEN - IFDEF STRICT THEN - let vala x = Ploc.VaVal x - ELSE - let vala x = x - END -ELSE - let vala x = x -END - -(** Fix a quotation difference in [str_item] *) - -let declare_str_items loc l = -IFDEF CAMLP5 THEN - MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *) -ELSE - Ast.stSem_of_list l -END - -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) - -IFDEF CAMLP5 THEN - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - -ELSE - -let make_fun loc cl = - let mk_when = function - | Some w -> w - | None -> Ast.ExNil loc - in - let mk_clause (patt,optwhen,expr) = - (* correspond to <:match_case< ... when ... -> ... >> *) - Ast.McArr (loc, patt, mk_when optwhen, expr) in - let init = mk_clause (default_patt loc) in - let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in - let l = List.fold_right add_clause cl init in - Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *) - -END diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 37ec1d56a..5b3eb3202 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open GramCompat (* necessary for camlp4 *) - type argument_type = | ListArgType of argument_type | OptArgType of argument_type diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 0dd096ef7..8b930cf36 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -8,8 +8,6 @@ (* This file defines standard combinators to build ml expressions *) -open GramCompat - type argument_type = | ListArgType of argument_type | OptArgType of argument_type @@ -33,17 +31,17 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) - l (let loc = CompatLoc.ghost in <:expr< [] >>) + l (let loc = Ploc.dummy in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> (* We don't give location for tactic quotation! *) -let loc = CompatLoc.ghost +let loc = Ploc.dummy let mlexpr_of_bool = function diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 8c0614a7b..f57be9022 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -10,7 +10,15 @@ open Q_util open Argextend -open GramCompat + +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, Ploc.VaVal None, <:expr< failwith "Extension: cannot occur" >>) + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, Ploc.VaVal l) (* correspond to <:expr< fun [ $list:l$ ] >> *) let dloc = <:expr< Loc.ghost >> @@ -41,11 +49,11 @@ let rec make_let raw e = function let make_clause (pt,_,e) = (make_patt pt, - vala None, + Ploc.VaVal None, make_let false e pt) let make_fun_clauses loc s l = - let map c = GramCompat.make_fun loc [make_clause c] in + let map c = make_fun loc [make_clause c] in mlexpr_of_list map l let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> @@ -100,7 +108,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with whole-prof tactics like [shelve_unifiable]. *) <:expr< fun _ $lid:"ist"$ -> $tac$ >> | _ -> - let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in + let f = make_fun loc [patt, Ploc.VaVal None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> in (** Arguments are not passed directly to the ML tactic in the TacML node, @@ -129,7 +137,6 @@ let declare_tactic loc tacname ~level classification clause = match clause with ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 04b117fba..d4857b1df 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -11,7 +11,6 @@ open Q_util open Argextend open Tacextend -open GramCompat type rule = { r_head : string option; @@ -37,7 +36,7 @@ let rec make_let e = function let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - vala None, + Ploc.VaVal None, make_let e pt) (* To avoid warnings *) @@ -55,11 +54,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - vala None, + Ploc.VaVal None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - vala None, + Ploc.VaVal None, <:expr< fun () -> $cg$ $str:s$ >>) | None, None -> prerr_endline (("Vernac entry \""^s^"\" misses a classifier. "^ @@ -82,7 +81,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = ("Specific classifiers have precedence over global "^ "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, - vala None, + Ploc.VaVal None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = @@ -91,13 +90,13 @@ let make_fun_clauses loc s l = | None -> false | Some () -> true in - let cl = GramCompat.make_fun loc [make_clause c] in + let cl = make_fun loc [make_clause c] in <:expr< ($mlexpr_of_bool depr$, $cl$)>> in mlexpr_of_list map l let make_fun_classifiers loc s c l = - let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in + let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl let make_prod_item = function @@ -128,7 +127,6 @@ let declare_command loc s c nt cl = } >> ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/intf/extend.mli b/intf/extend.mli index 7ba332f70..99401d06f 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -8,7 +8,7 @@ (** Entry keys for constr notations *) -type 'a entry = 'a Compat.GrammarMake(CLexer).entry +type 'a entry = 'a Grammar.GMake(CLexer).Entry.e type side = Left | Right diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 3b84eaa81..6d259e1b1 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -9,7 +9,17 @@ open Pp open Util open Tok -open Compat + +let to_coqloc 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 (!@) = to_coqloc (* Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. *) @@ -110,11 +120,52 @@ module Error = struct end open Error -let err loc str = Loc.raise ~loc:(Compat.to_coqloc loc) (Error.E str) +let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) -(* Lexer conventions on tokens *) +(** Location utilities *) +let file_loc_of_file = function +| None -> "" +| Some f -> f + +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 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) + +(** Lexer conventions on tokens *) type token_kind = | Utf8Token of (Unicode.status * int) @@ -186,7 +237,7 @@ 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 + match unlocated lookup_utf8 Ploc.dummy s with | Utf8Token (_,n) -> njunk n s; loop_symb s | AsciiChar -> Stream.junk s; loop_symb s | EmptyStream -> () @@ -200,7 +251,7 @@ let check_ident str = | [< ' ('0'..'9' | ''') when intail; s >] -> loop_id true s | [< s >] -> - match unlocated lookup_utf8 Compat.CompatLoc.ghost s with + match unlocated lookup_utf8 Ploc.dummy s with | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s | Utf8Token (Unicode.IdentPart, n) when intail -> njunk n s; @@ -233,10 +284,10 @@ let remove_keyword str = let keywords () = ttree_elements !token_tree (* Freeze and unfreeze the state of the lexer *) -type frozen_t = ttree +type keyword_state = ttree -let freeze () = !token_tree -let unfreeze tt = (token_tree := tt) +let get_keyword_state () = !token_tree +let set_keyword_state tt = (token_tree := tt) (* The string buffering machinery *) @@ -621,8 +672,6 @@ let loct_add loct i loc = Hashtbl.add loct i loc 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 *) @@ -640,12 +689,12 @@ let token_text = function let func cs = let loct = loct_create () in - let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in + let cur_loc = ref (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; + cur_loc := after loc; loct_add loct i loc; Some tok) in (ts, loct_func loct) @@ -661,41 +710,6 @@ let lexer = { 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 = diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index e0fdf8cb5..1a1c302f2 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -6,27 +6,57 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This should be functional but it is not due to the interface *) val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool val keywords : unit -> CString.Set.t +type keyword_state +val set_keyword_state : keyword_state -> unit +val get_keyword_state : unit -> keyword_state + 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 +(* modtype Grammar.GLexerType: sig + type te val + lexer : te Plexing.lexer + end + +where + + type lexer 'te = + { tok_func : lexer_func 'te; + tok_using : pattern -> unit; + tok_removing : pattern -> unit; + tok_match : pattern -> 'te -> string; + tok_text : pattern -> string; + tok_comm : mutable option (list location) } + *) +include Grammar.GLexerType with type te = Tok.t + +module Error : sig + type t + exception E of t + val to_string : t -> string +end + +(* Mainly for comments state, etc... *) +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 + +(* Retrieve the comments lexed at a given location of the stream + currently being processeed *) +val extract_comments : int -> string list diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 deleted file mode 100644 index 4a36af2d8..000000000 --- a/parsing/compat.ml4 +++ /dev/null @@ -1,421 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Compatibility file depending on ocaml/camlp4 version *) - -(** Locations *) - -let file_loc_of_file = function -| None -> "" -| Some f -> f - -IFDEF CAMLP5 THEN - -module CompatLoc = struct - include Ploc - let ghost = dummy - let merge = encl -end - -exception Exc_located = Ploc.Exc - -let to_coqloc 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 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 - -module CompatLoc = Camlp4.PreCast.Loc - -exception Exc_located = CompatLoc.Exc_located - -let to_coqloc 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 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 - -let (!@) = to_coqloc - -(** Misc module emulation *) - -IFDEF CAMLP5 THEN - -module PcamlSig = struct end -module Token = Token -module CompatGramext = struct include Gramext type assoc = g_assoc end - -ELSE - -module PcamlSig = Camlp4.Sig -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 - -(** Signature of CLexer *) - -IFDEF CAMLP5 THEN - -module type LexerSig = sig - include Grammar.GLexerType with type te = Tok.t - module Error : sig - type t - 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 = 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 - -(** Signature and implementation of grammars *) - -IFDEF CAMLP5 THEN - -module type GrammarSig = sig - include Grammar.S with type te = Tok.t - type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - 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 -> 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 - -module GrammarMake (L:LexerSig) : GrammarSig = struct - include Grammar.GMake (L) - type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - 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,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 - let srules' = Gramext.srules - let parse_tokens_after_filter = Entry.parse_token -end - -ELSE - -module type GrammarSig = sig - include Camlp4.Sig.Grammar.Static - with module Loc = CompatLoc and type Token.t = Tok.t - type 'a entry = 'a Entry.t - type action = Action.t - 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 -> 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 - -module GrammarMake (L:LexerSig) : GrammarSig = struct - (* We need to refer to Coq's module Loc before it is hidden by include *) - let raise_coq_loc loc e = Loc.raise ~loc:(to_coqloc loc) e - include Camlp4.Struct.Grammar.Static.Make (L) - type 'a entry = 'a Entry.t - type action = Action.t - 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,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 *) - -(** - The lexer produces streams made of pairs in camlp4 *) - -let get_tok = IFDEF CAMLP5 THEN fun x -> x ELSE fst END - -(** - Gram.extend is more currified in camlp5 than in camlp4 *) - -IFDEF CAMLP5 THEN -let maybe_curry f x y = f (x,y) -let maybe_uncurry f (x,y) = f x y -ELSE -let maybe_curry f = f -let maybe_uncurry f = f -END - -(** Compatibility with camlp5 strict mode *) -IFDEF CAMLP5 THEN - IFDEF STRICT THEN - let vala x = Ploc.VaVal x - ELSE - let vala x = x - END -ELSE - let vala x = x -END - -(** Fix a quotation difference in [str_item] *) - -let declare_str_items loc l = -IFDEF CAMLP5 THEN - MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *) -ELSE - Ast.stSem_of_list l -END - -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) - -IFDEF CAMLP5 THEN - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - -ELSE - -let make_fun loc cl = - let mk_when = function - | Some w -> w - | None -> Ast.ExNil loc - in - let mk_clause (patt,optwhen,expr) = - (* correspond to <:match_case< ... when ... -> ... >> *) - Ast.McArr (loc, patt, mk_when optwhen, expr) in - let init = mk_clause (default_patt loc) in - let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in - let l = List.fold_right add_clause cl init in - Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *) - -END - -IFDEF CAMLP5 THEN -let warning_verbose = Gramext.warning_verbose -ELSE -(* 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/g_constr.ml4 b/parsing/g_constr.ml4 index c127e7880..05cb74ddc 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -12,7 +12,6 @@ open Constrexpr open Constrexpr_ops open Util open Tok -open Compat open Misctypes open Decl_kinds @@ -81,11 +80,11 @@ let err () = raise Stream.Failure let lpar_id_coloneq = Gram.Entry.of_parser "test_lpar_id_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT s -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":=" -> stream_njunk 3 strm; Names.Id.of_string s @@ -96,9 +95,9 @@ let lpar_id_coloneq = let impl_ident_head = Gram.Entry.of_parser "impl_ident_head" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "{" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT ("wf"|"struct"|"measure") -> err () | IDENT s -> stream_njunk 2 strm; @@ -109,15 +108,15 @@ let impl_ident_head = let name_colon = Gram.Entry.of_parser "name_colon" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | IDENT s -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | KEYWORD ":" -> stream_njunk 2 strm; Name (Names.Id.of_string s) | _ -> err ()) | KEYWORD "_" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | KEYWORD ":" -> stream_njunk 2 strm; Anonymous diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 2db91b8f8..2af4ed533 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Names open Libnames open Tok (* necessary for camlp4 *) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 4c5280538..7ca2e4a4f 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Constrexpr open Vernacexpr open Misctypes diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ded7a557c..71b93439b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Compat open CErrors open Util open Names @@ -407,7 +406,7 @@ let only_starredidentrefs = Gram.Entry.of_parser "test_only_starredidentrefs" (fun strm -> let rec aux n = - match get_tok (Util.stream_nth n strm) with + match Util.stream_nth n strm with | KEYWORD "." -> () | KEYWORD ")" -> () | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 0e1c79c91..2a73d7bc6 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,5 +1,4 @@ Tok -Compat CLexer Pcoq Egramml diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b8405ca8c..92d249e53 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -7,31 +7,203 @@ (************************************************************************) open Pp -open Compat open CErrors open Util open Extend open Genarg +let curry f x y = f (x, y) +let uncurry f (x,y) = f x y + +(** Location Utils *) +let to_coqloc 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 (!@) = to_coqloc + (** The parser of Coq *) +module G : sig + + include Grammar.S with type te = Tok.t + +(* where Grammar.S + +module type S = + sig + type te = 'x; + type parsable = 'x; + value parsable : Stream.t char -> parsable; + value tokens : string -> list (string * int); + value glexer : Plexing.lexer te; + value set_algorithm : parse_algorithm -> unit; + module Entry : + sig + type e 'a = 'y; + value create : string -> e 'a; + value parse : e 'a -> parsable -> 'a; + value parse_token : e 'a -> Stream.t te -> 'a; + value name : e 'a -> string; + value of_parser : string -> (Stream.t te -> 'a) -> e 'a; + value print : Format.formatter -> e 'a -> unit; + external obj : e 'a -> Gramext.g_entry te = "%identity"; + end + ; + module Unsafe : + sig + value gram_reinit : Plexing.lexer te -> unit; + value clear_entry : Entry.e 'a -> unit; + end + ; + value extend : + Entry.e 'a -> option Gramext.position -> + list + (option string * option Gramext.g_assoc * + list (list (Gramext.g_symbol te) * Gramext.g_action)) -> + unit; + value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; + end + *) + + type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action + type production_rule = symbol list * action + type single_extend_statment = + 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 -> 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 with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct + + include Grammar.GMake(CLexer) + + type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action + type production_rule = symbol list * action + type single_extend_statment = + string option * Gramext.g_assoc option * production_rule list + type extend_statment = + Gramext.position option * single_extend_statment list + type coq_parsable = parsable * CLexer.lexer_state ref + + let parsable ?file c = + let state = ref (CLexer.init_lexer_state file) in + CLexer.set_lexer_state !state; + let a = parsable c in + state := CLexer.release_lexer_state (); + (a,state) + + let action = Gramext.action + let entry_create = Entry.create + + let entry_parse e (p,state) = + CLexer.set_lexer_state !state; + try + let c = Entry.parse e p in + state := CLexer.release_lexer_state (); + c + with Ploc.Exc (loc,e) -> + CLexer.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 = + CLexer.set_lexer_state !state; + try + let a = f x in + state := CLexer.release_lexer_state (); + a + with e -> + CLexer.drop_lexer_state (); + raise e + + let entry_print ft x = Entry.print ft x + + (* Not used *) + let srules' = Gramext.srules + let parse_tokens_after_filter = Entry.parse_token + +end -module G = GrammarMake (CLexer) -let warning_verbose = Compat.warning_verbose +let warning_verbose = Gramext.warning_verbose let of_coq_assoc = function -| Extend.RightA -> CompatGramext.RightA -| Extend.LeftA -> CompatGramext.LeftA -| Extend.NonA -> CompatGramext.NonA +| Extend.RightA -> Gramext.RightA +| Extend.LeftA -> Gramext.LeftA +| Extend.NonA -> Gramext.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 +| 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 + +module Symbols : 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 + + 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 + + let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) + let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) + + 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 -module Symbols = GramextMake(G) + let snterml_level = function + | Gramext.Snterml (_, l) -> l + | _ -> failwith "snterml_level" + +end let camlp4_verbosity silent f x = let a = !warning_verbose in @@ -55,7 +227,7 @@ let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x (** 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)) +| Stop -> fun f -> G.action (fun loc -> f (!@ 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 @@ -121,10 +293,10 @@ let grammar_delete e reinit (pos,rls) = let a = of_coq_assoc a in let ext = of_coq_position ext in let lev = match pos with - | Some (CompatGramext.Level n) -> n + | Some (Gramext.Level n) -> n | _ -> assert false in - maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) + (G.extend e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -132,13 +304,13 @@ let grammar_delete e reinit (pos,rls) = 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 + let redo () = camlp4_verbosity false (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) + camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -147,13 +319,13 @@ module Gram = struct include G let extend e = - maybe_curry + curry (fun ext -> camlp4_state := (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> maybe_uncurry (G.extend e) ext))) + (fun () -> uncurry (G.extend e) ext))) :: !camlp4_state; - maybe_uncurry (G.extend e) ext) + 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. @@ -194,14 +366,14 @@ 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]); + 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]); + uncurry (Gram.extend e) (None, make_rule [symbs, act]); e (* Parse a string, does NOT check if the entire string was read @@ -345,13 +517,13 @@ module Vernac_ = let noedit_mode = gec_vernac "noedit_command" let () = - let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in + let act_vernac = Gram.action (fun v loc -> Some (to_coqloc 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) + uncurry (Gram.extend main_entry) (None, make_rule rule) let command_entry_ref = ref noedit_mode let command_entry = @@ -369,7 +541,7 @@ 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 + let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -418,9 +590,9 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command ta (* 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 +type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.keyword_state -let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ()) +let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) @@ -435,7 +607,7 @@ let unfreeze (grams, lex) = let n = number_of_entries undo in remove_grammars n; grammar_stack := common; - CLexer.unfreeze lex; + CLexer.set_keyword_state lex; List.iter extend_dyn_grammar (List.rev_map pi2 redo) (** No need to provide an init function : the grammar state is diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 6c148d393..4248db697 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -18,7 +18,73 @@ open Genredexpr (** The parser of Coq *) -module Gram : module type of Compat.GrammarMake(CLexer) +module Gram : sig + + include Grammar.S with type te = Tok.t + +(* Where Grammar.S is + +module type S = + sig + type te = 'x; + type parsable = 'x; + value parsable : Stream.t char -> parsable; + value tokens : string -> list (string * int); + value glexer : Plexing.lexer te; + value set_algorithm : parse_algorithm -> unit; + module Entry : + sig + type e 'a = 'y; + value create : string -> e 'a; + value parse : e 'a -> parsable -> 'a; + value parse_token : e 'a -> Stream.t te -> 'a; + value name : e 'a -> string; + value of_parser : string -> (Stream.t te -> 'a) -> e 'a; + value print : Format.formatter -> e 'a -> unit; + external obj : e 'a -> Gramext.g_entry te = "%identity"; + end + ; + module Unsafe : + sig + value gram_reinit : Plexing.lexer te -> unit; + value clear_entry : Entry.e 'a -> unit; + end + ; + value extend : + Entry.e 'a -> option Gramext.position -> + list + (option string * option Gramext.g_assoc * + list (list (Gramext.g_symbol te) * Gramext.g_action)) -> + unit; + value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; + end + +*) + + type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action + type production_rule = symbol list * action + type single_extend_statment = + 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 -> coq_parsable -> 'a + val entry_print : Format.formatter -> 'a entry -> unit + val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b + + (* Apparently not used *) + val srules' : production_rule list -> symbol + val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a + +end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e (** The parser of Coq is built from three kinds of rule declarations: @@ -242,3 +308,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list (** Recover the current stack of grammar extensions. *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b + +(** Location Utils *) +val to_coqloc : Ploc.t -> Loc.t +val (!@) : Ploc.t -> Loc.t diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 368b23be3..cf2e42d2c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -7,7 +7,6 @@ (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin -open Compat open Util open Term open Pp @@ -17,6 +16,7 @@ open Indfun open Genarg open Stdarg open Misctypes +open Pcoq open Pcoq.Prim open Pcoq.Constr open Pltac diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index fd33a779d..ece0adb07 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,7 +12,6 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp -open Compat open Constrexpr open Tacexpr open Misctypes @@ -68,9 +67,9 @@ let _ = let test_bracket_ident = Gram.Entry.of_parser "test_bracket_ident" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "[" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> () | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index fa01baab7..4b3ca80af 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -14,7 +14,6 @@ open Genredexpr open Constrexpr open Libnames open Tok -open Compat open Misctypes open Locus open Decl_kinds @@ -34,11 +33,11 @@ let err () = raise Stream.Failure let test_lpar_id_coloneq = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":=" -> () | _ -> err ()) | _ -> err ()) @@ -48,11 +47,11 @@ let test_lpar_id_coloneq = let test_lpar_id_rpar = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ")" -> () | _ -> err ()) | _ -> err ()) @@ -62,11 +61,11 @@ let test_lpar_id_rpar = let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ | INT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":=" -> () | _ -> err ()) | _ -> err ()) @@ -76,11 +75,11 @@ let test_lpar_idnum_coloneq = let test_lpar_id_colon = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":" -> () | _ -> err ()) | _ -> err ()) @@ -91,30 +90,30 @@ let check_for_coloneq = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = - match get_tok (List.last (Stream.npeek n strm)) with + match List.last (Stream.npeek n strm) with | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1) | KEYWORD "." -> err () | _ -> skip_to_rpar p (n+1) in let rec skip_names n = - match get_tok (List.last (Stream.npeek n strm)) with + match List.last (Stream.npeek n strm) with | IDENT _ | KEYWORD "_" -> skip_names (n+1) | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) | _ -> err () in let rec skip_binders n = - match get_tok (List.last (Stream.npeek n strm)) with + match List.last (Stream.npeek n strm) with | KEYWORD "(" -> skip_binders (skip_names (n+1)) | IDENT _ | KEYWORD "_" -> skip_binders (n+1) | KEYWORD ":=" -> () | _ -> err () in - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> skip_binders 2 | _ -> err ()) let lookup_at_as_comma = Gram.Entry.of_parser "lookup_at_as_comma" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD (","|"at"|"as") -> () | _ -> err ()) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 4d5594633..3d0232d94 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -10,7 +10,7 @@ (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = CLexer.freeze () ;; +let frozen_lexer = CLexer.get_keyword_state () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) @@ -1040,7 +1040,7 @@ let interp_open_constr ist gl gc = let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c let interp_term ist gl (_, c) = (interp_open_constr ist gl c) let pr_ssrterm _ _ _ = pr_term -let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with +let input_ssrtermkind strm = match stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' @@ -1057,8 +1057,6 @@ ARGUMENT EXTEND cpattern | [ "Qed" constr(c) ] -> [ mk_lterm c ] END -let (!@) = Compat.to_coqloc - GEXTEND Gram GLOBAL: cpattern; cpattern: [[ k = ssrtermkind; c = constr -> @@ -1444,6 +1442,6 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = CLexer.unfreeze frozen_lexer ;; +let () = CLexer.set_keyword_state frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 8e6f9ffb5..2282932d4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -255,7 +255,7 @@ let set_prompt prompt = (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot st = match Compat.get_tok (Stream.next st) with + let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () | Tok.EOI -> raise End_of_input | _ -> dot st @@ -270,7 +270,7 @@ let rec discard_to_dot () = try Gram.entry_parse parse_to_dot top_buffer.tokens with - | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot () + | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | End_of_input -> raise End_of_input | e when CErrors.noncritical e -> () diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index f1e0c48f0..2c99f35d4 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -27,7 +27,7 @@ exception EvaluatedError of std_ppcmds * exn option let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") |