From: Enrico Tassi Date: Wed, 25 Mar 2009 20:41:04 +0000 (+0000) Subject: new tactics are almost ready X-Git-Tag: make_still_working~4139 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git new tactics are almost ready --- diff --git a/helm/software/components/METAS/meta.helm-grafite.src b/helm/software/components/METAS/meta.helm-grafite.src index 0ae4a09d3..d58e0f87f 100644 --- a/helm/software/components/METAS/meta.helm-grafite.src +++ b/helm/software/components/METAS/meta.helm-grafite.src @@ -1,4 +1,4 @@ -requires="helm-cic" +requires="helm-cic helm-acic_content" version="0.0.1" archive(byte)="grafite.cma" archive(native)="grafite.cmxa" diff --git a/helm/software/components/METAS/meta.helm-grafite_engine.src b/helm/software/components/METAS/meta.helm-grafite_engine.src index bcd72841e..45a02a30b 100644 --- a/helm/software/components/METAS/meta.helm-grafite_engine.src +++ b/helm/software/components/METAS/meta.helm-grafite_engine.src @@ -1,4 +1,4 @@ -requires="helm-library helm-grafite helm-tactics helm-ng_refiner" +requires="helm-library helm-grafite helm-tactics helm-ng_tactics helm-ng_refiner" version="0.0.1" archive(byte)="grafite_engine.cma" archive(native)="grafite_engine.cmxa" diff --git a/helm/software/components/METAS/meta.helm-ng_tactics.src b/helm/software/components/METAS/meta.helm-ng_tactics.src new file mode 100644 index 000000000..9b5db1359 --- /dev/null +++ b/helm/software/components/METAS/meta.helm-ng_tactics.src @@ -0,0 +1,4 @@ +requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-tactics" +version="0.0.1" +archive(byte)="ng_tactics.cma" +archive(native)="ng_tactics.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 1c937a855..1f13fc94a 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -36,8 +36,9 @@ MODULES = \ ng_kernel \ ng_refiner \ ng_disambiguation \ - grafite_engine \ grafite_parser \ + ng_tactics \ + grafite_engine \ tptp_grafite \ $(NULL) diff --git a/helm/software/components/acic_content/.depend b/helm/software/components/acic_content/.depend index 8ade458af..89dca0e44 100644 --- a/helm/software/components/acic_content/.depend +++ b/helm/software/components/acic_content/.depend @@ -1,3 +1,4 @@ +content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmo @@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmo termAcicContent.cmi: cicNotationPt.cmo +cicNotationPt.cmo: +cicNotationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi acic2content.cmo: content.cmi acic2content.cmi diff --git a/helm/software/components/acic_content/.depend.opt b/helm/software/components/acic_content/.depend.opt index fef879256..307fceaa0 100644 --- a/helm/software/components/acic_content/.depend.opt +++ b/helm/software/components/acic_content/.depend.opt @@ -1,3 +1,4 @@ +content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmx @@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmx cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmx termAcicContent.cmi: cicNotationPt.cmx +cicNotationPt.cmo: +cicNotationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi acic2content.cmo: content.cmi acic2content.cmi diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 122ed1938..bb44e4dfb 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,5 +1,12 @@ +proceduralHelpers.cmi: +proceduralClassify.cmi: +proceduralOptimizer.cmi: +proceduralTypes.cmi: +proceduralMode.cmi: +proceduralConversion.cmi: procedural1.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi +acic2Procedural.cmi: proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 122ed1938..bb44e4dfb 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,5 +1,12 @@ +proceduralHelpers.cmi: +proceduralClassify.cmi: +proceduralOptimizer.cmi: +proceduralTypes.cmi: +proceduralMode.cmi: +proceduralConversion.cmi: procedural1.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi +acic2Procedural.cmi: proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend index e69de29bb..0c39328ae 100644 --- a/helm/software/components/binaries/extractor/.depend +++ b/helm/software/components/binaries/extractor/.depend @@ -0,0 +1,4 @@ +extractor.cmo: +extractor.cmx: +extractor_manager.cmo: +extractor_manager.cmx: diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt index e69de29bb..0c39328ae 100644 --- a/helm/software/components/binaries/extractor/.depend.opt +++ b/helm/software/components/binaries/extractor/.depend.opt @@ -0,0 +1,4 @@ +extractor.cmo: +extractor.cmx: +extractor_manager.cmo: +extractor_manager.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend index e69de29bb..33147b949 100644 --- a/helm/software/components/binaries/table_creator/.depend +++ b/helm/software/components/binaries/table_creator/.depend @@ -0,0 +1,2 @@ +table_creator.cmo: +table_creator.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt index e69de29bb..33147b949 100644 --- a/helm/software/components/binaries/table_creator/.depend.opt +++ b/helm/software/components/binaries/table_creator/.depend.opt @@ -0,0 +1,2 @@ +table_creator.cmo: +table_creator.cmx: diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 660edb2f5..8121968e9 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,5 +1,10 @@ v8Parser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: v8Parser.cmo: types.cmo options.cmo v8Parser.cmi v8Parser.cmx: types.cmx options.cmx v8Parser.cmi v8Lexer.cmo: v8Parser.cmi options.cmo diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index 5e2c3e23c..b64d148de 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,5 +1,10 @@ v8Parser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: v8Parser.cmo: types.cmx options.cmx v8Parser.cmi v8Parser.cmx: types.cmx options.cmx v8Parser.cmi v8Lexer.cmo: v8Parser.cmi options.cmx diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index 595fd4b3a..36b6f6f0d 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -1,3 +1,4 @@ +cicUniv.cmi: unshare.cmi: cic.cmo deannotate.cmi: cic.cmo cicParser.cmi: cic.cmo diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt index 0ff8e697c..cdbbb8323 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -1,3 +1,4 @@ +cicUniv.cmi: unshare.cmi: cic.cmx deannotate.cmi: cic.cmx cicParser.cmi: cic.cmx diff --git a/helm/software/components/cic_acic/.depend b/helm/software/components/cic_acic/.depend index 3fc1e0dce..5449d50aa 100644 --- a/helm/software/components/cic_acic/.depend +++ b/helm/software/components/cic_acic/.depend @@ -1,3 +1,6 @@ +eta_fixing.cmi: +doubleTypeInference.cmi: +cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt index 3fc1e0dce..5449d50aa 100644 --- a/helm/software/components/cic_acic/.depend.opt +++ b/helm/software/components/cic_acic/.depend.opt @@ -1,3 +1,6 @@ +eta_fixing.cmi: +doubleTypeInference.cmi: +cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index e9bd1168f..a9ae65a5e 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,3 +1,5 @@ +cicDisambiguate.cmi: +disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt index e9bd1168f..a9ae65a5e 100644 --- a/helm/software/components/cic_disambiguation/.depend.opt +++ b/helm/software/components/cic_disambiguation/.depend.opt @@ -1,3 +1,5 @@ +cicDisambiguate.cmi: +disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index ed28894a7..3e9124e69 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -37,15 +37,26 @@ let rec string_context_of_context = ;; let refine_term metasenv subst context uri ~use_coercions - term ugraph ~localization_tbl = + term expty ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); let saved_use_coercions = !CicRefine.insert_coercions in try CicRefine.insert_coercions := use_coercions; + let term = + match expty with + | None -> term + | Some ty -> Cic.Cast(term,ty) + in let term', _, metasenv',ugraph1 = CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl + in + let term' = + match expty, term' with + | None,_ -> term' + | Some _,Cic.Cast (term',_) -> term' + | _ -> assert false in CicRefine.insert_coercions := saved_use_coercions; (Disambiguate.Ok (term', metasenv',[],ugraph1)) @@ -66,7 +77,7 @@ let refine_term metasenv subst context uri ~use_coercions in process_exn Stdpp.dummy_loc exn -let refine_obj metasenv subst context uri ~use_coercions obj ugraph +let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph ~localization_tbl = assert (context = []); assert (metasenv = []); @@ -627,25 +638,11 @@ let string_context_of_context = List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some (Cic.Anonymous,_) -> Some "_");; -let disambiguate_term ~context ~metasenv ~subst ?goal +let disambiguate_term ~context ~metasenv ~subst ~expty ?(initial_ugraph = CicUniv.oblivion_ugraph) ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = - let hint = match goal with - | None -> (fun _ x -> x), fun k -> k - | Some i -> - (fun metasenv t -> - let _,c,ty = CicUtil.lookup_meta i metasenv in - assert(c=context); - Cic.Cast(t,ty)), - function - | Disambiguate.Ok (t,m,s,ug) -> - (match t with - | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug) - | _ -> assert false) - | k -> k - in let mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst ~initial_ugraph ~aliases ~string_context_of_context @@ -655,14 +652,13 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) ~refine_thing:refine_term (text,prefix_len,term) ~mk_localization_tbl - ~hint + ~expty ~freshen_thing:CicNotationUtil.freshen_term ~passes:(MultiPassDisambiguator.passes ()) let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = - let hint = (fun _ x -> x), fun k -> k in let mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] ~aliases ~universe ~uri ~string_context_of_context @@ -673,7 +669,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:refine_obj ~mk_localization_tbl - ~hint + ~expty:None ~passes:(MultiPassDisambiguator.passes ()) ~freshen_thing:CicNotationUtil.freshen_obj (text,prefix_len,obj) diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli index 86ede901c..ecb592682 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli @@ -31,7 +31,7 @@ val disambiguate_term : context:Cic.context -> metasenv:Cic.metasenv -> subst:Cic.substitution -> - ?goal:int -> + expty:Cic.term option -> ?initial_ugraph:CicUniv.universe_graph -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> diff --git a/helm/software/components/cic_exportation/.depend b/helm/software/components/cic_exportation/.depend index 288ea5f6c..91be8d88d 100644 --- a/helm/software/components/cic_exportation/.depend +++ b/helm/software/components/cic_exportation/.depend @@ -1,2 +1,3 @@ +cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt index 288ea5f6c..91be8d88d 100644 --- a/helm/software/components/cic_exportation/.depend.opt +++ b/helm/software/components/cic_exportation/.depend.opt @@ -1,2 +1,3 @@ +cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend index 5d83fd0f3..f8a16629e 100644 --- a/helm/software/components/cic_proof_checking/.depend +++ b/helm/software/components/cic_proof_checking/.depend @@ -1,3 +1,13 @@ +cicLogger.cmi: +cicEnvironment.cmi: +cicPp.cmi: +cicUnivUtils.cmi: +cicSubstitution.cmi: +cicMiniReduction.cmi: +cicReduction.cmi: +cicTypeChecker.cmi: +freshNamesGenerator.cmi: +cicDischarge.cmi: cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi cicEnvironment.cmo: cicEnvironment.cmi diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt index 5d83fd0f3..f8a16629e 100644 --- a/helm/software/components/cic_proof_checking/.depend.opt +++ b/helm/software/components/cic_proof_checking/.depend.opt @@ -1,3 +1,13 @@ +cicLogger.cmi: +cicEnvironment.cmi: +cicPp.cmi: +cicUnivUtils.cmi: +cicSubstitution.cmi: +cicMiniReduction.cmi: +cicReduction.cmi: +cicTypeChecker.cmi: +freshNamesGenerator.cmi: +cicDischarge.cmi: cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi cicEnvironment.cmo: cicEnvironment.cmi diff --git a/helm/software/components/cic_unification/.depend b/helm/software/components/cic_unification/.depend index a7b23ceb4..2e054f73d 100644 --- a/helm/software/components/cic_unification/.depend +++ b/helm/software/components/cic_unification/.depend @@ -1,3 +1,10 @@ +cicMetaSubst.cmi: +cicMkImplicit.cmi: +termUtil.cmi: +coercGraph.cmi: +cicUnification.cmi: +cicReplace.cmi: +cicRefine.cmi: cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt index a7b23ceb4..2e054f73d 100644 --- a/helm/software/components/cic_unification/.depend.opt +++ b/helm/software/components/cic_unification/.depend.opt @@ -1,3 +1,10 @@ +cicMetaSubst.cmi: +cicMkImplicit.cmi: +termUtil.cmi: +coercGraph.cmi: +cicUnification.cmi: +cicReplace.cmi: +cicRefine.cmi: cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 6dd0e78a1..8d74439eb 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -1,3 +1,9 @@ +renderingAttrs.cmi: +cicNotationLexer.cmi: +cicNotationParser.cmi: +mpresentation.cmi: +box.cmi: +content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt index 6dd0e78a1..8d74439eb 100644 --- a/helm/software/components/content_pres/.depend.opt +++ b/helm/software/components/content_pres/.depend.opt @@ -1,3 +1,9 @@ +renderingAttrs.cmi: +cicNotationLexer.cmi: +cicNotationParser.cmi: +mpresentation.cmi: +box.cmi: +content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi diff --git a/helm/software/components/disambiguation/.depend b/helm/software/components/disambiguation/.depend index aba9ffea7..9fdbeeeaf 100644 --- a/helm/software/components/disambiguation/.depend +++ b/helm/software/components/disambiguation/.depend @@ -1,3 +1,4 @@ +disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt index aba9ffea7..9fdbeeeaf 100644 --- a/helm/software/components/disambiguation/.depend.opt +++ b/helm/software/components/disambiguation/.depend.opt @@ -1,3 +1,4 @@ +disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 44498d088..fa63d1f48 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -409,7 +409,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context - ~initial_ugraph:base_univ ~hint + ~initial_ugraph:base_univ ~expty ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing @@ -489,14 +489,9 @@ let disambiguate_thing interpretate_thing ~context ~env:filled_env ~uri ~is_path:false thing ~localization_tbl in - let cic_thing = (fst hint) metasenv cic_thing in let foo () = - let k = refine_thing metasenv subst context uri - ~use_coercions cic_thing ugraph ~localization_tbl - in - let k = (snd hint) k in - k + ~use_coercions cic_thing expty ugraph ~localization_tbl in refine_profiler.HExtlib.profile foo () with | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli index 822f14092..ffbdf884d 100644 --- a/helm/software/components/disambiguation/disambiguate.mli +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -93,10 +93,7 @@ val disambiguate_thing: use_coercions:bool -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> - hint: - ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv,'subst,'ugraph) test_result -> - ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> + expty: 'refined_thing option -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> aliases:'alias DisambiguateTypes.Environment.t -> @@ -119,7 +116,7 @@ val disambiguate_thing: 'raw_thing) -> refine_thing:( 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> - 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> + 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> mk_localization_tbl:(int -> 'cichash) -> 'ast_thing disambiguator_input -> diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index 63bcaa587..86d037742 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -143,7 +143,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing aux 1 [] passes let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst - ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit + ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing = @@ -151,7 +151,7 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst let thing = if fresh_instances then freshen_thing thing else thing in Disambiguate.disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context - ~initial_ugraph ~hint ~mk_implicit ~description_of_alias + ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl (txt,len,thing) diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli index 21818816c..4977a81d9 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.mli +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -45,10 +45,7 @@ val disambiguate_thing: subst:'subst -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> - hint: - ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result -> - ('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result) -> + expty: 'refined_thing option -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> aliases:'alias DisambiguateTypes.Environment.t -> @@ -73,7 +70,7 @@ val disambiguate_thing: 'raw_thing) -> refine_thing:( 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> - 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> + 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) -> mk_localization_tbl:(int -> 'cichash) -> string * int * 'ast_thing -> diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend index 6d96e61e2..3f72e1d24 100644 --- a/helm/software/components/extlib/.depend +++ b/helm/software/components/extlib/.depend @@ -1,3 +1,12 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt index 6d96e61e2..3f72e1d24 100644 --- a/helm/software/components/extlib/.depend.opt +++ b/helm/software/components/extlib/.depend.opt @@ -1,3 +1,12 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi diff --git a/helm/software/components/getter/.depend b/helm/software/components/getter/.depend index 20f69cf0c..ca64d8ec0 100644 --- a/helm/software/components/getter/.depend +++ b/helm/software/components/getter/.depend @@ -1,6 +1,13 @@ +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: http_getter_env.cmi: http_getter_types.cmo +http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmo http_getter.cmi: http_getter_types.cmo +http_getter_types.cmo: +http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi diff --git a/helm/software/components/getter/.depend.opt b/helm/software/components/getter/.depend.opt index 554fb1ec7..64da37f13 100644 --- a/helm/software/components/getter/.depend.opt +++ b/helm/software/components/getter/.depend.opt @@ -1,6 +1,13 @@ +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: http_getter_env.cmi: http_getter_types.cmx +http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmx http_getter.cmi: http_getter_types.cmx +http_getter_types.cmo: +http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi diff --git a/helm/software/components/grafite/.depend b/helm/software/components/grafite/.depend index dc225e221..f305b1580 100644 --- a/helm/software/components/grafite/.depend +++ b/helm/software/components/grafite/.depend @@ -1,5 +1,7 @@ grafiteAstPp.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo +grafiteAst.cmo: +grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi diff --git a/helm/software/components/grafite/.depend.opt b/helm/software/components/grafite/.depend.opt index 0f64ba789..e01d5bbfa 100644 --- a/helm/software/components/grafite/.depend.opt +++ b/helm/software/components/grafite/.depend.opt @@ -1,5 +1,7 @@ grafiteAstPp.cmi: grafiteAst.cmx grafiteMarshal.cmi: grafiteAst.cmx +grafiteAst.cmo: +grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index d114d9322..018c5a44f 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -46,6 +46,9 @@ type 'term just = [ `Term of 'term | `Auto of 'term auto_params ] +type ntactic = + NApply of loc * CicNotationPt.term + type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Higher order tactics (i.e. tacticals) *) | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic @@ -150,7 +153,7 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 16 +let magic = 17 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -167,8 +170,9 @@ type ('term,'obj) command = | Set of loc * string * string | Print of loc * string | Qed of loc + | NObj of loc * CicNotationPt.term CicNotationPt.obj -type ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical = +type punctuation_tactical = | Dot of loc | Semicolon of loc | Branch of loc @@ -177,7 +181,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical = | Wildcard of loc | Merge of loc -type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical = +type non_punctuation_tactical = | Focus of loc * int list | Unfocus of loc | Skip of loc @@ -185,11 +189,11 @@ type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical = type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = | Command of loc * ('term, 'obj) command | Macro of loc * ('term,'lazy_term) macro + | NTactic of loc * ntactic option * punctuation_tactical | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option - * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical - | NonPunctuationTactical of loc - * ('term, 'lazy_term, 'reduction, 'ident) non_punctuation_tactical - * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical + * punctuation_tactical + | NonPunctuationTactical of loc * non_punctuation_tactical + * punctuation_tactical type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = | Note of loc * string diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 56ac59c7a..a33bf6d9d 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -89,6 +89,10 @@ let pp_just ~term_pp = | `Auto params -> pp_auto_params ~term_pp params ;; +let pp_ntactic ~map_unicode_to_tex = function + | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t +;; + let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = let pp_terms = pp_terms ~term_pp in let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in @@ -337,8 +341,9 @@ let pp_command ~term_pp ~obj_pp = function | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value + | NObj (_,o) -> "not supported" -let pp_punctuation_tactical ~term_pp ~lazy_term_pp = +let pp_punctuation_tactical = function | Dot _ -> "." | Semicolon _ -> ";" @@ -348,7 +353,7 @@ let pp_punctuation_tactical ~term_pp ~lazy_term_pp = | Wildcard _ -> "*:" | Merge _ -> "]" -let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = +let pp_non_punctuation_tactical = function | Focus (_, goals) -> Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) @@ -359,13 +364,18 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "." | Tactic (_, Some tac, punct) -> - pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac - ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac + ^ pp_punctuation_tactical punct | Tactic (_, None, punct) -> - pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + pp_punctuation_tactical punct + | NTactic (_,Some tac, punct) -> + pp_ntactic ~map_unicode_to_tex tac + ^ pp_punctuation_tactical punct + | NTactic (_,None, punct) -> + pp_punctuation_tactical punct | NonPunctuationTactical (_, tac, punct) -> - pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac - ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + pp_non_punctuation_tactical tac + ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = diff --git a/helm/software/components/grafite/grafiteAstPp.mli b/helm/software/components/grafite/grafiteAstPp.mli index 8f6904545..4ae11a59b 100644 --- a/helm/software/components/grafite/grafiteAstPp.mli +++ b/helm/software/components/grafite/grafiteAstPp.mli @@ -78,10 +78,5 @@ val pp_statement: map_unicode_to_tex:bool -> string -val pp_punctuation_tactical: - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - ('term, 'lazy_term, 'term GrafiteAst.reduction, string) - GrafiteAst.punctuation_tactical -> - string +val pp_punctuation_tactical: GrafiteAst.punctuation_tactical -> string diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend index b0d4b7048..2dca47091 100644 --- a/helm/software/components/grafite_engine/.depend +++ b/helm/software/components/grafite_engine/.depend @@ -1,3 +1,4 @@ +grafiteTypes.cmi: grafiteSync.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.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 7f5327b56..b0df46ba3 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -665,6 +665,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status, [] (*CSC: TO BE FIXED *) | GrafiteAst.Set (loc, name, value) -> status, [] (* GrafiteTypes.set_option status name value,[] *) + | GrafiteAst.NObj (loc,obj) -> + let ty, name = + match obj with + | CicNotationPt.Theorem (_,name,ty,_) -> ty, name + | _ -> assert false + in + let suri = "cic:/ng_matita/" ^ name ^ ".def" in + let nmenv, nsubst, nlexicon_status, nty = + GrafiteDisambiguate.disambiguate_nterm None + LexiconEngine.initial_status [] [] [] (text,prefix_len,ty) + in + let nmenv, nsubst, nlexicon_status, nbo = + GrafiteDisambiguate.disambiguate_nterm (Some nty) + LexiconEngine.initial_status [] nmenv nsubst ("",0,CicNotationPt.Implicit) + in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv); + { status with + GrafiteTypes.ng_status = Some { NTactics.gstatus = ninitial_stack; + istatus = { + NTactics.pstatus = + NUri.uri_of_string suri, 0, nmenv, nsubst, + (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular))); + lstatus = nlexicon_status} } + }, + [] | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -716,7 +742,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let initial_stack = Continuationals.Stack.of_metasenv metasenv' in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof - { GrafiteTypes.proof = initial_proof; stack = initial_stack } }, + { GrafiteTypes.proof = initial_proof; stack = initial_stack } ; + }, [] | _ -> if metasenv <> [] then @@ -755,6 +782,22 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteAst.Tactic (_, None, punct) -> eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + | GrafiteAst.NTactic (_(*loc*), Some (GrafiteAst.NApply (_loc, t)), punct) -> + (match status.GrafiteTypes.ng_status with + | None -> assert false + | Some status -> + let nts = NTactics.apply_tac (text,prefix_len,t) status in + prerr_endline "esco da apply"; + NTactics.pp_tac_status nts; + (* + let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in + let status = eval_tactical status (tactic_of_ast' tac) in + eval_tactical status + (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + *) assert false) + | GrafiteAst.NTactic (_, None, _punct) -> assert false (* + eval_tactical status + (punctuation_tactical_of_ast (text,prefix_len,punct)),[] *) | GrafiteAst.NonPunctuationTactical (_, tac, punct) -> let status = eval_tactical status diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index c1b23c928..3fc67f2fd 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -122,6 +122,7 @@ let initial_status baseuri = { coercions = CoercDb.empty_coerc_db; universe = Universe.empty; baseuri = baseuri; + ng_status = None; } diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 244ce615f..aa90dc0e0 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -51,6 +51,7 @@ type status = { coercions: CoercDb.coerc_db; universe:Universe.universe; baseuri: string; + ng_status: NTactics.tac_status option; } let get_current_proof status = diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index 95f65f360..3a833f6da 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -49,6 +49,7 @@ type status = { coercions: CoercDb.coerc_db; universe:Universe.universe; (** universe of terms used by auto *) baseuri: string; + ng_status: NTactics.tac_status option; } val dump_status : status -> unit diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index 9fb3357e7..568021042 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -1,4 +1,9 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +grafiteDisambiguate.cmi: grafiteWalker.cmi: grafiteParser.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index 9fb3357e7..568021042 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -1,4 +1,9 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +grafiteDisambiguate.cmi: grafiteWalker.cmi: grafiteParser.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 23ec1770e..027cde4a5 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -153,14 +153,14 @@ let lookup_in_library ;; (** @param term not meaningful when context is given *) -let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv +let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, subst, cic, _) = singleton "first" (CicDisambiguate.disambiguate_term ~aliases:lexicon_status.LexiconEngine.aliases - ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~lookup_in_library ~mk_choice:cic_mk_choice ~mk_implicit @@ -172,12 +172,32 @@ term = metasenv,(*subst,*) cic ;; +let disambiguate_nterm expty lexicon_status context metasenv subst thing += + let diff, metasenv, subst, cic = + singleton "first" + (NCicDisambiguate.disambiguate_term + ~coercion_db:(NCicCoercion.db ()) + ~aliases:lexicon_status.LexiconEngine.aliases + ~expty + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~lookup_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 +;; + + (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term * rationale: lazy_term will be invoked in different context to obtain a term, * each invocation will disambiguate the term and can add aliases. Once all * disambiguations have been performed, the first returned function can be * used to obtain the resulting aliases *) -let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = +let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term = (fun context metasenv ugraph -> let lexicon_status = !lexicon_status_ref in let (diff, metasenv, _, cic, ugraph) = @@ -189,8 +209,8 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = ~description_of_alias:LexiconAst.description_of_alias ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - ~context ~metasenv ~subst:[] ?goal - (text,prefix_len,term)) in + ~context ~metasenv ~subst:[] + (text,prefix_len,term) ~expty) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status_ref := lexicon_status; cic, metasenv, ugraph) @@ -253,7 +273,10 @@ let rec disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tactic) = let disambiguate_term_hint = - disambiguate_term goal text prefix_len lexicon_status_ref in + let _,_,expty = + List.find (fun (x,_,_) -> Some x = goal) metasenv + in + disambiguate_term (Some expty) text prefix_len lexicon_status_ref in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in let disambiguate_pattern = @@ -573,7 +596,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = in UriManager.uri_of_string (baseuri ^ "/" ^ name) in - let try_new cic = + let _try_new cic = (NCicLibrary.clear_cache (); NCicEnvironment.invalidate (); OCic2NCic.clear (); @@ -701,6 +724,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= match cmd with + | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj) | GrafiteAst.Index(loc,key,uri) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index 1543387ee..163e6db6d 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -54,3 +54,9 @@ val disambiguate_macro: Cic.context -> ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input -> Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro + +val disambiguate_nterm : + NCic.term option -> LexiconEngine.status -> + NCic.context -> NCic.metasenv -> NCic.substitution -> + CicNotationPt.term Disambiguate.disambiguator_input -> + NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 28d61d9e5..7fbd49968 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -180,6 +180,11 @@ EXTEND ] ]; using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; + ntactic: [ + [ IDENT "napply"; t = tactic_term -> + GrafiteAst.NApply (loc, t) + ] + ]; tactic: [ [ IDENT "absurd"; t = tactic_term -> GrafiteAst.Absurd (loc, t) @@ -462,6 +467,10 @@ EXTEND | IDENT "skip" -> GrafiteAst.Skip loc ] ]; + ntheorem_flavour: [ + [ [ IDENT "ntheorem" ] -> `Theorem + ] + ]; theorem_flavour: [ [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact @@ -666,6 +675,9 @@ EXTEND GrafiteAst.Obj (loc, Ast.Theorem (`Variant,name,typ,Some (Ast.Ident (newname, None)))) + | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body)) | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body)) @@ -731,6 +743,8 @@ EXTEND | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> GrafiteAst.Tactic (loc, Some tac, punct) | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct) + | tac = ntactic; punct = punctuation_tactical -> + GrafiteAst.NTactic (loc, Some tac, punct) | tac = non_punctuation_tactical; punct = punctuation_tactical -> GrafiteAst.NonPunctuationTactical (loc, tac, punct) | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) diff --git a/helm/software/components/hgdome/.depend b/helm/software/components/hgdome/.depend index bf9c09af7..072d9697a 100644 --- a/helm/software/components/hgdome/.depend +++ b/helm/software/components/hgdome/.depend @@ -1,3 +1,5 @@ +domMisc.cmi: +xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt index bf9c09af7..072d9697a 100644 --- a/helm/software/components/hgdome/.depend.opt +++ b/helm/software/components/hgdome/.depend.opt @@ -1,3 +1,5 @@ +domMisc.cmi: +xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend index 16e6e9da7..ce439d961 100644 --- a/helm/software/components/hmysql/.depend +++ b/helm/software/components/hmysql/.depend @@ -1,2 +1,7 @@ +hSql.cmi: +hSqlite3.cmo: +hSqlite3.cmx: +hMysql.cmo: +hMysql.cmx: hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt index 602c901b8..c2289bff2 100644 --- a/helm/software/components/hmysql/.depend.opt +++ b/helm/software/components/hmysql/.depend.opt @@ -1,2 +1,7 @@ +hSql.cmi: +hSqlite3.cmo: +hSqlite3.cmx: +hMysql.cmo: +hMysql.cmx: hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/lexicon/.depend b/helm/software/components/lexicon/.depend index 33e89a7d9..baa009488 100644 --- a/helm/software/components/lexicon/.depend +++ b/helm/software/components/lexicon/.depend @@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmo cicNotation.cmi: lexiconAst.cmo lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo +lexiconAst.cmo: +lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt index 1b4992009..4d156c5f5 100644 --- a/helm/software/components/lexicon/.depend.opt +++ b/helm/software/components/lexicon/.depend.opt @@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmx cicNotation.cmi: lexiconAst.cmx lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx +lexiconAst.cmo: +lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend index a9f24f814..cfa1295ed 100644 --- a/helm/software/components/library/.depend +++ b/helm/software/components/library/.depend @@ -1,4 +1,13 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi libraryMisc.cmo: libraryMisc.cmi diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt index a9f24f814..cfa1295ed 100644 --- a/helm/software/components/library/.depend.opt +++ b/helm/software/components/library/.depend.opt @@ -1,4 +1,13 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi libraryMisc.cmo: libraryMisc.cmi diff --git a/helm/software/components/logger/.depend b/helm/software/components/logger/.depend index 28268d29e..dfb4400ff 100644 --- a/helm/software/components/logger/.depend +++ b/helm/software/components/logger/.depend @@ -1,2 +1,3 @@ +helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/logger/.depend.opt b/helm/software/components/logger/.depend.opt index 28268d29e..dfb4400ff 100644 --- a/helm/software/components/logger/.depend.opt +++ b/helm/software/components/logger/.depend.opt @@ -1,2 +1,3 @@ +helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/metadata/.depend b/helm/software/components/metadata/.depend index 492a34e3a..78cd97a0d 100644 --- a/helm/software/components/metadata/.depend +++ b/helm/software/components/metadata/.depend @@ -1,3 +1,5 @@ +sqlStatements.cmi: +metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt index 492a34e3a..78cd97a0d 100644 --- a/helm/software/components/metadata/.depend.opt +++ b/helm/software/components/metadata/.depend.opt @@ -1,3 +1,5 @@ +sqlStatements.cmi: +metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend index 6b4ef95c1..2de54dc5e 100644 --- a/helm/software/components/ng_disambiguation/.depend +++ b/helm/software/components/ng_disambiguation/.depend @@ -1,2 +1,3 @@ +nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt index 6b4ef95c1..2de54dc5e 100644 --- a/helm/software/components/ng_disambiguation/.depend.opt +++ b/helm/software/components/ng_disambiguation/.depend.opt @@ -1,2 +1,3 @@ +nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 50a0c59da..f426f7126 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -28,7 +28,7 @@ let cic_name_of_name = function ;; let refine_term - metasenv subst context uri ~coercion_db ~use_coercions term _ ~localization_tbl= + metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl= assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); @@ -46,7 +46,7 @@ let refine_term if use_coercions then NCicCoercion.look_for_coercion coercion_db else (fun _ _ _ _ _ -> [])) - metasenv subst context term None ~localise + metasenv subst context term expty ~localise in Disambiguate.Ok (term, metasenv, subst, ()) with @@ -62,7 +62,7 @@ let refine_term let refine_obj ~coercion_db metasenv subst context uri - ~use_coercions obj ugraph ~localization_tbl + ~use_coercions obj _ ugraph ~localization_tbl = assert (metasenv=[]); assert (subst=[]); @@ -562,26 +562,12 @@ let interpretate_obj *) ;; -let disambiguate_term ~context ~metasenv ~subst ?goal +let disambiguate_term ~context ~metasenv ~subst ~expty ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~coercion_db ~lookup_in_library (text,prefix_len,term) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in - let hint = - match goal with - None -> (fun _ y -> y),(fun x -> x) - | Some n -> - (fun metasenv y -> - let _,_,ty = NCicUtils.lookup_meta n metasenv in - NCic.LetIn ("_",ty,y,NCic.Rel 1)), - (function - | Disambiguate.Ok (t,m,s,ug) -> - (match t with - | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug) - | _ -> assert false) - | k -> k) - in let res,b = MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_term @@ -593,7 +579,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~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) - ~mk_localization_tbl ~hint ~subst + ~mk_localization_tbl ~expty ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; @@ -604,7 +590,6 @@ let disambiguate_obj (text,prefix_len,obj) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in - let hint = (fun x y -> y), (fun x -> x) in let res,b = MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_obj @@ -619,7 +604,7 @@ let disambiguate_obj ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:(refine_obj ~coercion_db) (text,prefix_len,obj) - ~mk_localization_tbl ~hint + ~mk_localization_tbl ~expty:None in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 6af6733d8..d1175648a 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -15,7 +15,7 @@ val disambiguate_term : context:NCic.context -> metasenv:NCic.metasenv -> subst:NCic.substitution -> - ?goal:int -> + expty:NCic.term option -> mk_implicit: (bool -> 'alias) -> description_of_alias:('alias -> string) -> mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 5d08f2d21..bb269130e 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,3 +1,4 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index fc55a7f7d..eab572e22 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,3 +1,4 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 83422cd8f..c4c66374a 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -172,37 +172,6 @@ let ppterm ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = ppterm ~context ~subst ~metasenv ?inside_fix t ;; - -let ppobj = function - | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) -> - "{"^NUri.string_of_uri u^"}\n"^ - (if b then "let rec " else "let corec ") ^ - String.concat "\nand " - (List.map (fun (_,name,n,ty,bo) -> - name^ " on " ^ string_of_int n ^ " : " ^ - ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ - ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl) - | (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) -> - "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^ - (if b then "inductive " else "coinductive ")^ - String.concat "\nand " - (List.map (fun (_,name,ty,cl) -> - name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^ - String.concat "\n" - (List.map (fun (_,name,ty) -> - " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty) - cl)) tyl) ^ "." - | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) -> - "{"^NUri.string_of_uri u^"}\n"^ - "axiom " ^ name ^ " : " ^ - ppterm ~metasenv ~subst ~context:[] ty ^ "\n" - | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) -> - "{"^NUri.string_of_uri u^"}\n"^ - "definition " ^ name ^ " : " ^ - ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^ - ppterm ~metasenv ~subst ~context:[] bo ^ "\n" -;; - let rec ppcontext ?(sep="\n") ~subst ~metasenv = function | [] -> "" | (name, NCic.Decl t) :: tl -> @@ -240,5 +209,38 @@ let rec ppsubst ~subst ~metasenv = function let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;; + +let ppobj (u,_,metasenv, subst, o) = + "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^ + match o with + | NCic.Fixpoint (b, fl, _) -> + "{"^NUri.string_of_uri u^"}\n"^ + (if b then "let rec " else "let corec ") ^ + String.concat "\nand " + (List.map (fun (_,name,n,ty,bo) -> + name^ " on " ^ string_of_int n ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ + ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl) + | NCic.Inductive (b, leftno,tyl, _) -> + "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^ + (if b then "inductive " else "coinductive ")^ + String.concat "\nand " + (List.map (fun (_,name,ty,cl) -> + name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^ + String.concat "\n" + (List.map (fun (_,name,ty) -> + " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty) + cl)) tyl) ^ "." + | NCic.Constant (_,name,None,ty, _) -> + "{"^NUri.string_of_uri u^"}\n"^ + "axiom " ^ name ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ "\n" + | NCic.Constant (_,name,Some bo,ty, _) -> + "{"^NUri.string_of_uri u^"}\n"^ + "definition " ^ name ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^ + ppterm ~metasenv ~subst ~context:[] bo ^ "\n" +;; + let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);; diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 11418eb59..6d8a1b69a 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,3 +1,7 @@ +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicCoercion.cmi: +nCicUnifHint.cmi: nCicUnification.cmi: nCicUnifHint.cmi nCicRefiner.cmi: nCicUnifHint.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index 11418eb59..6d8a1b69a 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,3 +1,7 @@ +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicCoercion.cmi: +nCicUnifHint.cmi: nCicUnification.cmi: nCicUnifHint.cmi nCicRefiner.cmi: nCicUnifHint.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 1cd2e54b9..dd03356c4 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -153,7 +153,11 @@ let rec typeof hdb let _,_,_,ty = NCicUtils.lookup_subst n subst in ty with NCicUtils.Subst_not_found _ -> try let _,_,ty = NCicUtils.lookup_meta n metasenv in - match ty with C.Implicit _ -> assert false | _ -> ty + match ty with C.Implicit _ -> + prerr_endline (string_of_int n); + prerr_endline (NCicPp.ppmetasenv ~subst metasenv); + prerr_endline (NCicPp.ppsubst ~metasenv subst); + assert false | _ -> ty with NCicUtils.Meta_not_found _ -> raise (AssertFailure (lazy (Printf.sprintf "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t)))) diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend new file mode 100644 index 000000000..7333bd37b --- /dev/null +++ b/helm/software/components/ng_tactics/.depend @@ -0,0 +1,3 @@ +nTactics.cmi: +nTactics.cmo: nTactics.cmi +nTactics.cmx: nTactics.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt new file mode 100644 index 000000000..7333bd37b --- /dev/null +++ b/helm/software/components/ng_tactics/.depend.opt @@ -0,0 +1,3 @@ +nTactics.cmi: +nTactics.cmo: nTactics.cmi +nTactics.cmx: nTactics.cmi diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile new file mode 100644 index 000000000..64765023d --- /dev/null +++ b/helm/software/components/ng_tactics/Makefile @@ -0,0 +1,13 @@ +PACKAGE = ng_tactics + +INTERFACE_FILES = \ + nTactics.mli + +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + + +all: + + +include ../../Makefile.defs +include ../Makefile.common diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml new file mode 100644 index 000000000..492e55055 --- /dev/null +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -0,0 +1,219 @@ +(* + ||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 $ *) + +open Printf + +let debug = true +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +exception Error of string lazy_t +let fail msg = raise (Error msg) + +type lowtac_status = { + pstatus : NCic.obj; + lstatus : LexiconEngine.status +} + +type lowtactic = lowtac_status * int -> lowtac_status * int list * int list + +type tac_status = { + gstatus : Continuationals.Stack.t; + istatus : lowtac_status; +} + +type tactic = tac_status -> tac_status + +type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input + +let pp_tac_status status = + prerr_endline (NCicPp.ppobj status.istatus.pstatus) +;; + +open Continuationals.Stack + +let dot_tac status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | ([], _, [], _) :: _ as stack -> + (* backward compatibility: do-nothing-dot *) + stack + | (g, t, k, tag) :: s -> + match filter_open g, k with + | loc :: loc_tl, _ -> + (([ loc ], t, loc_tl @+ k, tag) :: s) + | [], loc :: k -> + assert (is_open loc); + (([ loc ], t, k, tag) :: s) + | _ -> fail (lazy "can't use \".\" here") + in + { status with gstatus = new_gstatus } +;; + +let branch_tac status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | (g, t, k, tag) :: s -> + match init_pos g with (* TODO *) + | [] | [ _ ] -> fail (lazy "too few goals to branch"); + | loc :: loc_tl -> + ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s + in + { status with gstatus = new_gstatus } +;; + +let shift_tac status = + let new_gstatus = + match status.gstatus with + | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + (match g' with + | [] -> fail (lazy "no more goals to shift") + | loc :: loc_tl -> + (([ loc ], t @+ filter_open g @+ k, [],`BranchTag) + :: (loc_tl, t', k', tag) :: s)) + | _ -> fail (lazy "can't shift goals here") + in + { status with gstatus = new_gstatus } +;; + +let pos_tac i_s status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in + ((l_js, t , [],`BranchTag) + :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + | _ -> fail (lazy "can't use relative positioning here") + in + { status with gstatus = new_gstatus } +;; + +let wildcard_tac status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s) + | _ -> fail (lazy "can't use wildcard here") + in + { status with gstatus = new_gstatus } +;; + +let merge_tac status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> + ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | _ -> fail (lazy "can't merge goals here") + in + { status with gstatus = new_gstatus } +;; + +let focus_tac gs status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | s -> assert(gs <> []); + let stack_locs = + let add_l acc _ _ l = if is_open l then l :: acc else acc in + fold ~env:add_l ~cont:add_l ~todo:add_l [] s + in + List.iter + (fun g -> + if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then + fail (lazy (sprintf "goal %d not found (or closed)" g))) + gs; + (zero_pos gs, [], [], `FocusTag) :: deep_close gs s + in + { status with gstatus = new_gstatus } +;; + +let unfocus_tac status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | ([], [], [], `FocusTag) :: s -> s + | _ -> fail (lazy "can't unfocus, some goals are still open") + in + { status with gstatus = new_gstatus } +;; + +let skip_tac status = + let new_gstatus = + match status.gstatus with + | [] -> assert false + | (gl, t, k, tag) :: s -> + let gl = List.map switch_of_loc gl in + if List.exists (function Open _ -> true | Closed _ -> false) gl then + fail (lazy "cannot skip an open goal") + else + ([],t,k,tag) :: s + in + { status with gstatus = new_gstatus } +;; + +let fold_tactic tac status = + match status.gstatus with + | [] -> assert false + | (g, t, k, tag) :: s -> + debug_print (lazy ("context length " ^string_of_int (List.length g))); + let rec aux s go gc = + function + | [] -> s, go, gc + | loc :: loc_tl -> + debug_print (lazy "inner eval tactical"); + let s, go, gc = + if List.exists ((=) (goal_of_loc loc)) gc then + s, go, gc + else + match switch_of_loc loc with + | Closed _ -> fail (lazy "cannot apply to a Closed goal") + | Open n -> + let s, go', gc' = tac (s,n) in + s, (go @- gc') @+ go', gc @+ gc' + in + aux s go gc loc_tl + in + let s0, go0, gc0 = status.istatus, [], [] in + let sn, gon, gcn = aux s0 go0 gc0 g in + debug_print (lazy ("opened: " + ^ String.concat " " (List.map string_of_int gon))); + debug_print (lazy ("closed: " + ^ String.concat " " (List.map string_of_int gcn))); + let stack = + (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s + in + { gstatus = stack; istatus = sn } +;; + + +let apply t (status,goal) = + let _,_,metasenv, subst,_ = status.pstatus in + let _,context,gty = List.assoc goal metasenv in + let metasenv, subst, lexicon_status, t = + GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t + in + prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t); + prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv); + prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv); + prerr_endline "fine napply"; + { status with lstatus = lexicon_status }, [goal], [] +;; + +let apply_tac t = fold_tactic (apply t) ;; + diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli new file mode 100644 index 000000000..831704924 --- /dev/null +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -0,0 +1,46 @@ +(* + ||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 lowtac_status = { + pstatus : NCic.obj; + lstatus : LexiconEngine.status +} + +type lowtactic = lowtac_status * int -> lowtac_status * int list * int list + +type tac_status = { + gstatus : Continuationals.Stack.t; + istatus : lowtac_status; +} + +type tactic = tac_status -> tac_status + +type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input + +val dot_tac: tactic +val branch_tac: tactic +val shift_tac: tactic +val pos_tac: int list -> tactic +val wildcard_tac: tactic +val merge_tac: tactic +val focus_tac: int list -> tactic +val unfocus_tac: tactic +val skip_tac: tactic + +val fold_tactic: lowtactic -> tactic + +val apply_tac: tactic_term -> tactic + + +val pp_tac_status: tac_status -> unit diff --git a/helm/software/components/registry/.depend b/helm/software/components/registry/.depend index cf4f36b68..40c03891a 100644 --- a/helm/software/components/registry/.depend +++ b/helm/software/components/registry/.depend @@ -1,2 +1,3 @@ +helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/registry/.depend.opt b/helm/software/components/registry/.depend.opt index cf4f36b68..40c03891a 100644 --- a/helm/software/components/registry/.depend.opt +++ b/helm/software/components/registry/.depend.opt @@ -1,2 +1,3 @@ +helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt index c0cd9c906..3d7dfc21f 100644 --- a/helm/software/components/syntax_extensions/.depend.opt +++ b/helm/software/components/syntax_extensions/.depend.opt @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index a278f6f08..a9f6e372e 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,11 +1,19 @@ +proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi +proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi +hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi +universe.cmi: autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: +paramodulation/utils.cmi: +closeCoercionGraph.cmi: +paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -25,10 +33,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.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: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index a278f6f08..a9f6e372e 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 @@ -25,10 +33,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.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: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi diff --git a/helm/software/components/tactics/continuationals.ml b/helm/software/components/tactics/continuationals.ml index 044fa45c8..183e8cabf 100644 --- a/helm/software/components/tactics/continuationals.ml +++ b/helm/software/components/tactics/continuationals.ml @@ -117,6 +117,10 @@ struct let of_metasenv metasenv = let goals = List.map (fun (g, _, _) -> g) metasenv in [ zero_pos goals, [], [], `NoTag ] + + let of_nmetasenv metasenv = + let goals = List.map (fun (g, _) -> g) metasenv in + [ zero_pos goals, [], [], `NoTag ] let head_switches = function diff --git a/helm/software/components/tactics/continuationals.mli b/helm/software/components/tactics/continuationals.mli index 277dfe362..12681db63 100644 --- a/helm/software/components/tactics/continuationals.mli +++ b/helm/software/components/tactics/continuationals.mli @@ -42,12 +42,28 @@ sig val find_goal: t -> goal (** find "next" goal *) val is_empty: t -> bool (** a singleton empty level *) val of_metasenv: Cic.metasenv -> t + val of_nmetasenv: (goal * 'a) list -> t val head_switches: t -> switch list (** top level switches *) val head_goals: t -> goal list (** top level goals *) val head_tag: t -> tag (** top level tag *) val shift_goals: t -> goal list (** second level goals *) val open_goals: t -> goal list (** all (Open) goals *) val goal_of_switch: switch -> goal + val filter_open : (goal * switch) list -> (goal * switch) list + val is_open: goal * switch -> bool + val is_fresh: goal * switch -> bool + val init_pos: (goal * switch) list -> (goal * switch) list + val goal_of_loc: goal * switch -> goal + val switch_of_loc: goal * switch -> switch + val zero_pos : goal list -> (goal * switch) list + val deep_close: goal list -> t -> t + + + val ( @+ ) : 'a list -> 'a list -> 'a list + val ( @- ) : 'a list -> 'a list -> 'a list + val ( @~- ) : ('a * switch) list -> goal list -> ('a * switch) list + + (** @param int depth, depth 0 is the top of the stack *) val fold: diff --git a/helm/software/components/thread/.depend b/helm/software/components/thread/.depend index 7759190c6..6616a03d0 100644 --- a/helm/software/components/thread/.depend +++ b/helm/software/components/thread/.depend @@ -1,3 +1,5 @@ +threadSafe.cmi: +extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/thread/.depend.opt b/helm/software/components/thread/.depend.opt index 7759190c6..6616a03d0 100644 --- a/helm/software/components/thread/.depend.opt +++ b/helm/software/components/thread/.depend.opt @@ -1,3 +1,5 @@ +threadSafe.cmi: +extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend index bc310327f..a8972f4cf 100644 --- a/helm/software/components/tptp_grafite/.depend +++ b/helm/software/components/tptp_grafite/.depend @@ -1,4 +1,7 @@ parser.cmi: ast.cmo +tptp2grafite.cmi: +ast.cmo: +ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmo parser.cmi diff --git a/helm/software/components/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt index c74300207..fb60fe8f2 100644 --- a/helm/software/components/tptp_grafite/.depend.opt +++ b/helm/software/components/tptp_grafite/.depend.opt @@ -1,4 +1,7 @@ parser.cmi: ast.cmx +tptp2grafite.cmi: +ast.cmo: +ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmx parser.cmi diff --git a/helm/software/components/urimanager/.depend b/helm/software/components/urimanager/.depend index 482148423..9cac9aa78 100644 --- a/helm/software/components/urimanager/.depend +++ b/helm/software/components/urimanager/.depend @@ -1,2 +1,3 @@ +uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt index 482148423..9cac9aa78 100644 --- a/helm/software/components/urimanager/.depend.opt +++ b/helm/software/components/urimanager/.depend.opt @@ -1,2 +1,3 @@ +uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/whelp/.depend b/helm/software/components/whelp/.depend index 39f37dfa9..65dc07955 100644 --- a/helm/software/components/whelp/.depend +++ b/helm/software/components/whelp/.depend @@ -1,3 +1,5 @@ +whelp.cmi: +fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt index 39f37dfa9..65dc07955 100644 --- a/helm/software/components/whelp/.depend.opt +++ b/helm/software/components/whelp/.depend.opt @@ -1,3 +1,5 @@ +whelp.cmi: +fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/xml/.depend b/helm/software/components/xml/.depend index 5ef59bdc9..e7e7ffbd7 100644 --- a/helm/software/components/xml/.depend +++ b/helm/software/components/xml/.depend @@ -1,3 +1,5 @@ +xml.cmi: +xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xml/.depend.opt b/helm/software/components/xml/.depend.opt index 5ef59bdc9..e7e7ffbd7 100644 --- a/helm/software/components/xml/.depend.opt +++ b/helm/software/components/xml/.depend.opt @@ -1,3 +1,5 @@ +xml.cmi: +xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xmldiff/.depend b/helm/software/components/xmldiff/.depend index e2832de33..65bd7b949 100644 --- a/helm/software/components/xmldiff/.depend +++ b/helm/software/components/xmldiff/.depend @@ -1,2 +1,3 @@ +xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt index e2832de33..65bd7b949 100644 --- a/helm/software/components/xmldiff/.depend.opt +++ b/helm/software/components/xmldiff/.depend.opt @@ -1,2 +1,3 @@ +xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi