diff options
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 |