diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:48 +0000 |
| commit | 1b089eb0231b4bd6d4cafb30f9e051bb53665978 (patch) | |
| tree | 489e0f8ce7b4a80db388c63219b9cf4380b7f185 | |
| parent | 259dde7928696593c2d3c6de474f5cf50fa4417d (diff) | |
Add (almost) compatibility with camlp4, without breaking support for camlp5
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
60 files changed, 1133 insertions, 808 deletions
diff --git a/Makefile.build b/Makefile.build index 42b2ee456..192092e4e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -97,9 +97,23 @@ $(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^ endef CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<` +ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) +else +CAMLP4USE=-D$(CAMLVERSION) +endif + +PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 + +ifeq ($(CAMLP4),camlp5) +SYSMOD:=str unix gramlib +else +SYSMOD:=str unix dynlink camlp4lib +endif + +SYSCMA:=$(addsuffix .cma,$(SYSMOD)) +SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) -PR_O := $(if $(READABLE_ML4),pr_o.cmo) ########################################################################### # Infrastructure for the rest of the Makefile @@ -202,12 +216,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(CHICKENOPT): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ $(SYSCMXA) $^ $(STRIP) $@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -216,13 +230,11 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) $(COQMKTOPBYTE): $(COQMKTOPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma\ - $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) $(COQMKTOPOPT): $(COQMKTOPCMO:.cmo=.cmx) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa\ - $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) @@ -239,11 +251,11 @@ scripts/tolink.ml: Makefile.build Makefile.common $(COQCBYTE): $(COQCCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) $(COQCOPT): $(COQCCMO:.cmo=.cmx) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) $(STRIP) $@ $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) @@ -464,7 +476,7 @@ $(COQDEPBOOT): tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml $(COQDEP): $(COQDEPCMO:.cmo=$(BESTOBJ)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), str unix gramlib) + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) $(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) $(SHOW)'OCAMLBEST -o $@' @@ -634,7 +646,7 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex dev/printers.cma: | dev/printers.mllib.d $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma gramlib.cma $^ -o test-printer + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $^ -linkall -a -o $@ diff --git a/Makefile.common b/Makefile.common index 9f44b3b6f..f4f6daf3f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -143,10 +143,6 @@ COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) -CLIBS:=unix.cma - -CAMLP4OBJS:=gramlib.cma - CONFIG:=config/coq_config.cmo BYTERUN:=$(addprefix kernel/byterun/, \ @@ -214,9 +210,6 @@ endif INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS)) -CMA:=$(CLIBS) $(CAMLP4OBJS) -CMXA:=$(CMA:.cma=.cmxa) - LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) diff --git a/checker/checker.ml b/checker/checker.ml index 9489dc94b..67691a706 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Util open System @@ -272,7 +273,7 @@ let rec explain_exn = function (* let ctx = Check.get_env() in hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) - | Stdpp.Exc_located (loc,exc) -> + | Loc.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn exc) diff --git a/config/Makefile.template b/config/Makefile.template index e29a4befe..8fb9e48c3 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -56,6 +56,7 @@ CAMLLIB="CAMLLIBDIRECTORY" CAMLHLIB="CAMLLIBDIRECTORY" # Camlp4 library directory (avoid CAMLP4LIB used on Windows) +CAMLP4=CAMLP4VARIANT CAMLP4O=CAMLP4TOOL CAMLP4COMPAT=CAMLP4COMPATFLAGS MYCAMLP4LIB="CAMLP4LIBDIRECTORY" @@ -57,6 +57,10 @@ usage () { printf "\tSpecifies the path to the OCaml library\n" echo "-lablgtkdir" printf "\tSpecifies the path to the Lablgtk library\n" + echo "-usecamlp5" + printf "\tSpecifies to use camlp5 instead of camlp4\n" + echo "-usecamlp4" + printf "\tSpecifies to use camlp4 instead of camlp5\n" echo "-camlp5dir" printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n" echo "-arch" @@ -141,6 +145,7 @@ with_doc=all with_doc_spec=no force_caml_version=no force_caml_version_spec=no +usecamlp5=yes COQSRC=`pwd` @@ -193,7 +198,12 @@ while : ; do -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes lablgtkdir="$2" shift;; + -usecamlp5|--usecamlp5) + usecamlp5=yes;; + -usecamlp4|--usecamlp4) + usecamlp5=no;; -camlp5dir|--camlp5dir) + usecamlp5=yes camlp5dir="$2" shift;; -arch|--arch) arch_spec=yes @@ -479,77 +489,81 @@ esac # Camlp4 / Camlp5 configuration -if [ "$camlp5dir" != "" ]; then +# Assume that camlp(4|5) binaries are at the same place as ocaml ones +# (this should become configurable some day) +CAMLP4BIN=${CAMLBIN} + +if [ "$usecamlp5" = "yes" ]; then CAMLP4=camlp5 - CAMLP4LIB=$camlp5dir - if [ ! -f $camlp5dir/camlp5.cma ]; then - echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)." + CAMLP4MOD=gramlib + if [ "$camlp5dir" != "" ]; then + if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then + CAMLP4LIB=$camlp5dir + FULLCAMLP4LIB=$camlp5dir + else + echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)." + echo "Configuration script failed!" + exit 1 + fi + elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then + CAMLP4LIB=+camlp5 + FULLCAMLP4LIB=${CAMLLIB}/camlp5 + elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then + CAMLP4LIB=+site-lib/camlp5 + FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5 + else + echo "Objective Caml $CAMLVERSION found but no Camlp5 installed." echo "Configuration script failed!" exit 1 fi + camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then - echo "Error: Camlp5 found, but in strict mode!" - echo "Please compile Camlp5 in transitional mode." + if [ "`$camlp4oexec -pmode 2>&1`" != "transitional" ]; then + echo "Error: $camlp4oexec not found, or not in transitional mode!" + echo "Configuration script failed!" exit 1 fi -else - case $CAMLTAG in - OCAML31*) - if [ -x "${CAMLLIB}/camlp5" ]; then - CAMLP4LIB=+camlp5 - elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then - CAMLP4LIB=+site-lib/camlp5 - else - echo "Objective Caml $CAMLVERSION found but no Camlp5 installed." - echo "Configuration script failed!" - exit 1 - fi - CAMLP4=camlp5 - camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then - echo "Error: Camlp5 found, but in strict mode!" - echo "Please compile Camlp5 in transitional mode." - exit 1 - fi - ;; - *) - CAMLP4=camlp4 - CAMLP4LIB=+camlp4 - ;; + case `$camlp4oexec -v 2>&1` in + *4.0*|*5.00*) + echo "Camlp5 version < 5.01 not supported." + echo "Configuration script failed!" + exit 1;; esac -fi - -if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then - echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK." - echo "Configuration script failed!" - exit 1 -fi +else # let's use camlp4 + CAMLP4=camlp4 + CAMLP4MOD=camlp4lib + CAMLP4LIB=+camlp4 + FULLCAMLP4LIB=${CAMLLIB}/camlp4 -case $CAMLP4LIB in - +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;; - *) FULLCAMLP4LIB=$CAMLP4LIB;; -esac + if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then + echo "Objective Caml $CAMLVERSION found but no Camlp4 installed." + echo "Configuration script failed!" + exit 1 + fi -# Assume that camlp(4|5) binaries are at the same place as ocaml ones -# (this should become configurable some day) -CAMLP4BIN=${CAMLBIN} + camlp4oexec=${camlp4oexec}rf + if [ "`$camlp4oexec 2>&1`" != "" ]; then + echo "Error: $camlp4oexec not found or not executable." + echo "Configuration script failed!" + exit 1 + fi +fi # do we have a native compiler: test of ocamlopt and its version if [ "$best_compiler" = "opt" ] ; then if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` - if [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then + if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cmxa" ]; then best_compiler=byte echo "Cannot find native-code $CAMLP4," echo "only the bytecode version of Coq will be available." else - if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then - echo "Native and bytecode compilers do not have the same version!" - fi - echo "You have native-code compilation. Good!" + if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then + echo "Native and bytecode compilers do not have the same version!" + fi + echo "You have native-code compilation. Good!" fi else best_compiler=byte @@ -1049,6 +1063,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \ -e "s|CAMLTAG|$CAMLTAG|" \ + -e "s|CAMLP4VARIANT|$CAMLP4|" \ -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ -e "s|CAMLP4TOOL|$camlp4oexec|" \ diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 21a690f95..e64b86a81 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -405,7 +405,7 @@ let _ = extend_vernac_command_grammar "PrintConstr" None [[GramTerminal "PrintConstr"; GramNonTerminal - (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + (dummy_loc,ConstrArgType,Aentry ("constr","constr"), Some (Names.id_of_string "c"))]] let _ = @@ -422,7 +422,7 @@ let _ = extend_vernac_command_grammar "PrintPureConstr" None [[GramTerminal "PrintPureConstr"; GramNonTerminal - (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + (dummy_loc,ConstrArgType,Aentry ("constr","constr"), Some (Names.id_of_string "c"))]] (* Setting printer of unbound global reference *) diff --git a/ide/coq.ml b/ide/coq.ml index 2338a8747..d2a2088d6 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -23,6 +23,7 @@ open Reductionops open Termops open Namegen open Ideutils +open Compat type coqtop = unit @@ -88,7 +89,7 @@ let is_in_loadpath coqtop dir = Library.is_in_load_paths (System.physical_path_of_string dir) let user_error_loc l s = - raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) + raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s))) let known_options = ref [] @@ -439,7 +440,7 @@ let forbid_vernac blacklist (loc,vernac) = let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e - | Stdpp.Exc_located (_,e) -> is_pervasive_exn e + | Loc.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e | _ -> false @@ -452,7 +453,7 @@ let print_toplevel_error exc = in let (loc,exc) = match exc with - | Stdpp.Exc_located (loc, ie) -> (Some loc),ie + | Loc.Exc_located (loc, ie) -> (Some loc),ie | Error_in_file (s, (_,fname, loc), ie) -> None, ie | _ -> dloc,exc in diff --git a/lib/compat.ml4 b/lib/compat.ml4 index c37758152..aba272045 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -8,19 +8,221 @@ (** Compatibility file depending on ocaml/camlp4 version *) +(** Locations *) + +IFDEF CAMLP5 THEN + +module Loc = struct + include Ploc + exception Exc_located = Exc + let ghost = dummy + let merge = encl +end + +let make_loc = Loc.make_unlined +let unloc loc = (Loc.first_pos loc, Loc.last_pos loc) + +ELSE + +module Loc = Camlp4.PreCast.Loc + +let make_loc (start,stop) = + Loc.of_tuple ("", 0, 0, start, 0, 0, stop, false) +let unloc loc = (Loc.start_off loc, Loc.stop_off loc) + +END + +(** Misc module emulation *) + IFDEF CAMLP5 THEN -type loc = Stdpp.location -let dummy_loc = Stdpp.dummy_loc -let make_loc = Stdpp.make_loc -let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc -let join_loc loc1 loc2 = - if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc - else Stdpp.encl_loc loc1 loc2 -type lexer = Tok.t Token.glexer +module PcamlSig = struct 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 + +END + -ELSE (* official camlp4 of ocaml >= 3.10 *) +(** Grammar auxiliary types *) + +IFDEF CAMLP5 THEN +type gram_assoc = Gramext.g_assoc = NonA | RightA | LeftA +type gram_position = Gramext.position = + | First + | Last + | Before of string + | After of string + | Like of string (** dont use it, not in camlp4 *) + | Level of string +ELSE +type gram_assoc = PcamlSig.Grammar.assoc = NonA | RightA | LeftA +type gram_position = PcamlSig.Grammar.position = + | First + | Last + | Before of string + | After of string + | Level of string +END + + +(** Signature of Lexer *) + +IFDEF CAMLP5 THEN + +module type LexerSig = sig + include Grammar.GLexerType with type te = Tok.t + module Error : sig + type t + exception E of t + end +end + +ELSE + +module type LexerSig = + Camlp4.Sig.Lexer with module Loc = Loc and type Token.t = Tok.t + +END + +(** Signature and implementation of grammars *) + +IFDEF CAMLP5 THEN -TODO +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 * gram_assoc option * production_rule list + type extend_statment = + gram_position option * single_extend_statment list + val action : 'a -> action + val entry_create : string -> 'a entry + val entry_parse : 'a entry -> parsable -> 'a + val entry_print : 'a entry -> unit + 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 * gram_assoc option * production_rule list + type extend_statment = + gram_position option * single_extend_statment list + let action = Gramext.action + let entry_create = Entry.create + let entry_parse = Entry.parse + let entry_print = Entry.print + 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 = Loc and type Token.t = Tok.t + type 'a entry = 'a Entry.t + type action = Action.t + type parsable + val parsable : char Stream.t -> parsable + val action : 'a -> action + val entry_create : string -> 'a entry + val entry_parse : 'a entry -> parsable -> 'a + val entry_print : 'a entry -> unit + val srules' : production_rule list -> symbol +end + +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 + let action = Action.mk + let entry_create = Entry.mk + let entry_parse e s = parse e (*FIXME*)Loc.ghost s + let entry_print x = Entry.print Format.std_formatter x + let srules' = srules (entry_create "dummy") +end + +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 + + +(** Fix a quotation difference in [str_item] *) + +let declare_str_items loc l = + let l' = <:str_item< open Pcoq >> :: <:str_item< open Extrawit >> :: l in +IFDEF CAMLP5 THEN + MLast.StDcl (loc,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< _ >>, None, <:expr< failwith "Extension: cannot occur" >>) + +IFDEF CAMLP5 THEN + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc,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 + +(** 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 diff --git a/lib/util.ml b/lib/util.ml index d08727d27..af5f2e33c 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -7,6 +7,7 @@ (***********************************************************************) open Pp +open Compat (* Errors *) @@ -27,17 +28,17 @@ let todo s = prerr_string ("TODO: "^s^"\n") exception Timeout -type loc = Compat.loc -let dummy_loc = Compat.dummy_loc -let unloc = Compat.unloc -let make_loc = Compat.make_loc -let join_loc = Compat.join_loc +type loc = Loc.t +let dummy_loc = Loc.ghost +let join_loc = Loc.merge +let make_loc = make_loc +let unloc = unloc (* raising located exceptions *) type 'a located = loc * 'a -let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) -let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) -let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) +let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm)) +let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm)) +let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s) let located_fold_left f x (_,a) = f x a let located_iter2 f (_,a) (_,b) = f a b diff --git a/lib/util.mli b/lib/util.mli index 9cef982fb..98d2b6cf9 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -7,6 +7,7 @@ **********************************************************************) open Pp +open Compat (** This module contains numerous utility functions on strings, lists, arrays, etc. *) @@ -36,17 +37,18 @@ val todo : string -> unit exception Timeout -type loc = Compat.loc +type loc = Loc.t type 'a located = loc * 'a val unloc : loc -> int * int val make_loc : int * int -> loc val dummy_loc : loc +val join_loc : loc -> loc -> loc + val anomaly_loc : loc * string * std_ppcmds -> 'a val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a -val join_loc : loc -> loc -> loc val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit diff --git a/library/nametab.ml b/library/nametab.ml index 4bb9f104d..0172048af 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -7,6 +7,7 @@ (************************************************************************) open Util +open Compat open Pp open Names open Libnames @@ -18,10 +19,10 @@ exception GlobalizationError of qualid exception GlobalizationConstantError of qualid let error_global_not_found_loc loc q = - Stdpp.raise_with_loc loc (GlobalizationError q) + Loc.raise loc (GlobalizationError q) let error_global_constant_not_found_loc loc q = - Stdpp.raise_with_loc loc (GlobalizationConstantError q) + Loc.raise loc (GlobalizationConstantError q) let error_global_not_found q = raise (GlobalizationError q) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index fd4952a52..e156bdc26 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -8,10 +8,10 @@ open Genarg open Q_util -open Q_coqast open Egrammar +open Pcoq +open Compat -let join_loc = Util.join_loc let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> @@ -92,16 +92,16 @@ let rec make_wit loc = function let make_act loc act pil = let rec make = function - | [] -> <:expr< Gramext.action (fun loc -> ($act$ : 'a)) >> + | [] -> <:expr< Gram.action (fun loc -> ($act$ : 'a)) >> | GramNonTerminal (_,t,_,Some p) :: tl -> let p = Names.string_of_id p in <:expr< - Gramext.action + Gram.action (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) >> | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl -> - <:expr< Gramext.action (fun _ -> $make tl$) >> in + <:expr< Gram.action (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function @@ -145,13 +145,13 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = let rawwit = <:expr< $lid:"rawwit_"^s$ >> in let globwit = <:expr< $lid:"globwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in - <:str_item< - declare - open Pcoq; - open Extrawit; + declare_str_items loc + [ <:str_item< value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) = - Genarg.create_arg $se$; - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; + Genarg.create_arg $se$ >>; + <:str_item< + value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + <:str_item< do { Tacinterp.add_interp_genarg $se$ ((fun e x -> (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))), @@ -159,14 +159,13 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))), (fun subst x -> (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))))); - Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None - [(None, None, $rules$)]; + Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) + (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $lid:rawpr$) ($globwit$, $lid:globpr$) - ($wit$, $lid:pr$); - end - >> + ($wit$, $lid:pr$) } + >> ] let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in @@ -177,31 +176,31 @@ let declare_vernac_argument loc s pr cl = let pr_rules = match pr with | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in - <:str_item< - declare - open Pcoq; - open Extrawit; + declare_str_items loc + [ <:str_item< value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel), ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel), - $lid:"rawwit_"^s$) = Genarg.create_arg $se$; - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; - Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None - [(None, None, $rules$)]; + $lid:"rawwit_"^s$) = Genarg.create_arg $se$ >>; + <:str_item< + value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + <:str_item< do { + Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) + (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $pr_rules$) ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer") - ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer"); - end - >> + ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer") } + >> ] open Vernacexpr open Pcoq open Pcaml +open PcamlSig EXTEND GLOBAL: str_item; str_item: - [ [ "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; + [ [ "ARGUMENT"; "EXTEND"; s = entry_name; "TYPED"; "AS"; typ = argtype; "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; @@ -216,15 +215,11 @@ EXTEND "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> - if String.capitalize s = s then - failwith "Argument entry names must be lowercase"; declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l - | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; + | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name; pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> - if String.capitalize s = s then - failwith "Argument entry names must be lowercase"; declare_vernac_argument loc s pr l ] ] ; argtype: @@ -253,5 +248,10 @@ EXTEND GramTerminal s ] ] ; + entry_name: + [ [ s = LIDENT -> s + | UIDENT -> failwith "Argument entry names must be lowercase" + ] ] + ; END diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index a07c52e84..a32bfdec4 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Compat open Util open Pcoq open Extend @@ -67,25 +68,25 @@ let make_constr_action (f : loc -> constr_expr action_env -> constr_expr) pil = let rec make (env,envlist as fullenv : constr_expr action_env) = function | [] -> - Gramext.action (fun loc -> f loc fullenv) + Gram.action (fun loc -> f loc fullenv) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullenv tl) + Gram.action (fun _ -> make fullenv tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) (match typ with | (ETConstr _| ETOther _) -> - Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl) + Gram.action (fun (v:constr_expr) -> make (v :: env, envlist) tl) | ETReference -> - Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl) + Gram.action (fun (v:reference) -> make (CRef v :: env, envlist) tl) | ETName -> - Gramext.action (fun (na:name located) -> + Gram.action (fun (na:name located) -> make (constr_expr_of_name na :: env, envlist) tl) | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> + Gram.action (fun (v:Bigint.bigint) -> make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl) | ETConstrList (_,n) -> - Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl) + Gram.action (fun (v:constr_expr list) -> make (env, v::envlist) tl) | ETPattern -> failwith "Unexpected entry of type cases pattern") | GramConstrListMark (n,b) :: tl -> @@ -100,26 +101,26 @@ let make_cases_pattern_action (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil = let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function | [] -> - Gramext.action (fun loc -> f loc fullenv) + Gram.action (fun loc -> f loc fullenv) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullenv tl) + Gram.action (fun _ -> make fullenv tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) (match typ with | ETConstr _ -> (* pattern non-terminal *) - Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) + Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) | ETReference -> - Gramext.action (fun (v:reference) -> + Gram.action (fun (v:reference) -> make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl) | ETName -> - Gramext.action (fun (na:name located) -> + Gram.action (fun (na:name located) -> make (cases_pattern_expr_of_name na :: env, envlist) tl) | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> + Gram.action (fun (v:Bigint.bigint) -> make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl) | ETConstrList (_,_) -> - Gramext.action (fun (vl:cases_pattern_expr list) -> + Gram.action (fun (vl:cases_pattern_expr list) -> make (env, vl :: envlist) tl) | (ETPattern | ETOther _) -> failwith "Unexpected entry of type cases pattern or other") @@ -143,17 +144,18 @@ let rec make_constr_prod_item assoc from forpat = function [] let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = - let entry = + let entry = if forpat then weaken_entry Constr.pattern else weaken_entry Constr.operconstr in - grammar_extend entry pos reinit [(name, p4assoc, [])] + grammar_extend entry reinit (pos,[(name, p4assoc, [])]) let pure_sublevels level symbs = - map_succeed (function - | Gramext.Snterml (_,n) when Some (int_of_string n) <> level -> - int_of_string n - | _ -> - failwith "") symbs + map_succeed + (function s -> + let i = level_of_snterml s in + if level = Some i then failwith ""; + i) + symbs let extend_constr (entry,level) (n,assoc) mkact forpat rules = List.iter (fun pt -> @@ -162,7 +164,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = let needed_levels = register_empty_levels forpat pure_sublevels in let pos,p4assoc,name,reinit = find_position forpat assoc level in List.iter (prepare_empty_levels forpat) needed_levels; - grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]) rules + grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])])) rules let extend_constr_notation (n,assoc,ntn,rules) = (* Add the notation in constr *) @@ -182,11 +184,11 @@ let make_generic_action (f:loc -> ('b * raw_generic_argument) list -> 'a) pil = let rec make env = function | [] -> - Gramext.action (fun loc -> f loc env) + Gram.action (fun loc -> f loc env) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gram.action (fun _ -> make env tl) | Some (p, t) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in + Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) let make_rule univ f g pt = @@ -200,7 +202,7 @@ let make_rule univ f g pt = type grammar_prod_item = | GramTerminal of string | GramNonTerminal of - loc * argument_type * Gram.te prod_entry_key * identifier option + loc * argument_type * prod_entry_key * identifier option let make_prod_item = function | GramTerminal s -> (gram_token_of_string s, None) @@ -213,7 +215,8 @@ let extend_tactic_grammar s gl = let univ = get_univ "tactic" in let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in let rules = List.map (make_rule univ mkact make_prod_item) gl in - Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)] + maybe_uncurry (Gram.extend Tactic.simple_tactic) + (None,[(None, None, List.rev rules)]) (* Vernac grammar extensions *) @@ -226,7 +229,7 @@ let extend_vernac_command_grammar s nt gl = let univ = get_univ "vernac" in let mkact loc l = VernacExtend (s,List.map snd l) in let rules = List.map (make_rule univ mkact make_prod_item) gl in - Gram.extend nt None [(None, None, List.rev rules)] + maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)]) (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) @@ -237,7 +240,7 @@ let get_tactic_entry n = else if n = 5 then weaken_entry Tactic.binder_tactic, None else if 1<=n && n<5 then - weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) + weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -261,13 +264,13 @@ let add_tactic_entry (key,lev,prods,tac) = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule univ (mkact key tac) make_prod_item prods in synchronize_level_positions (); - grammar_extend entry pos None [(None, None, List.rev [rules])] + grammar_extend entry None (pos,[(None, None, List.rev [rules])]) (**********************************************************************) (** State of the grammar extensions *) type notation_grammar = - int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list + int * gram_assoc option * notation * grammar_constr_prod_item list list type all_grammar_command = | Notation of (precedence * tolerability list) * notation_grammar diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 874aed570..a0004ce38 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,6 +6,7 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) +open Compat open Util open Names open Topconstr @@ -32,14 +33,14 @@ type grammar_constr_prod_item = concat with last parsed list if true *) type notation_grammar = - int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list + int * gram_assoc option * notation * grammar_constr_prod_item list list (** For tactic and vernac notations *) type grammar_prod_item = | GramTerminal of string | GramNonTerminal of loc * argument_type * - Gram.te prod_entry_key * identifier option + prod_entry_key * identifier option (** Adding notations *) @@ -55,7 +56,7 @@ val extend_tactic_grammar : string -> grammar_prod_item list list -> unit val extend_vernac_command_grammar : - string -> vernac_expr Gram.Entry.e option -> grammar_prod_item list list -> unit + string -> vernac_expr Gram.entry option -> grammar_prod_item list list -> unit val get_extend_vernac_grammars : unit -> (string * grammar_prod_item list list) list diff --git a/parsing/extend.ml b/parsing/extend.ml index cc3551d32..4674a7c90 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -6,35 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util -(**********************************************************************) -(* General entry keys *) - -(* This intermediate abstract representation of entries can *) -(* both be reified into mlexpr for the ML extensions and *) -(* dynamically interpreted as entries for the Coq level extensions *) - -type 'a prod_entry_key = - | Alist1 of 'a prod_entry_key - | Alist1sep of 'a prod_entry_key * string - | Alist0 of 'a prod_entry_key - | Alist0sep of 'a prod_entry_key * string - | Aopt of 'a prod_entry_key - | Amodifiers of 'a prod_entry_key - | Aself - | Anext - | Atactic of int - | Agram of 'a Gramext.g_entry - | Aentry of string * string - -(**********************************************************************) -(* Entry keys for constr notations *) +(** Entry keys for constr notations *) type side = Left | Right type production_position = - | BorderProd of side * Gramext.g_assoc option + | BorderProd of side * gram_assoc option | InternalProd type production_level = @@ -48,14 +28,17 @@ type ('lev,'pos) constr_entry_key_gen = | ETOther of string * string | ETConstrList of ('lev * 'pos) * Tok.t list -(* Entries level (left-hand-side of grammar rules) *) +(** Entries level (left-hand-side of grammar rules) *) + type constr_entry_key = (int,unit) constr_entry_key_gen -(* Entries used in productions (in right-hand-side of grammar rules) *) +(** Entries used in productions (in right-hand-side of grammar rules) *) + type constr_prod_entry_key = (production_level,production_position) constr_entry_key_gen -(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) +(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) + type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen diff --git a/parsing/extend.mli b/parsing/extend.mli index 99b83785c..597ff69a5 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -6,35 +6,14 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -open Util - -(********************************************************************* - General entry keys *) - -(** This intermediate abstract representation of entries can - both be reified into mlexpr for the ML extensions and - dynamically interpreted as entries for the Coq level extensions *) - -type 'a prod_entry_key = - | Alist1 of 'a prod_entry_key - | Alist1sep of 'a prod_entry_key * string - | Alist0 of 'a prod_entry_key - | Alist0sep of 'a prod_entry_key * string - | Aopt of 'a prod_entry_key - | Amodifiers of 'a prod_entry_key - | Aself - | Anext - | Atactic of int - | Agram of 'a Gramext.g_entry - | Aentry of string * string - -(********************************************************************* - Entry keys for constr notations *) +open Compat + +(** Entry keys for constr notations *) type side = Left | Right type production_position = - | BorderProd of side * Gramext.g_assoc option + | BorderProd of side * gram_assoc option | InternalProd type production_level = @@ -48,14 +27,17 @@ type ('lev,'pos) constr_entry_key_gen = | ETOther of string * string | ETConstrList of ('lev * 'pos) * Tok.t list -(* Entries level (left-hand-side of grammar rules) *) +(** Entries level (left-hand-side of grammar rules) *) + type constr_entry_key = (int,unit) constr_entry_key_gen -(* Entries used in productions (in right-hand-side of grammar rules) *) +(** Entries used in productions (in right-hand-side of grammar rules) *) + type constr_prod_entry_key = (production_level,production_position) constr_entry_key_gen -(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) +(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) + type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9ce65226d..ef18ad4eb 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -17,6 +17,7 @@ open Libnames open Topconstr open Util open Tok +open Compat let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; @@ -74,11 +75,11 @@ let err () = raise Stream.Failure let lpar_id_coloneq = Gram.Entry.of_parser "test_lpar_id_coloneq" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD "(" -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | IDENT s -> - (match stream_nth 2 strm with + (match get_tok (stream_nth 2 strm) with | KEYWORD ":=" -> stream_njunk 3 strm; Names.id_of_string s @@ -89,9 +90,9 @@ let lpar_id_coloneq = let impl_ident = Gram.Entry.of_parser "impl_ident" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD "{" -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | IDENT ("wf"|"struct"|"measure") -> err () | IDENT s -> stream_njunk 2 strm; @@ -102,9 +103,9 @@ let impl_ident = let ident_colon = Gram.Entry.of_parser "ident_colon" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | IDENT s -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | KEYWORD ":" -> stream_njunk 2 strm; Names.id_of_string s @@ -114,9 +115,9 @@ let ident_colon = let ident_with = Gram.Entry.of_parser "ident_with" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | IDENT s -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | KEYWORD "with" -> stream_njunk 2 strm; Names.id_of_string s diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index bfdd0773a..6ea55f874 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -15,6 +15,7 @@ open Vernacexpr open Pcoq open Prim open Tactic +open Tok let fail_default_value = ArgArg 0 diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index b1a2fa54b..9b962e823 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -10,6 +10,8 @@ open Pcoq open Names open Libnames open Topconstr +open Tok +open Compat let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] let _ = List.iter Lexer.add_keyword prim_kw @@ -41,7 +43,7 @@ GEXTEND Gram [ [ s = IDENT -> id_of_string s ] ] ; pattern_ident: - [ [ s = LEFTQMARK; id = ident -> id ] ] + [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: [ [ id = pattern_ident -> (loc, id) ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index dfb59a19d..aef2f05eb 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -15,6 +15,7 @@ open Topconstr open Vernacexpr open Prim open Constr +open Tok let thm_token = G_vernac.thm_token @@ -29,7 +30,7 @@ GEXTEND Gram ; opt_hintbases: [ [ -> [] - | ":"; l = LIST1 IDENT -> l ] ] + | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b39ea5770..0bff5ca8b 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -16,6 +16,7 @@ open Topconstr open Libnames open Termops open Tok +open Compat let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] @@ -29,11 +30,11 @@ let err () = raise Stream.Failure let test_lpar_id_coloneq = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD "(" -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | IDENT _ -> - (match stream_nth 2 strm with + (match get_tok (stream_nth 2 strm) with | KEYWORD ":=" -> () | _ -> err ()) | _ -> err ()) @@ -43,11 +44,11 @@ let test_lpar_id_coloneq = let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD "(" -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | IDENT _ | INT _ -> - (match stream_nth 2 strm with + (match get_tok (stream_nth 2 strm) with | KEYWORD ":=" -> () | _ -> err ()) | _ -> err ()) @@ -57,11 +58,11 @@ let test_lpar_idnum_coloneq = let test_lpar_id_colon = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD "(" -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | IDENT _ -> - (match stream_nth 2 strm with + (match get_tok (stream_nth 2 strm) with | KEYWORD ":" -> () | _ -> err ()) | _ -> err ()) @@ -72,33 +73,33 @@ let check_for_coloneq = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = - match list_last (Stream.npeek n strm) with + match get_tok (list_last (Stream.npeek n strm)) with | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) | KEYWORD ")" -> if 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 list_last (Stream.npeek n strm) with + match get_tok (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 list_last (Stream.npeek n strm) with + match get_tok (list_last (Stream.npeek n strm)) with | KEYWORD "(" -> skip_binders (skip_names (n+1)) | IDENT _ | KEYWORD "_" -> skip_binders (n+1) | KEYWORD ":=" -> () | _ -> err () in - match Stream.npeek 1 strm with - | [KEYWORD "("] -> skip_binders 2 + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> skip_binders 2 | _ -> err ()) let guess_lpar_ipat s strm = - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD "(" -> - (match stream_nth 1 strm with + (match get_tok (stream_nth 1 strm) with | KEYWORD ("("|"[") -> () | IDENT _ -> - (match stream_nth 2 strm with + (match get_tok (stream_nth 2 strm) with | KEYWORD s' when s = s' -> () | _ -> err ()) | _ -> err ()) @@ -113,7 +114,7 @@ let guess_lpar_colon = let lookup_at_as_coma = Gram.Entry.of_parser "lookup_at_as_coma" (fun strm -> - match stream_nth 0 strm with + match get_tok (stream_nth 0 strm) with | KEYWORD (","|"at"|"as") -> () | _ -> err ()) @@ -450,7 +451,7 @@ GEXTEND Gram ; hintbases: [ [ "with"; "*" -> None - | "with"; l = LIST1 IDENT -> Some l + | "with"; l = LIST1 [ x = IDENT -> x] -> Some l | -> Some [] ] ] ; auto_using: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e213660d9..cbeb7a01e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -10,6 +10,8 @@ open Pp +open Compat +open Tok open Util open Names open Topconstr @@ -33,20 +35,20 @@ let _ = List.iter Lexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -let check_command = Gram.Entry.create "vernac:check_command" +let check_command = Gram.entry_create "vernac:check_command" -let tactic_mode = Gram.Entry.create "vernac:tactic_command" -let noedit_mode = Gram.Entry.create "vernac:noedit_command" +let tactic_mode = Gram.entry_create "vernac:tactic_command" +let noedit_mode = Gram.entry_create "vernac:noedit_command" -let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" -let thm_token = Gram.Entry.create "vernac:thm_token" -let def_body = Gram.Entry.create "vernac:def_body" -let decl_notation = Gram.Entry.create "vernac:decl_notation" -let typeclass_context = Gram.Entry.create "vernac:typeclass_context" -let record_field = Gram.Entry.create "vernac:record_field" -let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion" -let subgoal_command = Gram.Entry.create "proof_mode:subgoal_command" -let instance_name = Gram.Entry.create "vernac:instance_name" +let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" +let thm_token = Gram.entry_create "vernac:thm_token" +let def_body = Gram.entry_create "vernac:def_body" +let decl_notation = Gram.entry_create "vernac:decl_notation" +let typeclass_context = Gram.entry_create "vernac:typeclass_context" +let record_field = Gram.entry_create "vernac:record_field" +let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" +let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" +let instance_name = Gram.entry_create "vernac:instance_name" let command_entry = ref noedit_mode let set_command_entry e = command_entry := e @@ -65,7 +67,7 @@ let _ = Proof_global.register_proof_mode {Proof_global. let default_command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm) + (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) let no_hook _ _ = () GEXTEND Gram @@ -758,7 +760,7 @@ GEXTEND Gram | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s - | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s + | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid) @@ -784,7 +786,7 @@ GEXTEND Gram | s = STRING -> StringRefValue s ] ] ; option_table: - [ [ fl = LIST1 IDENT -> fl ]] + [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]] ; as_dirpath: [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] @@ -911,16 +913,17 @@ GEXTEND Gram | IDENT "next"; IDENT "level" -> NextLevel ] ] ; syntax_modifier: - [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; + [ [ "at"; IDENT "level"; n = natural -> SetLevel n + | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA + | IDENT "right"; IDENT "associativity" -> SetAssoc RightA + | IDENT "no"; IDENT "associativity" -> SetAssoc NonA + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing + | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s + | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) - | "at"; IDENT "level"; n = natural -> SetLevel n - | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA - | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA - | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA + | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) - | IDENT "only"; IDENT "parsing" -> SetOnlyParsing - | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ] + ] ] ; syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 901f7ff10..2e2796a22 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -18,6 +18,7 @@ open Libnames open Nametab open Detyping +open Tok (* Generic xml parser without raw data *) @@ -29,7 +30,7 @@ let check_tags loc otag ctag = user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ str "does not match open xml tag " ++ str otag ++ str ".") -let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e) +let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry) GEXTEND Gram GLOBAL: xml_eoi; @@ -273,5 +274,5 @@ let rec interp_xml_tactic_arg = function let parse_tactic_arg ch = interp_xml_tactic_arg - (Pcoq.Gram.Entry.parse xml_eoi - (Pcoq.Gram.parsable (Stream.of_channel ch))) + (Pcoq.Gram.entry_parse xml_eoi + (Pcoq.Gram.parsable (Stream.of_channel ch))) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 175ce16a4..ba5a8c425 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -8,7 +8,7 @@ open Pp open Util -open Token +open Compat open Tok (* Dictionaries: trees annotated with string options, each node being a map @@ -71,18 +71,34 @@ let ttree_remove ttree str = (* Errors occuring while lexing (explained as "Lexer error: ...") *) -type error = - | Illegal_character - | Unterminated_comment - | Unterminated_string - | Undefined_token - | Bad_token of string +module Error = struct -exception Error of error + type t = + | Illegal_character + | Unterminated_comment + | Unterminated_string + | Undefined_token + | Bad_token of string -let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str) + exception E of t -let bad_token str = raise (Error (Bad_token str)) + 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) + + let print ppf x = Format.fprintf ppf "%s@." (to_string x) + +end +open Error + +let err loc str = Loc.raise (make_loc loc) (Error.E str) + +let bad_token str = raise (Error.E (Bad_token str)) (* Lexer conventions on tokens *) @@ -175,7 +191,7 @@ let check_ident str = let check_keyword str = try check_special_token str - with Error _ -> check_ident str + with Error.E _ -> check_ident str (* Keyword and symbol dictionary *) let token_tree = ref empty_ttree @@ -379,7 +395,7 @@ 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 -> c + | Some c -> KEYWORD c (* Must be a special token *) let process_chars bp c cs = @@ -438,7 +454,7 @@ let rec next_token = parser bp len = ident_tail (store 0 c); s >] ep -> let id = get_buff len in comment_stop bp; - (try KEYWORD (find_keyword id s) with Not_found -> IDENT id), (bp, ep) + (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)) @@ -461,7 +477,7 @@ let rec next_token = parser bp let id = get_buff len in let ep = Stream.count s in comment_stop bp; - (try KEYWORD (find_keyword id s) with Not_found -> IDENT id), (bp, ep) + (try find_keyword id s with Not_found -> IDENT id), (bp, ep) | AsciiChar | Utf8Token ((UnicodeSymbol | UnicodeIdentPart), _) -> let t = process_chars bp (Stream.next s) s in comment_stop bp; t @@ -473,53 +489,23 @@ let rec next_token = parser bp let locerr () = invalid_arg "Lexer: location function" -let tsz = 256 (* up to 2^29 entries on a 32-bit machine, 2^61 on 64-bit *) - -let loct_create () = ref [| [| |] |] +let loct_create () = Hashtbl.create 207 let loct_func loct i = - match - if i < 0 || i/tsz >= Array.length !loct then None - else if !loct.(i/tsz) = [| |] then None - else !loct.(i/tsz).(i mod tsz) - with - | Some loc -> Util.make_loc loc - | _ -> locerr () - -let loct_add loct i loc = - while i/tsz >= Array.length !loct do - let new_tmax = Array.length !loct * 2 in - let new_loct = Array.make new_tmax [| |] in - Array.blit !loct 0 new_loct 0 (Array.length !loct); - loct := new_loct; - done; - if !loct.(i/tsz) = [| |] then !loct.(i/tsz) <- Array.make tsz None; - !loct.(i/tsz).(i mod tsz) <- Some loc - -let current_location_table = ref (ref [| [| |] |]) - -let location_function n = - loct_func !current_location_table n + try Hashtbl.find loct i with Not_found -> locerr () -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 loc; Some tok) - in - current_location_table := loct; - (ts, loct_func loct) +let loct_add loct i loc = Hashtbl.add loct i loc -type location_table = (int * int) option array array ref +let current_location_table = ref (loct_create ()) + +type location_table = (int, loc) Hashtbl.t let location_table () = !current_location_table let restore_location_table t = current_location_table := t +let location_function n = loct_func !current_location_table n +(** {6 The lexer of Coq} *) -(* The lexer of Coq *) - -(* Note: removing a token. +(** 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 @@ -529,7 +515,9 @@ let restore_location_table t = current_location_table := t IFDEF CAMLP5 THEN -(* Names of tokens, for this lexer, used in Grammar error messages *) +type te = Tok.t + +(** Names of tokens, for this lexer, used in Grammar error messages *) let token_text = function | ("", t) -> "'" ^ t ^ "'" @@ -542,15 +530,23 @@ let token_text = function | (con, "") -> con | (con, prm) -> con ^ " \"" ^ prm ^ "\"" -(* Adding a new token (keyword or special token). *) - -let add_token pat = match Tok.of_pattern pat with - | KEYWORD s -> add_keyword s - | _ -> () +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 = add_token; + 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; @@ -558,11 +554,38 @@ let lexer = { ELSE (* official camlp4 for ocaml >= 3.10 *) -TODO +module M_ = Camlp4.ErrorHandler.Register (Error) + +module Loc = Loc +module Token = struct + include Tok (* Cf. tok.ml *) + module Loc = Loc + 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 *) +(** Terminal symbols interpretation *) let is_ident_not_keyword s = match s.[0] with diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 7f7d36b74..a8ae46fec 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -9,15 +9,6 @@ open Pp open Util -type error = - | Illegal_character - | Unterminated_comment - | Unterminated_string - | Undefined_token - | Bad_token of string - -exception Error of error - val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool @@ -45,6 +36,6 @@ val set_xml_output_comment : (string -> unit) -> unit val terminal : string -> Tok.t -(** The lexer of Coq *) +(** The lexer of Coq: *) -val lexer : Compat.lexer +include Compat.LexerSig diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 7d78f5371..a20c0d1ef 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -7,6 +7,8 @@ (************************************************************************) open Pp +open Compat +open Tok open Util open Names open Extend @@ -18,54 +20,67 @@ open Tacexpr open Extrawit open Ppextend -(* The parser of Coq *) +(** The parser of Coq *) + +module G = GrammarMake (Lexer) + +(* TODO: this is a workaround, since there isn't such + [warning_verbose] in new camlp4. In camlp5, this ref + gets hidden by [Gramext.warning_verbose] *) +let warning_verbose = ref true IFDEF CAMLP5 THEN +open Gramext +ELSE +open G +END -module L = - struct - type te = Tok.t - let lexer = Lexer.lexer - end +let gram_token_of_token tok = +IFDEF CAMLP5 THEN + Stoken (Tok.to_pattern tok) +ELSE + match tok with + | KEYWORD s -> Skeyword s + | tok -> Stoken ((=) tok, to_string tok) +END -module G = Grammar.GMake(L) +let gram_token_of_string s = gram_token_of_token (Lexer.terminal s) -ELSE (* official camlp4 of ocaml >= 3.10 *) +let camlp4_verbosity silent f x = + let a = !warning_verbose in + warning_verbose := silent; + f x; + warning_verbose := a -TODO +let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x -END -let gram_token_of_token tok = Gramext.Stoken (Tok.to_pattern tok) -let gram_token_of_string s = gram_token_of_token (Lexer.terminal s) +(** General entry keys *) -let grammar_delete e pos reinit rls = - List.iter - (fun (n,ass,lev) -> +(** This intermediate abstract representation of entries can + both be reified into mlexpr for the ML extensions and + dynamically interpreted as entries for the Coq level extensions +*) - (* Caveat: deletion is not the converse of extension: when an - empty level is extended, deletion removes the level instead - of keeping it empty. This has an effect on the empty levels 8, - 99 and 200. We didn't find a good solution to this problem - (e.g. using G.extend to know if the level exists results in a - printed error message as side effect). As a consequence an - extension at 99 or 8 (and for pattern 200 too) inside a section - corrupts the parser. *) +type prod_entry_key = + | Alist1 of prod_entry_key + | Alist1sep of prod_entry_key * string + | Alist0 of prod_entry_key + | Alist0sep of prod_entry_key * string + | Aopt of prod_entry_key + | Amodifiers of prod_entry_key + | Aself + | Anext + | Atactic of int + | Agram of G.internal_entry + | Aentry of string * string - List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) - (List.rev rls); - if reinit <> None then - let lev = match pos with Some (Gramext.Level n) -> n | _ -> assert false in - let pos = - if lev = "200" then Gramext.First - else Gramext.After (string_of_int (int_of_string lev + 1)) in - G.extend e (Some pos) [Some lev,reinit,[]]; +(** [grammar_object] is the superclass of all grammar entries *) -(* grammar_object is the superclass of all grammar entries *) module type Gramobj = sig type grammar_object - val weaken_entry : 'a G.Entry.e -> grammar_object G.Entry.e + val weaken_entry : 'a G.entry -> grammar_object G.entry end module Gramobj : Gramobj = @@ -74,9 +89,11 @@ struct let weaken_entry e = Obj.magic e end +(** Grammar entries with associated types *) + type entry_type = argument_type type grammar_object = Gramobj.grammar_object -type typed_entry = argument_type * grammar_object G.Entry.e +type typed_entry = argument_type * grammar_object G.entry let in_typed_entry t e = (t,Gramobj.weaken_entry e) let type_of_typed_entry (t,e) = t let object_of_typed_entry (t,e) = e @@ -85,8 +102,8 @@ let weaken_entry x = Gramobj.weaken_entry x module type Gramtypes = sig open Decl_kinds - val inGramObj : 'a raw_abstract_argument_type -> 'a G.Entry.e -> typed_entry - val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.Entry.e + val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry + val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry end module Gramtypes : Gramtypes = @@ -101,77 +118,107 @@ end open Gramtypes -type camlp4_rule = - Tok.t Gramext.g_symbol list * Gramext.g_action +(** 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] -type camlp4_entry_rules = - (* first two parameters are name and assoc iff a level is created *) - string option * Gramext.g_assoc option * camlp4_rule list + In [single_extend_statement, first two parameters are name and + assoc iff a level is created *) type ext_kind = | ByGrammar of - grammar_object G.Entry.e * Gramext.position option * - camlp4_entry_rules list * Gramext.g_assoc option - | ByGEXTEND of (unit -> unit) * (unit -> unit) + grammar_object G.entry + * gram_assoc option (** for reinitialization if ever needed *) + * G.extend_statment + | ByEXTEND of (unit -> unit) * (unit -> unit) + +(** The list of extensions *) let camlp4_state = ref [] -(* The apparent parser of Coq; encapsulate G to keep track of the - extensions. *) +(** Deletion + + Caveat: deletion is not the converse of extension: when an + empty level is extended, deletion removes the level instead + of keeping it empty. This has an effect on the empty levels 8, + 99 and 200. We didn't find a good solution to this problem + (e.g. using G.extend to know if the level exists results in a + printed error message as side effect). As a consequence an + extension at 99 or 8 (and for pattern 200 too) inside a section + corrupts the parser. *) + +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); + if reinit <> None then + let lev = match pos with Some (Level n) -> n | _ -> assert false in + let pos = + if lev = "200" then First + else After (string_of_int (int_of_string lev + 1)) in + maybe_uncurry (G.extend e) (Some pos, [Some lev,reinit,[]]) + +(** The apparent parser of Coq; encapsulate G to keep track + of the extensions. *) + module Gram = struct include G - let extend e pos rls = - camlp4_state := - (ByGEXTEND ((fun () -> grammar_delete e pos None rls), - (fun () -> G.extend e pos rls))) - :: !camlp4_state; - G.extend e pos rls + 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 - ByGEXTEND provides just the framework we need to allow this in section. + 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 +(** This extension command is used by the Grammar constr *) -let camlp4_verbosity silent f x = - let a = !Gramext.warning_verbose in - Gramext.warning_verbose := silent; - f x; - Gramext.warning_verbose := a +let grammar_extend e reinit ext = + camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) ext -(* This extension command is used by the Grammar constr *) +(** Remove extensions -let grammar_extend te pos reinit rls = - camlp4_state := ByGrammar (weaken_entry te,pos,rls,reinit) :: !camlp4_state; - camlp4_verbosity (Flags.is_verbose ()) (G.extend te pos) rls - -(* n is the number of extended entries (not the number of Grammar commands!) + [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 "Pcoq.remove_grammars: too many rules to remove" - | ByGrammar(g,pos,rls,reinit)::t -> - grammar_delete g pos reinit rls; + | ByGrammar(g,reinit,ext)::t -> + grammar_delete g reinit ext; camlp4_state := t; remove_grammars (n-1) - | ByGEXTEND (undo,redo)::t -> + | ByEXTEND (undo,redo)::t -> undo(); camlp4_state := t; remove_grammars n; redo(); - camlp4_state := ByGEXTEND (undo,redo) :: !camlp4_state) + camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) + +(** An entry that checks we reached the end of the input. *) -(* 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 e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in GEXTEND Gram e: [ [ x = en; EOI -> x ] ] ; @@ -179,7 +226,7 @@ let eoi_entry en = e let map_entry f en = - let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_map") in + let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in GEXTEND Gram e: [ [ x = en -> f x ] ] ; @@ -190,7 +237,7 @@ let map_entry f en = (use eoi_entry) *) let parse_string f x = - let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm) + let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) type gram_universe = string * (string, typed_entry) Hashtbl.t @@ -227,7 +274,7 @@ let get_entry_type (u, utab) s = let new_entry etyp (u, utab) s = if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr); let ename = u ^ ":" ^ s in - let e = in_typed_entry etyp (Gram.Entry.create ename) in + let e = in_typed_entry etyp (Gram.entry_create ename) in Hashtbl.add utab s e; e let create_entry (u, utab) s etyp = @@ -246,10 +293,10 @@ let create_generic_entry s wit = outGramObj wit (create_entry utactic s (unquote wit)) (* [make_gen_entry] builds entries extensible by giving its name (a string) *) -(* For entries extensible only via the ML name, Gram.Entry.create is enough *) +(* For entries extensible only via the ML name, Gram.entry_create is enough *) let make_gen_entry (u,univ) rawwit s = - let e = Gram.Entry.create (u ^ ":" ^ s) in + let e = Gram.entry_create (u ^ ":" ^ s) in Hashtbl.add univ s (inGramObj rawwit e); e (* Initial grammar entries *) @@ -258,35 +305,35 @@ module Prim = struct let gec_gen x = make_gen_entry uprim x - (* Entries that can be refered via the string -> Gram.Entry.e table *) + (* Entries that can be refered via the string -> Gram.entry table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen rawwit_pre_ident "preident" let ident = gec_gen rawwit_ident "ident" let natural = gec_gen rawwit_int "natural" let integer = gec_gen rawwit_int "integer" - let bigint = Gram.Entry.create "Prim.bigint" + let bigint = Gram.entry_create "Prim.bigint" let string = gec_gen rawwit_string "string" let reference = make_gen_entry uprim rawwit_ref "reference" - let by_notation = Gram.Entry.create "by_notation" - let smart_global = Gram.Entry.create "smart_global" + 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 rawwit_var "var" - let name = Gram.Entry.create "Prim.name" - let identref = Gram.Entry.create "Prim.identref" + let name = Gram.entry_create "Prim.name" + let identref = Gram.entry_create "Prim.identref" let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident" - let pattern_identref = Gram.Entry.create "pattern_identref" + 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 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 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" + let ne_string = Gram.entry_create "Prim.ne_string" + let ne_lstring = Gram.entry_create "Prim.ne_lstring" end @@ -295,7 +342,7 @@ module Constr = let gec_constr = make_gen_entry uconstr rawwit_constr let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr) - (* Entries that can be refered via the string -> Gram.Entry.e table *) + (* Entries that can be refered via the string -> Gram.entry table *) let constr = gec_constr "constr" let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr @@ -304,30 +351,30 @@ module Constr = let ident = make_gen_entry uconstr rawwit_ident "ident" let global = make_gen_entry uconstr rawwit_ref "global" let sort = make_gen_entry uconstr rawwit_sort "sort" - let pattern = Gram.Entry.create "constr:pattern" + let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" - let binder = Gram.Entry.create "constr:binder" - let binder_let = Gram.Entry.create "constr:binder_let" - let binders_let = Gram.Entry.create "constr:binders_let" - let binders_let_fixannot = Gram.Entry.create "constr:binders_let_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" + let binder = Gram.entry_create "constr:binder" + let binder_let = Gram.entry_create "constr:binder_let" + let binders_let = Gram.entry_create "constr:binders_let" + let binders_let_fixannot = Gram.entry_create "constr:binders_let_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" + 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" + let simple_tactic = Gram.entry_create "tactic:simple_tactic" - (* Entries that can be refered via the string -> Gram.Entry.e table *) + (* Entries that can be refered via the string -> Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr" @@ -346,9 +393,9 @@ module Tactic = make_gen_entry utactic rawwit_intro_pattern "simple_intropattern" (* Main entries for ltac *) - let tactic_arg = Gram.Entry.create "tactic:tactic_arg" - let tactic_expr = Gram.Entry.create "tactic:tactic_expr" - let binder_tactic = Gram.Entry.create "tactic:binder_tactic" + let tactic_arg = Gram.entry_create "tactic:tactic_arg" + let tactic_expr = Gram.entry_create "tactic:tactic_expr" + let binder_tactic = Gram.entry_create "tactic:binder_tactic" let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic" @@ -359,7 +406,7 @@ module Tactic = module Vernac_ = struct - let gec_vernac s = Gram.Entry.create ("vernac:" ^ s) + let gec_vernac s = Gram.entry_create ("vernac:" ^ s) (* The different kinds of vernacular commands *) let gallina = gec_vernac "gallina" @@ -370,7 +417,8 @@ module Vernac_ = let vernac_eoi = eoi_entry vernac (* Main vernac entry *) - let main_entry = Gram.Entry.create "vernac" + let main_entry = Gram.entry_create "vernac" + GEXTEND Gram main_entry: [ [ a = vernac -> Some (loc,a) | EOI -> None ] ] @@ -397,23 +445,23 @@ let main_entry = Vernac_.main_entry let constr_level = string_of_int let default_levels = - [200,Gramext.RightA,false; - 100,Gramext.RightA,false; - 99,Gramext.RightA,true; - 90,Gramext.RightA,false; - 10,Gramext.RightA,false; - 9,Gramext.RightA,false; - 8,Gramext.RightA,true; - 1,Gramext.LeftA,false; - 0,Gramext.RightA,false] + [200,RightA,false; + 100,RightA,false; + 99,RightA,true; + 90,RightA,false; + 10,RightA,false; + 9,RightA,false; + 8,RightA,true; + 1,LeftA,false; + 0,RightA,false] let default_pattern_levels = - [200,Gramext.RightA,true; - 100,Gramext.RightA,false; - 99,Gramext.RightA,true; - 10,Gramext.LeftA,false; - 1,Gramext.LeftA,false; - 0,Gramext.RightA,false] + [200,RightA,true; + 100,RightA,false; + 99,RightA,true; + 10,LeftA,false; + 1,LeftA,false; + 0,RightA,false] let level_stack = ref [(default_levels, default_pattern_levels)] @@ -424,19 +472,19 @@ let level_stack = open Ppextend let admissible_assoc = function - | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false - | Gramext.RightA, Some Gramext.LeftA -> false + | LeftA, Some (RightA | NonA) -> false + | RightA, Some LeftA -> false | _ -> true let create_assoc = function - | None -> Gramext.RightA + | None -> RightA | Some a -> a let error_level_assoc p current expected = let pr_assoc = function - | Gramext.LeftA -> str "left" - | Gramext.RightA -> str "right" - | Gramext.NonA -> str "non" in + | LeftA -> str "left" + | RightA -> str "right" + | 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 " ++ @@ -470,18 +518,18 @@ let find_position_gen forpat ensure assoc lev = let assoc = create_assoc assoc in if !init = None then (* Create the entry *) - (if !after = None then Some Gramext.First - else Some (Gramext.After (constr_level (Option.get !after)))), + (if !after = None then Some First + else Some (After (constr_level (Option.get !after)))), Some assoc, Some (constr_level n), None else (* The reinit flag has been updated *) - Some (Gramext.Level (constr_level n)), None, None, !init + Some (Level (constr_level n)), None, None, !init with (* Nothing has changed *) Exit -> level_stack := current :: !level_stack; (* Just inherit the existing associativity and name (None) *) - Some (Gramext.Level (constr_level n)), None, None, None + Some (Level (constr_level n)), None, None, None let remove_levels n = level_stack := list_skipn n !level_stack @@ -510,8 +558,8 @@ let synchronize_level_positions () = (* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) let camlp4_assoc = function - | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA - | None | Some Gramext.LeftA -> Gramext.LeftA + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA (* [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 @@ -526,20 +574,20 @@ let adjust_level assoc from = function | (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 (Gramext.NonA|Gramext.LeftA))) -> + | (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 Gramext.RightA)) -> + | (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 Gramext.NonA)) -> None + | (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 a = camlp4_assoc assoc -> None (* Otherwise, force the level, n or n-1, according to expected assoc *) | (NumLevel n,BorderProd (Left,Some a)) -> - if a = Gramext.LeftA then Some (Some (n,true)) else Some None + if a = LeftA then Some (Some (n,true)) else Some None (* None means NEXT *) | (NextLevel,_) -> Some None (* Compute production name elsewhere *) @@ -585,7 +633,7 @@ let interp_constr_prod_entry_key ass from forpat en = let is_self from e = match from, e with ETConstr(n,()), ETConstr(NumLevel n', - BorderProd(Right, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false + BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> n=n' | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint | ETPattern, ETPattern) -> true @@ -601,57 +649,60 @@ let is_binder_level from e = let rec symbol_of_constr_prod_entry_key assoc from forpat typ = if is_binder_level from typ then if forpat then - Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200") + Snterml (Gram.Entry.obj Constr.pattern,"200") else - Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200") + Snterml (Gram.Entry.obj Constr.operconstr,"200") else if is_self from typ then - Gramext.Sself + Sself else match typ with | ETConstrList (typ',[]) -> - Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) + Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) | ETConstrList (typ',tkl) -> - Gramext.Slist1sep + Slist1sep (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - Gramext.srules + Gram.srules' [List.map gram_token_of_token tkl, - List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl - (Gramext.action (fun loc -> ()))]) + List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl + (Gram.action (fun loc -> ()))]) | _ -> match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) - | (eobj,Some None,_) -> Gramext.Snext + | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj) + | (eobj,Some None,_) -> Snext | (eobj,Some (Some (lev,cur)),_) -> - Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev) + Snterml (Gram.Entry.obj eobj,constr_level lev) -(**********************************************************************) -(* Binding general entry keys to symbol *) +(** Binding general entry keys to symbol *) let rec symbol_of_prod_entry_key = function - | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s) + | Alist1 s -> Slist1 (symbol_of_prod_entry_key s) | Alist1sep (s,sep) -> - Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) - | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s) + Slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep) + | Alist0 s -> Slist0 (symbol_of_prod_entry_key s) | Alist0sep (s,sep) -> - Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) - | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s) + Slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep) + | Aopt s -> Sopt (symbol_of_prod_entry_key s) | Amodifiers s -> - Gramext.srules - [([], Gramext.action(fun _loc -> [])); + Gram.srules' + [([], Gram.action (fun _loc -> [])); ([gram_token_of_string "("; - Gramext.Slist1sep ((symbol_of_prod_entry_key s), gram_token_of_string ","); + Slist1sep ((symbol_of_prod_entry_key s), gram_token_of_string ","); gram_token_of_string ")"], - Gramext.action (fun _ l _ _loc -> l))] - | Aself -> Gramext.Sself - | Anext -> Gramext.Snext - | Atactic 5 -> Gramext.Snterm (Gram.Entry.obj Tactic.binder_tactic) + Gram.action (fun _ l _ _loc -> l))] + | Aself -> Sself + | Anext -> Snext + | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic) | Atactic n -> - Gramext.Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n) - | Agram s -> Gramext.Snterm s + Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n) + | Agram s -> Snterm s | Aentry (u,s) -> - Gramext.Snterm (Gram.Entry.obj + Snterm (Gram.Entry.obj (object_of_typed_entry (get_entry (get_univ u) s))) +let level_of_snterml = function + | Snterml (_,l) -> int_of_string l + | _ -> failwith "level_of_snterml" + (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ada016094..3ec149256 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -15,13 +15,13 @@ open Genarg open Topconstr open Tacexpr open Libnames +open Compat (** The parser of Coq *) -module Gram : Grammar.S with type te = Tok.t +module Gram : GrammarSig -(** - The parser of Coq is built from three kinds of rule declarations: +(** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using e.g. Notation, Infix, or Tactic Notation) @@ -96,24 +96,17 @@ module Gram : Grammar.S with type te = Tok.t *) -val gram_token_of_token : Tok.t -> Tok.t Gramext.g_symbol -val gram_token_of_string : string -> Tok.t Gramext.g_symbol +val gram_token_of_token : Tok.t -> Gram.symbol +val gram_token_of_string : string -> Gram.symbol (** The superclass of all grammar entries *) type grammar_object -type camlp4_rule = - Tok.t Gramext.g_symbol list * Gramext.g_action - -type camlp4_entry_rules = - (** first two parameters are name and assoc iff a level is created *) - string option * Gramext.g_assoc option * camlp4_rule list - (** Add one extension at some camlp4 position of some camlp4 entry *) val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> - (** for reinitialization if ever needed: *) Gramext.g_assoc option -> - camlp4_entry_rules list -> unit + grammar_object Gram.entry -> + gram_assoc option (** for reinitialization if ever needed *) -> + Gram.extend_statment -> unit (** Remove the last n extensions *) val remove_grammars : int -> unit @@ -128,8 +121,8 @@ type typed_entry type entry_type = argument_type val type_of_typed_entry : typed_entry -> entry_type -val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e -val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e +val object_of_typed_entry : typed_entry -> grammar_object Gram.entry +val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry (** Temporary activate camlp4 verbosity *) @@ -137,9 +130,9 @@ val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit (** Parse a string *) -val parse_string : 'a Gram.Entry.e -> string -> 'a -val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e -val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e +val parse_string : 'a Gram.entry -> string -> 'a +val eoi_entry : 'a Gram.entry -> 'a Gram.entry +val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry (** Table of Coq statically defined grammar entries *) @@ -161,130 +154,152 @@ val get_entry_type : gram_universe -> string -> entry_type val create_entry : gram_universe -> string -> entry_type -> typed_entry val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> - 'a Gram.Entry.e + 'a Gram.entry module Prim : sig open Util open Names open Libnames - val preident : string Gram.Entry.e - val ident : identifier Gram.Entry.e - val name : name located Gram.Entry.e - val identref : identifier located Gram.Entry.e - val pattern_ident : identifier Gram.Entry.e - val pattern_identref : identifier located Gram.Entry.e - val base_ident : identifier Gram.Entry.e - val natural : int Gram.Entry.e - val bigint : Bigint.bigint Gram.Entry.e - val integer : int Gram.Entry.e - val string : string Gram.Entry.e - val qualid : qualid located Gram.Entry.e - val fullyqualid : identifier list located Gram.Entry.e - val reference : reference Gram.Entry.e - val by_notation : (loc * string * string option) Gram.Entry.e - val smart_global : reference or_by_notation Gram.Entry.e - val dirpath : dir_path Gram.Entry.e - val ne_string : string Gram.Entry.e - val ne_lstring : string located Gram.Entry.e - val var : identifier located Gram.Entry.e + val preident : string Gram.entry + val ident : identifier Gram.entry + val name : name located Gram.entry + val identref : identifier located Gram.entry + val pattern_ident : identifier Gram.entry + val pattern_identref : identifier located Gram.entry + val base_ident : identifier Gram.entry + val natural : int Gram.entry + val bigint : Bigint.bigint Gram.entry + val integer : int Gram.entry + val string : string Gram.entry + val qualid : qualid located Gram.entry + val fullyqualid : identifier list located Gram.entry + val reference : reference Gram.entry + val by_notation : (loc * string * string option) Gram.entry + val smart_global : reference or_by_notation Gram.entry + val dirpath : dir_path Gram.entry + val ne_string : string Gram.entry + val ne_lstring : string located Gram.entry + val var : identifier located Gram.entry end module Constr : sig - val constr : constr_expr Gram.Entry.e - val constr_eoi : constr_expr Gram.Entry.e - val lconstr : constr_expr Gram.Entry.e - val binder_constr : constr_expr Gram.Entry.e - val operconstr : constr_expr Gram.Entry.e - val ident : identifier Gram.Entry.e - val global : reference Gram.Entry.e - val sort : rawsort Gram.Entry.e - val pattern : cases_pattern_expr Gram.Entry.e - val constr_pattern : constr_expr Gram.Entry.e - val lconstr_pattern : constr_expr Gram.Entry.e - val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e - val binder_let : local_binder list Gram.Entry.e - val binders_let : local_binder list Gram.Entry.e - val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e - val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e - val record_declaration : constr_expr Gram.Entry.e - val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e + val constr : constr_expr Gram.entry + val constr_eoi : constr_expr Gram.entry + val lconstr : constr_expr Gram.entry + val binder_constr : constr_expr Gram.entry + val operconstr : constr_expr Gram.entry + val ident : identifier Gram.entry + val global : reference Gram.entry + val sort : rawsort Gram.entry + val pattern : cases_pattern_expr Gram.entry + val constr_pattern : constr_expr Gram.entry + val lconstr_pattern : constr_expr Gram.entry + val binder : (name located list * binder_kind * constr_expr) Gram.entry + val binder_let : local_binder list Gram.entry + val binders_let : local_binder list Gram.entry + val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry + val typeclass_constraint : (name located * bool * constr_expr) Gram.entry + val record_declaration : constr_expr Gram.entry + val appl_arg : (constr_expr * explicitation located option) Gram.entry end module Module : sig - val module_expr : module_ast Gram.Entry.e - val module_type : module_ast Gram.Entry.e + val module_expr : module_ast Gram.entry + val module_type : module_ast Gram.entry end module Tactic : sig open Rawterm - val open_constr : open_constr_expr Gram.Entry.e - val casted_open_constr : open_constr_expr Gram.Entry.e - val constr_with_bindings : constr_expr with_bindings Gram.Entry.e - val bindings : constr_expr bindings Gram.Entry.e - val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.Entry.e - val quantified_hypothesis : quantified_hypothesis Gram.Entry.e - val int_or_var : int or_var Gram.Entry.e - val red_expr : raw_red_expr Gram.Entry.e - val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e - val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e - val tactic_arg : raw_tactic_arg Gram.Entry.e - val tactic_expr : raw_tactic_expr Gram.Entry.e - val binder_tactic : raw_tactic_expr Gram.Entry.e - val tactic : raw_tactic_expr Gram.Entry.e - val tactic_eoi : raw_tactic_expr Gram.Entry.e + val open_constr : open_constr_expr Gram.entry + val casted_open_constr : open_constr_expr Gram.entry + val constr_with_bindings : constr_expr with_bindings Gram.entry + val bindings : constr_expr bindings Gram.entry + val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry + val quantified_hypothesis : quantified_hypothesis Gram.entry + val int_or_var : int or_var Gram.entry + val red_expr : raw_red_expr Gram.entry + val simple_tactic : raw_atomic_tactic_expr Gram.entry + val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry + val tactic_arg : raw_tactic_arg Gram.entry + val tactic_expr : raw_tactic_expr Gram.entry + val binder_tactic : raw_tactic_expr Gram.entry + val tactic : raw_tactic_expr Gram.entry + val tactic_eoi : raw_tactic_expr Gram.entry end module Vernac_ : sig open Decl_kinds - val gallina : vernac_expr Gram.Entry.e - val gallina_ext : vernac_expr Gram.Entry.e - val command : vernac_expr Gram.Entry.e - val syntax : vernac_expr Gram.Entry.e - val vernac : vernac_expr Gram.Entry.e - val vernac_eoi : vernac_expr Gram.Entry.e + val gallina : vernac_expr Gram.entry + val gallina_ext : vernac_expr Gram.entry + val command : vernac_expr Gram.entry + val syntax : vernac_expr Gram.entry + val vernac : vernac_expr Gram.entry + val vernac_eoi : vernac_expr Gram.entry end (** The main entry: reads an optional vernac command *) -val main_entry : (loc * vernac_expr) option Gram.Entry.e +val main_entry : (loc * vernac_expr) option Gram.entry (** Mapping formal entries into concrete ones *) (** Binding constr entry keys to entries and symbols *) val interp_constr_entry_key : bool (** true for cases_pattern *) -> - constr_entry_key -> grammar_object Gram.Entry.e * int option + constr_entry_key -> grammar_object Gram.entry * int option -val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> +val symbol_of_constr_prod_entry_key : gram_assoc option -> constr_entry_key -> bool -> constr_prod_entry_key -> - Tok.t Gramext.g_symbol + Gram.symbol + +(** General entry keys *) + +(** This intermediate abstract representation of entries can + both be reified into mlexpr for the ML extensions and + dynamically interpreted as entries for the Coq level extensions +*) + +type prod_entry_key = + | Alist1 of prod_entry_key + | Alist1sep of prod_entry_key * string + | Alist0 of prod_entry_key + | Alist0sep of prod_entry_key * string + | Aopt of prod_entry_key + | Amodifiers of prod_entry_key + | Aself + | Anext + | Atactic of int + | Agram of Gram.internal_entry + | Aentry of string * string (** Binding general entry keys to symbols *) val symbol_of_prod_entry_key : - Gram.te prod_entry_key -> Gram.te Gramext.g_symbol + prod_entry_key -> Gram.symbol (** Interpret entry names of the form "ne_constr_list" as entry keys *) val interp_entry_name : bool (** true to fail on unknown entry *) -> - int option -> string -> string -> entry_type * Gram.te prod_entry_key + int option -> string -> string -> entry_type * prod_entry_key (** Registering/resetting the level of a constr entry *) val find_position : bool (** true if for creation in pattern entry; false if in constr entry *) -> - Gramext.g_assoc option -> int option -> - Gramext.position option * Gramext.g_assoc option * string option * - (** for reinitialization: *) Gramext.g_assoc option + gram_assoc option -> int option -> + gram_position option * gram_assoc option * string option * + (** for reinitialization: *) gram_assoc option val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> - (Gramext.position option * Gramext.g_assoc option * - string option * Gramext.g_assoc option) list + (gram_position option * gram_assoc option * + string option * gram_assoc option) list val remove_levels : int -> unit + +val level_of_snterml : Gram.symbol -> int diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a120253c1..5d21d26d8 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -10,6 +10,7 @@ open Pp open Names open Nameops open Nametab +open Compat open Util open Extend open Vernacexpr @@ -93,15 +94,15 @@ let pr_ne_sep sep pr = function | l -> sep() ++ pr l let pr_entry_prec = function - | Some Gramext.LeftA -> str"LEFTA " - | Some Gramext.RightA -> str"RIGHTA " - | Some Gramext.NonA -> str"NONA " + | Some LeftA -> str"LEFTA " + | Some RightA -> str"RIGHTA " + | Some NonA -> str"NONA " | None -> mt() let pr_prec = function - | Some Gramext.LeftA -> str", left associativity" - | Some Gramext.RightA -> str", right associativity" - | Some Gramext.NonA -> str", no associativity" + | Some LeftA -> str", left associativity" + | Some RightA -> str", right associativity" + | Some NonA -> str", no associativity" | None -> mt() let pr_set_entry_type = function @@ -398,9 +399,9 @@ let pr_syntax_modifier = function prlist_with_sep sep_v2 str l ++ spc() ++ str"at level" ++ spc() ++ int n | SetLevel n -> str"at level" ++ spc() ++ int n - | SetAssoc Gramext.LeftA -> str"left associativity" - | SetAssoc Gramext.RightA -> str"right associativity" - | SetAssoc Gramext.NonA -> str"no associativity" + | SetAssoc LeftA -> str"left associativity" + | SetAssoc RightA -> str"right associativity" + | SetAssoc NonA -> str"no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyParsing -> str"only parsing" | SetFormat s -> str"format " ++ pr_located qs s @@ -778,7 +779,7 @@ let rec pr_vernac = function (match b with None -> mt () | Some Dash -> str"-" | Some Star -> str"*" | Some Plus -> str"+") ++ pr_raw_tactic tac ++ (try if deftac then str ".." else mt () - with UserError _|Stdpp.Exc_located _ -> mt()) + with UserError _|Loc.Exc_located _ -> mt()) | VernacSolveExistential (i,c) -> str"Existential " ++ int i ++ pr_lconstrarg c diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 4c86e4415..fb34a5aa2 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -12,7 +12,9 @@ open Names open Pattern open Q_util open Util +open Compat open Pcaml +open PcamlSig let loc = dummy_loc let dloc = <:expr< Util.dummy_loc >> @@ -40,7 +42,7 @@ EXTEND [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] ; string: - [ [ UIDENT | LIDENT ] ] + [ [ s = UIDENT -> s | s = LIDENT -> s ] ] ; constr: [ "200" RIGHTA diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6d3e8e03a..d78486a0b 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -10,6 +10,7 @@ open Util open Names open Libnames open Q_util +open Compat let is_meta s = String.length s > 0 && s.[0] == '$' @@ -18,9 +19,7 @@ let purge_str s = else String.sub s 1 (String.length s - 1) let anti loc x = - let e = <:expr< $lid:purge_str x$ >> - in - <:expr< $anti:e$ >> + expl_anti loc <:expr< $lid:purge_str x$ >> (* We don't give location for tactic quotation! *) let loc = dummy_loc @@ -411,12 +410,6 @@ let rec mlexpr_of_atomic_tactic = function let lems = mlexpr_of_list mlexpr_of_constr lems in <:expr< Tacexpr.TacTrivial $lems$ $l$ >> -(* - | Tacexpr.TacExtend (s,l) -> - let l = mlexpr_of_list mlexpr_of_tactic_arg l in - let $dloc$ = MLast.loc_of_expr l in - <:expr< Tacexpr.TacExtend $mlexpr_of_string s$ $l$ >> -*) | _ -> failwith "Quotation of atomic tactic expressions: TODO" and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function @@ -492,18 +485,47 @@ and mlexpr_of_tactic_arg = function <:expr< Tacexpr.Reference $mlexpr_of_reference r$ >> | _ -> failwith "mlexpr_of_tactic_arg: TODO" + +IFDEF CAMLP5 THEN + +let not_impl x = + let desc = + if Obj.is_block (Obj.repr x) then + "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) + else "int_val = " ^ string_of_int (Obj.magic x) + in + failwith ("<Q_coqast.patt_of_expt, not impl: " ^ desc) + +(* The following function is written without quotation + in order to be parsable even by camlp4. The version with + quotation can be found in revision <= 12972 of [q_util.ml4] *) + +open MLast + +let rec patt_of_expr e = + let loc = loc_of_expr e in + match e with + | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2) + | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2) + | ExLid (_, "loc") -> PaAny loc + | ExLid (_, s) -> PaLid (loc, s) + | ExUid (_, s) -> PaUid (loc, s) + | ExStr (_, s) -> PaStr (loc, s) + | ExAnt (_, e) -> PaAnt (loc, patt_of_expr e) + | _ -> not_impl e + let fconstr e = let ee s = - mlexpr_of_constr (Pcoq.Gram.Entry.parse e - (Pcoq.Gram.parsable (Stream.of_string s))) + mlexpr_of_constr (Pcoq.Gram.entry_parse e + (Pcoq.Gram.parsable (Stream.of_string s))) in let ep s = patt_of_expr (ee s) in Quotation.ExAst (ee, ep) let ftac e = let ee s = - mlexpr_of_tactic (Pcoq.Gram.Entry.parse e - (Pcoq.Gram.parsable (Stream.of_string s))) + mlexpr_of_tactic (Pcoq.Gram.entry_parse e + (Pcoq.Gram.parsable (Stream.of_string s))) in let ep s = patt_of_expr (ee s) in Quotation.ExAst (ee, ep) @@ -512,3 +534,23 @@ let _ = Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi); Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi); Quotation.default := "constr" + +ELSE + +open Pcaml + +let expand_constr_quot_expr loc _loc_name_opt contents = + mlexpr_of_constr + (Pcoq.Gram.parse_string Pcoq.Constr.constr_eoi loc contents) + +let expand_tactic_quot_expr loc _loc_name_opt contents = + mlexpr_of_tactic + (Pcoq.Gram.parse_string Pcoq.Tactic.tactic_eoi loc contents) + +let _ = + (* FIXME: for the moment, we add quotations in expressions only, not pattern *) + Quotation.add "constr" Quotation.DynAst.expr_tag expand_constr_quot_expr; + Quotation.add "tactic" Quotation.DynAst.expr_tag expand_tactic_quot_expr; + Quotation.default := "constr" + +END diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 94319cc73..f90de041a 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -8,30 +8,9 @@ (* This file defines standard combinators to build ml expressions *) -open Util open Extrawit -open Pcoq - -let not_impl name x = - let desc = - if Obj.is_block (Obj.repr x) then - "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) - else - "int_val = " ^ string_of_int (Obj.magic x) - in - failwith ("<Q_util." ^ name ^ ", not impl: " ^ desc) - -let rec patt_of_expr e = - let loc = MLast.loc_of_expr e in - match e with - | <:expr< $e1$.$e2$ >> -> <:patt< $patt_of_expr e1$.$patt_of_expr e2$ >> - | <:expr< $e1$ $e2$ >> -> <:patt< $patt_of_expr e1$ $patt_of_expr e2$ >> - | <:expr< loc >> -> <:patt< _ >> - | <:expr< $lid:s$ >> -> <:patt< $lid:s$ >> - | <:expr< $uid:s$ >> -> <:patt< $uid:s$ >> - | <:expr< $str:s$ >> -> <:patt< $str:s$ >> - | <:expr< $anti:e$ >> -> <:patt< $anti:patt_of_expr e$ >> - | _ -> not_impl "patt_of_expr" e +open Compat +open Util let mlexpr_of_list f l = List.fold_right @@ -77,15 +56,15 @@ open Pcoq open Genarg let rec mlexpr_of_prod_entry_key = function - | Extend.Alist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key s$ >> - | Extend.Alist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Alist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key s$ >> - | Extend.Alist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Aopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key s$ >> - | Extend.Amodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Extend.Aself -> <:expr< Extend.Aself >> - | Extend.Anext -> <:expr< Extend.Anext >> - | Extend.Atactic n -> <:expr< Extend.Atactic $mlexpr_of_int n$ >> - | Extend.Agram s -> anomaly "Agram not supported" - | Extend.Aentry ("",s) -> <:expr< Extend.Agram (Gram.Entry.obj $lid:s$) >> - | Extend.Aentry (u,s) -> <:expr< Extend.Aentry $str:u$ $str:s$ >> + | Alist1 s -> <:expr< Alist1 $mlexpr_of_prod_entry_key s$ >> + | Alist1sep (s,sep) -> <:expr< Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Alist0 s -> <:expr< Alist0 $mlexpr_of_prod_entry_key s$ >> + | Alist0sep (s,sep) -> <:expr< Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Aopt s -> <:expr< Aopt $mlexpr_of_prod_entry_key s$ >> + | Amodifiers s -> <:expr< Amodifiers $mlexpr_of_prod_entry_key s$ >> + | Aself -> <:expr< Aself >> + | Anext -> <:expr< Anext >> + | Atactic n -> <:expr< Atactic $mlexpr_of_int n$ >> + | Agram s -> Util.anomaly "Agram not supported" + | Aentry ("",s) -> <:expr< Agram (Gram.Entry.obj $lid:s$) >> + | Aentry (u,s) -> <:expr< Aentry $str:u$ $str:s$ >> diff --git a/parsing/q_util.mli b/parsing/q_util.mli index 59b3f334c..c19a0ecf5 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -6,7 +6,7 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -val patt_of_expr : MLast.expr -> MLast.patt +open Compat val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr @@ -30,4 +30,4 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr -val mlexpr_of_prod_entry_key : Pcoq.Gram.te Extend.prod_entry_key -> MLast.expr +val mlexpr_of_prod_entry_key : Pcoq.prod_entry_key -> MLast.expr diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index fb1425e0e..f64c8f700 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -14,6 +14,7 @@ open Argextend open Pcoq open Extrawit open Egrammar +open Compat let rec make_patt = function | [] -> <:patt< [] >> @@ -48,11 +49,6 @@ let rec make_let e = function <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let e l -let add_clause s (pt,e) l = - let p = make_patt pt in - let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, w, make_let e pt)::l - let rec extract_signature = function | [] -> [] | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l @@ -65,11 +61,14 @@ let check_unicity s l = ("Two distinct rules of tactic entry "^s^" have the same\n"^ "non-terminals in the same order: put them in distinct tactic entries") -let make_clauses s l = +let make_clause (pt,e) = + (make_patt pt, + Some (make_when (MLast.loc_of_expr e) pt), + make_let e pt) + +let make_fun_clauses loc s l = check_unicity s l; - let default = - (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in - List.fold_right (add_clause s) l [default] + Compat.make_fun loc (List.map make_clause l) let rec make_args = function | [] -> <:expr< [] >> @@ -160,13 +159,11 @@ let declare_tactic loc s cl = let atomic_tactics = mlexpr_of_list mlexpr_of_string (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in - <:str_item< - declare - open Pcoq; - open Extrawit; - declare $list:hidden$ end; + declare_str_items loc + (hidden @ + [ <:str_item< do { try - let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in + let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in List.iter (fun s -> Tacinterp.add_primitive_tactic s (Tacexpr.TacAtom($default_loc$, @@ -174,16 +171,16 @@ let declare_tactic loc s cl = $atomic_tactics$ with e -> Pp.pp (Cerrors.explain_exn e); Egrammar.extend_tactic_grammar $se$ $gl$; - List.iter Pptactic.declare_extra_tactic_pprule $pp$; - end - >> + List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> + ]) open Pcaml +open PcamlSig EXTEND GLOBAL: str_item; str_item: - [ [ "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ]; + [ [ "TACTIC"; "EXTEND"; s = tac_name; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> declare_tactic loc s l ] ] @@ -209,5 +206,10 @@ EXTEND GramTerminal s ] ] ; + tac_name: + [ [ s = LIDENT -> s + | s = UIDENT -> s + ] ] + ; END diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index d8b6fba31..1fa0e7e99 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -14,6 +14,7 @@ open Argextend open Tacextend open Pcoq open Egrammar +open Compat let rec make_let e = function | [] -> e @@ -24,11 +25,6 @@ let rec make_let e = function <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> | _::l -> make_let e l -let add_clause s (_,pt,e) l = - let p = make_patt pt in - let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, w, make_let e pt)::l - let check_unicity s l = let l' = List.map (fun (_,l,_) -> extract_signature l) l in if not (Util.list_distinct l') then @@ -36,11 +32,14 @@ let check_unicity s l = ("Two distinct rules of entry "^s^" have the same\n"^ "non-terminals in the same order: put them in distinct vernac entries") -let make_clauses s l = +let make_clause (_,pt,e) = + (make_patt pt, + Some (make_when (MLast.loc_of_expr e) pt), + make_let e pt) + +let make_fun_clauses loc s l = check_unicity s l; - let default = - (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in - List.fold_right (add_clause s) l [default] + Compat.make_fun loc (List.map make_clause l) let mlexpr_of_clause = mlexpr_of_list @@ -49,18 +48,16 @@ let mlexpr_of_clause = let declare_command loc s nt cl = let gl = mlexpr_of_clause cl in - let icl = make_clauses s cl in - <:str_item< - declare - open Pcoq; - open Extrawit; - try Vernacinterp.vinterp_add $mlexpr_of_string s$ (fun [ $list:icl$ ]) - with e -> Pp.pp (Cerrors.explain_exn e); - Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$; - end - >> + let funcl = make_fun_clauses loc s cl in + declare_str_items loc + [ <:str_item< do { + try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ + with e -> Pp.pp (Cerrors.explain_exn e); + Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + } >> ] open Pcaml +open PcamlSig EXTEND GLOBAL: str_item; diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 1b91ef177..aebe1fca4 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -17,6 +17,7 @@ open Pretyping.Default open Rawterm open Term open Pp +open Compat (* INTERN *) @@ -85,10 +86,10 @@ let intern_fundecl args body globs= let rec add_vars_of_simple_pattern globs = function CPatAlias (loc,p,id) -> add_vars_of_simple_pattern (add_var id globs) p -(* Stdpp.raise_with_loc loc +(* Loc.raise loc (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) | CPatOr (loc, _)-> - Stdpp.raise_with_loc loc + Loc.raise loc (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 28aa93975..11862747a 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -11,7 +11,7 @@ (* arnaud: veiller à l'aspect tutorial des commentaires *) open Pp - +open Tok open Decl_expr open Names open Term @@ -85,9 +85,9 @@ let vernac_proof_instr instr = (* We create a new parser entry [proof_mode]. The Declarative proof mode will replace the normal parser entry for tactics with this one. *) -let proof_mode = Gram.Entry.create "vernac:proof_command" +let proof_mode = Gram.entry_create "vernac:proof_command" (* Auxiliary grammar entry. *) -let proof_instr = Gram.Entry.create "proofmode:instr" +let proof_instr = Gram.entry_create "proofmode:instr" (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 9e415b635..e186dd76d 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -33,11 +33,11 @@ module Tactic = Pcoq.Tactic module SubtacGram = struct - let gec s = Gram.Entry.create ("Subtac."^s) + let gec s = Gram.entry_create ("Subtac."^s) (* types *) - let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc" + let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc" - let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac" + let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac" end open Rawterm diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 569aba263..9214e451f 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Global open Pp open Util @@ -228,8 +229,8 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Stdpp.Exc_located (loc, e') as e) -> + | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Loc.Exc_located (loc, e') as e) -> debug 2 (str "Parsing exception: "); (match e' with | Type_errors.TypeError (env, exn) -> diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index c7d0eb67f..591e01c04 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -15,6 +15,7 @@ open Util open Evd open Declare open Proof_type +open Compat let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Util.errorlabstrm "Program" cmd @@ -484,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac = true else false with - | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) - | Stdpp.Exc_located(_, Refiner.FailError (_, s)) + | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) + | Loc.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s) | Util.Anomaly _ as e -> raise e diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 0dda9b9e8..87c67cc14 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Compat open Util open Names open Sign @@ -270,7 +271,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -357,7 +358,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let j' = pretype_type empty_valcon env' evdref lvar c2 in let resj = try judge_of_product env name j j' - with TypeError _ as e -> Stdpp.raise_with_loc loc e in + with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon | RLetIn(loc,name,c1,c2) -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4b565ddbd..1a30b4e2c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util open Names open Nameops @@ -42,7 +43,7 @@ type pattern_matching_error = exception PatternMatchingError of env * pattern_matching_error let raise_pattern_matching_error (loc,ctx,te) = - Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te)) + Loc.raise loc (PatternMatchingError(ctx,te)) let error_bad_pattern_loc loc cstr ind = raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind)) @@ -98,7 +99,7 @@ let rec list_try_compile f = function | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> + | Loc.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> list_try_compile f t let force_name = diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 6adaee81c..5b829e5bf 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util -open Stdpp open Names open Sign open Term @@ -41,7 +41,7 @@ exception PretypeError of env * pretype_error let precatchable_exception = function | Util.UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + | Loc.Exc_located(_,(Util.UserError _ | TypeError _ | Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false @@ -96,10 +96,10 @@ let contract3 env a b c = match contract env [a;b;c] with | env, [a;b;c] -> env,a,b,c | _ -> assert false let raise_pretype_error (loc,ctx,sigma,te) = - Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te)) + Loc.raise loc (PretypeError(env_ise sigma ctx,te)) let raise_located_type_error (loc,ctx,sigma,te) = - Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te)) + Loc.raise loc (TypeError(env_ise sigma ctx,te)) let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = @@ -155,11 +155,11 @@ let error_occur_check env sigma ev c = let error_not_clean env sigma ev c (loc,k) = let c = nf_evar sigma c in - raise_with_loc loc + Loc.raise loc (PretypeError (env_ise sigma env, NotClean (ev,c,k))) let error_unsolvable_implicit loc env sigma evi e explain = - raise_with_loc loc + Loc.raise loc (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain))) let error_cannot_unify env sigma (m,n) = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 70241238d..22a3451c4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -21,6 +21,7 @@ (* Secondary maintenance: collective *) +open Compat open Pp open Util open Names @@ -66,7 +67,7 @@ let search_guard loc env possible_indexes fixdefs = let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with - | e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e); + | e -> if loc = dummy_loc then raise e else Loc.raise loc e); indexes else (* we now search recursively amoungst all combinations *) @@ -396,7 +397,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -464,7 +465,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct in let resj = try judge_of_product env name j j' - with TypeError _ as e -> Stdpp.raise_with_loc loc e in + with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon | RLetIn(loc,name,c1,c2) -> diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 869a7845d..983942aba 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Compat open Util open Libnames (*i*) @@ -45,7 +46,7 @@ let unsatisfiable_constraints env evd ev = raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) | Some ev -> let loc, kind = Evd.evar_source ev evd in - raise (Stdpp.Exc_located (loc, TypeClassError + raise (Loc.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (ev, kind))))) let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) @@ -53,5 +54,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan let rec unsatisfiable_exception exn = match exn with | TypeClassError (_, UnsatisfiableConstraints _) -> true - | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e + | Loc.Exc_located(_, e) -> unsatisfiable_exception e | _ -> false diff --git a/proofs/logic.ml b/proofs/logic.ml index 93de5be69..840c71ec6 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Util open Names @@ -45,7 +46,7 @@ exception RefinerError of refiner_error open Pretype_errors let rec catchable_exception = function - | Stdpp.Exc_located(_,e) -> catchable_exception e + | Loc.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e | Util.UserError _ | TypeError _ | RefinerError _ | Indrec.RecursionSchemeError _ diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 427a8d613..a25409521 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat + (* The proofview datastructure is a pure datastructure underlying the notion of proof (namely, a proof is a proofview which can evolve and has safety mechanisms attached). @@ -392,7 +394,7 @@ let rec tclGOALBINDU s k = this should be maintained synchronized, probably. *) open Pretype_errors let rec catchable_exception = function - | Stdpp.Exc_located(_,e) -> catchable_exception e + | Loc.Exc_located(_,e) -> catchable_exception e | Util.UserError _ | Type_errors.TypeError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index d87d73d31..a66ab6081 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Util open Term @@ -255,15 +256,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let catch_failerror e = if catchable_exception e then check_for_interrupt () else match e with - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) - | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) -> + | FailError (0,_) | Loc.Exc_located(_, FailError (0,_)) + | Loc.Exc_located(_, LtacLocated (_,FailError (0,_))) -> check_for_interrupt () | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located(s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) - | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + | Loc.Exc_located(s,FailError (lvl,s')) -> + raise (Loc.Exc_located(s,FailError (lvl - 1, s'))) + | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> raise - (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) + (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) | e -> raise e (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index ea777e6c5..8c51ec9e9 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -17,7 +17,8 @@ open Unix (* 1. Core objects *) let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"] let dynobjs = ["dynlink.cma"] -let camlp4objs = ["gramlib.cma"] +let camlp4objs = + if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"] let libobjs = ocamlobjs @ camlp4objs let spaces = Str.regexp "[ \t\n]+" @@ -33,7 +34,11 @@ let camlp4topobjs = if Coq_config.camlp4 = "camlp5" then ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] else - ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + [ "Camlp4Top.cmo"; + "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo"; + "Camlp4Parsers/Camlp4OCamlParser.cmo"; + "Camlp4Parsers/Camlp4GrammarParser.cmo"; + "q_util.cmo"; "q_coqast.cmo" ] let topobjs = camlp4topobjs let gramobjs = [] diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 38ae4b905..ba83fb5a8 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -35,6 +35,7 @@ open Pfedit open Command open Libnames open Evd +open Compat let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" @@ -205,7 +206,7 @@ let e_possible_resolve db_list local_db gl = let rec catchable = function | Refiner.FailError _ -> true - | Stdpp.Exc_located (_, e) -> catchable e + | Loc.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e let is_ground gl = diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 595917bdf..b51cb9d4b 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -15,7 +15,7 @@ open Evd open Environ open Explore -val hintbases : hint_db_name list option Pcoq.Gram.Entry.e +val hintbases : hint_db_name list option Pcoq.Gram.entry val wit_hintbases : hint_db_name list option typed_abstract_argument_type val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index ffa1bd747..2c750be36 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -16,15 +16,15 @@ open Rawterm val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool typed_abstract_argument_type -val orient : bool Pcoq.Gram.Entry.e +val orient : bool Pcoq.Gram.entry -val occurrences : (int list or_var) Pcoq.Gram.Entry.e +val occurrences : (int list or_var) Pcoq.Gram.entry val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type val rawwit_raw : constr_expr raw_abstract_argument_type val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type -val raw : constr_expr Pcoq.Gram.Entry.e +val raw : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * hyp_location_flag,unit) location @@ -33,17 +33,17 @@ type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type val wit_hloc : place typed_abstract_argument_type -val hloc : loc_place Pcoq.Gram.Entry.e +val hloc : loc_place Pcoq.Gram.entry -val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.Entry.e +val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.entry val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type @@ -51,6 +51,6 @@ val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type (** Spiwack: Primitive for retroknowledge registration *) -val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e +val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index d2381332e..4827c77b6 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -36,6 +36,7 @@ open Pfedit open Command open Libnames open Evd +open Compat (** Typeclass-based generalized rewriting. *) @@ -1052,7 +1053,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = else tclIDTAC in tclTHENLIST [evartac; rewtac] gl with - | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) + | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> Refiner.tclFAIL_lazy 0 (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 59d5cc313..3d5f2ba1b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -46,6 +46,7 @@ open Pretyping open Pretyping.Default open Extrawit open Pcoq +open Compat let safe_msgnl s = try msgnl s with e -> @@ -90,15 +91,15 @@ let dloc = dummy_loc let catch_error call_trace tac g = if call_trace = [] then tac g else try tac g with | LtacLocated _ as e -> raise e - | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e + | Loc.Exc_located (_,LtacLocated _) as e -> raise e | e -> let (nrep,loc',c),tail = list_sep_last call_trace in - let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in + let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in if tail = [] then let loc = if loc = dloc then loc' else loc in - raise (Stdpp.Exc_located(loc,e')) + raise (Loc.Exc_located(loc,e')) else - raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) + raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = @@ -1955,14 +1956,14 @@ and eval_with_fail ist is_lazy goal tac = VRTactic (catch_error trace tac goal) | a -> a) with - | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) - | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> + | FailError (0,s) | Loc.Exc_located(_, FailError (0,s)) + | Loc.Exc_located(_,LtacLocated (_,FailError (0,s))) -> raise (Eval_fail (Lazy.force s)) | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located(s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) - | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> - raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) + | Loc.Exc_located(s,FailError (lvl,s')) -> + raise (Loc.Exc_located(s,FailError (lvl - 1, s'))) + | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist gl llc u = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 21a9ee258..5c96c138e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Util open Names @@ -951,9 +952,9 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> if with_destruct then descend_in_conjunctions - try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl + try_main_apply (fun _ -> Loc.raise loc exn) c gl else - Stdpp.raise_with_loc loc exn + Loc.raise loc exn in try_red_apply thm_ty0 in try_main_apply with_destruct c gl0 @@ -1109,7 +1110,7 @@ let clear_wildcards ids = try with_check (Tacmach.thin_no_check [id]) gl with ClearDependencyError (id,err) -> (* Intercept standard [thin] error message *) - Stdpp.raise_with_loc loc + Loc.raise loc (error_clear_dependency (pf_env gl) (id_of_string "_") err)) ids diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index a7c89e7af..450796a53 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -418,7 +418,7 @@ let main_targets vfiles mlfiles other_targets inc = let all_target (vfiles, mlfiles, sps, sds) inc = let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in - let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in + let other_targets = List.map (function x,_,_ -> x) special_targets @ sds in section "Definition of the \"all\" target."; main_targets vfiles mlfiles other_targets inc; custom sps; diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 0e2b3724c..1f5bbc521 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Util open Indtypes open Type_errors open Pretype_errors open Indrec -open Lexer let print_loc loc = if loc = dummy_loc then @@ -111,20 +111,10 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Error: Tactic failure" ++ (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ if i=0 then str "." else str " (level " ++ int i ++ str").") - | Stdpp.Exc_located (loc,exc) -> + | Loc.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn_default_aux anomaly_string report_fn exc) - | Lexer.Error Illegal_character -> - hov 0 (str "Syntax error: Illegal character.") - | Lexer.Error Unterminated_comment -> - hov 0 (str "Syntax error: Unterminated comment.") - | Lexer.Error Unterminated_string -> - hov 0 (str "Syntax error: Unterminated string.") - | Lexer.Error Undefined_token -> - hov 0 (str "Syntax error: Undefined token.") - | Lexer.Error (Bad_token s) -> - hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s <> "" then diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index b99078106..443ed4853 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -8,6 +8,7 @@ open Pp open Flags +open Compat open Util open Names open Topconstr @@ -105,33 +106,33 @@ let add_tactic_notation (n,prods,e) = let print_grammar = function | "constr" | "operconstr" | "binder_constr" -> msgnl (str "Entry constr is"); - Gram.Entry.print Pcoq.Constr.constr; + Gram.entry_print Pcoq.Constr.constr; msgnl (str "and lconstr is"); - Gram.Entry.print Pcoq.Constr.lconstr; + Gram.entry_print Pcoq.Constr.lconstr; msgnl (str "where binder_constr is"); - Gram.Entry.print Pcoq.Constr.binder_constr; + Gram.entry_print Pcoq.Constr.binder_constr; msgnl (str "and operconstr is"); - Gram.Entry.print Pcoq.Constr.operconstr; + Gram.entry_print Pcoq.Constr.operconstr; | "pattern" -> - Gram.Entry.print Pcoq.Constr.pattern + Gram.entry_print Pcoq.Constr.pattern | "tactic" -> msgnl (str "Entry tactic_expr is"); - Gram.Entry.print Pcoq.Tactic.tactic_expr; + Gram.entry_print Pcoq.Tactic.tactic_expr; msgnl (str "Entry binder_tactic is"); - Gram.Entry.print Pcoq.Tactic.binder_tactic; + Gram.entry_print Pcoq.Tactic.binder_tactic; msgnl (str "Entry simple_tactic is"); - Gram.Entry.print Pcoq.Tactic.simple_tactic; + Gram.entry_print Pcoq.Tactic.simple_tactic; | "vernac" -> msgnl (str "Entry vernac is"); - Gram.Entry.print Pcoq.Vernac_.vernac; + Gram.entry_print Pcoq.Vernac_.vernac; msgnl (str "Entry command is"); - Gram.Entry.print Pcoq.Vernac_.command; + Gram.entry_print Pcoq.Vernac_.command; msgnl (str "Entry syntax is"); - Gram.Entry.print Pcoq.Vernac_.syntax; + Gram.entry_print Pcoq.Vernac_.syntax; msgnl (str "Entry gallina is"); - Gram.Entry.print Pcoq.Vernac_.gallina; + Gram.entry_print Pcoq.Vernac_.gallina; msgnl (str "Entry gallina_ext is"); - Gram.Entry.print Pcoq.Vernac_.gallina_ext; + Gram.entry_print Pcoq.Vernac_.gallina_ext; | _ -> error "Unknown or unprintable grammar entry." (**********************************************************************) @@ -232,7 +233,7 @@ let parse_format (loc,str) = else error "Empty format." with e -> - Stdpp.raise_with_loc loc e + Loc.raise loc e (***********************) (* Analyzing notations *) @@ -311,7 +312,7 @@ let rec interp_list_parser hd = function (* Find non-terminal tokens of notation *) let is_normal_token str = - try let _ = Lexer.check_ident str in true with Lexer.Error _ -> false + try let _ = Lexer.check_ident str in true with Lexer.Error.E _ -> false (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = @@ -379,9 +380,9 @@ type printing_precedence = int * parenRelation type parsing_precedence = int option let prec_assoc = function - | Gramext.RightA -> (L,E) - | Gramext.LeftA -> (E,L) - | Gramext.NonA -> (L,L) + | RightA -> (L,E) + | LeftA -> (E,L) + | NonA -> (L,L) let precedence_of_entry_type from = function | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n @@ -655,9 +656,9 @@ let border = function let recompute_assoc typs = match border typs, border (List.rev typs) with - | Some Gramext.LeftA, Some Gramext.RightA -> assert false - | Some Gramext.LeftA, _ -> Some Gramext.LeftA - | _, Some Gramext.RightA -> Some Gramext.RightA + | Some LeftA, Some RightA -> assert false + | Some LeftA, _ -> Some LeftA + | _, Some RightA -> Some RightA | _ -> None (**************************************************************************) @@ -846,7 +847,7 @@ let remove_curly_brackets l = let compute_syntax_data (df,modifiers) = let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in (* Notation defaults to NONA *) - let assoc = match assoc with None -> Some Gramext.NonA | a -> a in + let assoc = match assoc with None -> Some NonA | a -> a in let toks = split_notation_string df in let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in let ntn_for_interp = make_notation_key symbols in diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index b9d643540..6e679c720 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -13,6 +13,7 @@ open Cerrors open Vernac open Vernacexpr open Pcoq +open Compat (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -272,7 +273,7 @@ let set_prompt prompt = let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e - | Stdpp.Exc_located (_,e) -> is_pervasive_exn e + | Loc.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e | DuringSyntaxChecking (_,e) -> is_pervasive_exn e | _ -> false @@ -290,7 +291,7 @@ let print_toplevel_error exc = in let (locstrm,exc) = match exc with - | Stdpp.Exc_located (loc, ie) -> + | Loc.Exc_located (loc, ie) -> if valid_buffer_loc top_buffer dloc loc then (print_highlight_location top_buffer loc, ie) else @@ -314,7 +315,7 @@ let print_toplevel_error exc = (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot st = match Stream.next st with + let rec dot st = match get_tok (Stream.next st) with | Tok.KEYWORD "." -> () | Tok.EOI -> raise End_of_input | _ -> dot st @@ -324,8 +325,8 @@ let parse_to_dot = (* We assume that when a lexer error occurs, at least one char was eaten *) let rec discard_to_dot () = try - Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> + Gram.entry_parse parse_to_dot top_buffer.tokens + with Loc.Exc_located(_,(Token.Error _|Lexer.Error.E _)) -> discard_to_dot() diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f88d7be79..b3ef57814 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -16,6 +16,7 @@ open System open Vernacexpr open Vernacinterp open Ppvernac +open Compat (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions @@ -40,14 +41,14 @@ let raise_with_file file exc = match re with | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc -> ((b, f, loc), e) - | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> + | Loc.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) | _ -> ((false,file,cmdloc), re) in raise (Error_in_file (file, inner, disable_drop inex)) let real_error = function - | Stdpp.Exc_located (_, e) -> e + | Loc.Exc_located (_, e) -> e | Error_in_file (_, _, e) -> e | e -> e @@ -90,7 +91,7 @@ let verbose_phrase verbch loc = exception End_of_input let parse_sentence (po, verbch) = - match Pcoq.Gram.Entry.parse Pcoq.main_entry po with + match Pcoq.Gram.entry_parse Pcoq.main_entry po with | Some (loc,_ as com) -> verbose_phrase verbch loc; com | None -> raise End_of_input diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index b8c8d261d..ebdec85ee 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util open Names open Tacexpr @@ -183,7 +184,7 @@ type grammar_tactic_prod_item_expr = type syntax_modifier = | SetItemLevel of string list * production_level | SetLevel of int - | SetAssoc of Gramext.g_assoc + | SetAssoc of gram_assoc | SetEntryType of string * simple_constr_prod_entry_key | SetOnlyParsing | SetFormat of string located |