From: Enrico Tassi Date: Mon, 5 Oct 2009 14:13:25 +0000 (+0000) Subject: added auto_cache in the dupable status after an X-Git-Tag: make_still_working~3383 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec07ff398325533d848da92e9dc69852d24b78a5;p=helm.git added auto_cache in the dupable status after an re-factoring and re-typing of the whole serialization code. --- diff --git a/helm/software/components/METAS/meta.helm-grafite_parser.src b/helm/software/components/METAS/meta.helm-grafite_parser.src index a214a83dc..bcde338d3 100644 --- a/helm/software/components/METAS/meta.helm-grafite_parser.src +++ b/helm/software/components/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation" +requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation helm-ng_library" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 25169744f..e12688b64 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -38,14 +38,14 @@ MODULES = \ cic_disambiguation \ lexicon \ ng_disambiguation \ - grafite_parser \ ng_paramodulation \ - ng_tactics \ - grafite_engine \ tptp_grafite \ ng_kernel \ ng_refiner \ - ng_library \ + ng_library \ + grafite_parser \ + ng_tactics \ + grafite_engine \ $(NULL) METAS = $(MODULES:%=METAS/META.helm-%) diff --git a/helm/software/components/acic_content/.depend b/helm/software/components/acic_content/.depend index 8ade458af..89dca0e44 100644 --- a/helm/software/components/acic_content/.depend +++ b/helm/software/components/acic_content/.depend @@ -1,3 +1,4 @@ +content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmo @@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmo termAcicContent.cmi: cicNotationPt.cmo +cicNotationPt.cmo: +cicNotationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi acic2content.cmo: content.cmi acic2content.cmi diff --git a/helm/software/components/acic_content/.depend.opt b/helm/software/components/acic_content/.depend.opt index fef879256..307fceaa0 100644 --- a/helm/software/components/acic_content/.depend.opt +++ b/helm/software/components/acic_content/.depend.opt @@ -1,3 +1,4 @@ +content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmx @@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmx cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmx termAcicContent.cmi: cicNotationPt.cmx +cicNotationPt.cmo: +cicNotationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi acic2content.cmo: content.cmi acic2content.cmi diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 8d0128744..97238c4d8 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,6 +1,13 @@ +proceduralHelpers.cmi: +proceduralClassify.cmi: +proceduralOptimizer.cmi: +proceduralTypes.cmi: +proceduralMode.cmi: +proceduralConversion.cmi: procedural1.cmi: proceduralTypes.cmi procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi +acic2Procedural.cmi: proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 8d0128744..97238c4d8 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,6 +1,13 @@ +proceduralHelpers.cmi: +proceduralClassify.cmi: +proceduralOptimizer.cmi: +proceduralTypes.cmi: +proceduralMode.cmi: +proceduralConversion.cmi: procedural1.cmi: proceduralTypes.cmi procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi +acic2Procedural.cmi: proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend index e69de29bb..0c39328ae 100644 --- a/helm/software/components/binaries/extractor/.depend +++ b/helm/software/components/binaries/extractor/.depend @@ -0,0 +1,4 @@ +extractor.cmo: +extractor.cmx: +extractor_manager.cmo: +extractor_manager.cmx: diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt index e69de29bb..0c39328ae 100644 --- a/helm/software/components/binaries/extractor/.depend.opt +++ b/helm/software/components/binaries/extractor/.depend.opt @@ -0,0 +1,4 @@ +extractor.cmo: +extractor.cmx: +extractor_manager.cmo: +extractor_manager.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend index e69de29bb..33147b949 100644 --- a/helm/software/components/binaries/table_creator/.depend +++ b/helm/software/components/binaries/table_creator/.depend @@ -0,0 +1,2 @@ +table_creator.cmo: +table_creator.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt index e69de29bb..33147b949 100644 --- a/helm/software/components/binaries/table_creator/.depend.opt +++ b/helm/software/components/binaries/table_creator/.depend.opt @@ -0,0 +1,2 @@ +table_creator.cmo: +table_creator.cmx: diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index c2c7105c7..a835b247f 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -1,8 +1,10 @@ +cicUniv.cmi: unshare.cmi: cic.cmo deannotate.cmi: cic.cmo cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo +libraryObjects.cmi: cic_indexable.cmi: cic.cmo path_indexing.cmi: cic.cmo cicInspect.cmi: cic.cmo diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt index 76d19c1ff..8cdd2a86a 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -1,8 +1,10 @@ +cicUniv.cmi: unshare.cmi: cic.cmx deannotate.cmi: cic.cmx cicParser.cmi: cic.cmx cicUtil.cmi: cic.cmx helmLibraryObjects.cmi: cic.cmx +libraryObjects.cmi: cic_indexable.cmi: cic.cmx path_indexing.cmi: cic.cmx cicInspect.cmi: cic.cmx diff --git a/helm/software/components/cic_acic/.depend b/helm/software/components/cic_acic/.depend index 3fc1e0dce..5449d50aa 100644 --- a/helm/software/components/cic_acic/.depend +++ b/helm/software/components/cic_acic/.depend @@ -1,3 +1,6 @@ +eta_fixing.cmi: +doubleTypeInference.cmi: +cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt index 3fc1e0dce..5449d50aa 100644 --- a/helm/software/components/cic_acic/.depend.opt +++ b/helm/software/components/cic_acic/.depend.opt @@ -1,3 +1,6 @@ +eta_fixing.cmi: +doubleTypeInference.cmi: +cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index e9bd1168f..a9ae65a5e 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,3 +1,5 @@ +cicDisambiguate.cmi: +disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt index e9bd1168f..a9ae65a5e 100644 --- a/helm/software/components/cic_disambiguation/.depend.opt +++ b/helm/software/components/cic_disambiguation/.depend.opt @@ -1,3 +1,5 @@ +cicDisambiguate.cmi: +disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_exportation/.depend b/helm/software/components/cic_exportation/.depend index 288ea5f6c..91be8d88d 100644 --- a/helm/software/components/cic_exportation/.depend +++ b/helm/software/components/cic_exportation/.depend @@ -1,2 +1,3 @@ +cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt index 288ea5f6c..91be8d88d 100644 --- a/helm/software/components/cic_exportation/.depend.opt +++ b/helm/software/components/cic_exportation/.depend.opt @@ -1,2 +1,3 @@ +cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend index 5d83fd0f3..f8a16629e 100644 --- a/helm/software/components/cic_proof_checking/.depend +++ b/helm/software/components/cic_proof_checking/.depend @@ -1,3 +1,13 @@ +cicLogger.cmi: +cicEnvironment.cmi: +cicPp.cmi: +cicUnivUtils.cmi: +cicSubstitution.cmi: +cicMiniReduction.cmi: +cicReduction.cmi: +cicTypeChecker.cmi: +freshNamesGenerator.cmi: +cicDischarge.cmi: cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi cicEnvironment.cmo: cicEnvironment.cmi diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt index 5d83fd0f3..f8a16629e 100644 --- a/helm/software/components/cic_proof_checking/.depend.opt +++ b/helm/software/components/cic_proof_checking/.depend.opt @@ -1,3 +1,13 @@ +cicLogger.cmi: +cicEnvironment.cmi: +cicPp.cmi: +cicUnivUtils.cmi: +cicSubstitution.cmi: +cicMiniReduction.cmi: +cicReduction.cmi: +cicTypeChecker.cmi: +freshNamesGenerator.cmi: +cicDischarge.cmi: cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi cicEnvironment.cmo: cicEnvironment.cmi diff --git a/helm/software/components/cic_unification/.depend b/helm/software/components/cic_unification/.depend index a7b23ceb4..2e054f73d 100644 --- a/helm/software/components/cic_unification/.depend +++ b/helm/software/components/cic_unification/.depend @@ -1,3 +1,10 @@ +cicMetaSubst.cmi: +cicMkImplicit.cmi: +termUtil.cmi: +coercGraph.cmi: +cicUnification.cmi: +cicReplace.cmi: +cicRefine.cmi: cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt index a7b23ceb4..2e054f73d 100644 --- a/helm/software/components/cic_unification/.depend.opt +++ b/helm/software/components/cic_unification/.depend.opt @@ -1,3 +1,10 @@ +cicMetaSubst.cmi: +cicMkImplicit.cmi: +termUtil.cmi: +coercGraph.cmi: +cicUnification.cmi: +cicReplace.cmi: +cicRefine.cmi: cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 6dd0e78a1..8d74439eb 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -1,3 +1,9 @@ +renderingAttrs.cmi: +cicNotationLexer.cmi: +cicNotationParser.cmi: +mpresentation.cmi: +box.cmi: +content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt index 6dd0e78a1..8d74439eb 100644 --- a/helm/software/components/content_pres/.depend.opt +++ b/helm/software/components/content_pres/.depend.opt @@ -1,3 +1,9 @@ +renderingAttrs.cmi: +cicNotationLexer.cmi: +cicNotationParser.cmi: +mpresentation.cmi: +box.cmi: +content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi diff --git a/helm/software/components/disambiguation/.depend b/helm/software/components/disambiguation/.depend index aba9ffea7..9fdbeeeaf 100644 --- a/helm/software/components/disambiguation/.depend +++ b/helm/software/components/disambiguation/.depend @@ -1,3 +1,4 @@ +disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt index aba9ffea7..9fdbeeeaf 100644 --- a/helm/software/components/disambiguation/.depend.opt +++ b/helm/software/components/disambiguation/.depend.opt @@ -1,3 +1,4 @@ +disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend index 201cd0cba..dcc6377a0 100644 --- a/helm/software/components/extlib/.depend +++ b/helm/software/components/extlib/.depend @@ -1,3 +1,13 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +discrimination_tree.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt index 201cd0cba..dcc6377a0 100644 --- a/helm/software/components/extlib/.depend.opt +++ b/helm/software/components/extlib/.depend.opt @@ -1,3 +1,13 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +discrimination_tree.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi diff --git a/helm/software/components/getter/.depend b/helm/software/components/getter/.depend index 20f69cf0c..ca64d8ec0 100644 --- a/helm/software/components/getter/.depend +++ b/helm/software/components/getter/.depend @@ -1,6 +1,13 @@ +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: http_getter_env.cmi: http_getter_types.cmo +http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmo http_getter.cmi: http_getter_types.cmo +http_getter_types.cmo: +http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi diff --git a/helm/software/components/getter/.depend.opt b/helm/software/components/getter/.depend.opt index 554fb1ec7..64da37f13 100644 --- a/helm/software/components/getter/.depend.opt +++ b/helm/software/components/getter/.depend.opt @@ -1,6 +1,13 @@ +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: http_getter_env.cmi: http_getter_types.cmx +http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmx http_getter.cmi: http_getter_types.cmx +http_getter_types.cmo: +http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi diff --git a/helm/software/components/grafite/.depend b/helm/software/components/grafite/.depend index dc225e221..f305b1580 100644 --- a/helm/software/components/grafite/.depend +++ b/helm/software/components/grafite/.depend @@ -1,5 +1,7 @@ grafiteAstPp.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo +grafiteAst.cmo: +grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi diff --git a/helm/software/components/grafite/.depend.opt b/helm/software/components/grafite/.depend.opt index 0f64ba789..e01d5bbfa 100644 --- a/helm/software/components/grafite/.depend.opt +++ b/helm/software/components/grafite/.depend.opt @@ -1,5 +1,7 @@ grafiteAstPp.cmi: grafiteAst.cmx grafiteMarshal.cmi: grafiteAst.cmx +grafiteAst.cmo: +grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend index a545f14e3..10236823a 100644 --- a/helm/software/components/grafite_engine/.depend +++ b/helm/software/components/grafite_engine/.depend @@ -1,3 +1,4 @@ +grafiteTypes.cmi: grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi diff --git a/helm/software/components/grafite_engine/.depend.opt b/helm/software/components/grafite_engine/.depend.opt index a545f14e3..10236823a 100644 --- a/helm/software/components/grafite_engine/.depend.opt +++ b/helm/software/components/grafite_engine/.depend.opt @@ -1,3 +1,4 @@ +grafiteTypes.cmi: grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 5ae6e92ed..9fa8dbb00 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -487,8 +487,10 @@ let inject_unification_hint = = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in - NCicLibrary.Serializer.register - "unification_hints" basic_eval_unification_hint + NCicLibrary.Serializer.register#run "unification_hints" + object(_ : 'a NCicLibrary.register_type) + method run = basic_eval_unification_hint + end ;; let eval_unification_hint status t n = @@ -502,6 +504,45 @@ let eval_unification_hint status t n = status,`New [] ;; +let basic_index_obj l status = + status#set_auto_cache + (List.fold_left + (fun t (k,v) -> + NDiscriminationTree.DiscriminationTree.index t k v) + status#auto_cache l) +;; + +let record_index_obj = + let aux l + ~refresh_uri_in_universe + ~refresh_uri_in_term + = + basic_index_obj + (List.map + (fun k,v -> refresh_uri_in_term k, refresh_uri_in_term v) + l) + in + NCicLibrary.Serializer.register#run "index_obj" + object(_ : 'a NCicLibrary.register_type) + method run = aux + end +;; + +let index_obj_for_auto status (uri, height, _, _, kind) = + let data = + match kind with + | NCic.Fixpoint _ -> [] + | NCic.Inductive _ -> [] + | NCic.Constant (_,_,_, ty, _) -> + [ ty, NCic.Const(NReference.reference_of_spec + uri (NReference.Def height)) ] + in + let status = basic_index_obj data status in + let dump = record_index_obj data :: status#dump in + status#set_dump dump +;; + + let basic_eval_add_constraint (u1,u2) status = NCicLibrary.add_constraint status u1 u2 ;; @@ -515,7 +556,10 @@ let inject_constraint = let u2 = refresh_uri_in_universe u2 in basic_eval_add_constraint (u1,u2) in - NCicLibrary.Serializer.register "constraints" basic_eval_add_constraint + NCicLibrary.Serializer.register#run "constraints" + object(_:'a NCicLibrary.register_type) + method run = basic_eval_add_constraint + end ;; let eval_add_constraint status u1 u2 = @@ -709,6 +753,7 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; + let rec eval_ncommand opts status (text,prefix_len,cmd) = match cmd with | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n @@ -748,6 +793,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let obj = uri,height,[],[],obj_kind in let old_status = status in let status = NCicLibrary.add_obj status obj in + let status = index_obj_for_auto status obj in (* prerr_endline (NCicPp.ppobj obj); *) HLog.message ("New object: " ^ NUri.string_of_uri uri); (try diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml index 2f103cf83..ea112bf4e 100644 --- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml @@ -294,7 +294,10 @@ let record_ncoercion = let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term = List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l in - NCicLibrary.Serializer.register "ncoercion" aux_l + NCicLibrary.Serializer.register#run "ncoercion" + object(self : 'a NCicLibrary.register_type) + method run = aux_l + end ;; let basic_eval_and_record_ncoercion infos status = diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index 97bf4d7c2..2766b04d0 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -1,4 +1,9 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +nEstatus.cmi: grafiteDisambiguate.cmi: nEstatus.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index 97bf4d7c2..2766b04d0 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -1,4 +1,9 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +nEstatus.cmi: grafiteDisambiguate.cmi: nEstatus.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi diff --git a/helm/software/components/hgdome/.depend b/helm/software/components/hgdome/.depend index bf9c09af7..072d9697a 100644 --- a/helm/software/components/hgdome/.depend +++ b/helm/software/components/hgdome/.depend @@ -1,3 +1,5 @@ +domMisc.cmi: +xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt index bf9c09af7..072d9697a 100644 --- a/helm/software/components/hgdome/.depend.opt +++ b/helm/software/components/hgdome/.depend.opt @@ -1,3 +1,5 @@ +domMisc.cmi: +xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend index 16e6e9da7..ce439d961 100644 --- a/helm/software/components/hmysql/.depend +++ b/helm/software/components/hmysql/.depend @@ -1,2 +1,7 @@ +hSql.cmi: +hSqlite3.cmo: +hSqlite3.cmx: +hMysql.cmo: +hMysql.cmx: hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt index 602c901b8..c2289bff2 100644 --- a/helm/software/components/hmysql/.depend.opt +++ b/helm/software/components/hmysql/.depend.opt @@ -1,2 +1,7 @@ +hSql.cmi: +hSqlite3.cmo: +hSqlite3.cmx: +hMysql.cmo: +hMysql.cmx: hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/lexicon/.depend b/helm/software/components/lexicon/.depend index 847a4a807..16c114516 100644 --- a/helm/software/components/lexicon/.depend +++ b/helm/software/components/lexicon/.depend @@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmo cicNotation.cmi: lexiconAst.cmo lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo +lexiconAst.cmo: +lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt index 463d8a7bc..0fee4b18e 100644 --- a/helm/software/components/lexicon/.depend.opt +++ b/helm/software/components/lexicon/.depend.opt @@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmx cicNotation.cmi: lexiconAst.cmx lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx +lexiconAst.cmo: +lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend index a9f24f814..cfa1295ed 100644 --- a/helm/software/components/library/.depend +++ b/helm/software/components/library/.depend @@ -1,4 +1,13 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi libraryMisc.cmo: libraryMisc.cmi diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt index a9f24f814..cfa1295ed 100644 --- a/helm/software/components/library/.depend.opt +++ b/helm/software/components/library/.depend.opt @@ -1,4 +1,13 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi libraryMisc.cmo: libraryMisc.cmi diff --git a/helm/software/components/logger/.depend b/helm/software/components/logger/.depend index 28268d29e..dfb4400ff 100644 --- a/helm/software/components/logger/.depend +++ b/helm/software/components/logger/.depend @@ -1,2 +1,3 @@ +helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/logger/.depend.opt b/helm/software/components/logger/.depend.opt index 28268d29e..dfb4400ff 100644 --- a/helm/software/components/logger/.depend.opt +++ b/helm/software/components/logger/.depend.opt @@ -1,2 +1,3 @@ +helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/metadata/.depend b/helm/software/components/metadata/.depend index 492a34e3a..78cd97a0d 100644 --- a/helm/software/components/metadata/.depend +++ b/helm/software/components/metadata/.depend @@ -1,3 +1,5 @@ +sqlStatements.cmi: +metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt index 492a34e3a..78cd97a0d 100644 --- a/helm/software/components/metadata/.depend.opt +++ b/helm/software/components/metadata/.depend.opt @@ -1,3 +1,5 @@ +sqlStatements.cmi: +metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend index b4e17fa99..1316c8eab 100644 --- a/helm/software/components/ng_cic_content/.depend +++ b/helm/software/components/ng_cic_content/.depend @@ -1,3 +1,5 @@ +ncic2astMatcher.cmi: +nTermCicContent.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi diff --git a/helm/software/components/ng_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt index b4e17fa99..1316c8eab 100644 --- a/helm/software/components/ng_cic_content/.depend.opt +++ b/helm/software/components/ng_cic_content/.depend.opt @@ -1,3 +1,5 @@ +ncic2astMatcher.cmi: +nTermCicContent.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend index 6b4ef95c1..2de54dc5e 100644 --- a/helm/software/components/ng_disambiguation/.depend +++ b/helm/software/components/ng_disambiguation/.depend @@ -1,2 +1,3 @@ +nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt index 6b4ef95c1..2de54dc5e 100644 --- a/helm/software/components/ng_disambiguation/.depend.opt +++ b/helm/software/components/ng_disambiguation/.depend.opt @@ -1,2 +1,3 @@ +nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index fa6e42064..365aaf261 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,3 +1,4 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 7720472e8..f50abe93c 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,3 +1,4 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend index c76001c01..48127a325 100644 --- a/helm/software/components/ng_library/.depend +++ b/helm/software/components/ng_library/.depend @@ -1,2 +1,3 @@ +nCicLibrary.cmi: nCicLibrary.cmo: nCicLibrary.cmi nCicLibrary.cmx: nCicLibrary.cmi diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt index c76001c01..48127a325 100644 --- a/helm/software/components/ng_library/.depend.opt +++ b/helm/software/components/ng_library/.depend.opt @@ -1,2 +1,3 @@ +nCicLibrary.cmi: nCicLibrary.cmo: nCicLibrary.cmi nCicLibrary.cmx: nCicLibrary.cmi diff --git a/helm/software/components/ng_library/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml index 6987ec1aa..c5b43d7ca 100644 --- a/helm/software/components/ng_library/nCicLibrary.ml +++ b/helm/software/components/ng_library/nCicLibrary.ml @@ -143,6 +143,23 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let init = load_db;; +type automation_cache = NDiscriminationTree.DiscriminationTree.t + +class type g_auto_status = + object + method auto_cache : automation_cache + end + +class auto_status = + object(self) + val auto_cache = NDiscriminationTree.DiscriminationTree.empty + method auto_cache = auto_cache + method set_auto_cache v = {< auto_cache = v >} + method set_auto_status + : 'status. #g_auto_status as 'status -> 'self + = fun o -> self#set_auto_cache o#auto_cache + end + class type g_status = object inherit NRstatus.g_status @@ -150,27 +167,14 @@ class type g_status = end class status = - object + object(self) inherit NRstatus.status val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} method set_library_status : 'status. #g_status as 'status -> 'self - = fun o -> {< timestamp = o#timestamp >} - end - - -module type SerializerT = - sig - type status - type obj - val register: - string -> - ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> - ('a -> obj) - val serialize: baseuri:NUri.uri -> obj list -> unit - val require: baseuri:NUri.uri -> status -> status + = fun o -> self#set_timestamp o#timestamp end let time_travel status = @@ -198,65 +202,66 @@ let serialize ~baseuri dump = List.iter (fun u -> add_deps u [baseuri]) !includes; time_travel (new status) ;; + +type obj = string * Obj.t -module SerializerF(S: sig type status end) = - struct - type status = S.status - type obj = string * Obj.t - - let require1 = ref (fun _ -> assert false (* unknown data*)) - let already_registered = ref [] - - let register tag require = - assert (not (List.mem tag !already_registered)); - already_registered := tag :: !already_registered; - let old_require1 = !require1 in - require1 := - (fun (tag',data) as x -> - if tag=tag' then - require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term - else - old_require1 x); - (fun x -> tag,Obj.repr x) - - let serialize = serialize - - let require ~baseuri status = - includes := baseuri::!includes; - let dump = require0 ~baseuri in - List.fold_right !require1 dump status -end - -type sstatus = status - -module Serializer = - struct - include SerializerF(struct type status = sstatus end) - - let require ~baseuri status = - let rstatus = require ~baseuri (status : #status :> status) in - let status = status#set_coerc_db (rstatus#coerc_db) in - let status = status#set_uhint_db (rstatus#uhint_db) in - let status = status#set_timestamp (rstatus#timestamp) in - status - end class type g_dumpable_status = object inherit g_status - method dump: Serializer.obj list + inherit g_auto_status + method dump: obj list end class dumpable_status = object(self) inherit status - val dump = ([] : Serializer.obj list) + inherit auto_status + val dump = ([] : obj list) method dump = dump method set_dump v = {< dump = v >} method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self - = fun o -> (self#set_dump o#dump)#set_coercion_status o + = fun o -> ((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o end +type 'a register_type = + < run: 'status. + 'a -> refresh_uri_in_universe:(NCic.universe -> + NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> + (#dumpable_status as 'status) -> 'status > + +module Serializer = + struct + let require1 = ref (object method run : 'status. obj -> (#dumpable_status as 'status) -> 'status = fun _ -> assert false end (* unknown data*)) + let already_registered = ref [] + + let register = + object + method run : 'a. string -> 'a register_type -> ('a -> obj) + = fun tag require -> + assert (not (List.mem tag !already_registered)); + already_registered := tag :: !already_registered; + let old_require1 = !require1 in + require1 := + object + method run : 'status. obj -> (#dumpable_status as 'status) -> 'status = + fun ((tag',data) as x) -> + if tag=tag' then + require#run (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term + else + old_require1#run x + end; + (fun x -> tag,Obj.repr x) + end + + let serialize = serialize + + let require ~baseuri status = + includes := baseuri::!includes; + let dump = require0 ~baseuri in + List.fold_right !require1#run dump status +end + let decompile ~baseuri = let baseuris = get_deps baseuri in diff --git a/helm/software/components/ng_library/nCicLibrary.mli b/helm/software/components/ng_library/nCicLibrary.mli index e155aaf4a..ea1cfd4e5 100644 --- a/helm/software/components/ng_library/nCicLibrary.mli +++ b/helm/software/components/ng_library/nCicLibrary.mli @@ -13,6 +13,20 @@ exception LibraryOutOfSync of string Lazy.t +type automation_cache = NDiscriminationTree.DiscriminationTree.t + +class type g_auto_status = + object + method auto_cache : automation_cache + end + +class auto_status : + object('self) + inherit g_auto_status + method set_auto_cache: automation_cache -> 'self + method set_auto_status: #g_auto_status -> 'self + end + type timestamp class type g_status = @@ -42,40 +56,39 @@ val clear_cache : unit -> unit val time_travel: #status -> unit val decompile: baseuri:NUri.uri -> unit -module type SerializerT = - sig - type status - type obj - val register: - string -> - ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> - ('a -> obj) - val serialize: baseuri:NUri.uri -> obj list -> unit - val require: baseuri:NUri.uri -> status -> status - end - val init: unit -> unit -module Serializer: - sig - include SerializerT with type status = status - val require: baseuri:NUri.uri -> (#status as 'status) -> 'status - end +type obj class type g_dumpable_status = object inherit g_status - method dump: Serializer.obj list + inherit g_auto_status + method dump: obj list end - + class dumpable_status : object ('self) inherit status + inherit auto_status inherit g_dumpable_status - method set_dump: Serializer.obj list -> 'self + method set_dump: obj list -> 'self method set_dumpable_status: #g_dumpable_status -> 'self end +type 'a register_type = + < run: 'status. + 'a -> refresh_uri_in_universe:(NCic.universe -> + NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> + (#dumpable_status as 'status) -> 'status > + +module Serializer: + sig + val register: < run: 'a. string -> 'a register_type -> ('a -> obj) > + val serialize: baseuri:NUri.uri -> obj list -> unit + val require: baseuri:NUri.uri -> (#dumpable_status as 'status) -> 'status + end + (* CSC: only required during old-to-NG phase, to be deleted *) val refresh_uri: NUri.uri -> NUri.uri diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 3ace51014..369ed6b69 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,3 +1,4 @@ +terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi @@ -10,6 +11,7 @@ paramod.cmi: terms.cmi orderings.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi +nCicParamod.cmi: terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 3ace51014..369ed6b69 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,3 +1,4 @@ +terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi @@ -10,6 +11,7 @@ paramod.cmi: terms.cmi orderings.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi +nCicParamod.cmi: terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index f30b906fd..db7e52884 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,3 +1,6 @@ +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index f30b906fd..db7e52884 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,3 +1,6 @@ +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 86ae2b375..7a49c201b 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,3 +1,6 @@ +nCicTacReduction.cmi: +nTacStatus.cmi: +nCicElim.cmi: nTactics.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index 86ae2b375..7a49c201b 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,3 +1,6 @@ +nCicTacReduction.cmi: +nTacStatus.cmi: +nCicElim.cmi: nTactics.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi diff --git a/helm/software/components/registry/.depend b/helm/software/components/registry/.depend index cf4f36b68..40c03891a 100644 --- a/helm/software/components/registry/.depend +++ b/helm/software/components/registry/.depend @@ -1,2 +1,3 @@ +helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/registry/.depend.opt b/helm/software/components/registry/.depend.opt index cf4f36b68..40c03891a 100644 --- a/helm/software/components/registry/.depend.opt +++ b/helm/software/components/registry/.depend.opt @@ -1,2 +1,3 @@ +helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt index c0cd9c906..3d7dfc21f 100644 --- a/helm/software/components/syntax_extensions/.depend.opt +++ b/helm/software/components/syntax_extensions/.depend.opt @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 169fc76b0..d9d6034a1 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,11 +1,19 @@ +proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi +proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi +hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi +universe.cmi: autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: +paramodulation/utils.cmi: +closeCoercionGraph.cmi: +paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -27,10 +35,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi +inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi +fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi +history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index 169fc76b0..d9d6034a1 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -1,11 +1,19 @@ +proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi +proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi +hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi +universe.cmi: autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: +paramodulation/utils.cmi: +closeCoercionGraph.cmi: +paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -27,10 +35,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi +inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi +fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi +history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi diff --git a/helm/software/components/thread/.depend b/helm/software/components/thread/.depend index 7759190c6..6616a03d0 100644 --- a/helm/software/components/thread/.depend +++ b/helm/software/components/thread/.depend @@ -1,3 +1,5 @@ +threadSafe.cmi: +extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/thread/.depend.opt b/helm/software/components/thread/.depend.opt index 7759190c6..6616a03d0 100644 --- a/helm/software/components/thread/.depend.opt +++ b/helm/software/components/thread/.depend.opt @@ -1,3 +1,5 @@ +threadSafe.cmi: +extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend index bc310327f..a8972f4cf 100644 --- a/helm/software/components/tptp_grafite/.depend +++ b/helm/software/components/tptp_grafite/.depend @@ -1,4 +1,7 @@ parser.cmi: ast.cmo +tptp2grafite.cmi: +ast.cmo: +ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmo parser.cmi diff --git a/helm/software/components/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt index c74300207..fb60fe8f2 100644 --- a/helm/software/components/tptp_grafite/.depend.opt +++ b/helm/software/components/tptp_grafite/.depend.opt @@ -1,4 +1,7 @@ parser.cmi: ast.cmx +tptp2grafite.cmi: +ast.cmo: +ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmx parser.cmi diff --git a/helm/software/components/urimanager/.depend b/helm/software/components/urimanager/.depend index 482148423..9cac9aa78 100644 --- a/helm/software/components/urimanager/.depend +++ b/helm/software/components/urimanager/.depend @@ -1,2 +1,3 @@ +uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt index 482148423..9cac9aa78 100644 --- a/helm/software/components/urimanager/.depend.opt +++ b/helm/software/components/urimanager/.depend.opt @@ -1,2 +1,3 @@ +uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/whelp/.depend b/helm/software/components/whelp/.depend index 39f37dfa9..65dc07955 100644 --- a/helm/software/components/whelp/.depend +++ b/helm/software/components/whelp/.depend @@ -1,3 +1,5 @@ +whelp.cmi: +fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt index 39f37dfa9..65dc07955 100644 --- a/helm/software/components/whelp/.depend.opt +++ b/helm/software/components/whelp/.depend.opt @@ -1,3 +1,5 @@ +whelp.cmi: +fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/xml/.depend b/helm/software/components/xml/.depend index 5ef59bdc9..e7e7ffbd7 100644 --- a/helm/software/components/xml/.depend +++ b/helm/software/components/xml/.depend @@ -1,3 +1,5 @@ +xml.cmi: +xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xml/.depend.opt b/helm/software/components/xml/.depend.opt index 5ef59bdc9..e7e7ffbd7 100644 --- a/helm/software/components/xml/.depend.opt +++ b/helm/software/components/xml/.depend.opt @@ -1,3 +1,5 @@ +xml.cmi: +xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xmldiff/.depend b/helm/software/components/xmldiff/.depend index e2832de33..65bd7b949 100644 --- a/helm/software/components/xmldiff/.depend +++ b/helm/software/components/xmldiff/.depend @@ -1,2 +1,3 @@ +xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt index e2832de33..65bd7b949 100644 --- a/helm/software/components/xmldiff/.depend.opt +++ b/helm/software/components/xmldiff/.depend.opt @@ -1,2 +1,3 @@ +xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi