From ec6924edf26b16a808a58bc26356b41450b29cfa Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 12 Oct 2007 18:12:38 +0000 Subject: [PATCH] Move to OCaml 3.10. Requires debian packages from unstable (soon in testing). --- Makefile.defs.in | 2 +- components/METAS/meta.helm-content_pres.src | 2 +- components/METAS/meta.helm-extlib.src | 2 +- components/METAS/meta.helm-grafite_parser.src | 2 +- components/METAS/meta.helm-lexicon.src | 2 +- .../METAS/meta.helm-syntax_extensions.src | 2 +- components/Makefile.common | 8 ++++---- components/acic_content/cicNotationPt.ml | 2 +- components/binaries/extractor/Makefile | 8 ++++---- components/binaries/heights/Makefile | 4 ++-- components/binaries/table_creator/Makefile | 4 ++-- components/binaries/transcript/Makefile | 4 ++-- components/binaries/utilities/Makefile | 2 +- components/cic_disambiguation/disambiguate.ml | 10 +++++----- .../cic_disambiguation/disambiguate.mli | 4 ++-- .../cic_disambiguation/disambiguateTypes.ml | 2 +- .../cic_disambiguation/disambiguateTypes.mli | 2 +- components/cic_proof_checking/Makefile | 4 ---- components/cic_unification/cicRefine.mli | 4 ++-- components/content_pres/Makefile | 4 ++-- components/content_pres/cicNotationLexer.ml | 16 +++++---------- components/content_pres/cicNotationParser.ml | 2 +- components/extlib/hExtlib.ml | 20 +++++-------------- components/extlib/hExtlib.mli | 10 +++++----- components/grafite/grafiteAst.ml | 2 +- components/grafite_parser/Makefile | 4 ++-- .../grafite_parser/grafiteDisambiguator.ml | 6 +++--- .../grafite_parser/grafiteDisambiguator.mli | 6 +++--- components/lexicon/lexiconAst.ml | 2 +- components/library/refinementTool.ml | 2 +- components/syntax_extensions/Makefile | 8 ++++---- components/syntax_extensions/README.syntax | 2 +- .../syntax_extensions/pa_unicode_macro.ml | 7 +------ components/tactics/Makefile | 2 +- configure.ac | 10 +++++----- matita/Makefile | 2 +- matita/library/algebra/finite_groups.ma | 6 +----- matita/library/nat/orders.ma | 6 ++++++ matita/matitaExcPp.ml | 5 +---- matita/matitaExcPp.mli | 2 +- matita/matitaGtkMisc.mli | 2 +- 41 files changed, 85 insertions(+), 111 deletions(-) diff --git a/Makefile.defs.in b/Makefile.defs.in index 804d2489d..faa0c41f4 100644 --- a/Makefile.defs.in +++ b/Makefile.defs.in @@ -3,7 +3,7 @@ OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@ else OCAMLFIND = @OCAMLFIND@ endif -CAMLP4O = @CAMLP4O@ +CAMLP5O = @CAMLP5O@ LABLGLADECC = @LABLGLADECC@ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ DISTRIBUTED = @DISTRIBUTED@ diff --git a/components/METAS/meta.helm-content_pres.src b/components/METAS/meta.helm-content_pres.src index 1e76f9fe8..976b8f10c 100644 --- a/components/METAS/meta.helm-content_pres.src +++ b/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-acic_content helm-syntax_extensions camlp4.gramlib ulex helm-grafite" +requires="helm-acic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/components/METAS/meta.helm-extlib.src b/components/METAS/meta.helm-extlib.src index bfee89e3d..2002fccf1 100644 --- a/components/METAS/meta.helm-extlib.src +++ b/components/METAS/meta.helm-extlib.src @@ -1,4 +1,4 @@ -requires="unix camlp4.gramlib" +requires="unix camlp5.gramlib" version="0.0.1" archive(byte)="extlib.cma" archive(native)="extlib.cmxa" diff --git a/components/METAS/meta.helm-grafite_parser.src b/components/METAS/meta.helm-grafite_parser.src index d921b5588..abf16caeb 100644 --- a/components/METAS/meta.helm-grafite_parser.src +++ b/components/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-lexicon helm-grafite ulex" +requires="helm-lexicon helm-grafite ulex08" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/components/METAS/meta.helm-lexicon.src b/components/METAS/meta.helm-lexicon.src index 35ab5dd36..741fd603e 100644 --- a/components/METAS/meta.helm-lexicon.src +++ b/components/METAS/meta.helm-lexicon.src @@ -1,4 +1,4 @@ -requires="helm-content_pres helm-cic_disambiguation camlp4.gramlib" +requires="helm-content_pres helm-cic_disambiguation camlp5.gramlib" version="0.0.1" archive(byte)="lexicon.cma" archive(native)="lexicon.cmxa" diff --git a/components/METAS/meta.helm-syntax_extensions.src b/components/METAS/meta.helm-syntax_extensions.src index eb25adac0..f9e210f6e 100644 --- a/components/METAS/meta.helm-syntax_extensions.src +++ b/components/METAS/meta.helm-syntax_extensions.src @@ -2,6 +2,6 @@ requires="str" version="0.0.1" archive(byte)="utf8_macros.cma" archive(native)="utf8_macros.cmxa" -requires(syntax,preprocessor)="camlp4" +requires(syntax,preprocessor)="camlp5" archive(syntax,preprocessor)="pa_extend.cmo pa_unicode_macro.cma profiling_macros.cma" linkopts="" diff --git a/components/Makefile.common b/components/Makefile.common index 59b35aa73..5090dcc78 100644 --- a/components/Makefile.common +++ b/components/Makefile.common @@ -11,10 +11,10 @@ H=@ # $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH= -PREPROCOPTIONS = -pp camlp4o -SYNTAXOPTIONS = -syntax camlp4o +PREPROCOPTIONS = -pp camlp5o +SYNTAXOPTIONS = -syntax camlp5o PREREQ = -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes OCAMLDEBUGOPTIONS = -g #OCAML_PROF=p -p a OCAMLARCHIVEOPTIONS = @@ -22,7 +22,7 @@ REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE)) OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS) #OCAMLOPT_DEBUG_FLAGS = -p OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS) $(OCAMLOPT_DEBUG_FLAGS) -OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4 $(CAMLP4REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) +OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp5 $(CAMLP5REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) OCAMLLEX = ocamllex OCAMLYACC = ocamlyacc diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml index 73eeb017d..27ec5734f 100644 --- a/components/acic_content/cicNotationPt.ml +++ b/components/acic_content/cicNotationPt.ml @@ -32,7 +32,7 @@ type induction_kind = [ `Inductive | `CoInductive ] type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] type fold_kind = [ `Left | `Right ] -type location = Token.flocation +type location = Stdpp.location let fail floc msg = let (x, y) = HExtlib.loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) diff --git a/components/binaries/extractor/Makefile b/components/binaries/extractor/Makefile index 323f405d4..512b13e73 100644 --- a/components/binaries/extractor/Makefile +++ b/components/binaries/extractor/Makefile @@ -11,22 +11,22 @@ clean: extractor: extractor.ml $(H)echo " OCAMLC $<" $(H)$(OCAMLFIND) ocamlc \ - -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $< + -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $< extractor.opt: extractor.ml $(H)echo " OCAMLOPT $<" $(H)$(OCAMLFIND) ocamlopt \ - -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $< + -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $< extractor_manager: extractor_manager.ml $(H)echo " OCAMLC $<" $(H)$(OCAMLFIND) ocamlc \ - -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $< + -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $< extractor_manager.opt: extractor_manager.ml $(H)echo " OCAMLOPT $<" $(H)$(OCAMLFIND) ocamlopt \ - -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $< + -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $< export: extractor.opt extractor_manager.opt nice -n 20 \ diff --git a/components/binaries/heights/Makefile b/components/binaries/heights/Makefile index d989d9c58..cd270082a 100644 --- a/components/binaries/heights/Makefile +++ b/components/binaries/heights/Makefile @@ -16,8 +16,8 @@ CMXS = $(MLS:%.ml=%.cmx) CMIS = $(MLIS:%.mli=%.cmi) EXTRAS = -OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg +OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes +OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes OCAMLDEP = $(OCAMLFIND) ocamldep OCAMLYACC = ocamlyacc OCAMLLEX = ocamllex diff --git a/components/binaries/table_creator/Makefile b/components/binaries/table_creator/Makefile index 23e732629..d5889699f 100644 --- a/components/binaries/table_creator/Makefile +++ b/components/binaries/table_creator/Makefile @@ -16,7 +16,7 @@ opt: table_creator.opt table_destructor.opt table_creator: table_creator.ml $(H)echo " OCAMLC $<" $(H)$(OCAMLFIND) ocamlc \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< + -thread -package mysql,helm-metadata -linkpkg -rectypes -o $@ $< table_destructor: table_creator $(H)ln -f $< $@ @@ -24,7 +24,7 @@ table_destructor: table_creator table_creator.opt: table_creator.ml $(H)echo " OCAMLOPT $<" $(H)$(OCAMLFIND) ocamlopt \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< + -thread -package mysql,helm-metadata -linkpkg -rectypes -o $@ $< table_destructor.opt: table_creator.opt $(H)ln -f $< $@ diff --git a/components/binaries/transcript/Makefile b/components/binaries/transcript/Makefile index 7d6cd364f..b9bfc6109 100644 --- a/components/binaries/transcript/Makefile +++ b/components/binaries/transcript/Makefile @@ -18,8 +18,8 @@ CMXS = $(MLS:%.ml=%.cmx) CMIS = $(MLIS:%.mli=%.cmi) EXTRAS = -OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg +OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes +OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes OCAMLDEP = $(OCAMLFIND) ocamldep OCAMLYACC = ocamlyacc OCAMLLEX = ocamllex diff --git a/components/binaries/utilities/Makefile b/components/binaries/utilities/Makefile index 1874a2385..db76fb51d 100644 --- a/components/binaries/utilities/Makefile +++ b/components/binaries/utilities/Makefile @@ -2,7 +2,7 @@ H=@ UTILITIES = create_environment parse_library list_uris test_library UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES)) -LINKOPTS = -linkpkg -thread +LINKOPTS = -linkpkg -rectypes -thread LIBS = helm-cic_proof_checking OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS) OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index e93c54808..0b8674c0c 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -35,9 +35,9 @@ module Ast = CicNotationPt (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of int * - ((Token.flocation list * string * string) list * + ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t * bool) list + Stdpp.location option * string Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -47,7 +47,7 @@ type aliases = bool * DisambiguateTypes.environment type 'a disambiguator_input = string * int * 'a type domain = domain_tree list -and domain_tree = Node of Token.flocation list * domain_item * domain +and domain_tree = Node of Stdpp.location list * domain_item * domain let rec string_of_domain = function @@ -105,8 +105,8 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko of Token.flocation option * string Lazy.t - | Uncertain of Token.flocation option * string Lazy.t + | Ko of Stdpp.location option * string Lazy.t + | Uncertain of Stdpp.location option * string Lazy.t let refine_term metasenv context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli index 4fe40da91..5dc0df28b 100644 --- a/components/cic_disambiguation/disambiguate.mli +++ b/components/cic_disambiguation/disambiguate.mli @@ -35,9 +35,9 @@ * useless for the final user ... *) exception NoWellTypedInterpretation of int * - ((Token.flocation list * string * string) list * + ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t * bool) list + Stdpp.location option * string Lazy.t * bool) list exception PathNotWellFormed val interpretate_path : diff --git a/components/cic_disambiguation/disambiguateTypes.ml b/components/cic_disambiguation/disambiguateTypes.ml index 8263fd315..150482fbf 100644 --- a/components/cic_disambiguation/disambiguateTypes.ml +++ b/components/cic_disambiguation/disambiguateTypes.ml @@ -116,7 +116,7 @@ module type Callbacks = UriManager.uri list val interactive_interpretation_choice: string -> int -> - (Token.flocation list * string * string) list list -> int list + (Stdpp.location list * string * string) list list -> int list val input_or_locate_uri: title:string -> ?id:string -> unit -> UriManager.uri option end diff --git a/components/cic_disambiguation/disambiguateTypes.mli b/components/cic_disambiguation/disambiguateTypes.mli index b584f0bec..961056701 100644 --- a/components/cic_disambiguation/disambiguateTypes.mli +++ b/components/cic_disambiguation/disambiguateTypes.mli @@ -72,7 +72,7 @@ module type Callbacks = val interactive_interpretation_choice : string -> int -> - (Token.flocation list * string * string) list list -> int list + (Stdpp.location list * string * string) list list -> int list (** @param title gtk window title for user prompting * @param id unbound identifier which originated this callback invocation *) diff --git a/components/cic_proof_checking/Makefile b/components/cic_proof_checking/Makefile index 83b211447..b2ee8993f 100644 --- a/components/cic_proof_checking/Makefile +++ b/components/cic_proof_checking/Makefile @@ -25,7 +25,3 @@ EXTRA_OBJECTS_TO_CLEAN = include ../../Makefile.defs include ../Makefile.common - -cicReduction.cmo: OCAMLOPTIONS+=-rectypes -cicReduction.cmx: OCAMLOPTIONS+=-rectypes - diff --git a/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli index 30b264455..924020cbb 100644 --- a/components/cic_unification/cicRefine.mli +++ b/components/cic_unification/cicRefine.mli @@ -31,7 +31,7 @@ exception AssertFailure of string Lazy.t;; (* refines [term] and returns the refined form of [term], *) (* its type, the new metasenv and universe graph. *) val type_of_aux': - ?localization_tbl:Token.flocation Cic.CicHash.t -> + ?localization_tbl:Stdpp.location Cic.CicHash.t -> Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph @@ -40,7 +40,7 @@ val type_of_aux': (* the new metasenv and universe graph. *) (* the [uri] is required only for inductive definitions *) val typecheck : - localization_tbl:Token.flocation Cic.CicHash.t -> + localization_tbl:Stdpp.location Cic.CicHash.t -> Cic.metasenv -> UriManager.uri option -> Cic.obj -> Cic.obj * Cic.metasenv * CicUniv.universe_graph diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile index fb6d0fe46..2eadef187 100644 --- a/components/content_pres/Makefile +++ b/components/content_pres/Makefile @@ -47,8 +47,8 @@ include ../Makefile.common # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by # "_loc" occurrences UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions) -ULEXDIR := $(shell $(OCAMLFIND) query ulex) -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" +ULEXDIR := $(shell $(OCAMLFIND) query ulex08) +MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/components/content_pres/cicNotationLexer.ml b/components/content_pres/cicNotationLexer.ml index f157af406..bd071c5b9 100644 --- a/components/content_pres/cicNotationLexer.ml +++ b/components/content_pres/cicNotationLexer.ml @@ -144,14 +144,8 @@ let error_at_end lexbuf msg = raise (Error (begin_cnum, end_cnum, msg)) let return_with_loc token begin_cnum end_cnum = - (* TODO handle line/column numbers *) - let flocation_begin = - { Lexing.pos_fname = ""; - Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = begin_cnum } - in - let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in - (token, (flocation_begin, flocation_end)) + let flocation = HExtlib.floc_of_loc (begin_cnum,end_cnum) in + token, flocation let return lexbuf token = let begin_cnum, end_cnum = Ulexing.loc lexbuf in @@ -169,17 +163,17 @@ let mk_lexer token = (* let lexbuf = Ulexing.from_utf8_stream stream in *) (** XXX Obj.magic rationale. * The problem. - * camlp4 constraints the tok_func field of Token.glexer to have type: + * camlp5 constraints the tok_func field of Token.glexer to have type: * Stream.t char -> (Stream.t 'te * flocation_function) * In order to use ulex we have (in theory) to instantiate a new lexbuf each * time a char Stream.t is passed, destroying the previous lexbuf which may * have consumed a character from the old stream which is lost forever :-( * The "solution". - * Instead of passing to camlp4 a char Stream.t we pass a lexbuf, casting it to + * Instead of passing to camlp5 a char Stream.t we pass a lexbuf, casting it to * char Stream.t with Obj.magic where needed. *) let lexbuf = Obj.magic stream in - Token.make_stream_and_flocation + Token.make_stream_and_location (fun () -> try token lexbuf diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml index d110bda9a..05075f0c3 100644 --- a/components/content_pres/cicNotationParser.ml +++ b/components/content_pres/cicNotationParser.ml @@ -224,7 +224,7 @@ let level_of precedence associativity = in string_of_int precedence ^ assoc_string -type rule_id = Token.t Gramext.g_symbol list +type rule_id = Grammar.token Gramext.g_symbol list (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *) let owned_keywords = Hashtbl.create 23 diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index 9e2277b43..24f0dd196 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -403,30 +403,20 @@ let finally at_end f arg = (** {2 Localized exceptions } *) -exception Localized of Token.flocation * exn +exception Localized of Stdpp.location * exn -let loc_of_floc = function - | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> - (loc_begin, loc_end) +let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;; let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) + Stdpp.make_loc (loc_begin, loc_end) let dummy_floc = floc_of_loc (-1, -1) let raise_localized_exception ~offset floc exn = - let (x, y) = loc_of_floc floc in + let x, y = loc_of_floc floc in let x = offset + x in let y = offset + y in - let flocb,floce = floc in - let floc = - { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } - in + let floc = floc_of_loc (x,y) in raise (Localized (floc, exn)) let estimate_size x = diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli index 5f6626b14..f951a6709 100644 --- a/components/extlib/hExtlib.mli +++ b/components/extlib/hExtlib.mli @@ -102,14 +102,14 @@ val set_profiling_printings : (string -> bool) -> unit (** {2 Localized exceptions } *) -exception Localized of Token.flocation * exn +exception Localized of Stdpp.location * exn -val loc_of_floc: Token.flocation -> int * int -val floc_of_loc: int * int -> Token.flocation +val loc_of_floc: Stdpp.location -> int * int +val floc_of_loc: int * int -> Stdpp.location -val dummy_floc: Lexing.position * Lexing.position +val dummy_floc: Stdpp.location -val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a +val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a (* size in KB (SLOW) *) val estimate_size: 'a -> int diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index b0c25bc1e..a0bb2e4f9 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -27,7 +27,7 @@ type direction = [ `LeftToRight | `RightToLeft ] -type loc = Token.flocation +type loc = Stdpp.location type ('term, 'lazy_term, 'ident) pattern = 'lazy_term option * ('ident * 'term) list * 'term option diff --git a/components/grafite_parser/Makefile b/components/grafite_parser/Makefile index 06824b141..eb2f1b1eb 100644 --- a/components/grafite_parser/Makefile +++ b/components/grafite_parser/Makefile @@ -18,8 +18,8 @@ clean: clean_tests # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by # "_loc" occurrences UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) -ULEXDIR = $(shell $(OCAMLFIND) query ulex) -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" +ULEXDIR = $(shell $(OCAMLFIND) query ulex08) +MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml index 4f812ff2f..fc2cbc74e 100644 --- a/components/grafite_parser/grafiteDisambiguator.ml +++ b/components/grafite_parser/grafiteDisambiguator.ml @@ -31,9 +31,9 @@ exception Ambiguous_input (* the integer is an offset to be added to each location *) exception DisambiguationError of int * - ((Token.flocation list * string * string) list * + ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t * bool) list list + Stdpp.location option * string Lazy.t * bool) list list (** parameters are: option name, error message *) exception Unbound_identifier of string @@ -42,7 +42,7 @@ type choose_uris_callback = type choose_interp_callback = string -> int -> - (Token.flocation list * string * string) list list -> int list + (Stdpp.location list * string * string) list list -> int list let mono_uris_callback ~id = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true diff --git a/components/grafite_parser/grafiteDisambiguator.mli b/components/grafite_parser/grafiteDisambiguator.mli index f37991f93..88940c2c3 100644 --- a/components/grafite_parser/grafiteDisambiguator.mli +++ b/components/grafite_parser/grafiteDisambiguator.mli @@ -29,9 +29,9 @@ exception Ambiguous_input (* the integer is an offset to be added to each location *) exception DisambiguationError of int * - ((Token.flocation list * string * string) list * + ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t * bool) list list + Stdpp.location option * string Lazy.t * bool) list list (** parameters are: option name, error message *) (** initially false; for debugging only (???) *) @@ -39,7 +39,7 @@ val only_one_pass: bool ref type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list type choose_interp_callback = - string -> int -> (Token.flocation list * string * string) list list -> + string -> int -> (Stdpp.location list * string * string) list list -> int list val set_choose_uris_callback: choose_uris_callback -> unit diff --git a/components/lexicon/lexiconAst.ml b/components/lexicon/lexiconAst.ml index 65bb7ce64..5a09d590a 100644 --- a/components/lexicon/lexiconAst.ml +++ b/components/lexicon/lexiconAst.ml @@ -27,7 +27,7 @@ type direction = [ `LeftToRight | `RightToLeft ] -type loc = Token.flocation +type loc = Stdpp.location type alias_spec = | Ident_alias of string * string (* identifier, uri *) diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml index e9dae40d9..b78246987 100644 --- a/components/library/refinementTool.ml +++ b/components/library/refinementTool.ml @@ -30,7 +30,7 @@ type type_of_rc = (* these are the same functions of cic_unification/ (eventually wrapped) *) type kit = { type_of_aux': - ?localization_tbl:Token.flocation Cic.CicHash.t -> + ?localization_tbl:Stdpp.location Cic.CicHash.t -> Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> type_of_rc; pack_coercion_obj: Cic.obj -> Cic.obj; diff --git a/components/syntax_extensions/Makefile b/components/syntax_extensions/Makefile index 92ed07776..f274c6a8e 100644 --- a/components/syntax_extensions/Makefile +++ b/components/syntax_extensions/Makefile @@ -18,18 +18,18 @@ utf8MacroTable.ml: ./make_table $@ utf8MacroTable.cmo: utf8MacroTable.ml @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -c $< + $(H)@$(OCAMLFIND) ocamlc -c -rectypes $< pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $< + $(H)@$(OCAMLFIND) ocamlc -package camlp5 -rectypes -pp "camlp5o q_MLast.cmo pa_extend.cmo -loc loc" -c $< pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo @echo " OCAMLC -a $@" $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ profiling_macros.cmo: profiling_macros.ml @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o -loc loc" -c $< + $(H)@$(OCAMLFIND) ocamlc -package camlp5 -pp "camlp5o -loc loc" -c $< profiling_macros.cma:profiling_macros.cmo @echo " OCAMLC -a $@" $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ @@ -37,7 +37,7 @@ profiling_macros.cma:profiling_macros.cmo .PHONY: test test: test.ml - $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp4o $< -o $@ + $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp5o $< -o $@ clean: distclean: extra_clean diff --git a/components/syntax_extensions/README.syntax b/components/syntax_extensions/README.syntax index 210ecc095..eddc7f45b 100644 --- a/components/syntax_extensions/README.syntax +++ b/components/syntax_extensions/README.syntax @@ -11,5 +11,5 @@ Sample file: Compile it with: - ocamlfind ocamlc -package helm-utf8_macros -syntax camlp4o test.ml + ocamlfind ocamlc -package helm-utf8_macros -syntax camlp5o test.ml diff --git a/components/syntax_extensions/pa_unicode_macro.ml b/components/syntax_extensions/pa_unicode_macro.ml index dda7d4cab..436766862 100644 --- a/components/syntax_extensions/pa_unicode_macro.ml +++ b/components/syntax_extensions/pa_unicode_macro.ml @@ -28,12 +28,7 @@ let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) -let loc = - let dummy_pos = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = -1 } - in - (dummy_pos, dummy_pos) +let loc = Stdpp.make_loc (-1, -1) let expand_unicode_macro macro = debug_print (lazy (Printf.sprintf "Expanding macro '%s' ..." macro)); diff --git a/components/tactics/Makefile b/components/tactics/Makefile index b576f830b..c4e020005 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -42,7 +42,7 @@ tactics.mli: tactics.ml UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) STR=$(shell $(OCAMLFIND) query str) -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc" +MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc" paramodulation/%.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) paramodulation/%.cmo: OCAMLC = $(OCAMLC_P4) paramodulation/%.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/configure.ac b/configure.ac index 0af17fcad..4e7814399 100644 --- a/configure.ac +++ b/configure.ac @@ -30,11 +30,11 @@ if test $HAVE_LABLGLADECC = "yes"; then else AC_MSG_ERROR(could not find lablgladecc2) fi -AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no) -if test $HAVE_CAMLP4O = "yes"; then - CAMLP4O="camlp4o" +AC_CHECK_PROG(HAVE_CAMLP5O, camlp5o, yes, no) +if test $HAVE_CAMLP5O = "yes"; then + CAMLP5O="camlp5o" else - AC_MSG_ERROR(could not find camlp4o) + AC_MSG_ERROR(could not find camlp5o) fi # look for METAS dir @@ -168,7 +168,7 @@ if test "yes" = "$DBHOST"; then fi AC_MSG_RESULT($MSG) -AC_SUBST(CAMLP4O) +AC_SUBST(CAMLP5O) AC_SUBST(DBHOST) AC_SUBST(DEBUG) AC_SUBST(DISTRIBUTED) diff --git a/matita/Makefile b/matita/Makefile index 93a6fc6cb..923a0f614 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -5,7 +5,7 @@ include ../Makefile.defs NULL = H=@ -OCAML_FLAGS = -pp $(CAMLP4O) +OCAML_FLAGS = -pp $(CAMLP5O) -rectypes PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" OCAML_THREADS_FLAGS = -thread diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma index 79521e206..7f76ae0c8 100644 --- a/matita/library/algebra/finite_groups.ma +++ b/matita/library/algebra/finite_groups.ma @@ -175,11 +175,7 @@ intro; apply (not_le_Sn_n ? H3). qed. -theorem lt_S_S: ∀n,m. n < m → S n < S m. -intros; -unfold lt in H; -apply (le_S_S ? ? H). -qed. + (* moved to nat/order.ma theorem lt_O_S: ∀n. O < S n. diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma index 8053d50de..42454393c 100644 --- a/matita/library/nat/orders.ma +++ b/matita/library/nat/orders.ma @@ -100,6 +100,12 @@ theorem lt_S_S_to_lt: \forall n,m. intros. apply le_S_S_to_le. assumption. qed. +theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m. +intros; +unfold lt in H; +apply (le_S_S ? ? H). +qed. + theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m. intros.elim H.exact I.exact I. qed. diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml index 339971fea..42777735c 100644 --- a/matita/matitaExcPp.ml +++ b/matita/matitaExcPp.ml @@ -96,10 +96,7 @@ let rec to_string = let (x, y) = HExtlib.loc_of_floc floc in let x = x + offset in let y = y + offset in - let flocb,floce = floc in - let floc = - {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y} - in + let floc = HExtlib.floc_of_loc (x,y) in Some floc | _ -> None in let rec explain = diff --git a/matita/matitaExcPp.mli b/matita/matitaExcPp.mli index 9d8c7739f..4abe0b4f9 100644 --- a/matita/matitaExcPp.mli +++ b/matita/matitaExcPp.mli @@ -23,5 +23,5 @@ * http://helm.cs.unibo.it/ *) -val to_string: exn -> Token.flocation option * string +val to_string: exn -> Stdpp.location option * string diff --git a/matita/matitaGtkMisc.mli b/matita/matitaGtkMisc.mli index 40fc9373b..0f78a4a61 100644 --- a/matita/matitaGtkMisc.mli +++ b/matita/matitaGtkMisc.mli @@ -146,7 +146,7 @@ val report_error: (* given an utf8 string a floc returns the parsed substring and its length * in bytes *) -val utf8_parsed_text: string -> Token.flocation -> string * int +val utf8_parsed_text: string -> Stdpp.location -> string * int (* the length in characters, not bytes *) val utf8_string_length: string -> int -- 2.39.2