From: Claudio Sacerdoti Coen Date: Fri, 30 Dec 2022 01:19:16 +0000 (+0100) Subject: Porting to ocaml 5 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b76c5b3b82753966cabffd8536d8dd9f8cada20;p=helm.git Porting to ocaml 5 - old hashing dropped from ocaml code => hash.c is not part of ng_paramodulation - as a consequence, bytecode is now compile in -custom mode - requires patched versions of ocaml-expant, ocamlnet and ulex-camlp5 (all currently not accepted upstream yet) - plenty of new warnings either turned off or applied to code - ported to most recent version of camlp5 --- diff --git a/matita/components/METAS/meta.helm-ng_paramodulation.src b/matita/components/METAS/meta.helm-ng_paramodulation.src index e09fa226a..01d35b829 100644 --- a/matita/components/METAS/meta.helm-ng_paramodulation.src +++ b/matita/components/METAS/meta.helm-ng_paramodulation.src @@ -1,5 +1,5 @@ requires="helm-ng_refiner" version="0.0.1" -archive(byte)="ng_paramodulation.cma" -archive(native)="ng_paramodulation.cmxa" -linkopts="" +archive(byte)="ng_paramodulation.cma hash.o" +archive(native)="ng_paramodulation.cmxa hash.o" +linkopts(byte)="-custom" diff --git a/matita/components/METAS/meta.helm-thread.src b/matita/components/METAS/meta.helm-thread.src index 5253060d2..8ee48782a 100644 --- a/matita/components/METAS/meta.helm-thread.src +++ b/matita/components/METAS/meta.helm-thread.src @@ -1,4 +1,4 @@ -requires="" +requires="str unix" version="0.0.1" archive(byte,mt)="thread.cma" archive(native,mt)="thread.cmxa" diff --git a/matita/components/METAS/meta.helm-xml.src b/matita/components/METAS/meta.helm-xml.src index 626e644fc..5cde1bdb8 100644 --- a/matita/components/METAS/meta.helm-xml.src +++ b/matita/components/METAS/meta.helm-xml.src @@ -1,4 +1,4 @@ -requires="zip expat helm-extlib" +requires="zip expat helm-extlib camlp-streams" version="0.0.1" archive(byte)="xml.cma" archive(native)="xml.cmxa" diff --git a/matita/components/Makefile.common b/matita/components/Makefile.common index 74a54a821..0c61faaf7 100644 --- a/matita/components/Makefile.common +++ b/matita/components/Makefile.common @@ -20,7 +20,7 @@ endif PREPROCOPTIONS = -pp camlp5o SYNTAXOPTIONS = -syntax camlp5o PREREQ = -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3 # -57-3 for ocaml 4.0.5 +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70 # -57-3 for ocaml 4.0.5, -68-69-70 for ocaml 5.0 OCAMLDEBUGOPTIONS = -g #OCAML_PROF=p -p a OCAMLARCHIVEOPTIONS = diff --git a/matita/components/binaries/matitaprover/matitaprover.ml b/matita/components/binaries/matitaprover/matitaprover.ml index f72a7ebc5..5e773bd09 100644 --- a/matita/components/binaries/matitaprover/matitaprover.ml +++ b/matita/components/binaries/matitaprover/matitaprover.ml @@ -11,7 +11,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -module OT = struct type t = string let compare = Pervasives.compare end +module OT = struct type t = string let compare = Stdlib.compare end module HC = Map.Make(OT) module TS = HTopoSort.Make(OT) @@ -159,7 +159,7 @@ end let compute_stats goal hypotheses = let module C = - struct type t = leaf let cmp (a,_) (b,_) = Pervasives.compare a b end + struct type t = leaf let cmp (a,_) (b,_) = Stdlib.compare a b end in let module B = MakeBlob(C) in let module Pp = Pp.Pp(B) in @@ -189,8 +189,8 @@ end if a1 = 0 && a2 = 0 then 0 else if a1 = 0 then -1 else if a2 = 0 then 1 - else let res = Pervasives.compare (a1,o1,-go1,p1) (a2,o2,-go2,p2) - in if res = 0 then Pervasives.compare (HExtlib.list_index ((=) n1) oplist) (HExtlib.list_index ((=) n2) oplist) + else let res = Stdlib.compare (a1,o1,-go1,p1) (a2,o2,-go2,p2) + in if res = 0 then Stdlib.compare (HExtlib.list_index ((=) n1) oplist) (HExtlib.list_index ((=) n2) oplist) else res) data ;; @@ -211,12 +211,12 @@ let worker order ~useage ~printmsg goal hypotheses = then ((*prerr_endline "NO CLASH, using fixed ground order";*) fun a b -> - Pervasives.compare + Stdlib.compare (pos a stats) (pos b stats)) else ((*prerr_endline "CLASH, statistics insufficient";*) - fun (a,_) (b,_) -> Pervasives.compare a b) + fun (a,_) (b,_) -> Stdlib.compare a b) ;; end in diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 9c0b365c6..4ef84ec5d 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,9 +1,22 @@ -content.cmx : content.cmi +content.cmx : \ + content.cmi content.cmi : -notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi -notationEnv.cmi : notationPt.cmx -notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi -notationPp.cmi : notationPt.cmx notationEnv.cmi +notationEnv.cmx : \ + notationUtil.cmx \ + notationPt.cmx \ + notationEnv.cmi +notationEnv.cmi : \ + notationPt.cmx +notationPp.cmx : \ + notationPt.cmx \ + notationEnv.cmx \ + notationPp.cmi +notationPp.cmi : \ + notationPt.cmx \ + notationEnv.cmi notationPt.cmx : -notationUtil.cmx : notationPt.cmx notationUtil.cmi -notationUtil.cmi : notationPt.cmx +notationUtil.cmx : \ + notationPt.cmx \ + notationUtil.cmi +notationUtil.cmi : \ + notationPt.cmx diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 211b4fc51..1e74dfbf4 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -1,24 +1,55 @@ -box.cmx : renderingAttrs.cmx box.cmi +box.cmx : \ + renderingAttrs.cmx \ + box.cmi box.cmi : -boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ +boxPp.cmx : \ + renderingAttrs.cmx \ + mpresentation.cmx \ + cicNotationPres.cmx \ + box.cmx \ boxPp.cmi -boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi -cicNotationLexer.cmx : cicNotationLexer.cmi +boxPp.cmi : \ + mpresentation.cmi \ + cicNotationPres.cmi \ + box.cmi +cicNotationLexer.cmx : \ + cicNotationLexer.cmi cicNotationLexer.cmi : -cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi +cicNotationParser.cmx : \ + cicNotationLexer.cmx \ + cicNotationParser.cmi cicNotationParser.cmi : -cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ +cicNotationPres.cmx : \ + renderingAttrs.cmx \ + mpresentation.cmx \ + box.cmx \ cicNotationPres.cmi -cicNotationPres.cmi : mpresentation.cmi box.cmi -content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi -content2pres.cmi : termContentPres.cmi cicNotationPres.cmi -content2presMatcher.cmx : content2presMatcher.cmi +cicNotationPres.cmi : \ + mpresentation.cmi \ + box.cmi +content2pres.cmx : \ + termContentPres.cmx \ + renderingAttrs.cmx \ + mpresentation.cmx \ + cicNotationPres.cmx \ + box.cmx \ + content2pres.cmi +content2pres.cmi : \ + termContentPres.cmi \ + cicNotationPres.cmi +content2presMatcher.cmx : \ + content2presMatcher.cmi content2presMatcher.cmi : -mpresentation.cmx : mpresentation.cmi +mpresentation.cmx : \ + mpresentation.cmi mpresentation.cmi : -renderingAttrs.cmx : renderingAttrs.cmi +renderingAttrs.cmx : \ + renderingAttrs.cmi renderingAttrs.cmi : -termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi -termContentPres.cmi : cicNotationParser.cmi +termContentPres.cmx : \ + renderingAttrs.cmx \ + content2presMatcher.cmx \ + cicNotationParser.cmx \ + termContentPres.cmi +termContentPres.cmi : \ + cicNotationParser.cmi diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 3341b0feb..36a3fb017 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -36,6 +36,11 @@ exception Level_not_found of int let min_precedence = 0 let max_precedence = 100 +let hash_expr e = + e + |> Hashtbl.hash + |> Printf.sprintf "%08x" + type ('a,'b,'c,'d,'e) grammars = { level1_pattern: 'a Grammar.Entry.e; level2_ast: 'b Grammar.Entry.e; @@ -74,7 +79,7 @@ type db = { let int_of_string s = try - Pervasives.int_of_string s + Stdlib.int_of_string s with Failure _ -> failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) @@ -197,7 +202,8 @@ let extract_term_production status pattern = in [ Env (List.map Env.opt_declaration p_names), Gramext.srules - [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ], + [ [ Gramext.Sopt (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ], + hash_expr action, Gramext.action action ] ] | Ast.List0 (p, _) | Ast.List1 (p, _) -> @@ -215,7 +221,8 @@ let extract_term_production status pattern = in [ Env (List.map Env.list_declaration p_names), Gramext.srules - [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ], + [ [ gram_of_list (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ], + hash_expr action, Gramext.action action ] ] | _ -> assert false and aux_variable = @@ -246,7 +253,7 @@ let compare_rule_id x y = | _,[] -> 1 | ((s1::tl1) as x),((s2::tl2) as y) -> if Gramext.eq_symbol s1 s2 then aux (tl1,tl2) - else Pervasives.compare x y + else Stdlib.compare x y in aux (x,y) @@ -384,7 +391,7 @@ let initialize_grammars grammars = in (* Needed since campl4 on "delete_rule" remove the precedence level if it gets * empty after the deletion. The lexer never generate the Stoken below. *) - let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in + let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], "DUMMY", dummy_action ] in let mk_level_list first last = let rec aux acc = function | i when i < first -> acc @@ -862,6 +869,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action = [ None, Some (*Gramext.NonA*) Gramext.NonA, [ p_atoms, + hash_expr "(make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings)", (make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) diff --git a/matita/components/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt index 1f1711ae7..867ae4666 100644 --- a/matita/components/disambiguation/.depend.opt +++ b/matita/components/disambiguation/.depend.opt @@ -1,7 +1,15 @@ -disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi -disambiguate.cmi : disambiguateTypes.cmi -disambiguateTypes.cmx : disambiguateTypes.cmi +disambiguate.cmx : \ + disambiguateTypes.cmx \ + disambiguate.cmi +disambiguate.cmi : \ + disambiguateTypes.cmi +disambiguateTypes.cmx : \ + disambiguateTypes.cmi disambiguateTypes.cmi : -multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \ +multiPassDisambiguator.cmx : \ + disambiguateTypes.cmx \ + disambiguate.cmx \ multiPassDisambiguator.cmi -multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi +multiPassDisambiguator.cmi : \ + disambiguateTypes.cmi \ + disambiguate.cmi diff --git a/matita/components/disambiguation/disambiguateTypes.ml b/matita/components/disambiguation/disambiguateTypes.ml index 19c16d130..9c37fa36c 100644 --- a/matita/components/disambiguation/disambiguateTypes.ml +++ b/matita/components/disambiguation/disambiguateTypes.ml @@ -41,7 +41,7 @@ exception Invalid_choice of (Stdpp.location * string) Lazy.t module OrderedDomain = struct type t = domain_item - let compare = Pervasives.compare + let compare = Stdlib.compare end (* module Domain = Set.Make (OrderedDomain) *) diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index 12de49274..72b64d1cf 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -1,18 +1,30 @@ -componentsConf.cmx : componentsConf.cmi +componentsConf.cmx : \ + componentsConf.cmi componentsConf.cmi : -discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi +discrimination_tree.cmx : \ + trie.cmx \ + hExtlib.cmx \ + discrimination_tree.cmi discrimination_tree.cmi : -graphvizPp.cmx : graphvizPp.cmi +graphvizPp.cmx : \ + graphvizPp.cmi graphvizPp.cmi : -hExtlib.cmx : hExtlib.cmi +hExtlib.cmx : \ + hExtlib.cmi hExtlib.cmi : -hLog.cmx : hLog.cmi +hLog.cmx : \ + hLog.cmi hLog.cmi : -hMarshal.cmx : hExtlib.cmx hMarshal.cmi +hMarshal.cmx : \ + hExtlib.cmx \ + hMarshal.cmi hMarshal.cmi : -hTopoSort.cmx : hTopoSort.cmi +hTopoSort.cmx : \ + hTopoSort.cmi hTopoSort.cmi : -patternMatcher.cmx : patternMatcher.cmi +patternMatcher.cmx : \ + patternMatcher.cmi patternMatcher.cmi : -trie.cmx : trie.cmi +trie.cmx : \ + trie.cmi trie.cmi : diff --git a/matita/components/extlib/patternMatcher.ml b/matita/components/extlib/patternMatcher.ml index fa8c6061e..4e3e75fa5 100644 --- a/matita/components/extlib/patternMatcher.ml +++ b/matita/components/extlib/patternMatcher.ml @@ -33,7 +33,7 @@ type pattern_id = int module OrderedInt = struct type t = int - let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) + let compare (x1:t) (x2:t) = Stdlib.compare x2 x1 (* reverse order *) end module IntSet = Set.Make (OrderedInt) diff --git a/matita/components/getter/.depend.opt b/matita/components/getter/.depend.opt index 1d016d277..cb0f289ac 100644 --- a/matita/components/getter/.depend.opt +++ b/matita/components/getter/.depend.opt @@ -1,23 +1,50 @@ -http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ +http_getter.cmx : \ + http_getter_wget.cmx \ + http_getter_types.cmx \ + http_getter_storage.cmx \ + http_getter_misc.cmx \ + http_getter_logger.cmx \ + http_getter_env.cmx \ + http_getter_const.cmx \ + http_getter_common.cmx \ http_getter.cmi -http_getter.cmi : http_getter_types.cmx -http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi -http_getter_common.cmi : http_getter_types.cmx -http_getter_const.cmx : http_getter_const.cmi +http_getter.cmi : \ + http_getter_types.cmx +http_getter_common.cmx : \ + http_getter_types.cmx \ + http_getter_misc.cmx \ + http_getter_logger.cmx \ + http_getter_env.cmx \ + http_getter_common.cmi +http_getter_common.cmi : \ + http_getter_types.cmx +http_getter_const.cmx : \ + http_getter_const.cmi http_getter_const.cmi : -http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi -http_getter_env.cmi : http_getter_types.cmx -http_getter_logger.cmx : http_getter_logger.cmi +http_getter_env.cmx : \ + http_getter_types.cmx \ + http_getter_misc.cmx \ + http_getter_logger.cmx \ + http_getter_const.cmx \ + http_getter_env.cmi +http_getter_env.cmi : \ + http_getter_types.cmx +http_getter_logger.cmx : \ + http_getter_logger.cmi http_getter_logger.cmi : -http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi +http_getter_misc.cmx : \ + http_getter_logger.cmx \ + http_getter_misc.cmi http_getter_misc.cmi : -http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi +http_getter_storage.cmx : \ + http_getter_wget.cmx \ + http_getter_types.cmx \ + http_getter_misc.cmx \ + http_getter_env.cmx \ + http_getter_storage.cmi http_getter_storage.cmi : http_getter_types.cmx : -http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi +http_getter_wget.cmx : \ + http_getter_types.cmx \ + http_getter_wget.cmi http_getter_wget.cmi : diff --git a/matita/components/getter/http_getter_misc.ml b/matita/components/getter/http_getter_misc.ml index 38a943bc5..fa5d780b0 100644 --- a/matita/components/getter/http_getter_misc.ml +++ b/matita/components/getter/http_getter_misc.ml @@ -183,7 +183,7 @@ let gunzip ?(keep = false) ?output fname = (try while true do let bytes = Gzip.input ic buf 0 bufsiz in - if bytes = 0 then raise End_of_file else Pervasives.output oc buf 0 bytes + if bytes = 0 then raise End_of_file else Stdlib.output oc buf 0 bytes done with End_of_file -> ()); close_out oc; diff --git a/matita/components/getter/http_getter_storage.ml b/matita/components/getter/http_getter_storage.ml index 4ff552a4b..be5cad2a9 100644 --- a/matita/components/getter/http_getter_storage.ml +++ b/matita/components/getter/http_getter_storage.ml @@ -70,7 +70,7 @@ let normalize_root uri = (* add trailing slash to roots *) with Invalid_argument _ -> uri let remove_duplicates l = - Http_getter_misc.list_uniq (List.stable_sort Pervasives.compare l) + Http_getter_misc.list_uniq (List.stable_sort Stdlib.compare l) let has_rdonly l = List.exists ((=) `Read_only) l let has_legacy l = List.exists ((=) `Legacy) l diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index 5dabb8012..be6de9f62 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,3 +1,6 @@ grafiteAst.cmx : -grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi -grafiteAstPp.cmi : grafiteAst.cmx +grafiteAstPp.cmx : \ + grafiteAst.cmx \ + grafiteAstPp.cmi +grafiteAstPp.cmi : \ + grafiteAst.cmx diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index 696b45881..6e9ccb21a 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,7 +1,14 @@ -grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ +grafiteEngine.cmx : \ + nCicCoercDeclaration.cmx \ + grafiteTypes.cmx \ grafiteEngine.cmi -grafiteEngine.cmi : grafiteTypes.cmi -grafiteTypes.cmx : grafiteTypes.cmi +grafiteEngine.cmi : \ + grafiteTypes.cmi +grafiteTypes.cmx : \ + grafiteTypes.cmi grafiteTypes.cmi : -nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmi : grafiteTypes.cmi +nCicCoercDeclaration.cmx : \ + grafiteTypes.cmx \ + nCicCoercDeclaration.cmi +nCicCoercDeclaration.cmi : \ + grafiteTypes.cmi diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e0e6dac9c..4b014236d 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,4 +1,7 @@ -grafiteParser.cmx : grafiteParser.cmi +grafiteParser.cmx : \ + grafiteParser.cmi grafiteParser.cmi : -print_grammar.cmx : print_grammar.cmi -print_grammar.cmi : grafiteParser.cmi +print_grammar.cmx : \ + print_grammar.cmi +print_grammar.cmi : \ + grafiteParser.cmi diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml index 9fea12e40..995140282 100644 --- a/matita/components/grafite_parser/print_grammar.ml +++ b/matita/components/grafite_parser/print_grammar.ml @@ -84,7 +84,6 @@ and is_entry_dummy = function and is_symbol_dummy = function | Stoken ("DUMMY", _) -> true | Stoken _ -> false - | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt | Snterm e | Snterml (e, _) -> is_entry_dummy e | Slist1 x | Slist0 x -> is_symbol_dummy x | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y @@ -170,15 +169,6 @@ let visit_description desc fmt self = and visit_symbol s todo is_son = match s with - | Smeta (name, sl, _) -> - Format.fprintf fmt "%s " name; - List.fold_left ( - fun acc s -> - let todo = visit_symbol s acc is_son in - if is_son then - Format.fprintf fmt "@ "; - todo) - todo sl | Snterm entry -> visit_entry entry todo is_son | Snterml (entry,level) -> visit_entry entry ~level todo is_son | Slist0 symbol -> @@ -256,7 +246,7 @@ let rec visit_entries fmt todo pped = ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2)) (List.sort (fun e1 e2 -> - Pervasives.compare (name_of_entry e1) (name_of_entry e2)) + Stdlib.compare (name_of_entry e1) (name_of_entry e2)) todo), pped in diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt index 27ecf9383..d960dc9be 100644 --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@ -1,6 +1,9 @@ -librarian.cmx : librarian.cmi +librarian.cmx : \ + librarian.cmi librarian.cmi : -libraryClean.cmx : libraryClean.cmi +libraryClean.cmx : \ + libraryClean.cmi libraryClean.cmi : -libraryMisc.cmx : libraryMisc.cmi +libraryMisc.cmx : \ + libraryMisc.cmi libraryMisc.cmi : diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml index 1b3df75f8..ebd02bd1b 100644 --- a/matita/components/library/libraryClean.ml +++ b/matita/components/library/libraryClean.ml @@ -85,7 +85,7 @@ let one_step_depend cache_of_processed_baseuri suri dbtype dbd = Filename.dirname (strip_xpointer occ) = buri -> l := uri :: !l | _ -> ()); - let l = List.sort Pervasives.compare !l in + let l = List.sort Stdlib.compare !l in HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) @@ -120,7 +120,7 @@ let db_uris_of_baseuri buri = | Some uri when Filename.dirname (strip_xpointer uri) = buri -> l := uri :: !l | _ -> ()); - let l = List.sort Pervasives.compare !l in + let l = List.sort Stdlib.compare !l in HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) @@ -135,7 +135,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove = (* to remove an uri you have to remove the whole script *) let buri_to_remove = HExtlib.list_uniq - (List.fast_sort Pervasives.compare + (List.fast_sort Stdlib.compare (List.map safe_buri_of_suri uri_to_remove)) in (* cleand the already visided baseuris *) @@ -177,7 +177,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove = in let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in let uri_to_remove = - HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in + HExtlib.list_uniq (List.sort Stdlib.compare uri_to_remove) in (* now we want the list of all uri that depend on them *) let depend = List.fold_left @@ -185,7 +185,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove = [] uri_to_remove in let depend = - HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) + HExtlib.list_uniq (List.fast_sort Stdlib.compare depend) in uri_to_remove, depend ;; @@ -229,7 +229,7 @@ let clean_baseuris ?verbose:(_=true) _buris = if debug then List.iter debug_prerr buris; let l = close_db cache_of_processed_baseuri [] buris in - let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in + let l = HExtlib.list_uniq (List.fast_sort Stdlib.compare l) in let l = List.map NUri.uri_of_string l in debug_prerr "clean_baseuri will remove:"; if debug then @@ -245,6 +245,6 @@ let clean_baseuris ?verbose:(_=true) _buris = HExtlib.safe_remove lexiconfile; HExtlib.rmdir_descend (Filename.chop_extension lexiconfile) with Http_getter_types.Key_not_found _ -> ()) - (HExtlib.list_uniq (List.fast_sort Pervasives.compare + (HExtlib.list_uniq (List.fast_sort Stdlib.compare (List.map NUri.baseuri_of_uri l @ buris))) *) diff --git a/matita/components/logger/.depend.opt b/matita/components/logger/.depend.opt index ed934897f..f68fdd43e 100644 --- a/matita/components/logger/.depend.opt +++ b/matita/components/logger/.depend.opt @@ -1,2 +1,3 @@ -helmLogger.cmx : helmLogger.cmi +helmLogger.cmx : \ + helmLogger.cmi helmLogger.cmi : diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index df8d6d635..b526a0df5 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,4 +1,7 @@ -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi +interpretations.cmx : \ + ncic2astMatcher.cmx \ + interpretations.cmi interpretations.cmi : -ncic2astMatcher.cmx : ncic2astMatcher.cmi +ncic2astMatcher.cmx : \ + ncic2astMatcher.cmi ncic2astMatcher.cmi : diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index 794859369..44d7751d5 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -38,10 +38,12 @@ let hide_coercions = ref true;; type cic_id = string +(* type term_info = { sort: (cic_id, Ast.sort_kind) Hashtbl.t; uri: (cic_id, NReference.reference) Hashtbl.t; } +*) module IntMap = Map.Make(struct type t = int let compare = compare end);; module StringMap = Map.Make(String);; @@ -185,7 +187,7 @@ let lookup_interpretations status ?(sorted=true) symbol = dsc, args, appl_pattern ) (StringMap.find symbol status#interp_db.interpretations) in - if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw) + if sorted then HExtlib.list_uniq (List.sort Stdlib.compare raw) else raw with Not_found -> raise Interpretation_not_found diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index d5eef6bc0..6904cfd3b 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,9 +1,15 @@ -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi +disambiguateChoices.cmx : \ + nnumber_notation.cmx \ + disambiguateChoices.cmi disambiguateChoices.cmi : -grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ +grafiteDisambiguate.cmx : \ + nCicDisambiguate.cmx \ + disambiguateChoices.cmx \ grafiteDisambiguate.cmi grafiteDisambiguate.cmi : -nCicDisambiguate.cmx : nCicDisambiguate.cmi +nCicDisambiguate.cmx : \ + nCicDisambiguate.cmi nCicDisambiguate.cmi : -nnumber_notation.cmx : nnumber_notation.cmi +nnumber_notation.cmx : \ + nnumber_notation.cmi nnumber_notation.cmi : diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 59fe713e5..8ed903be1 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -103,7 +103,7 @@ let find_in_context name context = aux 1 context let interpretate_term_and_interpretate_term_option (status: #NCic.status) - ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path + ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) diff --git a/matita/components/ng_extraction/.depend.opt b/matita/components/ng_extraction/.depend.opt index 3b0b9b57c..a527ad0c4 100644 --- a/matita/components/ng_extraction/.depend.opt +++ b/matita/components/ng_extraction/.depend.opt @@ -1,20 +1,61 @@ -common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi -common.cmi : ocamlExtractionTable.cmi coq.cmi -coq.cmx : coq.cmi +common.cmx : \ + ocamlExtractionTable.cmx \ + mlutil.cmx \ + coq.cmx \ + common.cmi +common.cmi : \ + ocamlExtractionTable.cmi \ + coq.cmi +coq.cmx : \ + coq.cmi coq.cmi : -extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi -extraction.cmi : ocamlExtractionTable.cmi miniml.cmx -miniml.cmx : coq.cmx -mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi -mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi -nCicExtraction.cmx : nCicExtraction.cmi +extraction.cmx : \ + ocamlExtractionTable.cmx \ + mlutil.cmx \ + miniml.cmx \ + coq.cmx \ + common.cmx \ + extraction.cmi +extraction.cmi : \ + ocamlExtractionTable.cmi \ + miniml.cmx +miniml.cmx : \ + coq.cmx +mlutil.cmx : \ + ocamlExtractionTable.cmx \ + miniml.cmx \ + coq.cmx \ + mlutil.cmi +mlutil.cmi : \ + ocamlExtractionTable.cmi \ + miniml.cmx \ + coq.cmi +nCicExtraction.cmx : \ + nCicExtraction.cmi nCicExtraction.cmi : -ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx ocaml.cmi -ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi -ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ - coq.cmx ocamlExtraction.cmi -ocamlExtraction.cmi : ocamlExtractionTable.cmi -ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi -ocamlExtractionTable.cmi : miniml.cmx coq.cmi +ocaml.cmx : \ + ocamlExtractionTable.cmx \ + mlutil.cmx \ + miniml.cmx \ + coq.cmx \ + common.cmx \ + ocaml.cmi +ocaml.cmi : \ + ocamlExtractionTable.cmi \ + miniml.cmx \ + coq.cmi +ocamlExtraction.cmx : \ + ocamlExtractionTable.cmx \ + ocaml.cmx \ + extraction.cmx \ + coq.cmx \ + ocamlExtraction.cmi +ocamlExtraction.cmi : \ + ocamlExtractionTable.cmi +ocamlExtractionTable.cmx : \ + miniml.cmx \ + coq.cmx \ + ocamlExtractionTable.cmi +ocamlExtractionTable.cmi : \ + miniml.cmx \ + coq.cmi diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index 97f4e283a..fe01e3cc1 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -1,24 +1,74 @@ -nCic.cmx : nUri.cmx nReference.cmx -nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi -nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx -nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi -nCicPp.cmi : nReference.cmi nCic.cmx -nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi -nCicReduction.cmi : nCic.cmx -nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi -nCicSubstitution.cmi : nCic.cmx -nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ +nCic.cmx : \ + nUri.cmx \ + nReference.cmx +nCicEnvironment.cmx : \ + nUri.cmx \ + nReference.cmx \ + nCic.cmx \ + nCicEnvironment.cmi +nCicEnvironment.cmi : \ + nUri.cmi \ + nReference.cmi \ + nCic.cmx +nCicPp.cmx : \ + nUri.cmx \ + nReference.cmx \ + nCicSubstitution.cmx \ + nCicReduction.cmx \ + nCicEnvironment.cmx \ + nCic.cmx \ + nCicPp.cmi +nCicPp.cmi : \ + nReference.cmi \ + nCic.cmx +nCicReduction.cmx : \ + nReference.cmx \ + nCicUtils.cmx \ + nCicSubstitution.cmx \ + nCicEnvironment.cmx \ + nCic.cmx \ + nCicReduction.cmi +nCicReduction.cmi : \ + nCic.cmx +nCicSubstitution.cmx : \ + nCicUtils.cmx \ + nCic.cmx \ + nCicSubstitution.cmi +nCicSubstitution.cmi : \ + nCic.cmx +nCicTypeChecker.cmx : \ + nUri.cmx \ + nReference.cmx \ + nCicUtils.cmx \ + nCicSubstitution.cmx \ + nCicReduction.cmx \ + nCicEnvironment.cmx \ + nCic.cmx \ nCicTypeChecker.cmi -nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx -nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicUntrusted.cmi : nCic.cmx -nCicUtils.cmx : nCic.cmx nCicUtils.cmi -nCicUtils.cmi : nCic.cmx -nReference.cmx : nUri.cmx nReference.cmi -nReference.cmi : nUri.cmi -nUri.cmx : nUri.cmi +nCicTypeChecker.cmi : \ + nUri.cmi \ + nReference.cmi \ + nCic.cmx +nCicUntrusted.cmx : \ + nReference.cmx \ + nCicUtils.cmx \ + nCicSubstitution.cmx \ + nCicReduction.cmx \ + nCicEnvironment.cmx \ + nCic.cmx \ + nCicUntrusted.cmi +nCicUntrusted.cmi : \ + nCic.cmx +nCicUtils.cmx : \ + nCic.cmx \ + nCicUtils.cmi +nCicUtils.cmi : \ + nCic.cmx +nReference.cmx : \ + nUri.cmx \ + nReference.cmi +nReference.cmi : \ + nUri.cmi +nUri.cmx : \ + nUri.cmi nUri.cmi : diff --git a/matita/components/ng_kernel/nCicReduction.ml b/matita/components/ng_kernel/nCicReduction.ml index 7542a52e0..9234f07aa 100644 --- a/matita/components/ng_kernel/nCicReduction.ml +++ b/matita/components/ng_kernel/nCicReduction.ml @@ -206,7 +206,7 @@ module R = Reduction(RS);; let whd = R.whd -let (===) x y = Pervasives.compare x y = 0 ;; +let (===) x y = Stdlib.compare x y = 0 ;; let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);; diff --git a/matita/components/ng_kernel/nCicUntrusted.ml b/matita/components/ng_kernel/nCicUntrusted.ml index 5df06d28d..e60bf7e50 100644 --- a/matita/components/ng_kernel/nCicUntrusted.ml +++ b/matita/components/ng_kernel/nCicUntrusted.ml @@ -69,7 +69,7 @@ let metas_of_term status subst context term = List.fold_left (aux ctx) (i::acc) l) | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t in - HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term)) + HExtlib.list_uniq (List.sort Stdlib.compare (aux context [] term)) ;; module NCicHash = @@ -282,7 +282,7 @@ let max_kind k1 k2 = module OT = struct type t = int * NCic.conjecture - let compare (i,_) (j,_) = Pervasives.compare i j + let compare (i,_) (j,_) = Stdlib.compare i j end module MS = HTopoSort.Make(OT) diff --git a/matita/components/ng_kernel/nReference.ml b/matita/components/ng_kernel/nReference.ml index 102f25046..5fd28044d 100644 --- a/matita/components/ng_kernel/nReference.ml +++ b/matita/components/ng_kernel/nReference.ml @@ -37,7 +37,7 @@ let hash (Ref (uri,spec)) = module OrderedStrings = struct type t = string - let compare (s1 : t) (s2 : t) = Pervasives.compare s1 s2 + let compare (s1 : t) (s2 : t) = Stdlib.compare s1 s2 end ;; diff --git a/matita/components/ng_library/.depend.opt b/matita/components/ng_library/.depend.opt index 07d53f5dd..ee5e8bd16 100644 --- a/matita/components/ng_library/.depend.opt +++ b/matita/components/ng_library/.depend.opt @@ -1,2 +1,3 @@ -nCicLibrary.cmx : nCicLibrary.cmi +nCicLibrary.cmx : \ + nCicLibrary.cmi nCicLibrary.cmi : diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 9593d8958..32cbf605d 100644 --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@ -1,29 +1,98 @@ -foSubst.cmx : terms.cmx foSubst.cmi -foSubst.cmi : terms.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -foUnif.cmi : terms.cmi orderings.cmi -foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUtils.cmi : terms.cmi orderings.cmi -index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi -index.cmi : terms.cmi orderings.cmi -nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi -nCicBlob.cmi : terms.cmi -nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi -nCicParamod.cmi : terms.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi -nCicProof.cmi : terms.cmi -orderings.cmx : terms.cmx foSubst.cmx orderings.cmi -orderings.cmi : terms.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx paramod.cmi -paramod.cmi : terms.cmi orderings.cmi -pp.cmx : terms.cmx pp.cmi -pp.cmi : terms.cmi -stats.cmx : terms.cmx stats.cmi -stats.cmi : terms.cmi orderings.cmi -superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -terms.cmx : terms.cmi +foSubst.cmx : \ + terms.cmx \ + foSubst.cmi +foSubst.cmi : \ + terms.cmi +foUnif.cmx : \ + terms.cmx \ + orderings.cmx \ + foUtils.cmx \ + foSubst.cmx \ + foUnif.cmi +foUnif.cmi : \ + terms.cmi \ + orderings.cmi +foUtils.cmx : \ + terms.cmx \ + orderings.cmx \ + foSubst.cmx \ + foUtils.cmi +foUtils.cmi : \ + terms.cmi \ + orderings.cmi +index.cmx : \ + terms.cmx \ + orderings.cmx \ + foUtils.cmx \ + index.cmi +index.cmi : \ + terms.cmi \ + orderings.cmi +nCicBlob.cmx : \ + terms.cmx \ + foUtils.cmx \ + nCicBlob.cmi +nCicBlob.cmi : \ + terms.cmi +nCicParamod.cmx : \ + terms.cmx \ + pp.cmx \ + paramod.cmx \ + orderings.cmx \ + nCicProof.cmx \ + nCicBlob.cmx \ + nCicParamod.cmi +nCicParamod.cmi : \ + terms.cmi +nCicProof.cmx : \ + terms.cmx \ + pp.cmx \ + nCicBlob.cmx \ + foSubst.cmx \ + nCicProof.cmi +nCicProof.cmi : \ + terms.cmi +orderings.cmx : \ + terms.cmx \ + foSubst.cmx \ + orderings.cmi +orderings.cmi : \ + terms.cmi +paramod.cmx : \ + terms.cmx \ + superposition.cmx \ + pp.cmx \ + orderings.cmx \ + index.cmx \ + foUtils.cmx \ + paramod.cmi +paramod.cmi : \ + terms.cmi \ + orderings.cmi +pp.cmx : \ + terms.cmx \ + pp.cmi +pp.cmi : \ + terms.cmi +stats.cmx : \ + terms.cmx \ + stats.cmi +stats.cmi : \ + terms.cmi \ + orderings.cmi +superposition.cmx : \ + terms.cmx \ + pp.cmx \ + orderings.cmx \ + index.cmx \ + foUtils.cmx \ + foUnif.cmx \ + foSubst.cmx \ + superposition.cmi +superposition.cmi : \ + terms.cmi \ + orderings.cmi \ + index.cmi +terms.cmx : \ + terms.cmi terms.cmi : diff --git a/matita/components/ng_paramodulation/Makefile b/matita/components/ng_paramodulation/Makefile index f4c102239..ca2e5d1af 100644 --- a/matita/components/ng_paramodulation/Makefile +++ b/matita/components/ng_paramodulation/Makefile @@ -8,7 +8,11 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -all: +all: hash.o +opt: hash.o + +hash.o: + gcc -I `ocamlc -where`/caml/ -c hash.c include ../../Makefile.defs include ../Makefile.common diff --git a/matita/components/ng_paramodulation/foUtils.ml b/matita/components/ng_paramodulation/foUtils.ml index 826687afc..9bb7891c3 100644 --- a/matita/components/ng_paramodulation/foUtils.ml +++ b/matita/components/ng_paramodulation/foUtils.ml @@ -58,7 +58,7 @@ module Utils (B : Orderings.Blob) = struct match l1, l2 with | Terms.Predicate p1, Terms.Predicate p2 -> compare_foterm p1 p2 | Terms.Equation (l1,r1,ty1,o1), Terms.Equation (l2,r2,ty2,o2) -> - let c = Pervasives.compare o1 o2 in + let c = Stdlib.compare o1 o2 in if c <> 0 then c else let c = compare_foterm l1 l2 in if c <> 0 then c else @@ -70,7 +70,7 @@ module Utils (B : Orderings.Blob) = struct ;; let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2 - let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2 + let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Stdlib.compare id1 id2 let relocate maxvar varlist subst = List.fold_right diff --git a/matita/components/ng_paramodulation/hash.c b/matita/components/ng_paramodulation/hash.c new file mode 100644 index 000000000..262c36e0f --- /dev/null +++ b/matita/components/ng_paramodulation/hash.c @@ -0,0 +1,152 @@ +/***********************************************************************/ +/* */ +/* OCaml */ +/* */ +/* Xavier Leroy, projet Cristal, INRIA Rocquencourt */ +/* */ +/* Copyright 1996 Institut National de Recherche en Informatique et */ +/* en Automatique. All rights reserved. This file is distributed */ +/* under the terms of the GNU Library General Public License, with */ +/* the special exception on linking described in file ../LICENSE. */ +/* */ +/***********************************************************************/ + +/* $Id: hash.c 12149 2012-02-10 16:15:24Z doligez $ */ + +/* The generic hashing primitive */ + +/* The interface of this file is in "mlvalues.h" (for [caml_hash_variant]) + and in "hash.h" (for the other exported functions). */ + +#include "mlvalues.h" +#include "custom.h" +#include "memory.h" +#include "hash.h" +#include "address_class.h" + +/*#ifdef ARCH_INT64_TYPE +#include "int64_native.h" +#else +#include "int64_emul.h" +#endif*/ + +/* The old implementation */ + +static uintnat hash_accu; +static intnat hash_univ_limit, hash_univ_count; + +static void hash_aux(value obj); + +CAMLprim value caml_hash_univ_param(value count, value limit, value obj) +{ + hash_univ_limit = Long_val(limit); + hash_univ_count = Long_val(count); + hash_accu = 0; + hash_aux(obj); + return Val_long(hash_accu & 0x3FFFFFFF); + /* The & has two purposes: ensure that the return value is positive + and give the same result on 32 bit and 64 bit architectures. */ +} + +#define Alpha 65599 +#define Beta 19 +#define Combine(new) (hash_accu = hash_accu * Alpha + (new)) +#define Combine_small(new) (hash_accu = hash_accu * Beta + (new)) + +static void hash_aux(value obj) +{ + unsigned char * p; + mlsize_t i, j; + tag_t tag; + + hash_univ_limit--; + if (hash_univ_count < 0 || hash_univ_limit < 0) return; + + again: + if (Is_long(obj)) { + hash_univ_count--; + Combine(Long_val(obj)); + return; + } + + /* Pointers into the heap are well-structured blocks. So are atoms. + We can inspect the block contents. */ + + CAMLassert (Is_block (obj)); + if (Is_in_value_area(obj)) { + tag = Tag_val(obj); + switch (tag) { + case String_tag: + hash_univ_count--; + i = caml_string_length(obj); + for (p = &Byte_u(obj, 0); i > 0; i--, p++) + Combine_small(*p); + break; + case Double_tag: + /* For doubles, we inspect their binary representation, LSB first. + The results are consistent among all platforms with IEEE floats. */ + hash_univ_count--; +#ifdef ARCH_BIG_ENDIAN + for (p = &Byte_u(obj, sizeof(double) - 1), i = sizeof(double); + i > 0; + p--, i--) +#else + for (p = &Byte_u(obj, 0), i = sizeof(double); + i > 0; + p++, i--) +#endif + Combine_small(*p); + break; + case Double_array_tag: + hash_univ_count--; + for (j = 0; j < Bosize_val(obj); j += sizeof(double)) { +#ifdef ARCH_BIG_ENDIAN + for (p = &Byte_u(obj, j + sizeof(double) - 1), i = sizeof(double); + i > 0; + p--, i--) +#else + for (p = &Byte_u(obj, j), i = sizeof(double); + i > 0; + p++, i--) +#endif + Combine_small(*p); + } + break; + case Abstract_tag: + /* We don't know anything about the contents of the block. + Better do nothing. */ + break; + case Infix_tag: + hash_aux(obj - Infix_offset_val(obj)); + break; + case Forward_tag: + obj = Forward_val (obj); + goto again; + case Object_tag: + hash_univ_count--; + Combine(Oid_val(obj)); + break; + case Custom_tag: + /* If no hashing function provided, do nothing */ + if (Custom_ops_val(obj)->hash != NULL) { + hash_univ_count--; + Combine(Custom_ops_val(obj)->hash(obj)); + } + break; + default: + hash_univ_count--; + Combine_small(tag); + i = Wosize_val(obj); + while (i != 0) { + i--; + hash_aux(Field(obj, i)); + } + break; + } + return; + } + + /* Otherwise, obj is a pointer outside the heap, to an object with + a priori unknown structure. Use its physical address as hash key. */ + Combine((intnat) obj); +} diff --git a/matita/components/ng_paramodulation/index.ml b/matita/components/ng_paramodulation/index.ml index c1e12a34d..fa5d86ee3 100644 --- a/matita/components/ng_paramodulation/index.ml +++ b/matita/components/ng_paramodulation/index.ml @@ -21,7 +21,7 @@ module Index(B : Orderings.Blob) = struct type t = Terms.direction * B.t Terms.unit_clause let compare (d1,uc1) (d2,uc2) = - let c = Pervasives.compare d1 d2 in + let c = Stdlib.compare d1 d2 in if c <> 0 then c else U.compare_unit_clause uc1 uc2 ;; end @@ -61,7 +61,7 @@ module Index(B : Orderings.Blob) = struct match e1,e2 with | Constant (a1,ar1), Constant (a2,ar2) -> let c = B.compare a1 a2 in - if c <> 0 then c else Pervasives.compare ar1 ar2 + if c <> 0 then c else Stdlib.compare ar1 ar2 | Variable, Variable -> 0 | Constant _, Variable -> ~-1 | Variable, Constant _ -> 1 diff --git a/matita/components/ng_paramodulation/nCicBlob.ml b/matita/components/ng_paramodulation/nCicBlob.ml index b1f2cfa6f..9ca541a65 100644 --- a/matita/components/ng_paramodulation/nCicBlob.ml +++ b/matita/components/ng_paramodulation/nCicBlob.ml @@ -80,7 +80,7 @@ with type t = NCic.term and type input = NCic.term = struct | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1 | NCic.Appl _, NCic.Meta _ -> ~-1 | NCic.Meta _, NCic.Appl _ -> 1 - | _ -> Pervasives.compare x y + | _ -> Stdlib.compare x y (* was assert false, but why? *) ;; diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml index d5f35a3a3..8da829e75 100644 --- a/matita/components/ng_paramodulation/orderings.ml +++ b/matita/components/ng_paramodulation/orderings.ml @@ -130,7 +130,7 @@ let compare_weights (h1, w1) (h2, w2) = | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) -> if var1 = var2 then let diffs = (w1 - w2) + diffs in - let r = Pervasives.compare w1 w2 in + let r = Stdlib.compare w1 w2 in let lt = lt || (r < 0) in let gt = gt || (r > 0) in if lt && gt then XINCOMPARABLE else diff --git a/matita/components/ng_paramodulation/stats.ml b/matita/components/ng_paramodulation/stats.ml index da00eb551..a1e892902 100644 --- a/matita/components/ng_paramodulation/stats.ml +++ b/matita/components/ng_paramodulation/stats.ml @@ -129,7 +129,7 @@ module Stats (B : Terms.Blob) = | _ -> dependencies op tl acc ;; - let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));; + let dependencies op clauses = HExtlib.list_uniq (List.sort Stdlib.compare (dependencies op clauses []));; (* let max_weight_hyp = *) diff --git a/matita/components/ng_paramodulation/terms.ml b/matita/components/ng_paramodulation/terms.ml index 87b4f383b..0aa2a7d2b 100644 --- a/matita/components/ng_paramodulation/terms.ml +++ b/matita/components/ng_paramodulation/terms.ml @@ -63,7 +63,7 @@ let vars_of_term t = module OT = struct type t = int - let compare = Pervasives.compare + let compare = Stdlib.compare end module M : Map.S with type key = int diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index dab873890..a25cbdb11 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -1,17 +1,36 @@ -nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi -nCicCoercion.cmi : nCicUnifHint.cmi -nCicMetaSubst.cmx : nCicMetaSubst.cmi +nCicCoercion.cmx : \ + nDiscriminationTree.cmx \ + nCicUnifHint.cmx \ + nCicMetaSubst.cmx \ + nCicCoercion.cmi +nCicCoercion.cmi : \ + nCicUnifHint.cmi +nCicMetaSubst.cmx : \ + nCicMetaSubst.cmi nCicMetaSubst.cmi : -nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi +nCicRefineUtil.cmx : \ + nCicMetaSubst.cmx \ + nCicRefineUtil.cmi nCicRefineUtil.cmi : -nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi -nCicRefiner.cmi : nCicCoercion.cmi -nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ +nCicRefiner.cmx : \ + nCicUnification.cmx \ + nCicRefineUtil.cmx \ + nCicMetaSubst.cmx \ + nCicCoercion.cmx \ + nCicRefiner.cmi +nCicRefiner.cmi : \ + nCicCoercion.cmi +nCicUnifHint.cmx : \ + nDiscriminationTree.cmx \ + nCicMetaSubst.cmx \ nCicUnifHint.cmi nCicUnifHint.cmi : -nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicUnification.cmi : nCicCoercion.cmi -nDiscriminationTree.cmx : nDiscriminationTree.cmi +nCicUnification.cmx : \ + nCicUnifHint.cmx \ + nCicMetaSubst.cmx \ + nCicUnification.cmi +nCicUnification.cmi : \ + nCicCoercion.cmi +nDiscriminationTree.cmx : \ + nDiscriminationTree.cmi nDiscriminationTree.cmi : diff --git a/matita/components/ng_refiner/nCicCoercion.ml b/matita/components/ng_refiner/nCicCoercion.ml index cfb9d1b6b..7447a68f2 100644 --- a/matita/components/ng_refiner/nCicCoercion.ml +++ b/matita/components/ng_refiner/nCicCoercion.ml @@ -21,7 +21,7 @@ module COT : Set.OrderedType with type t = string * NCic.term * int * int * NCic.term * NCic.term = struct type t = string * NCic.term * int * int * NCic.term * NCic.term - let compare = Pervasives.compare + let compare = Stdlib.compare end module CoercionSet = Set.Make(COT) diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml index 5c7f92f99..d37ec4032 100644 --- a/matita/components/ng_refiner/nCicUnifHint.ml +++ b/matita/components/ng_refiner/nCicUnifHint.ml @@ -21,14 +21,14 @@ with type t = int * NCic.term * NCic.term * NCic.term = struct (* precedence, skel1, skel2, term *) type t = int * NCic.term * NCic.term * NCic.term - let compare = Pervasives.compare + let compare = Stdlib.compare end module EOT : Set.OrderedType with type t = int * NCic.term = struct type t = int * NCic.term - let compare = Pervasives.compare + let compare = Stdlib.compare end module HintSet = Set.Make(HOT) @@ -310,7 +310,7 @@ let look_for_hint (status:#status) metasenv subst context t1 t2 = rc in let rc = - List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc + List.sort (fun (x,_,_,_) (y,_,_,_) -> Stdlib.compare x y) rc in let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 7d8a45d0e..553e1e671 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -19,7 +19,7 @@ exception KeepReducingThis of string Lazy.t * (NCicReduction.machine * bool) * (NCicReduction.machine * bool) ;; -let (===) x y = Pervasives.compare x y = 0 ;; +let (===) x y = Stdlib.compare x y = 0 ;; let mk_msg (status:#NCic.status) metasenv subst context t1 t2 = (lazy ( diff --git a/matita/components/ng_refiner/nDiscriminationTree.ml b/matita/components/ng_refiner/nDiscriminationTree.ml index 4d746ad8b..b5338715d 100644 --- a/matita/components/ng_refiner/nDiscriminationTree.ml +++ b/matita/components/ng_refiner/nDiscriminationTree.ml @@ -29,7 +29,7 @@ open Discrimination_tree module TermOT : Set.OrderedType with type t = NCic.term = struct type t = NCic.term - let compare = Pervasives.compare + let compare = Stdlib.compare end module TermSet = Set.Make(TermOT) @@ -37,7 +37,7 @@ module TermSet = Set.Make(TermOT) module TermListOT : Set.OrderedType with type t = NCic.term list = struct type t = NCic.term list - let compare = Pervasives.compare + let compare = Stdlib.compare end module TermListSet : Set.S with type elt = NCic.term list = @@ -91,8 +91,8 @@ let compare e1 e2 = match e1,e2 with | Constant (u1,a1),Constant (u2,a2) -> let x = NReference.compare u1 u2 in - if x = 0 then Pervasives.compare a1 a2 else x - | e1,e2 -> Pervasives.compare e1 e2 + if x = 0 then Stdlib.compare a1 a2 else x + | e1,e2 -> Stdlib.compare e1 e2 ;; let string_of_path l = String.concat "." (List.map ppelem l) ;; diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index 75b2d57f8..ca420895d 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -1,22 +1,55 @@ -continuationals.cmx : continuationals.cmi +continuationals.cmx : \ + continuationals.cmi continuationals.cmi : -declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \ - continuationals.cmx declarative.cmi -declarative.cmi : nnAuto.cmi nTacStatus.cmi -nCicElim.cmx : nCicElim.cmi +declarative.cmx : \ + nnAuto.cmx \ + nTactics.cmx \ + nTacStatus.cmx \ + nCicElim.cmx \ + continuationals.cmx \ + declarative.cmi +declarative.cmi : \ + nnAuto.cmi \ + nTacStatus.cmi +nCicElim.cmx : \ + nCicElim.cmi nCicElim.cmi : -nCicTacReduction.cmx : nCicTacReduction.cmi +nCicTacReduction.cmx : \ + nCicTacReduction.cmi nCicTacReduction.cmi : -nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ +nDestructTac.cmx : \ + nTactics.cmx \ + nTacStatus.cmx \ + continuationals.cmx \ nDestructTac.cmi -nDestructTac.cmi : nTacStatus.cmi -nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ - continuationals.cmx nInversion.cmi -nInversion.cmi : nTacStatus.cmi -nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi -nTacStatus.cmi : continuationals.cmi -nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi -nTactics.cmi : nTacStatus.cmi -nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ - continuationals.cmx nnAuto.cmi -nnAuto.cmi : nTacStatus.cmi +nDestructTac.cmi : \ + nTacStatus.cmi +nInversion.cmx : \ + nTactics.cmx \ + nTacStatus.cmx \ + nCicElim.cmx \ + continuationals.cmx \ + nInversion.cmi +nInversion.cmi : \ + nTacStatus.cmi +nTacStatus.cmx : \ + nCicTacReduction.cmx \ + continuationals.cmx \ + nTacStatus.cmi +nTacStatus.cmi : \ + continuationals.cmi +nTactics.cmx : \ + nTacStatus.cmx \ + nCicElim.cmx \ + continuationals.cmx \ + nTactics.cmi +nTactics.cmi : \ + nTacStatus.cmi +nnAuto.cmx : \ + nTactics.cmx \ + nTacStatus.cmx \ + nCicTacReduction.cmx \ + continuationals.cmx \ + nnAuto.cmi +nnAuto.cmi : \ + nTacStatus.cmi diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 118261af0..819160eab 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -568,8 +568,8 @@ let compare e1 e2 = match e1,e2 with | Constant (u1,a1),Constant (u2,a2) -> let x = NUri.compare u1 u2 in - if x = 0 then Pervasives.compare a1 a2 else x - | e1,e2 -> Pervasives.compare e1 e2 + if x = 0 then Stdlib.compare a1 a2 else x + | e1,e2 -> Stdlib.compare e1 e2 ;; @@ -578,7 +578,7 @@ end module Ncic_termOT : Set.OrderedType with type t = cic_term = struct type t = cic_term - let compare = Pervasives.compare + let compare = Stdlib.compare end module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT) diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index d371409d2..2dc0be3f4 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -70,7 +70,7 @@ let print_stat _status tbl = let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in let relevance v = float !(v.uses) /. float !(v.nominations) in let vcompare (_,v1) (_,v2) = - Pervasives.compare (relevance v1) (relevance v2) in + Stdlib.compare (relevance v1) (relevance v2) in let l = List.sort vcompare l in let short_name r = Filename.chop_extension @@ -1490,7 +1490,7 @@ let pp_goals status l = module M = struct type t = int - let compare = Pervasives.compare + let compare = Stdlib.compare end ;; diff --git a/matita/components/registry/.depend.opt b/matita/components/registry/.depend.opt index f28210446..c8aaec531 100644 --- a/matita/components/registry/.depend.opt +++ b/matita/components/registry/.depend.opt @@ -1,2 +1,3 @@ -helm_registry.cmx : helm_registry.cmi +helm_registry.cmx : \ + helm_registry.cmi helm_registry.cmi : diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml index f3309633b..c6b2a58fd 100644 --- a/matita/components/registry/helm_registry.ml +++ b/matita/components/registry/helm_registry.ml @@ -412,7 +412,7 @@ let ls registry prefix = | _ -> assert false) ([], []) matching_keys in - (list_uniq (List.sort Pervasives.compare sections), keys) + (list_uniq (List.sort Stdlib.compare sections), keys) (** {2 API implementation} * functional methods above are wrapped so that they work on a default diff --git a/matita/components/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend index 8b3261bc8..8863d5405 100644 --- a/matita/components/syntax_extensions/.depend +++ b/matita/components/syntax_extensions/.depend @@ -1,5 +1,11 @@ -utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmo : \ + utf8MacroTable.cmi \ + utf8Macro.cmi +utf8Macro.cmx : \ + utf8MacroTable.cmx \ + utf8Macro.cmi utf8Macro.cmi : -utf8MacroTable.cmo : -utf8MacroTable.cmx : +utf8MacroTable.cmo : \ + utf8MacroTable.cmi +utf8MacroTable.cmx : \ + utf8MacroTable.cmi diff --git a/matita/components/syntax_extensions/.depend.opt b/matita/components/syntax_extensions/.depend.opt index 98ac1d844..84b72a664 100644 --- a/matita/components/syntax_extensions/.depend.opt +++ b/matita/components/syntax_extensions/.depend.opt @@ -1,3 +1,5 @@ -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmx : \ + utf8MacroTable.cmx \ + utf8Macro.cmi utf8Macro.cmi : utf8MacroTable.cmx : diff --git a/matita/components/syntax_extensions/Makefile b/matita/components/syntax_extensions/Makefile index c2710d414..4f34ae818 100644 --- a/matita/components/syntax_extensions/Makefile +++ b/matita/components/syntax_extensions/Makefile @@ -18,7 +18,7 @@ utf8MacroTable.ml: ./make_table $@ $@.txt utf8MacroTable.cmo: utf8MacroTable.ml @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -c $< + $(H)@$(OCAMLFIND) ocamlc -rectypes -c $< pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo @echo " OCAMLC $<" @@ -29,7 +29,7 @@ pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo profiling_macros.cmo: profiling_macros.ml @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -package camlp5 -pp "camlp5o -loc loc" -c $< + $(H)@$(OCAMLFIND) ocamlc -package camlp5 -package str -pp "camlp5o -loc loc" -c $< profiling_macros.cma:profiling_macros.cmo @echo " OCAMLC -a $@" $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ diff --git a/matita/components/syntax_extensions/utf8Macro.ml b/matita/components/syntax_extensions/utf8Macro.ml index c95282d58..090807bce 100644 --- a/matita/components/syntax_extensions/utf8Macro.ml +++ b/matita/components/syntax_extensions/utf8Macro.ml @@ -50,7 +50,7 @@ let tex_of_unicode s = (Hashtbl.find_all Utf8MacroTable.utf82macro s) in List.sort - (fun x y -> Pervasives.compare (String.length x) (String.length y)) + (fun x y -> Stdlib.compare (String.length x) (String.length y)) alt with Not_found -> [] diff --git a/matita/components/syntax_extensions/utf8MacroTable.mli b/matita/components/syntax_extensions/utf8MacroTable.mli new file mode 100644 index 000000000..b5f51893d --- /dev/null +++ b/matita/components/syntax_extensions/utf8MacroTable.mli @@ -0,0 +1,2 @@ +val macro2utf8 : (string,string) Hashtbl.t +val utf82macro : (string,string) Hashtbl.t diff --git a/matita/components/thread/.depend.opt b/matita/components/thread/.depend.opt index 8ee8dbbec..e022019db 100644 --- a/matita/components/thread/.depend.opt +++ b/matita/components/thread/.depend.opt @@ -1,4 +1,6 @@ -extThread.cmx : extThread.cmi +extThread.cmx : \ + extThread.cmi extThread.cmi : -threadSafe.cmx : threadSafe.cmi +threadSafe.cmx : \ + threadSafe.cmi threadSafe.cmi : diff --git a/matita/components/thread/extThread.ml b/matita/components/thread/extThread.ml index d59cccd26..f81775ff2 100644 --- a/matita/components/thread/extThread.ml +++ b/matita/components/thread/extThread.ml @@ -37,7 +37,7 @@ exception Thread_not_found of Thread.t module OrderedPid = struct type t = int - let compare = Pervasives.compare + let compare = Stdlib.compare end module PidSet = Set.Make (OrderedPid) diff --git a/matita/components/xml/.depend.opt b/matita/components/xml/.depend.opt index 36a543808..31b27a176 100644 --- a/matita/components/xml/.depend.opt +++ b/matita/components/xml/.depend.opt @@ -1,4 +1,6 @@ -xml.cmx : xml.cmi +xml.cmx : \ + xml.cmi xml.cmi : -xmlPushParser.cmx : xmlPushParser.cmi +xmlPushParser.cmx : \ + xmlPushParser.cmi xmlPushParser.cmi : diff --git a/matita/configure.ac b/matita/configure.ac index 04b7da8bd..ba25fab4d 100644 --- a/matita/configure.ac +++ b/matita/configure.ac @@ -1,4 +1,5 @@ -AC_INIT(matita/matitaTypes.ml) +AC_INIT +AC_CONFIG_SRCDIR([matita/matitaTypes.ml]) # Distribution settings # (i.e. settings (automatically) manipulated before a release) @@ -63,6 +64,7 @@ echo "done" FINDLIB_LIBSREQUIRES="\ expat \ http \ +camlp-streams \ pcre \ str \ unix \ @@ -205,11 +207,12 @@ AC_SUBST(RT_BASE_DIR) AC_SUBST(SRCROOT) AC_SUBST(TRANSFORMER_MODULE) -AC_OUTPUT([ +AC_CONFIG_FILES([ components/extlib/componentsConf.ml matita/matita.conf.xml matita/buildTimeConf.ml matita/help/C/version.txt Makefile.defs ]) +AC_OUTPUT diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index 447ce30aa..f1994ce59 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -1,47 +1,117 @@ -applyTransformation.cmx : applyTransformation.cmi +applyTransformation.cmx : \ + applyTransformation.cmi applyTransformation.cmi : buildTimeConf.cmx : -cicMathView.cmx : matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ - buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi -cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi -lablGraphviz.cmx : lablGraphviz.cmi +cicMathView.cmx : \ + matitaMisc.cmx \ + matitaGuiTypes.cmi \ + matitaGtkMisc.cmx \ + buildTimeConf.cmx \ + applyTransformation.cmx \ + cicMathView.cmi +cicMathView.cmi : \ + matitaGuiTypes.cmi \ + applyTransformation.cmi +lablGraphviz.cmx : \ + lablGraphviz.cmi lablGraphviz.cmi : -matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \ - matitaInit.cmx matitaGui.cmx buildTimeConf.cmx applyTransformation.cmx -matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi -matitaEngine.cmi : applyTransformation.cmi -matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi +matita.cmx : \ + predefined_virtuals.cmx \ + matitaScript.cmx \ + matitaMisc.cmx \ + matitaInit.cmx \ + matitaGui.cmx \ + buildTimeConf.cmx \ + applyTransformation.cmx +matitaEngine.cmx : \ + applyTransformation.cmx \ + matitaEngine.cmi +matitaEngine.cmi : \ + applyTransformation.cmi +matitaExcPp.cmx : \ + matitaEngine.cmx \ + matitaExcPp.cmi matitaExcPp.cmi : matitaGeneratedGui.cmx : -matitaGtkMisc.cmx : matitaGeneratedGui.cmx buildTimeConf.cmx \ +matitaGtkMisc.cmx : \ + matitaGeneratedGui.cmx \ + buildTimeConf.cmx \ matitaGtkMisc.cmi -matitaGtkMisc.cmi : matitaGeneratedGui.cmx -matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ - matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi -matitaGui.cmi : matitaGuiTypes.cmi +matitaGtkMisc.cmi : \ + matitaGeneratedGui.cmx +matitaGui.cmx : \ + matitaTypes.cmx \ + matitaScript.cmx \ + matitaMisc.cmx \ + matitaMathView.cmx \ + matitaGuiTypes.cmi \ + matitaGtkMisc.cmx \ + matitaGeneratedGui.cmx \ + matitaExcPp.cmx \ + buildTimeConf.cmx \ + matitaGui.cmi +matitaGui.cmi : \ + matitaGuiTypes.cmi matitaGuiInit.cmx : -matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi -matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi +matitaGuiTypes.cmi : \ + matitaGeneratedGui.cmx \ + applyTransformation.cmi +matitaInit.cmx : \ + matitaExcPp.cmx \ + buildTimeConf.cmx \ + matitaInit.cmi matitaInit.cmi : -matitaMathView.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \ - matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaMathView.cmi -matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi -matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi -matitaMisc.cmi : matitaGuiTypes.cmi -matitaScript.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \ - buildTimeConf.cmx matitaScript.cmi +matitaMathView.cmx : \ + virtuals.cmx \ + matitaTypes.cmx \ + matitaMisc.cmx \ + matitaGuiTypes.cmi \ + matitaGtkMisc.cmx \ + matitaGeneratedGui.cmx \ + matitaExcPp.cmx \ + lablGraphviz.cmx \ + cicMathView.cmx \ + buildTimeConf.cmx \ + applyTransformation.cmx \ + matitaMathView.cmi +matitaMathView.cmi : \ + matitaTypes.cmi \ + matitaGuiTypes.cmi +matitaMisc.cmx : \ + matitaGuiTypes.cmi \ + buildTimeConf.cmx \ + matitaMisc.cmi +matitaMisc.cmi : \ + matitaGuiTypes.cmi +matitaScript.cmx : \ + virtuals.cmx \ + matitaTypes.cmx \ + matitaMisc.cmx \ + matitaMathView.cmx \ + matitaGtkMisc.cmx \ + matitaEngine.cmx \ + cicMathView.cmx \ + buildTimeConf.cmx \ + matitaScript.cmi matitaScript.cmi : -matitaTypes.cmx : matitaTypes.cmi +matitaTypes.cmx : \ + matitaTypes.cmi matitaTypes.cmi : -matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \ +matitac.cmx : \ + matitaclean.cmx \ + matitaMisc.cmx \ + matitaInit.cmx \ + matitaExcPp.cmx \ matitaEngine.cmx -matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi +matitaclean.cmx : \ + matitaMisc.cmx \ + matitaInit.cmx \ + matitaclean.cmi matitaclean.cmi : -predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi +predefined_virtuals.cmx : \ + virtuals.cmx \ + predefined_virtuals.cmi predefined_virtuals.cmi : -virtuals.cmx : virtuals.cmi +virtuals.cmx : \ + virtuals.cmi virtuals.cmi : diff --git a/matita/matita/Makefile b/matita/matita/Makefile index d40a15c7a..527699110 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -11,7 +11,8 @@ else ANNOTOPTION = endif -OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7 +#OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-70-31 +OCAML_FLAGS = -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-70-31-29 OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index ec42ee8df..8f6bd6204 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -637,7 +637,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> + 'status. (#ApplyTransformation.status as 'status) -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -654,7 +654,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit + 'status. (#ApplyTransformation.status as 'status) -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -675,7 +675,7 @@ object (self) ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) end;*) self#load_root ~root:txt; - (*current_mathml <- Some mathml*)(*)*); + (*current_mathml <- Some mathml*)(* ) *); end (** constructors *) @@ -686,7 +686,7 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi GContainer.pack_container ~create:(fun pl -> let obj = SourceView.new_ () in Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl; - new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView) + new _cicMathView obj)(* )) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView) let screenshot _status _sequents _metasenv _subst (_filename (*as ofn*)) = () (*MATITA 1.0 diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml index e31efac1f..2d6e3b431 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml @@ -41,7 +41,7 @@ let read_dir file = Filename.remove_extension name in let dir = Array.to_list (Sys.readdir file) in - let mods = List.fast_sort Pervasives.compare (list_rev_filter_map filter map dir) in + let mods = List.fast_sort Stdlib.compare (list_rev_filter_map filter map dir) in { ET.cdir = file; mods; } @@ -62,7 +62,7 @@ let read_index dir = try read_mods mods ich with | End_of_file -> close_in ich end; - let mods = List.fast_sort Pervasives.compare !mods in + let mods = List.fast_sort Stdlib.compare !mods in { ET.cdir = dir; mods; } diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index b0a5c7f12..169800e59 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -106,7 +106,7 @@ let compact_disambiguation_errors all_passes errorll = filter choices in filter_phase_3 - (List.map (fun o,l -> o,List.sort choices_compare_by_passes l) + (List.map (fun (o,l) -> o,List.sort choices_compare_by_passes l) (uniq (List.stable_sort choices_compare choices))) in choices @@ -155,8 +155,7 @@ let rec to_string exn = | MatitaEngine.TryingToAdd msg -> None, "Attempt to insert an alias in batch mode: " ^ Lazy.force msg | MatitaEngine.AlreadyLoaded msg -> - None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is - already loaded; undo the inclusion and try again." + None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is already loaded; undo the inclusion and try again." | MatitaEngine.FailureCompiling (filename,exn) -> None, "Compiling " ^ filename ^ ":\n" ^ snd (to_string exn) | NCicRefiner.AssertFailure msg -> diff --git a/matita/matita/matitaGtkMisc.mli b/matita/matita/matitaGtkMisc.mli index 04a531216..6884e232e 100644 --- a/matita/matita/matitaGtkMisc.mli +++ b/matita/matita/matitaGtkMisc.mli @@ -76,7 +76,9 @@ class multiStringListModel: method list_store: GTree.list_store (** list_store forwarding *) method easy_mappend: string list -> unit (** append + set *) + method easy_minsert: int -> string list -> unit (** insert + set *) + method easy_mselection: unit -> string list list end @@ -87,7 +89,9 @@ class stringListModel: inherit multiStringListModel method easy_append: string -> unit (** append + set *) + method easy_insert: int -> string -> unit (** insert + set *) + method easy_selection: unit -> string list end diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index ad34b7a57..7e2b0401b 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -169,7 +169,7 @@ class interpErrorModel = tree_store#clear (); let idx1 = ref ~-1 in List.iter - (fun _,lll -> + (fun (_,lll) -> incr idx1; let loc_row = if List.length choices = 1 then @@ -196,7 +196,7 @@ class interpErrorModel = Some loc_row) in let idx2 = ref ~-1 in List.iter - (fun passes,envs_and_diffs,_,_ -> + (fun (passes,envs_and_diffs,_,_) -> incr idx2; let msg_row = if List.length lll = 1 then @@ -375,7 +375,7 @@ let interactive_error_interp ~all_passes String.concat "\n" ("" :: List.map - (fun k,desc -> + (fun (k,desc) -> let alias = match k with | DisambiguateTypes.Id id -> @@ -716,7 +716,6 @@ class gui () = "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n"); - let module Hr = Helm_registry in MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem ~callback:(function | true -> main#toplevel#fullscreen () diff --git a/matita/matita/matitaInit.ml b/matita/matita/matitaInit.ml index 2c2a818a2..9f7ae3ac2 100644 --- a/matita/matita/matitaInit.ml +++ b/matita/matita/matitaInit.ml @@ -59,7 +59,7 @@ let registry_defaults = [ let set_registry_values = List.iter - (fun key, value -> + (fun (key, value) -> if not (Helm_registry.has key) then Helm_registry.set ~key ~value) let fill_registry init_status = @@ -116,7 +116,7 @@ let initialize_environment init_status = let status = ref [] -let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *) +let usages = Hashtbl.create 11 (* app name (e.g. "matitac") -> usage string *) let _ = List.iter (fun (name, s) -> Hashtbl.replace usages name s) diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 271a7b19a..93a0b65ea 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -97,7 +97,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = goal2win <- []; _metasenv <- [],[] - method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit + method nload_sequents : 'status. (#GrafiteTypes.status as 'status) -> unit = fun (status : #GrafiteTypes.status) -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- metasenv,subst; @@ -151,7 +151,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = end in let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in - Stack.iter (** populate notebook with tabs *) + Stack.iter (* populate notebook with tabs *) ~env:(fun depth _tag (pos, sw) -> let markup = match depth, pos with @@ -172,7 +172,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #ApplyTransformation.status as 'status -> page:int -> + 'status. (#ApplyTransformation.status as 'status) -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page:_ ~goal_switch -> (match goal_switch with @@ -204,7 +204,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = (w#vadjustment#upper -. w#vadjustment#page_size)); with Not_found -> assert false) - method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit + method goto_sequent: 'status. (#ApplyTransformation.status as 'status) -> int -> unit = fun status goal -> let goal_switch, page = try @@ -532,10 +532,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (Virtuals.get_all_eqclass ())); Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n"; List.iter - (fun tag, items -> + (fun (tag, items) -> Printf.bprintf b " %s:\n" tag; List.iter - (fun names, symbol -> + (fun (names, symbol) -> Printf.bprintf b " \t%s\t%s\n" (Glib.Utf8.from_unichar symbol) (String.concat ", " names)) diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli index dd1e18955..567f67d42 100644 --- a/matita/matita/matitaMathView.mli +++ b/matita/matita/matitaMathView.mli @@ -30,6 +30,7 @@ val sequentsViewer_instance: GPack.notebook -> MatitaGuiTypes.sequentsViewer val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) (** {2 Rendering in a browser} *) + (** @param reuse if set reused last opened cic browser otherwise * opens a new one. default is false *) val cicBrowser: ?reuse:bool -> MatitaTypes.mathViewer_entry option -> unit @@ -42,6 +43,7 @@ val has_selection: unit -> bool * @raise Failure "no selection" *) val copy_selection: unit -> unit val has_clipboard: unit -> bool (** clipboard is not empty *) + val empty_clipboard: unit -> unit (** empty the clipboard *) (** @raise Failure "empty clipboard" *) diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index 53d1d1f67..e773fc977 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -38,8 +38,8 @@ let strip_suffix ~suffix s = let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file -let is_proof_script _fname = true (** TODO Zack *) -let is_proof_object _fname = true (** TODO Zack *) +let is_proof_script _fname = true (* TODO Zack *) +let is_proof_object _fname = true (* TODO Zack *) let append_phrase_sep s = if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then diff --git a/matita/matita/matitaMisc.mli b/matita/matita/matitaMisc.mli index b3bd617b2..c189861c6 100644 --- a/matita/matita/matitaMisc.mli +++ b/matita/matita/matitaMisc.mli @@ -35,7 +35,8 @@ val is_proof_object: string -> bool * it *) val append_phrase_sep: string -> string -val normalize_dir: string -> string (** add trailing "/" if missing *) + (** add trailing "/" if missing *) +val normalize_dir: string -> string val strip_suffix: suffix:string -> string -> string (** @return tl tail of a list starting at a given element @@ -50,8 +51,12 @@ type 'a memento class type ['a] history = object ('b) method add : 'a -> unit - method next : 'a (** @raise History_failure *) - method previous : 'a (** @raise History_failure *) + + (** @raise History_failure *) + method next : 'a + + (** @raise History_failure *) + method previous : 'a method load: 'a memento -> unit method save: 'a memento method is_begin: bool diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index c39e1de40..240122134 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -102,7 +102,7 @@ let eval_nmacro _include_paths (_buffer : GText.buffer) status _unparsed_text pa let name = Filename.dirname (script#filename) ^ "/" ^ name in let sequents = let selected = Continuationals.Stack.head_goals status#stack in - List.filter (fun x,_ -> List.mem x selected) menv + List.filter (fun (x,_) -> List.mem x selected) menv in CicMathView.screenshot status sequents menv subst name; [status, parsed_text], "", parsed_text_length diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index f90ab14bd..45f3829dd 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1497,7 +1497,7 @@ let predefined_virtuals = [ let load_predefined_virtuals () = List.iter - (fun a,b,c -> + (fun (a,b,c) -> Virtuals.add_virtual a (Glib.Utf8.first_char b) c) predefined_virtuals ;;