- 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
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"
-requires=""
+requires="str unix"
version="0.0.1"
archive(byte,mt)="thread.cma"
archive(native,mt)="thread.cmxa"
-requires="zip expat helm-extlib"
+requires="zip expat helm-extlib camlp-streams"
version="0.0.1"
archive(byte)="xml.cma"
archive(native)="xml.cmxa"
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 =
(* $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)
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
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
;;
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
-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
-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
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;
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)
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, _) ->
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 =
| _,[] -> 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)
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
[ 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))
-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
module OrderedDomain =
struct
type t = domain_item
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
(* module Domain = Set.Make (OrderedDomain) *)
-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 :
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)
-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 :
(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;
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
grafiteAst.cmx :
-grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi
-grafiteAstPp.cmi : grafiteAst.cmx
+grafiteAstPp.cmx : \
+ grafiteAst.cmx \
+ grafiteAstPp.cmi
+grafiteAstPp.cmi : \
+ grafiteAst.cmx
-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
-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
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
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 ->
~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
-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 :
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 *)
| 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 *)
(* 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 *)
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
[] 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
;;
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
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)))
*)
-helmLogger.cmx : helmLogger.cmi
+helmLogger.cmx : \
+ helmLogger.cmi
helmLogger.cmi :
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
+interpretations.cmx : \
+ ncic2astMatcher.cmx \
+ interpretations.cmi
interpretations.cmi :
-ncic2astMatcher.cmx : ncic2astMatcher.cmi
+ncic2astMatcher.cmx : \
+ ncic2astMatcher.cmi
ncic2astMatcher.cmi :
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);;
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
-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 :
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 *)
-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
-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 :
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);;
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 =
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)
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
;;
-nCicLibrary.cmx : nCicLibrary.cmi
+nCicLibrary.cmx : \
+ nCicLibrary.cmi
nCicLibrary.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
+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 :
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
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
;;
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
--- /dev/null
+/***********************************************************************/
+/* */
+/* 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);
+}
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
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
| ( 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? *)
;;
| ((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
| _ -> 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 = *)
module OT =
struct
type t = int
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module M : Map.S with type key = int
-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 :
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)
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)
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
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 (
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)
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 =
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) ;;
-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
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
;;
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)
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
module M =
struct
type t = int
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
;;
-helm_registry.cmx : helm_registry.cmi
+helm_registry.cmx : \
+ helm_registry.cmi
helm_registry.cmi :
| _ -> 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
-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
-utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmx : \
+ utf8MacroTable.cmx \
+ utf8Macro.cmi
utf8Macro.cmi :
utf8MacroTable.cmx :
./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 $<"
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 $@ $^
(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 -> []
--- /dev/null
+val macro2utf8 : (string,string) Hashtbl.t
+val utf82macro : (string,string) Hashtbl.t
-extThread.cmx : extThread.cmi
+extThread.cmx : \
+ extThread.cmi
extThread.cmi :
-threadSafe.cmx : threadSafe.cmi
+threadSafe.cmx : \
+ threadSafe.cmi
threadSafe.cmi :
module OrderedPid =
struct
type t = int
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module PidSet = Set.Make (OrderedPid)
-xml.cmx : xml.cmi
+xml.cmx : \
+ xml.cmi
xml.cmi :
-xmlPushParser.cmx : xmlPushParser.cmi
+xmlPushParser.cmx : \
+ xmlPushParser.cmi
xmlPushParser.cmi :
-AC_INIT(matita/matitaTypes.ml)
+AC_INIT
+AC_CONFIG_SRCDIR([matita/matitaTypes.ml])
# Distribution settings
# (i.e. settings (automatically) manipulated before a release)
FINDLIB_LIBSREQUIRES="\
expat \
http \
+camlp-streams \
pcre \
str \
unix \
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
-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 :
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)"
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
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
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
end;*)
self#load_root ~root:txt;
- (*current_mathml <- Some mathml*)(*)*);
+ (*current_mathml <- Some mathml*)(* ) *);
end
(** constructors *)
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
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;
}
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;
}
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
| 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 ->
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
inherit multiStringListModel
method easy_append: string -> unit (** append + set *)
+
method easy_insert: int -> string -> unit (** insert + set *)
+
method easy_selection: unit -> string list
end
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
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
String.concat "\n"
("" ::
List.map
- (fun k,desc ->
+ (fun (k,desc) ->
let alias =
match k with
| DisambiguateTypes.Id id ->
"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 ()
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 =
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)
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;
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
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
(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
(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))
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
* @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" *)
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
* 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
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
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
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
;;
projects / helm.git / commitdiff