From 25533df336888df4255e3882e21d5d5420e5de28 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 9 Jul 2010 17:40:36 +0000 Subject: Finish adding out-of-the-box support for camlp4 If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.build | 27 +++++++++++++++++++++++---- parsing/argextend.ml4 | 2 ++ parsing/q_constr.ml4 | 2 ++ parsing/tacextend.ml4 | 2 ++ parsing/vernacextend.ml4 | 2 ++ tactics/extratactics.ml4 | 9 +++++---- tools/compat5.ml | 13 +++++++++++++ tools/compat5.mlp | 23 +++++++++++++++++++++++ tools/compat5b.ml | 13 +++++++++++++ tools/compat5b.mlp | 23 +++++++++++++++++++++++ 10 files changed, 108 insertions(+), 8 deletions(-) create mode 100644 tools/compat5.ml create mode 100644 tools/compat5.mlp create mode 100644 tools/compat5b.ml create mode 100644 tools/compat5b.mlp diff --git a/Makefile.build b/Makefile.build index adba237537..0540b9a9ae 100644 --- a/Makefile.build +++ b/Makefile.build @@ -499,6 +499,20 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) +# Special rule for the compatibility-with-camlp5 extension for camlp4 + +ifeq ($(CAMLP4),camlp4) +tools/compat5.cmo: tools/compat5.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< +tools/compat5b.cmo: tools/compat5b.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< +else +tools/compat5.cmo: tools/compat5.ml + $(OCAMLC) -c $< +tools/compat5b.cmo: tools/compat5b.ml + $(OCAMLC) -c $< +endif + ########################################################################### # Installation ########################################################################### @@ -673,11 +687,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< $(TOTARGET) + $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@ toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< $(TOTARGET) + $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@ # pretty printing of the revision number when compiling a checked out # source tree @@ -796,12 +810,17 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ $(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ -%.ml: %.ml4 | %.ml4.d +# NB: compatibility modules for camlp4: +# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded +# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with +# syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps + +%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo $(SHOW)'CAMLP4O $<' $(HIDE)\ DEPS=$(CAMLP4DEPS); \ if ls $${DEPS} > /dev/null 2>&1; then \ - $(CAMLP4O) $(PR_O) -I $(CAMLLIB) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \ + $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \ else echo $< : Dependency $${DEPS} not ready yet; false; fi %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index e156bdc266..fc1f05dad2 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Genarg open Q_util open Egrammar diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index fb34a5aa27..43f4559246 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Rawterm open Term open Names diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index f64c8f700c..3aac36c08a 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Util open Genarg open Q_util diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 1fa0e7e99b..9ed89536c5 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Util open Genarg open Q_util diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0ddb4da755..e71e6366ca 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -21,6 +21,7 @@ open Util open Termops open Evd open Equality +open Compat (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) @@ -543,7 +544,7 @@ let subst_var_with_hole occ tid t = | RVar (_,id) as x -> if id = tid then (decr occref; if !occref = 0 then x - else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))) + else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) else x | c -> map_rawconstr_left_to_right substrec c in let t' = substrec t @@ -556,7 +557,7 @@ let subst_hole_with_term occ tc t = let rec substrec = function | RHole (_,Evd.QuestionMark(Evd.Define true)) -> decr occref; if !occref = 0 then tc - else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))) + else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) | c -> map_rawconstr_left_to_right substrec c in substrec t @@ -578,8 +579,8 @@ let hResolve id c occ t gl = try Pretyping.Default.understand sigma env t_hole with - | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> - resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole) + | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> + resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) in let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in let t_constr_type = Retyping.get_type_of env sigma t_constr in diff --git a/tools/compat5.ml b/tools/compat5.ml new file mode 100644 index 0000000000..6a76895cd9 --- /dev/null +++ b/tools/compat5.ml @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] -> + [< '(KEYWORD "EXTEND", loc); my_token_filter s >] + | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] + | [< >] -> [< >] + +let _ = + Token.Filter.define_filter (Gram.get_filter()) + (fun prev strm -> prev (my_token_filter strm)) diff --git a/tools/compat5b.ml b/tools/compat5b.ml new file mode 100644 index 0000000000..03bdb358b0 --- /dev/null +++ b/tools/compat5b.ml @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] -> + [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] + | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] + | [< >] -> [< >] + +let _ = + Token.Filter.define_filter (Gram.get_filter()) + (fun prev strm -> prev (my_token_filter strm)) -- cgit v1.2.3