From dcdbb979433a61e2ef2842d96604098728824416 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 15 Jun 2009 11:04:24 +0000 Subject: [PATCH] huge commit regarding the grafite_status: - in the ng_status component it embeds the lexicon status - the lexicon status is not passed around alone anymore - coercions/hints for the ng system are no longer imperative (are in the e (for external) status of the tac_status - ng_refiner does not take in input a look_for_coercions function but an aggregate type "rdb" comprising hints and coercions (and empty one is passed to disable hints/coercions) functionalities losses: - old (generated) hint are no longer translated on the fly - old coercions are translated in a best effort way (no universes calculation) --- .../components/acic_content/.depend.opt | 3 + .../components/acic_procedural/.depend.opt | 7 ++ .../components/binaries/extractor/.depend.opt | 4 + .../binaries/table_creator/.depend.opt | 2 + .../components/binaries/transcript/.depend | 5 + helm/software/components/cic/.depend.opt | 2 + helm/software/components/cic_acic/.depend.opt | 3 + .../components/cic_disambiguation/.depend.opt | 2 + .../components/cic_exportation/.depend.opt | 1 + .../components/cic_proof_checking/.depend.opt | 10 ++ .../components/cic_unification/.depend.opt | 7 ++ .../components/cic_unification/coercGraph.ml | 6 +- .../components/content_pres/.depend.opt | 6 ++ .../components/disambiguation/.depend.opt | 1 + helm/software/components/getter/.depend.opt | 7 ++ .../components/grafite_engine/.depend.opt | 1 + .../grafite_engine/grafiteEngine.ml | 15 +-- .../components/grafite_engine/grafiteSync.ml | 21 ++++- .../components/grafite_engine/grafiteTypes.ml | 49 +++++++++- .../grafite_engine/grafiteTypes.mli | 7 +- .../components/grafite_parser/.depend | 8 ++ .../components/grafite_parser/.depend.opt | 12 ++- .../components/grafite_parser/Makefile | 1 + .../grafite_parser/grafiteDisambiguate.ml | 92 ++++++++++--------- .../grafite_parser/grafiteDisambiguate.mli | 14 +-- .../components/grafite_parser/nEstatus.ml | 18 ++++ .../components/grafite_parser/nEstatus.mli | 18 ++++ helm/software/components/hgdome/.depend.opt | 2 + helm/software/components/hmysql/.depend.opt | 5 + helm/software/components/lexicon/.depend.opt | 2 + helm/software/components/library/.depend.opt | 9 ++ helm/software/components/library/coercDb.ml | 4 +- helm/software/components/library/coercDb.mli | 8 +- .../components/library/librarySync.ml | 2 +- helm/software/components/logger/.depend.opt | 1 + helm/software/components/metadata/.depend.opt | 2 + .../components/ng_disambiguation/.depend.opt | 1 + .../ng_disambiguation/nCicDisambiguate.ml | 30 +++--- .../ng_disambiguation/nCicDisambiguate.mli | 4 +- .../software/components/ng_kernel/.depend.opt | 13 ++- helm/software/components/ng_refiner/.depend | 7 ++ .../components/ng_refiner/.depend.opt | 23 +++-- helm/software/components/ng_refiner/Makefile | 1 + helm/software/components/ng_refiner/check.ml | 10 +- .../components/ng_refiner/nCicCoercion.ml | 10 +- .../components/ng_refiner/nCicCoercion.mli | 4 +- .../components/ng_refiner/nCicRefiner.ml | 85 ++++++++--------- .../components/ng_refiner/nCicRefiner.mli | 20 +--- .../components/ng_refiner/nCicUnifHint.ml | 2 +- .../components/ng_refiner/nCicUnifHint.mli | 2 - .../components/ng_refiner/nCicUnification.ml | 65 ++++++------- .../components/ng_refiner/nCicUnification.mli | 2 +- .../components/ng_refiner/nRstatus.ml | 18 ++++ .../components/ng_refiner/nRstatus.mli | 17 ++++ .../components/ng_tactics/.depend.opt | 3 + helm/software/components/ng_tactics/README | 54 +++++++++++ .../components/ng_tactics/nTacStatus.ml | 20 ++-- .../components/ng_tactics/nTacStatus.mli | 2 +- helm/software/components/registry/.depend.opt | 1 + .../components/syntax_extensions/.depend | 3 + .../components/syntax_extensions/.depend.opt | 3 + helm/software/components/tactics/.depend.opt | 11 +++ .../components/tactics/closeCoercionGraph.ml | 2 +- .../tactics/paramodulation/equality.ml | 1 - helm/software/components/thread/.depend.opt | 2 + .../components/urimanager/.depend.opt | 1 + helm/software/components/whelp/.depend.opt | 2 + helm/software/components/xml/.depend.opt | 2 + helm/software/components/xmldiff/.depend.opt | 1 + helm/software/matita/Makefile | 2 +- helm/software/matita/matita.ml | 8 +- helm/software/matita/matitaEngine.ml | 85 +++++++++-------- helm/software/matita/matitaEngine.mli | 10 +- helm/software/matita/matitaExcPp.ml | 4 +- helm/software/matita/matitaGui.ml | 11 +-- helm/software/matita/matitaScript.ml | 69 +++++++------- helm/software/matita/matitaScript.mli | 4 +- helm/software/matita/matitaWiki.ml | 40 ++++---- helm/software/matita/matitacLib.ml | 23 ++--- helm/software/matita/tests/ng_coercions.ma | 30 ++++++ helm/software/matita/tests/ng_lexiconn.ma | 40 ++++++++ 81 files changed, 751 insertions(+), 354 deletions(-) create mode 100644 helm/software/components/grafite_parser/nEstatus.ml create mode 100644 helm/software/components/grafite_parser/nEstatus.mli create mode 100644 helm/software/components/ng_refiner/nRstatus.ml create mode 100644 helm/software/components/ng_refiner/nRstatus.mli create mode 100644 helm/software/components/ng_tactics/README create mode 100644 helm/software/matita/tests/ng_coercions.ma create mode 100644 helm/software/matita/tests/ng_lexiconn.ma 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.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.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.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/cic/.depend.opt b/helm/software/components/cic/.depend.opt index 3a0f72fd2..f880a0243 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: discrimination_tree.cmi: cic.cmx path_indexing.cmi: cic.cmx cicInspect.cmi: cic.cmx 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.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.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.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.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/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index 61df4ceb5..9dfd6613d 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -136,7 +136,7 @@ let source_of t = ;; let generate_dot_file () = - let l = CoercDb.to_list () in + let l = CoercDb.to_list (CoercDb.dump ()) in let module Pp = GraphvizPp.Dot in let buf = Buffer.create 10240 in let fmt = Format.formatter_of_buffer buf in @@ -263,7 +263,7 @@ let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;; (* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_to carr = - let l = CoercDb.to_list () in + let l = CoercDb.to_list (CoercDb.dump ()) in let splat_coercion_to carr (src,tgt,cl) = if CoercDb.eq_carr tgt carr then Some (splat src cl) else None in @@ -273,7 +273,7 @@ let get_coercions_to carr = (* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_from carr = - let l = CoercDb.to_list () in + let l = CoercDb.to_list (CoercDb.dump ()) in let splat_coercion_from carr (src,tgt,cl) = if CoercDb.eq_carr src carr then Some (splat tgt cl) else None in 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.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/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_engine/.depend.opt b/helm/software/components/grafite_engine/.depend.opt index b0d4b7048..2dca47091 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 grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 6d7632f75..1e777ab83 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -773,7 +773,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (match status.GrafiteTypes.ng_status with | GrafiteTypes.ProofMode { NTacStatus.istatus = - {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } -> + { NTacStatus.pstatus = pstatus; estatus = estatus } } -> let uri,height,menv,subst,obj_kind = pstatus in if menv <> [] then raise @@ -798,7 +798,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status in {status with GrafiteTypes.ng_status = - GrafiteTypes.CommandMode lexicon_status },`New uris + GrafiteTypes.CommandMode estatus },`New uris | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; @@ -809,12 +809,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status NCicEnvironment.add_constraint strict [false,u1] [false,u2]; status, `New [u1;u2] | GrafiteAst.NObj (loc,obj) -> - let lexicon_status = + let estatus = match status.GrafiteTypes.ng_status with | GrafiteTypes.ProofMode _ -> assert false - | GrafiteTypes.CommandMode ls -> ls in - let lexicon_status,obj = - GrafiteDisambiguate.disambiguate_nobj lexicon_status + | GrafiteTypes.CommandMode es -> es + in + let estatus,obj = + GrafiteDisambiguate.disambiguate_nobj estatus ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in let uri,height,nmenv,nsubst,nobj = obj in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in @@ -824,7 +825,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status GrafiteTypes.ProofMode (subst_metasenv_and_fix_names { NTacStatus.gstatus = ninitial_stack; - istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}) + istatus = { NTacStatus.pstatus = obj; estatus = estatus}}) } in (match nmenv with diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 49545e5f4..a773ea401 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -142,10 +142,17 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity let lemmas = LibrarySync.add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri in + let status = { status with GrafiteTypes.coercions = CoercDb.dump () ; - objects = lemmas @ status.GrafiteTypes.objects - }, - lemmas + objects = lemmas @ status.GrafiteTypes.objects; + } + in + let db = + NCicCoercion.index_old_db (CoercDb.dump ()) + (GrafiteTypes.get_coercions status) + in + let status = GrafiteTypes.set_coercions db status in + status, lemmas let prefer_coercion s u = CoercDb.prefer u; @@ -173,8 +180,14 @@ let initial_status lexicon_status baseuri = { coercions = CoercDb.empty_coerc_db; automation_cache = AutomationCache.empty (); baseuri = baseuri; - ng_status = GrafiteTypes.CommandMode lexicon_status; + ng_status = GrafiteTypes.CommandMode { + NEstatus.lstatus = lexicon_status; + NEstatus.rstatus = { + NRstatus.uhint_db = NCicUnifHint.empty_db; + NRstatus.coerc_db = NCicCoercion.empty_db; + }; } +} let init baseuri = diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 66da43c8f..2ee136dfe 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -46,7 +46,7 @@ type proof_status = type ng_status = | ProofMode of NTacStatus.tac_status - | CommandMode of LexiconEngine.status + | CommandMode of NEstatus.extra_status type status = { moo_content_rev: GrafiteMarshal.moo; @@ -58,6 +58,48 @@ type status = { ng_status: ng_status; } +let get_lexicon x = + match x.ng_status with + | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus + | CommandMode e -> e.NEstatus.lstatus +;; + +let set_lexicon new_lexicon_status new_grafite_status = + { new_grafite_status with ng_status = + match new_grafite_status.ng_status with + | CommandMode estatus -> + CommandMode + { estatus with NEstatus.lstatus = new_lexicon_status } + | ProofMode t -> + ProofMode + { t with NTacStatus.istatus = + { t.NTacStatus.istatus with NTacStatus.estatus = + { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus = + new_lexicon_status }}}} +;; + +let set_coercions db new_grafite_status = + { new_grafite_status with ng_status = + match new_grafite_status.ng_status with + | CommandMode estatus -> + CommandMode + { estatus with NEstatus.rstatus = + { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }} + | ProofMode t -> + ProofMode + { t with NTacStatus.istatus = + { t.NTacStatus.istatus with NTacStatus.estatus = + { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus = + { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db + }}}}} +;; + +let get_estatus x = + match x.ng_status with + | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus + | CommandMode e -> e +;; + let get_current_proof status = match status.proof_status with | Incomplete_proof { proof = p } -> p @@ -191,3 +233,8 @@ let dump_status status = List.iter (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects +let get_coercions new_grafite_status = + let e = get_estatus new_grafite_status in + e.NEstatus.rstatus.NRstatus.coerc_db +;; + diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index e75c8aa3c..c874d43f6 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -44,7 +44,7 @@ type proof_status = type ng_status = | ProofMode of NTacStatus.tac_status - | CommandMode of LexiconEngine.status + | CommandMode of NEstatus.extra_status type status = { moo_content_rev: GrafiteMarshal.moo; @@ -73,7 +73,12 @@ val get_proof_metasenv: status -> Cic.metasenv val get_stack: status -> Continuationals.Stack.t val get_proof_context : status -> int -> Cic.context val get_proof_conclusion : status -> int -> Cic.term +val get_lexicon : status -> LexiconEngine.status +val get_estatus : status -> NEstatus.extra_status +val get_coercions: status -> NCicCoercion.db val set_stack: Continuationals.Stack.t -> status -> status val set_metasenv: Cic.metasenv -> status -> status +val set_lexicon : LexiconEngine.status -> status -> status +val set_coercions: NCicCoercion.db -> status -> status diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index 9fb3357e7..e970a6d1c 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -1,10 +1,18 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +nEstatus.cmi: +grafiteDisambiguate.cmi: grafiteWalker.cmi: grafiteParser.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi +nEstatus.cmo: nEstatus.cmi +nEstatus.cmx: nEstatus.cmi grafiteDisambiguate.cmo: grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguate.cmi grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index 9fb3357e7..86bad9e17 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -1,12 +1,20 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +nEstatus.cmi: +grafiteDisambiguate.cmi: nEstatus.cmi grafiteWalker.cmi: grafiteParser.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi -grafiteDisambiguate.cmo: grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguate.cmi +nEstatus.cmo: nEstatus.cmi +nEstatus.cmx: nEstatus.cmi +grafiteDisambiguate.cmo: nEstatus.cmi grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: nEstatus.cmx grafiteDisambiguate.cmi grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi print_grammar.cmo: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/Makefile b/helm/software/components/grafite_parser/Makefile index ef263f3d8..3a4acb3e1 100644 --- a/helm/software/components/grafite_parser/Makefile +++ b/helm/software/components/grafite_parser/Makefile @@ -5,6 +5,7 @@ INTERFACE_FILES = \ dependenciesParser.mli \ grafiteParser.mli \ cicNotation2.mli \ + nEstatus.mli \ grafiteDisambiguate.mli \ grafiteWalker.mli \ print_grammar.mli \ diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 9c12d1173..5002e58ab 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -195,23 +195,24 @@ term = metasenv,(*subst,*) cic ;; -let disambiguate_nterm expty lexicon_status context metasenv subst thing +let disambiguate_nterm expty estatus context metasenv subst thing = let diff, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term - ~coercion_db:(NCicCoercion.db ()) - ~aliases:lexicon_status.LexiconEngine.aliases + ~rdb:estatus.NEstatus.rstatus + ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases ~expty - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) ~lookup_in_library:nlookup_in_library ~mk_choice:ncic_mk_choice ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst thing) in - let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in - metasenv, subst, lexicon_status, cic + let lexicon_status = + LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in + metasenv, subst, { estatus with NEstatus.lstatus = lexicon_status }, cic ;; @@ -619,7 +620,7 @@ let rec disambiguate_tactic | `Proof as t -> metasenv,t in metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) -let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = +let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = let uri = let baseuri = match baseuri with Some x -> x | None -> raise BaseUriNotSetYet @@ -668,7 +669,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let _,g = CicTypeChecker.typecheck uri in CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri)) graph l) - graph (CoercDb.to_list ()) + graph (CoercDb.to_list (CoercDb.dump ())) in ignore(CicUniv.do_rank graph); @@ -687,14 +688,14 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = (try (match NCicDisambiguate.disambiguate_obj + ~rdb:estatus.NEstatus.rstatus ~lookup_in_library:nlookup_in_library ~description_of_alias:LexiconAst.description_of_alias ~mk_choice:ncic_mk_choice ~mk_implicit ~uri:(OCic2NCic.nuri_of_ouri uri) - ~coercion_db:(NCicCoercion.db ()) - ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases + ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) (text,prefix_len,obj) with | [_,_,_,obj],_ -> @@ -727,6 +728,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = (* let time = Unix.gettimeofday () in *) + let lexicon_status = estatus.NEstatus.lstatus in let (diff, metasenv, _, cic, _) = singleton "third" (CicDisambiguate.disambiguate_obj @@ -737,7 +739,8 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri:(Some uri) - (text,prefix_len,obj)) in + (text,prefix_len,obj)) + in (* @@ -749,7 +752,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in - lexicon_status, metasenv, cic + { estatus with NEstatus.lstatus = lexicon_status }, metasenv, cic with | Sys.Break as exn -> raise exn @@ -758,7 +761,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = raise exn ;; -let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) = +let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = let uri = let baseuri = match baseuri with Some x -> x | None -> raise BaseUriNotSetYet @@ -780,19 +783,20 @@ let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) = ~mk_choice:ncic_mk_choice ~mk_implicit ~uri:(OCic2NCic.nuri_of_ouri uri) - ~coercion_db:(NCicCoercion.db ()) - ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~rdb:estatus.NEstatus.rstatus + ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases + ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) (text,prefix_len,obj)) in - let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in - lexicon_status, cic + let lexicon_status = + LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in + { estatus with NEstatus.lstatus = lexicon_status }, cic ;; -let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= +let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= match cmd with - | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj) + | GrafiteAst.NObj(loc,obj) -> estatus, metasenv, GrafiteAst.NObj(loc,obj) | GrafiteAst.Index(loc,key,uri) -> - let lexicon_status_ref = ref lexicon_status in + let lexicon_status_ref = ref estatus.NEstatus.lstatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let disambiguate_term_option metasenv = @@ -803,34 +807,40 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= metasenv, Some t in let metasenv,key = disambiguate_term_option metasenv key in - !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri) + { estatus with NEstatus.lstatus = !lexicon_status_ref }, + metasenv,GrafiteAst.Index(loc,key,uri) | GrafiteAst.Select (loc,uri) -> - lexicon_status, metasenv, GrafiteAst.Select(loc,uri) + estatus, metasenv, GrafiteAst.Select(loc,uri) | GrafiteAst.Pump(loc,i) -> - lexicon_status, metasenv, GrafiteAst.Pump(loc,i) + estatus, metasenv, GrafiteAst.Pump(loc,i) | GrafiteAst.PreferCoercion (loc,t) -> - let lexicon_status_ref = ref lexicon_status in + let lexicon_status_ref = ref estatus.NEstatus.lstatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in - !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t) + { estatus with NEstatus.lstatus = !lexicon_status_ref}, + metasenv, GrafiteAst.PreferCoercion (loc,t) | GrafiteAst.Coercion (loc,t,b,a,s) -> - let lexicon_status_ref = ref lexicon_status in + let lexicon_status_ref = ref estatus.NEstatus.lstatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in - !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) + { estatus with NEstatus.lstatus = !lexicon_status_ref }, + metasenv, GrafiteAst.Coercion (loc,t,b,a,s) | GrafiteAst.Inverter (loc,n,indty,params) -> - let lexicon_status_ref = ref lexicon_status in - let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in - let metasenv,indty = disambiguate_term metasenv indty in - !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params) + let lexicon_status_ref = ref estatus.NEstatus.lstatus in + let disambiguate_term = + disambiguate_term None text prefix_len lexicon_status_ref [] in + let metasenv,indty = disambiguate_term metasenv indty in + { estatus with NEstatus.lstatus = !lexicon_status_ref }, + metasenv, GrafiteAst.Inverter (loc,n,indty,params) | GrafiteAst.UnificationHint (loc, t, n) -> - let lexicon_status_ref = ref lexicon_status in + let lexicon_status_ref = ref estatus.NEstatus.lstatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in - !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n) + { estatus with NEstatus.lstatus = !lexicon_status_ref }, + metasenv, GrafiteAst.UnificationHint (loc,t,n) | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ @@ -839,13 +849,13 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= | GrafiteAst.NQed _ | GrafiteAst.NUnivConstraint _ | GrafiteAst.Set _ as cmd -> - lexicon_status,metasenv,cmd + estatus,metasenv,cmd | GrafiteAst.Obj (loc,obj) -> - let lexicon_status,metasenv,obj = - disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in - lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) + let estatus,metasenv,obj = + disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in + estatus, metasenv, GrafiteAst.Obj (loc,obj) | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> - let lexicon_status_ref = ref lexicon_status in + let lexicon_status_ref = ref estatus.NEstatus.lstatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let disambiguate_term_option metasenv = @@ -860,7 +870,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= let metasenv,refl = disambiguate_term_option metasenv refl in let metasenv,sym = disambiguate_term_option metasenv sym in let metasenv,trans = disambiguate_term_option metasenv trans in - !lexicon_status_ref, metasenv, + { estatus with NEstatus.lstatus = !lexicon_status_ref }, metasenv, GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) let disambiguate_macro diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index f13fc418c..11fcbab1d 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -42,11 +42,11 @@ val disambiguate_tactic: Cic.metasenv * lazy_tactic val disambiguate_command: - LexiconEngine.status -> + NEstatus.extra_status -> ?baseuri:string -> Cic.metasenv -> ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> - LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command + NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command val disambiguate_macro: LexiconEngine.status ref -> @@ -56,15 +56,17 @@ val disambiguate_macro: Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro val disambiguate_nterm : - NCic.term option -> LexiconEngine.status -> + NCic.term option -> + NEstatus.extra_status -> NCic.context -> NCic.metasenv -> NCic.substitution -> CicNotationPt.term Disambiguate.disambiguator_input -> - NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term + NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term val disambiguate_nobj : - LexiconEngine.status -> ?baseuri:string -> + NEstatus.extra_status -> + ?baseuri:string -> (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input -> - LexiconEngine.status * NCic.obj + NEstatus.extra_status * NCic.obj type pattern = CicNotationPt.term Disambiguate.disambiguator_input option * diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml new file mode 100644 index 000000000..a225f439d --- /dev/null +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +type extra_status = { + lstatus : LexiconEngine.status; + rstatus : NRstatus.refiner_status; +} + diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli new file mode 100644 index 000000000..a225f439d --- /dev/null +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +type extra_status = { + lstatus : LexiconEngine.status; + rstatus : NRstatus.refiner_status; +} + 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.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.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.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/library/coercDb.ml b/helm/software/components/library/coercDb.ml index c8be370f2..b7e390229 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/components/library/coercDb.ml @@ -85,8 +85,8 @@ let eq_carr ?(exact=false) src tgt = | _, _ -> false ;; -let to_list () = - List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db +let to_list db = + List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db ;; let rec myfilter p = function diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index 83e61dbfb..59c07f447 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -37,15 +37,15 @@ val string_of_carr: coerc_carr -> string (* takes a term in whnf ~delta:false and a desired ariety *) val coerc_carr_of_term: Cic.term -> int -> coerc_carr -val to_list: - unit -> - (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list - type coerc_db val empty_coerc_db : coerc_db val dump: unit -> coerc_db val restore: coerc_db -> unit +val to_list: + coerc_db -> + (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list + (* src carr, tgt carr, uri, saturations, coerced position * invariant: * if the constant pointed by uri has n argments diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index a0a0f324e..185ae5315 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -338,7 +338,7 @@ and ) ul) - (CoercDb.to_list ()) + (CoercDb.to_list (CoercDb.dump ())) in let cpos = no_args - arity - saturations - 1 in if not add_composites then 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.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_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_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 6e72042e8..108c845c6 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -34,7 +34,7 @@ let rec mk_rels howmany from = ;; let refine_term - metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl= + metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl= assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); @@ -46,12 +46,10 @@ let refine_term (*assert false*) HExtlib.dummy_floc in let metasenv, subst, term, _ = - NCicRefiner.typeof - (NCicUnifHint.db ()) - ~look_for_coercion:( - if use_coercions then - NCicCoercion.look_for_coercion coercion_db - else (fun _ _ _ _ _ -> [])) + NCicRefiner.typeof + { rdb with NRstatus.coerc_db = + if use_coercions then rdb.NRstatus.coerc_db + else NCicCoercion.empty_db } metasenv subst context term expty ~localise in Disambiguate.Ok (term, metasenv, subst, ()) @@ -67,7 +65,7 @@ let refine_term ;; let refine_obj - ~coercion_db metasenv subst context _uri + ~rdb metasenv subst context _uri ~use_coercions obj _ _ugraph ~localization_tbl = assert (metasenv=[]); @@ -81,11 +79,9 @@ let refine_obj try let obj = NCicRefiner.typeof_obj - (NCicUnifHint.db ()) - ~look_for_coercion:( - if use_coercions then - NCicCoercion.look_for_coercion coercion_db - else (fun _ _ _ _ _ -> [])) + { rdb with NRstatus.coerc_db = + if use_coercions then rdb.NRstatus.coerc_db + else NCicCoercion.empty_db } obj ~localise in Disambiguate.Ok (obj, [], [], ()) @@ -607,7 +603,7 @@ let interpretate_obj let disambiguate_term ~context ~metasenv ~subst ~expty ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~coercion_db ~lookup_in_library + ~aliases ~universe ~rdb ~lookup_in_library (text,prefix_len,term) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in @@ -621,7 +617,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None)) - ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term) + ~refine_thing:(refine_term ~rdb) (text,prefix_len,term) ~mk_localization_tbl ~expty ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b @@ -629,7 +625,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~coercion_db ~lookup_in_library ~uri + ~aliases ~universe ~rdb ~lookup_in_library ~uri (text,prefix_len,obj) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in @@ -645,7 +641,7 @@ let disambiguate_obj ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj ~interpretate_thing:(interpretate_obj ~mk_choice) - ~refine_thing:(refine_obj ~coercion_db) + ~refine_thing:(refine_obj ~rdb) (text,prefix_len,obj) ~mk_localization_tbl ~expty:None in diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 6ae8bb036..0eb018b9d 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -21,7 +21,7 @@ val disambiguate_term : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> - coercion_db:NCicCoercion.db -> + rdb:NRstatus.refiner_status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> @@ -40,7 +40,7 @@ val disambiguate_obj : mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'a DisambiguateTypes.Environment.t -> universe:'a list DisambiguateTypes.Environment.t option -> - coercion_db:NCicCoercion.db -> + rdb:NRstatus.refiner_status -> lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> 'a list) -> diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index da9901b80..a6ea216ac 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 @@ -8,7 +9,7 @@ nCicPp.cmi: nReference.cmi nCic.cmx nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicUntrusted.cmi: nCic.cmx +nCicUntrusted.cmi: nUri.cmi nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -49,7 +50,9 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi -nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicReduction.cmi nCic.cmx nCicUntrusted.cmi -nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicReduction.cmx nCic.cmx nCicUntrusted.cmi +nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicTypeChecker.cmi \ + nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \ + nCicUntrusted.cmi +nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicTypeChecker.cmx \ + nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ + nCicUntrusted.cmi diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 11418eb59..ee4b6b3d3 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,3 +1,8 @@ +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicCoercion.cmi: +nCicUnifHint.cmi: +nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi nCicUnification.cmi: nCicUnifHint.cmi nCicRefiner.cmi: nCicUnifHint.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi @@ -8,6 +13,8 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi +nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi +nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index 11418eb59..632748f92 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,5 +1,10 @@ -nCicUnification.cmi: nCicUnifHint.cmi -nCicRefiner.cmi: nCicUnifHint.cmi +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicCoercion.cmi: +nCicUnifHint.cmi: +nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi +nCicUnification.cmi: nRstatus.cmi +nCicRefiner.cmi: nRstatus.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi @@ -8,7 +13,13 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi -nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi -nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi +nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi +nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi +nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ + nCicUnification.cmi +nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ + nCicUnification.cmi +nCicRefiner.cmo: nRstatus.cmi nCicUnification.cmi nCicMetaSubst.cmi \ + nCicCoercion.cmi nCicRefiner.cmi +nCicRefiner.cmx: nRstatus.cmx nCicUnification.cmx nCicMetaSubst.cmx \ + nCicCoercion.cmx nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index 1b2c293bc..1fa79cd1c 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -6,6 +6,7 @@ INTERFACE_FILES = \ nCicMetaSubst.mli \ nCicCoercion.mli \ nCicUnifHint.mli \ + nRstatus.mli \ nCicUnification.mli \ nCicRefiner.mli diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index e039f1129..51f0482a5 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -271,14 +271,16 @@ let _ = prerr_endline ("start: " ^ NUri.string_of_uri u); let bo = curryfy [] bo in (try + let rdb = { + NRstatus.uhint_db = NCicUnifHint.empty_db; + NRstatus.coerc_db = NCicCoercion.empty_db + } in let metasenv, subst, bo, infty = - NCicRefiner.typeof - ~look_for_coercion:(fun _ _ _ _ _ -> []) - NCicUnifHint.empty_db [] [] [] bo None + NCicRefiner.typeof rdb [] [] [] bo None in let metasenv, subst = try - NCicUnification.unify NCicUnifHint.empty_db metasenv subst [] infty ty + NCicUnification.unify rdb metasenv subst [] infty ty with | NCicUnification.Uncertain msg | NCicUnification.UnificationFailure msg diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index a4b10296f..e62d4eed3 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -37,11 +37,12 @@ let index_coercion (db_src,db_tgt) c src tgt arity arg = db_src, db_tgt ;; -let db () = +let index_old_db odb db = List.fold_left (fun db (_,tgt,clist) -> List.fold_left (fun db (uri,_,arg) -> + try let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in let src, tgt = @@ -66,9 +67,12 @@ let db () = NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t); assert false in - index_coercion db c src tgt arity arg) + index_coercion db c src tgt arity arg + with + | NCicEnvironment.BadDependency _ + | NCicTypeChecker.TypeCheckerFailure _ -> db) db clist) - (DB.empty,DB.empty) (CoercDb.to_list ()) + db (CoercDb.to_list odb) ;; let empty_db = (DB.empty,DB.empty) ;; diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index 5e60b7685..73c88005c 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -19,8 +19,8 @@ type db val index_coercion: db -> NCic.term -> NCic.term -> NCic.term -> int -> int -> db - (* gets the old imperative coercion DB *) -val db : unit -> db + (* gets the old imperative coercion DB (list format) *) +val index_old_db: CoercDb.coerc_db -> db -> db val empty_db : db diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 64911e198..0f835961e 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -46,7 +46,7 @@ let exp_implicit metasenv context expty = ;; -let check_allowed_sort_elimination hdb localise r orig = +let check_allowed_sort_elimination rdb localise r orig = let mkapp he arg = match he with | C.Appl l -> C.Appl (l @ [arg]) @@ -64,7 +64,7 @@ let check_allowed_sort_elimination hdb localise r orig = NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type in let metasenv, subst = - try NCicUnification.unify hdb metasenv subst context + try NCicUnification.unify rdb metasenv subst context arity2 (C.Prod (name, so1, meta)) with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf "expected %s, found %s" (* XXX localizzare meglio *) @@ -76,7 +76,7 @@ let check_allowed_sort_elimination hdb localise r orig = | C.Sort _ (* , t ==?== C.Prod _ *) -> let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in let metasenv, subst = - try NCicUnification.unify hdb metasenv subst context + try NCicUnification.unify rdb metasenv subst context arity2 (C.Prod ("_", ind, meta)) with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf "expected %s, found %s" (* XXX localizzare meglio *) @@ -94,9 +94,9 @@ let check_allowed_sort_elimination hdb localise r orig = aux ;; -let rec typeof hdb +let rec typeof rdb ?(localise=fun _ -> Stdpp.dummy_loc) - ~look_for_coercion metasenv subst context term expty + metasenv subst context term expty = let force_ty skip_lambda metasenv subst context orig t infty expty = (*D*)inside 'F'; try let rc = @@ -111,11 +111,11 @@ let rec typeof hdb (NCicPp.ppterm ~metasenv ~subst:[] ~context expty))); try let metasenv, subst = - NCicUnification.unify hdb metasenv subst context infty expty + NCicUnification.unify rdb metasenv subst context infty expty in metasenv, subst, t, expty with exc -> - try_coercions hdb ~look_for_coercion ~localise + try_coercions rdb ~localise metasenv subst context t orig infty expty true exc) | None -> metasenv, subst, t, infty (*D*)in outside(); rc with exc -> outside (); raise exc @@ -168,12 +168,12 @@ let rec typeof hdb | C.Prod (name,(s as orig_s),(t as orig_t)) -> let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in let metasenv, subst, s, s1 = - force_to_sort hdb ~look_for_coercion + force_to_sort rdb metasenv subst context s orig_s localise s1 in let context1 = (name,(C.Decl s))::context in let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in let metasenv, subst, t, s2 = - force_to_sort hdb ~look_for_coercion + force_to_sort rdb metasenv subst context1 t orig_t localise s2 in let metasenv, subst, s, t, ty = sort_of_prod localise metasenv subst @@ -192,12 +192,12 @@ let rec typeof hdb let metasenv, subst, s, ty_s = typeof_aux metasenv subst context None s in let metasenv, subst, s, _ = - force_to_sort hdb ~look_for_coercion + force_to_sort rdb metasenv subst context s orig_s localise ty_s in let (metasenv,subst), exp_ty_t = match exp_s with | Some exp_s -> - (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t + (try NCicUnification.unify rdb metasenv subst context s exp_s,exp_ty_t with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context @@ -217,7 +217,7 @@ let rec typeof hdb let metasenv, subst, ty, ty_ty = typeof_aux metasenv subst context None ty in let metasenv, subst, ty, _ = - force_to_sort hdb ~look_for_coercion + force_to_sort rdb metasenv subst context ty orig_ty localise ty_ty in let metasenv, subst, t, _ = typeof_aux metasenv subst context (Some ty) t in @@ -234,7 +234,7 @@ let rec typeof hdb let metasenv, subst, he, ty_he = typeof_aux metasenv subst context None he in let metasenv, subst, t, ty = - eat_prods hdb ~localise ~look_for_coercion + eat_prods rdb ~localise metasenv subst context orig_he he ty_he args in let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in @@ -272,7 +272,7 @@ let rec typeof hdb let metasenv,metanoouttype,newouttype,metaoutsort = NCicMetaSubst.mk_meta metasenv context `Term in let metasenv,subst = - NCicUnification.unify hdb metasenv subst context outsort metaoutsort in + NCicUnification.unify rdb metasenv subst context outsort metaoutsort in let metasenv = List.filter (function (j,_) -> j <> metanoouttype) metasenv in let subst = @@ -286,7 +286,7 @@ let rec typeof hdb let metasenv, subst, ind, ind_ty = typeof_aux metasenv subst context None ind in let metasenv, subst = - check_allowed_sort_elimination hdb localise r orig_term metasenv subst + check_allowed_sort_elimination rdb localise r orig_term metasenv subst context ind ind_ty outsort in (* let's check if the type of branches are right *) @@ -298,7 +298,7 @@ let rec typeof hdb match expty with | None -> metasenv, subst | Some expty -> - NCicUnification.unify hdb metasenv subst context resty expty + NCicUnification.unify rdb metasenv subst context resty expty in *) let _, metasenv, subst, pl = @@ -334,8 +334,8 @@ let rec typeof hdb in typeof_aux metasenv subst context expty term -and try_coercions hdb - ~localise ~look_for_coercion +and try_coercions rdb + ~localise metasenv subst context t orig_t infty expty perform_unification exc = (* we try with a coercion *) @@ -356,7 +356,7 @@ and try_coercions hdb NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n")); let metasenv, subst = - NCicUnification.unify hdb metasenv subst context meta t + NCicUnification.unify rdb metasenv subst context meta t in pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context @@ -367,7 +367,7 @@ and try_coercions hdb NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n")); let metasenv, subst = if perform_unification then - NCicUnification.unify hdb metasenv subst context newtype expty + NCicUnification.unify rdb metasenv subst context newtype expty else metasenv, subst in metasenv, subst, newterm, newtype @@ -376,11 +376,10 @@ and try_coercions hdb | NCicUnification.Uncertain _ as exc -> first exc tl in first exc - (look_for_coercion metasenv subst context infty expty) + (NCicCoercion.look_for_coercion + rdb.NRstatus.coerc_db metasenv subst context infty expty) -and force_to_sort hdb - ~look_for_coercion metasenv subst context t orig_t localise ty -= +and force_to_sort rdb metasenv subst context t orig_t localise ty = match NCicReduction.whd ~subst context ty with | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> metasenv, subst, t, ty @@ -396,7 +395,7 @@ and force_to_sort hdb metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0)) | C.Sort _ as ty -> metasenv, subst, t, ty | ty -> - try_coercions hdb ~localise ~look_for_coercion metasenv subst context + try_coercions rdb ~localise metasenv subst context t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false (Uncertain (lazy (localise orig_t, "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t @@ -438,8 +437,8 @@ and guess_name subst ctx ty = with NCicUtils.Subst_not_found _ -> aux 'M') | _ -> aux 'H' -and eat_prods hdb - ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args +and eat_prods rdb + ~localise metasenv subst context orig_he he ty_he args = (*D*)inside 'E'; try let rc = let rec aux metasenv subst args_so_far he ty_he = function @@ -448,14 +447,14 @@ and eat_prods hdb match NCicReduction.whd ~subst context ty_he with | C.Prod (_,s,t) -> let metasenv, subst, arg, _ = - typeof hdb ~look_for_coercion ~localise + typeof rdb ~localise metasenv subst context arg (Some s) in let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in aux metasenv subst (arg :: args_so_far) he t tl | C.Meta _ | C.Appl (C.Meta _ :: _) as t -> let metasenv, subst, arg, ty_arg = - typeof hdb ~look_for_coercion ~localise + typeof rdb ~localise metasenv subst context arg None in let name = guess_name subst context ty_arg in let metasenv, _, meta, _ = @@ -465,7 +464,7 @@ and eat_prods hdb let flex_prod = C.Prod (name, ty_arg, meta) in (* next line grants that ty_args is a type *) let metasenv,subst, flex_prod, _ = - typeof hdb ~look_for_coercion ~localise metasenv subst + typeof rdb ~localise metasenv subst context flex_prod None in pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context @@ -473,7 +472,7 @@ and eat_prods hdb NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n")); let metasenv, subst = - try NCicUnification.unify hdb metasenv subst context t flex_prod + try NCicUnification.unify rdb metasenv subst context t flex_prod with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf ("The term %s has an inferred type %s, but is applied to the" ^^ " argument %s of type %s") @@ -494,7 +493,7 @@ and eat_prods hdb (List.length args) (List.length args_so_far)))) | ty -> let metasenv, subst, newhead, newheadty = - try_coercions hdb ~localise ~look_for_coercion metasenv subst context + try_coercions rdb ~localise metasenv subst context (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) false @@ -557,18 +556,16 @@ let undebruijnate inductive ref t rev_fl = ;; -let typeof_obj hdb - ?(localise=fun _ -> Stdpp.dummy_loc) - ~look_for_coercion (uri,height,metasenv,subst,obj) +let typeof_obj + rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj) = prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj)); let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *) let metasenv, subst, ty, sort = - typeof hdb ~localise ~look_for_coercion metasenv subst context ty None + typeof rdb ~localise metasenv subst context ty None in let metasenv, subst, ty, sort = - force_to_sort hdb ~look_for_coercion - metasenv subst context ty orig_ty localise sort + force_to_sort rdb metasenv subst context ty orig_ty localise sort in metasenv, subst, ty, sort in @@ -579,8 +576,7 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj match bo with | Some bo -> let metasenv, subst, bo, ty = - typeof hdb ~localise ~look_for_coercion - metasenv subst [] bo (Some ty) + typeof rdb ~localise metasenv subst [] bo (Some ty) in let height = (* XXX recalculate *) height in metasenv, subst, Some bo, ty, height @@ -604,8 +600,7 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj List.fold_left (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) -> let metasenv, subst, dbo, ty = - typeof hdb ~localise ~look_for_coercion - metasenv subst types dbo (Some ty) + typeof rdb ~localise metasenv subst types dbo (Some ty) in metasenv, subst, (relevance,name,k,ty,dbo)::fl) (metasenv, subst, []) rev_fl @@ -660,17 +655,17 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj match item1,item2 with (n1,C.Decl ty1),(n2,C.Decl ty2) -> if n1 = n2 then - NCicUnification.unify hdb ~test_eq_only:true metasenv + NCicUnification.unify rdb ~test_eq_only:true metasenv subst context ty1 ty2,true else (metasenv,subst),false | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> if n1 = n2 then let metasenv,subst = - NCicUnification.unify hdb ~test_eq_only:true metasenv + NCicUnification.unify rdb ~test_eq_only:true metasenv subst context ty1 ty2 in - NCicUnification.unify hdb ~test_eq_only:true metasenv + NCicUnification.unify rdb ~test_eq_only:true metasenv subst context bo1 bo2,true else (metasenv,subst),false diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index d43a09f20..b601db963 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -16,31 +16,15 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;; exception AssertFailure of string Lazy.t;; val typeof : - NCicUnifHint.db -> + NRstatus.refiner_status -> ?localise:(NCic.term -> Stdpp.location) -> - look_for_coercion:( - NCic.metasenv -> NCic.substitution -> NCic.context -> - (* inferred type, expected type *) - NCic.term -> NCic.term -> - (* enriched metasenv, new term, its type, metavriable to - * be unified with the old term *) - (NCic.metasenv * NCic.term * NCic.term * NCic.term) list - ) -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term option -> (* term, expected type *) NCic.metasenv * NCic.substitution * NCic.term * NCic.term (* menv, subst,refined term, type *) val typeof_obj : - NCicUnifHint.db -> + NRstatus.refiner_status -> ?localise:(NCic.term -> Stdpp.location) -> - look_for_coercion:( - NCic.metasenv -> NCic.substitution -> NCic.context -> - (* inferred type, expected type *) - NCic.term -> NCic.term -> - (* enriched metasenv, new term, its type, metavriable to - * be unified with the old term *) - (NCic.metasenv * NCic.term * NCic.term * NCic.term) list - ) -> NCic.obj -> NCic.obj diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index b7d2b67d7..9bd934c3b 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -137,7 +137,7 @@ let db () = if List.length l > 1 then combine mk_hint l else []) - [] (CoercDb.to_list ()) + [] (CoercDb.to_list (CoercDb.dump ())) in List.fold_left (fun db -> function diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 49df40bf9..7582c3df6 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -16,8 +16,6 @@ type db val index_hint: db -> NCic.context -> NCic.term -> NCic.term -> int -> db - (* gets the old imperative coercion DB *) -val db : unit -> db val add_user_provided_hint : Cic.term -> int -> unit val empty_db : db diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 59bc5d7e7..9ee056aed 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -134,13 +134,13 @@ let rec lambda_intros metasenv subst context t args = in mk_lambda context 0 argsty -and instantiate hdb test_eq_only metasenv subst context n lc t swap = +and instantiate rdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = pp (lazy(string_of_int n ^ " :=?= "^ NCicPp.ppterm ~metasenv ~subst ~context t)); let unify test_eq_only m s c t1 t2 = - if swap then unify hdb test_eq_only m s c t2 t1 - else unify hdb test_eq_only m s c t1 t2 + if swap then unify rdb test_eq_only m s c t2 t1 + else unify rdb test_eq_only m s c t1 t2 in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in let metasenv, subst, t = @@ -234,7 +234,7 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap = metasenv, subst (*D*) in outside(); rc with exn -> outside (); raise exn -and unify hdb test_eq_only metasenv subst context t1 t2 = +and unify rdb test_eq_only metasenv subst context t1 t2 = (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst t1 t2 = (*D*) inside 'F'; try let rc = @@ -261,13 +261,13 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let metasenv, subst = unify hdb true metasenv subst context s1 s2 in - unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 + let metasenv, subst = unify rdb true metasenv subst context s1 s2 in + unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in - let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in + let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 in + let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 in let context = (name1, C.Def (s1,ty1))::context in - unify hdb test_eq_only metasenv subst context t1 t2 + unify rdb test_eq_only metasenv subst context t1 t2 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> (try @@ -278,7 +278,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = (fun t1 t2 (metasenv, subst, to_restrict, i) -> try let metasenv, subst = - unify hdb test_eq_only metasenv subst context + unify rdb test_eq_only metasenv subst context (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) in metasenv, subst, to_restrict, i-1 @@ -299,7 +299,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let _,_,term,_ = NCicUtils.lookup_subst n1 subst in let term1 = NCicSubstitution.subst_meta lc1 term in let term2 = NCicSubstitution.subst_meta lc2 term in - unify hdb test_eq_only metasenv subst context term1 term2 + unify rdb test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) | _, NCic.Meta (n, _) when is_locked n subst -> @@ -311,7 +311,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let metasenv, lambda_Mj = lambda_intros metasenv subst context t1 args in - unify hdb test_eq_only metasenv subst context + unify rdb test_eq_only metasenv subst context (C.Meta (i,l)) lambda_Mj, i | NCic.Meta (i,_) -> (metasenv, subst), i @@ -322,7 +322,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false in let metasenv, subst = - instantiate hdb test_eq_only metasenv subst context j lj t2 true + instantiate rdb test_eq_only metasenv subst context j lj t2 true in (try let name, ctx, term, ty = NCicUtils.lookup_subst i subst in @@ -335,30 +335,30 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - unify hdb test_eq_only metasenv subst context term t + unify rdb test_eq_only metasenv subst context term t with NCicUtils.Subst_not_found _-> - instantiate hdb test_eq_only metasenv subst context n lc + instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) false) | t, C.Meta (n,lc) -> (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - unify hdb test_eq_only metasenv subst context t term + unify rdb test_eq_only metasenv subst context t term with NCicUtils.Subst_not_found _-> - instantiate hdb test_eq_only metasenv subst context n lc + instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) true) | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - unify hdb test_eq_only metasenv subst context + unify rdb test_eq_only metasenv subst context (mk_appl ~upto:(List.length args) term args) t2 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - unify hdb test_eq_only metasenv subst context t1 + unify rdb test_eq_only metasenv subst context t1 (mk_appl ~upto:(List.length args) term args) | NCic.Appl (NCic.Meta (i,_)::_ as l1), @@ -366,7 +366,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = (try List.fold_left2 (fun (metasenv, subst) t1 t2 -> - unify hdb test_eq_only metasenv subst context t1 t2) + unify rdb test_eq_only metasenv subst context t1 t2) (metasenv,subst) l1 l2 with Invalid_argument _ -> raise (fail_exc metasenv subst context t1 t2)) @@ -379,11 +379,11 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = lambda_intros metasenv subst context t1 args in let metasenv, subst = - unify hdb test_eq_only metasenv subst context + unify rdb test_eq_only metasenv subst context (C.Meta (i,l)) lambda_Mj in let metasenv, subst = - unify hdb test_eq_only metasenv subst context t1 t2 + unify rdb test_eq_only metasenv subst context t1 t2 in (try let name, ctx, term, ty = NCicUtils.lookup_subst i subst in @@ -398,11 +398,11 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = lambda_intros metasenv subst context t2 args in let metasenv, subst = - unify hdb test_eq_only metasenv subst context + unify rdb test_eq_only metasenv subst context lambda_Mj (C.Meta (i,l)) in let metasenv, subst = - unify hdb test_eq_only metasenv subst context t1 t2 + unify rdb test_eq_only metasenv subst context t1 t2 in (try let name, ctx, term, ty = NCicUtils.lookup_subst i subst in @@ -431,7 +431,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let b, relevance = match relevance with b::tl -> b,tl | _ -> true, [] in let metasenv, subst = - try unify hdb test_eq_only metasenv subst context t1 t2 + try unify rdb test_eq_only metasenv subst context t1 t2 with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in @@ -463,16 +463,16 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = raise (uncert_exc metasenv subst context t1 t2) else let metasenv, subst = - unify hdb test_eq_only metasenv subst context outtype1 outtype2 in + unify rdb test_eq_only metasenv subst context outtype1 outtype2 in let metasenv, subst = - try unify hdb test_eq_only metasenv subst context term1 term2 + try unify rdb test_eq_only metasenv subst context term1 term2 with UnificationFailure _ | Uncertain _ when is_prop -> metasenv, subst in (try List.fold_left2 (fun (metasenv,subst) -> - unify hdb test_eq_only metasenv subst context) + unify rdb test_eq_only metasenv subst context) (metasenv, subst) pl1 pl2 with Invalid_argument _ -> raise (uncert_exc metasenv subst context t1 t2)) @@ -490,7 +490,8 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = NCicPp.ppterm ~metasenv ~subst ~context t2); *) let candidates = - NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2 + NCicUnifHint.look_for_hint + rdb.NRstatus.uhint_db metasenv subst context t1 t2 in let rec cand_iter = function | [] -> None (* raise exc *) @@ -514,7 +515,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let metasenv,subst = List.fold_left (fun (metasenv, subst) (x,y) -> - unify hdb test_eq_only metasenv subst context x y) + unify rdb test_eq_only metasenv subst context x y) (metasenv, subst) premises in Some (metasenv, subst) @@ -615,6 +616,6 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify hdb ?(test_eq_only=false) = +let unify rdb ?(test_eq_only=false) = indent := ""; - unify hdb test_eq_only;; + unify rdb test_eq_only;; diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index a2d6c7d78..23728e4f8 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -16,7 +16,7 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; val unify : - NCicUnifHint.db -> + NRstatus.refiner_status -> ?test_eq_only:bool -> (* default: false *) NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml new file mode 100644 index 000000000..02eee9837 --- /dev/null +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) + +type refiner_status = { + coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; +} + diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli new file mode 100644 index 000000000..46634a679 --- /dev/null +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -0,0 +1,17 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) + +type refiner_status = { + coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; +} diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index 3ce24c446..636e38f58 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,4 +1,7 @@ +nCicTacReduction.cmi: +nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi +nCicElim.cmi: nCicTacReduction.cmo: nCicTacReduction.cmi nCicTacReduction.cmx: nCicTacReduction.cmi nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi diff --git a/helm/software/components/ng_tactics/README b/helm/software/components/ng_tactics/README new file mode 100644 index 000000000..af7ba92be --- /dev/null +++ b/helm/software/components/ng_tactics/README @@ -0,0 +1,54 @@ ++letin: basta la refine fatta con occurcheck ++cut: letin; clearbody ~-1 (cosa sia ~-1 è da capirsi) + +-generalize: + a) verificare che tutti i termini selezionati siano convertibili + b) spostare i termini selezionati nel contesto corrente/spostare il + termine bucato sotto un lambda + c) bucare e liftare deve essere fatto contemporaneamente + d) poi usare tatticali per fare cut + apply + +=fail: +=id: + +apply: +applyS: +intros: +elim: +cases: +rewrite: +??replace: rewrite (?:A=B); [2: apply eq_a_b ] +=auto/demodulate/solve_rewrite: +change: +clear/clearbody: +destruct: +inversion: +lapply: +??compose: +whd/simpl/normalize: +fold: +unfold: + +assumption: +constructor: +exists: +left: +right: +reflexivity: +symmetry: +transitivity: +split: + +decompose: + +##### +absurd: +contradiction: +exact: +elim_type: +fourier: +ring: + +#### +applyP: +fwd_simpl: diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index a2847a410..6aaf4a4a8 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -16,7 +16,7 @@ let fail msg = raise (Error msg) type lowtac_status = { pstatus : NCic.obj; - lstatus : LexiconEngine.status + estatus : NEstatus.extra_status; } type lowtactic = lowtac_status -> int -> lowtac_status @@ -80,11 +80,11 @@ let relocate status destination (name,source,t as orig) = (List.rev destination, List.rev source) in let lc = (0,NCic.Ctx (List.rev lc)) in - let db = NCicUnifHint.db () in (* XXX fixme *) let (metasenv, subst), t = NCicMetaSubst.delift ~unify:(fun m s c t1 t2 -> - try Some (NCicUnification.unify db m s c t1 t2) + try Some (NCicUnification.unify + status.estatus.NEstatus.rstatus m s c t1 t2) with | NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) @@ -113,12 +113,12 @@ let disambiguate status t ty context = let status, (_,_,x) = relocate status context ty in status, Some x in let uri,height,metasenv,subst,obj = status.pstatus in - let metasenv, subst, lexicon_status, t = + let metasenv, subst, estatus, t = GrafiteDisambiguate.disambiguate_nterm expty - status.lstatus context metasenv subst t + status.estatus context metasenv subst t in let new_pstatus = uri,height,metasenv,subst,obj in - { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) + { estatus = estatus; pstatus = new_pstatus }, (None, context, t) ;; let typeof status ctx t = @@ -147,7 +147,7 @@ let unify status ctx a b = let status, (_,_,b) = relocate status ctx b in let n,h,metasenv,subst,o = status.pstatus in let metasenv, subst = - NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx a b + NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b in { status with pstatus = n,h,metasenv,subst,o } ;; @@ -160,11 +160,9 @@ let refine status ctx term expty = let status, (n,_, e) = relocate status ctx e in status, n, Some e in let name,height,metasenv,subst,obj = status.pstatus in - let db = NCicUnifHint.db () in (* XXX fixme *) - let coercion_db = NCicCoercion.db () in - let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in + let rdb = status.estatus.NEstatus.rstatus in let metasenv, subst, t, ty = - NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term expty + NCicRefiner.typeof rdb metasenv subst ctx term expty in { status with pstatus = name,height,metasenv,subst,obj }, (nt,ctx,t), (ne,ctx,ty) diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index c04df8d37..cf94862eb 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -16,7 +16,7 @@ val fail: string lazy_t -> 'a type lowtac_status = { pstatus : NCic.obj; - lstatus : LexiconEngine.status + estatus : NEstatus.extra_status; } type lowtactic = lowtac_status -> int -> lowtac_status 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.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/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 2c67c95ee..64df14a42 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -476,7 +476,7 @@ let number_if_already_defined buri name l = *) let close_coercion_graph src tgt uri saturations baseuri = (* check if the coercion already exists *) - let coercions = CoercDb.to_list () in + let coercions = CoercDb.to_list (CoercDb.dump ()) in let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in debug_print (lazy("composed " ^ string_of_int (List.length todo_list))); let todo_list = filter_duplicates todo_list coercions in diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index cb12f7a77..2bf3600f2 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -716,7 +716,6 @@ let topological_sort bag l = rc ;; - (* returns the list of ids that should be factorized *) let get_duplicate_step_in_wfo bag l p = let ol = List.rev l in 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/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.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.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.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 diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index e822326d4..d8d81bf37 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -11,7 +11,7 @@ else ANNOTOPTION = endif -OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) +OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 9aa1fb2f1..658a3ad38 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -90,8 +90,8 @@ let _ = `NRef (NReference.reference_of_string uri) in (MatitaMathView.cicBrowser ())#load uri)); - let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in - let sequents_observer _ grafite_status = + let browser_observer _ = MatitaMathView.refresh_all_browsers () in + let sequents_observer grafite_status = sequents_viewer#reset; match grafite_status.proof_status with | Incomplete_proof ({ stack = stack } as incomplete_proof) -> @@ -140,7 +140,7 @@ let _ = ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ()) in addDebugItem "dump aliases" (fun _ -> - let status = script#lexicon_status in + let status = GrafiteTypes.get_lexicon script#grafite_status in LexiconEngine.dump_aliases HLog.debug "" status); (* FG: DEBUGGING addDebugItem "dump interpretations" (fun _ -> @@ -301,7 +301,7 @@ let _ = "(" ^ string_of_int saturations ^ ")") ul)) ^ ":" ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t)) - (CoercDb.to_list ())); + (CoercDb.to_list (CoercDb.dump ()))); addDebugSeparator (); let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in (* addDebugItem "save (sequent) MathML to matita.xml" diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index a8dcf9809..e3040f8b3 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -40,13 +40,14 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t in GrafiteTypes.set_metasenv metasenv grafite_status,tac -let disambiguate_command lexicon_status_ref grafite_status cmd = +let disambiguate_command estatus lexicon_status_ref grafite_status cmd = let baseuri = GrafiteTypes.get_baseuri grafite_status in - let lexicon_status,metasenv,cmd = + let estatus,metasenv,cmd = GrafiteDisambiguate.disambiguate_command ~baseuri - !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd + { estatus with NEstatus.lstatus = !lexicon_status_ref } + (GrafiteTypes.get_proof_metasenv grafite_status) cmd in - lexicon_status_ref := lexicon_status; + lexicon_status_ref := estatus.NEstatus.lstatus; GrafiteTypes.set_metasenv metasenv grafite_status,cmd let disambiguate_macro lexicon_status_ref grafite_status macro context = @@ -58,24 +59,13 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = in GrafiteTypes.set_metasenv metasenv grafite_status,macro -let eval_ast ?do_heavy_checks lexicon_status - grafite_status (text,prefix_len,ast) -= +let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = + let lexicon_status = GrafiteTypes.get_lexicon grafite_status in let dump = not (Helm_registry.get_bool "matita.moo") in let lexicon_status_ref = ref lexicon_status in let baseuri = GrafiteTypes.get_baseuri grafite_status in let changed_lexicon = ref false in let wrap f x = changed_lexicon := true; f x in - let grafite_status = - match grafite_status.GrafiteTypes.ng_status with - | GrafiteTypes.CommandMode _ -> - { grafite_status with GrafiteTypes.ng_status = - GrafiteTypes.CommandMode lexicon_status } - | GrafiteTypes.ProofMode s -> - { grafite_status with GrafiteTypes.ng_status = - GrafiteTypes.ProofMode - { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus = lexicon_status }}} - in let new_grafite_status,new_objs = match ast with | G.Executable (_, G.Command (_, G.Coercion _)) when dump -> @@ -85,17 +75,17 @@ let eval_ast ?do_heavy_checks lexicon_status | ast -> GrafiteEngine.eval_ast ~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref)) - ~disambiguate_command:(wrap (disambiguate_command lexicon_status_ref)) + ~disambiguate_command:(wrap + (disambiguate_command + (GrafiteTypes.get_estatus grafite_status) lexicon_status_ref)) ~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref)) ?do_heavy_checks grafite_status (text,prefix_len,ast) in let new_lexicon_status = if !changed_lexicon then !lexicon_status_ref - else - match new_grafite_status.GrafiteTypes.ng_status with - | GrafiteTypes.CommandMode l -> l - | GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus + else + GrafiteTypes.get_lexicon new_grafite_status in let new_lexicon_status = LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in @@ -128,46 +118,55 @@ let eval_ast ?do_heavy_checks lexicon_status let new_lexicon_status = LexiconEngine.set_proof_aliases lexicon_status [k,value] in - new_lexicon_status, - ((grafite_status,new_lexicon_status),Some (k,value))::acc + let grafite_status = + GrafiteTypes.set_lexicon new_lexicon_status grafite_status + in + new_lexicon_status, (grafite_status ,Some (k,value))::acc ) (lexicon_status,[]) new_aliases in - ((new_grafite_status,new_lexicon_status),None)::intermediate_states + let new_grafite_status = + GrafiteTypes.set_lexicon new_lexicon_status new_grafite_status + in + ((new_grafite_status),None)::intermediate_states +;; exception TryingToAdd of string -exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status +exception EnrichedWithStatus of exn * GrafiteTypes.status let eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks ?(enforce_no_new_aliases=true) - ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb + ?(watch_statuses=fun _ -> ()) grafite_status str cb = let matita_debug = Helm_registry.get_bool "matita.debug" in - let rec loop lexicon_status grafite_status statuses = + let rec loop grafite_status statuses = let loop = - if first_statement_only then fun _ _ statuses -> statuses + if first_statement_only then fun _ statuses -> statuses else loop in - let stop,l,g,s = + let stop,g,s = try let cont = try + let lexicon_status = GrafiteTypes.get_lexicon grafite_status in Some (GrafiteParser.parse_statement ~include_paths str lexicon_status) with End_of_file -> None in match cont with - | None -> true, lexicon_status, grafite_status, statuses + | None -> true, grafite_status, statuses | Some (lexicon_status,ast) -> + let grafite_status = + GrafiteTypes.set_lexicon lexicon_status grafite_status + in (match ast with GrafiteParser.LNone _ -> - watch_statuses lexicon_status grafite_status ; - false, lexicon_status, grafite_status, - (((grafite_status,lexicon_status),None)::statuses) + watch_statuses grafite_status ; + false, grafite_status, + (((grafite_status),None)::statuses) | GrafiteParser.LSome ast -> cb grafite_status ast; - let new_statuses = - eval_ast ?do_heavy_checks lexicon_status - grafite_status ("",0,ast) in + let new_statuses = + eval_ast ?do_heavy_checks grafite_status ("",0,ast) in if enforce_no_new_aliases then List.iter (fun (_,alias) -> @@ -176,17 +175,17 @@ let eval_from_stream ~first_statement_only ~include_paths | Some (k,value) -> let newtxt = LexiconAstPp.pp_alias value in raise (TryingToAdd newtxt)) new_statuses; - let grafite_status,lexicon_status = + let grafite_status = match new_statuses with [] -> assert false | (s,_)::_ -> s in - watch_statuses lexicon_status grafite_status ; - false, lexicon_status, grafite_status, (new_statuses @ statuses)) + watch_statuses grafite_status ; + false, grafite_status, (new_statuses @ statuses)) with exn when not matita_debug -> - raise (EnrichedWithStatus (exn, lexicon_status, grafite_status)) + raise (EnrichedWithStatus (exn, grafite_status)) in - if stop then s else loop l g s + if stop then s else loop g s in - loop lexicon_status grafite_status [] + loop grafite_status [] ;; diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index d5dcddd61..92b2d8e1c 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -25,20 +25,19 @@ val eval_ast : ?do_heavy_checks:bool -> - LexiconEngine.status -> GrafiteTypes.status -> string * int * ((CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement) -> - ((GrafiteTypes.status * LexiconEngine.status) * + (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) -exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status +exception EnrichedWithStatus of exn * GrafiteTypes.status (* should be used only by the compiler since it looses the * disambiguation_context (text,prefix_len,_) *) @@ -47,13 +46,12 @@ val eval_from_stream : include_paths:string list -> ?do_heavy_checks:bool -> ?enforce_no_new_aliases:bool -> (* default true *) - ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) -> - LexiconEngine.status -> + ?watch_statuses:(GrafiteTypes.status -> unit) -> GrafiteTypes.status -> Ulexing.lexbuf -> (GrafiteTypes.status -> (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement -> unit) -> - ((GrafiteTypes.status * LexiconEngine.status) * + (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index d728fb0b3..a2da0c3e0 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -150,6 +150,8 @@ let rec to_string = None, "NTypeChecker failure: " ^ Lazy.force msg | NCicTypeChecker.AssertFailure msg -> None, "NTypeChecker assert failure: " ^ Lazy.force msg + | NCicEnvironment.ObjectNotFound msg -> + None, "NCicEnvironment object not found: " ^ Lazy.force msg | NCicRefiner.AssertFailure msg -> None, "NRefiner assert failure: " ^ Lazy.force msg | NCicEnvironment.BadDependency (msg,e) -> @@ -165,7 +167,7 @@ let rec to_string = None, "Already defined: " ^ UriManager.string_of_uri s | DisambiguateChoices.Choice_not_found msg -> None, ("Disambiguation choice not found: " ^ Lazy.force msg) - | MatitaEngine.EnrichedWithStatus (exn,_,_) -> + | MatitaEngine.EnrichedWithStatus (exn,_) -> None, "EnrichedWithStatus "^snd(to_string exn) | NTacStatus.Error msg -> None, "NTactic error: " ^ Lazy.force msg diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 3df591bf8..d701a50ae 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -69,7 +69,7 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri grafite_status = LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status] -let save_moo lexicon_status grafite_status = +let save_moo grafite_status = let script = MatitaScript.current () in let baseuri = GrafiteTypes.get_baseuri grafite_status in let no_pstatus = @@ -88,7 +88,7 @@ let save_moo lexicon_status grafite_status = GrafiteMarshal.save_moo moo_fname grafite_status.GrafiteTypes.moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname - lexicon_status.LexiconEngine.lexicon_content_rev + (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev | _ -> clean_current_baseuri grafite_status ;; @@ -913,14 +913,13 @@ class gui () = else saveAsScript () in let abandon_script () = - let lexicon_status = (s ())#lexicon_status in let grafite_status = (s ())#grafite_status in if source_view#buffer#modified then (match ask_unsaved main#toplevel with | `YES -> saveScript () | `NO -> () | `CANCEL -> raise MatitaTypes.Cancel); - save_moo lexicon_status grafite_status + save_moo grafite_status in let loadScript () = let script = s () in @@ -969,12 +968,12 @@ class gui () = match ask_unsaved main#toplevel with | `YES -> saveScript (); - save_moo script#lexicon_status script#grafite_status; + save_moo script#grafite_status; GMain.Main.quit () | `NO -> GMain.Main.quit () | `CANCEL -> () else - (save_moo script#lexicon_status script#grafite_status; + (save_moo script#grafite_status; GMain.Main.quit ())); connect_button main#scriptAdvanceButton advance; connect_button main#scriptRetractButton retract; diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index b221919d2..05dad0572 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -71,7 +71,7 @@ type guistuff = { ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } -let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal +let eval_with_engine include_paths guistuff grafite_status user_goal skipped_txt nonskipped_txt st = let module TAPp = GrafiteAstPp in @@ -84,7 +84,7 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g let enriched_history_fragment = MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") - lexicon_status grafite_status (text,prefix_len,st) + grafite_status (text,prefix_len,st) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) @@ -368,7 +368,7 @@ let cic2grafite context menv t = stupid_indenter script ;; -let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac = +let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in let module MDB = LibraryDb in @@ -449,7 +449,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let loc = HExtlib.floc_of_loc (0,text_len) in let statement = `Ast (GrafiteParser.LSome (ast loc),text) in let res,_,_parsed_text_len = - eval_statement include_paths buffer guistuff lexicon_status + eval_statement include_paths buffer guistuff grafite_status user_goal script statement in (* we need to replace all the parsed_text *) @@ -485,7 +485,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status in let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [({grafite_status with proof_status = No_proof},lexicon_status), parsed_text ],"", + [({grafite_status with proof_status = No_proof}), parsed_text ],"", parsed_text_length | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in @@ -578,7 +578,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff -lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt +grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = let module TAPp = GrafiteAstPp in @@ -589,7 +589,7 @@ script ex loc ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; eval_with_engine include_paths - guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt + guistuff grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 @@ -599,10 +599,10 @@ script ex loc None -> [] | Some n -> GrafiteTypes.get_proof_context grafite_status n in let grafite_status,macro = lazy_macro context in - eval_macro include_paths buffer guistuff lexicon_status grafite_status + eval_macro include_paths buffer guistuff grafite_status user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro -and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status +and eval_statement include_paths (buffer : GText.buffer) guistuff grafite_status user_goal script statement = let (lexicon_status,st), unparsed_text = @@ -611,11 +611,13 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let ast = wrap_with_make include_paths - (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status + (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) + (GrafiteTypes.get_lexicon grafite_status) in ast, text - | `Ast (st, text) -> (lexicon_status, st), text + | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text in + let grafite_status = GrafiteTypes.set_lexicon lexicon_status grafite_status in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in let start, stop = HExtlib.loc_of_floc floc in @@ -628,7 +630,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status match st with | GrafiteParser.LNone loc -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in - [(grafite_status,lexicon_status),parsed_text],"", + [grafite_status,parsed_text],"", parsed_text_length | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in @@ -636,7 +638,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status let s = String.sub unparsed_text parsed_text_length remain_len in let s,text,len = try - eval_statement include_paths buffer guistuff lexicon_status + eval_statement include_paths buffer guistuff grafite_status user_goal script (`Raw s) with HExtlib.Localized (floc, exn) -> @@ -656,7 +658,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in - eval_executable include_paths buffer guistuff lexicon_status + eval_executable include_paths buffer guistuff grafite_status user_goal unparsed_text skipped nonskipped script ex loc let fresh_script_id = @@ -677,7 +679,7 @@ let initial_statuses baseuri = BuildTimeConf.core_notation_script in let grafite_status = GrafiteSync.init lexicon_status baseuri in - grafite_status,lexicon_status + grafite_status in let read_include_paths file = try @@ -766,8 +768,7 @@ object (self) (* history can't be empty, the invariant above grant that it contains at * least the init grafite_status *) - method grafite_status = match history with (s,_)::_ -> s | _ -> assert false - method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false + method grafite_status = match history with s::_ -> s | _ -> assert false method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in @@ -775,7 +776,7 @@ object (self) HLog.debug ("evaluating: " ^ first_line s ^ " ..."); let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff self#lexicon_status + eval_statement self#include_paths buffer guistuff self#grafite_status userGoal self (`Raw s) with End_of_file -> raise Margin in @@ -808,13 +809,15 @@ object (self) with Failure _ -> None) | _ -> userGoal <- None - method private _retract offset lexicon_status grafite_status new_statements + method private _retract offset grafite_status new_statements new_history = - let cur_grafite_status,cur_lexicon_status = + let cur_grafite_status = match history with s::_ -> s | [] -> assert false in - LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status; + LexiconSync.time_travel + ~present:(GrafiteTypes.get_lexicon cur_grafite_status) + ~past:(GrafiteTypes.get_lexicon grafite_status); GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; statements <- new_statements; history <- new_history; @@ -832,7 +835,7 @@ object (self) method retract () = try - let cmp,new_statements,new_history,(grafite_status,lexicon_status) = + let cmp,new_statements,new_history,grafite_status = match statements,history with stat::statements, _::(status::_ as history) -> assert (Glib.Utf8.validate stat); @@ -840,7 +843,7 @@ object (self) | [],[_] -> raise Margin | _,_ -> assert false in - self#_retract cmp lexicon_status grafite_status new_statements + self#_retract cmp grafite_status new_statements new_history; self#notify with @@ -917,13 +920,12 @@ object (self) val mutable observers = [] - method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) = + method addObserver (o: GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = - let lexicon_status = self#lexicon_status in let grafite_status = self#grafite_status in - List.iter (fun o -> o lexicon_status grafite_status) observers + List.iter (fun o -> o grafite_status) observers method loadFromString s = buffer#set_text s; @@ -972,17 +974,19 @@ object (self) end method private goto_top = - let grafite_status,lexicon_status = + let grafite_status = let rec last x = function | [] -> x | hd::tl -> last hd tl in - last (self#grafite_status,self#lexicon_status) history + last (self#grafite_status) history in (* FIXME: this is not correct since there is no undo for * library_objects.set_default... *) GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status; - LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status + LexiconSync.time_travel + ~present:(GrafiteTypes.get_lexicon self#grafite_status) + ~past:(GrafiteTypes.get_lexicon grafite_status) method private reset_buffer = statements <- []; @@ -1063,9 +1067,9 @@ object (self) in let rec back_until_cursor len = (* go backward until locked < cursor *) function - statements, ((grafite_status,lexicon_status)::_ as history) + statements, ((grafite_status)::_ as history) when len <= 0 -> - self#_retract (icmp - len) lexicon_status grafite_status statements + self#_retract (icmp - len) grafite_status statements history | statement::tl1, _::tl2 -> back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2) @@ -1137,7 +1141,8 @@ object (self) | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in try - is_there_only_comments self#lexicon_status self#getFuture + is_there_only_comments + (GrafiteTypes.get_lexicon self#grafite_status) self#getFuture with | LexiconEngine.IncludedFileNotCompiled _ | HExtlib.Localized _ diff --git a/helm/software/matita/matitaScript.mli b/helm/software/matita/matitaScript.mli index 304818f7b..a07735333 100644 --- a/helm/software/matita/matitaScript.mli +++ b/helm/software/matita/matitaScript.mli @@ -34,13 +34,11 @@ object method error_tag : GText.tag (** @return current status *) - method lexicon_status: LexiconEngine.status method grafite_status: GrafiteTypes.status (** {2 Observers} *) - method addObserver : - (LexiconEngine.status -> GrafiteTypes.status -> unit) -> unit + method addObserver : (GrafiteTypes.status -> unit) -> unit (** {2 History} *) diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 0fa8554ba..1f880575e 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -35,21 +35,19 @@ exception AttemptToInsertAnAlias (** {2 Initialization} *) let grafite_status = (ref [] : GrafiteTypes.status list ref) -let lexicon_status = (ref [] : LexiconEngine.status list ref) let run_script is eval_function = - let lexicon_status',grafite_status' = - match !lexicon_status,!grafite_status with - | ss::_, s::_ -> ss,s - | _,_ -> assert false + let grafite_status' = + match !grafite_status with + | s::_ -> s + | _ -> assert false in let cb = fun _ _ -> () in let matita_debug = Helm_registry.get_bool "matita.debug" in try - match eval_function lexicon_status' grafite_status' is cb with + match eval_function grafite_status' is cb with [] -> raise End_of_file - | ((grafite_status'',lexicon_status''),None)::_ -> - lexicon_status := lexicon_status''::!lexicon_status; + | (grafite_status'',None)::_ -> grafite_status := grafite_status''::!grafite_status | (s,Some _)::_ -> raise AttemptToInsertAnAlias with @@ -137,22 +135,20 @@ let rec interactive_loop () = | n,_::l -> drop (n-1,l) | _,[] -> assert false in - let to_be_dropped = List.length !lexicon_status - n in + let to_be_dropped = List.length !grafite_status - n in let safe_hd = function [] -> assert false | he::_ -> he in - let cur_lexicon_status = safe_hd !lexicon_status in let cur_grafite_status = safe_hd !grafite_status in - lexicon_status := drop (to_be_dropped, !lexicon_status) ; grafite_status := drop (to_be_dropped, !grafite_status) ; - let lexicon_status = safe_hd !lexicon_status in let grafite_status = safe_hd !grafite_status in LexiconSync.time_travel - ~present:cur_lexicon_status ~past:lexicon_status; + ~present:(GrafiteTypes.get_lexicon cur_grafite_status) + ~past:(GrafiteTypes.get_lexicon grafite_status); GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; interactive_loop (Some n) | `Do command -> let str = Ulexing.from_utf8_string command in - let watch_statuses lexicon_status grafite_status = + let watch_statuses grafite_status = match grafite_status.GrafiteTypes.proof_status with GrafiteTypes.Incomplete_proof {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ; @@ -172,7 +168,7 @@ let rec interactive_loop () = run_script str (MatitaEngine.eval_from_stream ~first_statement_only:true ~include_paths:(Lazy.force include_paths) ~watch_statuses) ; - interactive_loop (Some (List.length !lexicon_status)) + interactive_loop (Some (List.length !grafite_status)) with | GrafiteEngine.Macro (floc,_) -> let x, y = HExtlib.loc_of_floc floc in @@ -207,10 +203,8 @@ let main () = let system_mode = Helm_registry.get_bool "matita.system" in let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in - lexicon_status := - [CicNotation2.load_notation ~include_paths - BuildTimeConf.core_notation_script] ; - grafite_status := [GrafiteSync.init (List.hd !lexicon_status) "cic:/matita/tests/"]; + grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths + BuildTimeConf.core_notation_script) "cic:/matita/tests/"]; Sys.catch_break true; let origcb = HLog.get_log_callback () in let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in @@ -229,11 +223,11 @@ let main () = | GrafiteEngine.Drop -> clean_exit 1 ); let proof_status,moo_content_rev,lexicon_content_rev = - match !lexicon_status,!grafite_status with - | ss::_, s::_ -> + match !grafite_status with + | s::_ -> s.proof_status, s.moo_content_rev, - ss.LexiconEngine.lexicon_content_rev - | _,_ -> assert false + (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev + | _ -> assert false in if proof_status <> GrafiteTypes.No_proof then begin diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 1276300b1..a4e879a36 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -226,18 +226,19 @@ let compile atstart options fname = if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) else pp_ast_statement in - let lexicon_status, grafite_status = - let rec aux_for_dump x lexicon_status grafite_status = + let grafite_status = + let rec aux_for_dump x grafite_status = try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths - lexicon_status grafite_status buf x + grafite_status buf x with - | [] -> lexicon_status, grafite_status - | ((grafite,lexicon),None)::_ -> lexicon, grafite - | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l) + | [] -> grafite_status + | (g,None)::_ -> g + | (g,Some _)::_ -> + raise (AttemptToInsertAnAlias (GrafiteTypes.get_lexicon g)) with MatitaEngine.EnrichedWithStatus - (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn -> + (GrafiteEngine.Macro (floc, f), grafite) as exn -> match f (get_macro_context (Some grafite)) with | _, GrafiteAst.Inline (_, _suri, _params) -> (* @@ -249,15 +250,15 @@ let compile atstart options fname = in !out str; *) - aux_for_dump x lexicon grafite + aux_for_dump x grafite |_-> raise exn in - aux_for_dump print_cb lexicon_status grafite_status + aux_for_dump print_cb grafite_status in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = grafite_status.proof_status, grafite_status.moo_content_rev, - lexicon_status.LexiconEngine.lexicon_content_rev + (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev in if proof_status <> GrafiteTypes.No_proof then (HLog.error @@ -299,7 +300,7 @@ let compile atstart options fname = ~present:lexicon_status ~past:initial_lexicon_status; *) clean_exit baseuri false - | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' -> + | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' -> (match exn with | Sys.Break -> HLog.error "user break!" | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> diff --git a/helm/software/matita/tests/ng_coercions.ma b/helm/software/matita/tests/ng_coercions.ma new file mode 100644 index 000000000..1a1686267 --- /dev/null +++ b/helm/software/matita/tests/ng_coercions.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +axiom A : Type. +axiom B : Type. +axiom C : Type. + +axiom f : A → B. +axiom g : B → C. + +(* nlemma xxx : ∀P:C → Prop. ∀x:A. P x. *) + +coercion f. coercion g. + +axiom T : Type. + +axiom h : A → T. coercion h. + +nlemma xxx : ∀P:C → Prop. ∀x:A. P x. \ No newline at end of file diff --git a/helm/software/matita/tests/ng_lexiconn.ma b/helm/software/matita/tests/ng_lexiconn.ma new file mode 100644 index 000000000..134d13fa8 --- /dev/null +++ b/helm/software/matita/tests/ng_lexiconn.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ng_pts.ma". + +axiom A : Type. + +axiom a : A. +axiom b : A. + +axiom B : Type. + +axiom c : B. +axiom d : B. + + +notation "#" with precedence 90 for @{ 'foo }. +interpretation "a" 'foo = a. +interpretation "b" 'foo = b. +interpretation "c" 'foo = c. +interpretation "d" 'foo = d. + +alias symbol "foo" = "c". +alias symbol "foo" = "b". +alias symbol "foo" = "d". +alias symbol "foo" = "b". + +lemma xx : ∀P: A → B → Prop. P # #. (* NON STAMPA GLI ALIAS *) + -- 2.39.2