From dd627e471392375ca7b6dad78a931a8682e06dbe Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Sat, 13 Apr 2019 17:32:48 +0200 Subject: [PATCH] Many changes Change auto_params in grafiteAst.ml from being abstract on the 'term list to being concretized to nterm list. Modify type just accordingly. Modify ntactic types accordingly. Add ExistsElim, AndElim, RewritingStep, Thesisbecomes types to ntactic. Add pretty printing for ExistsElim, AndElim, RewritingStep, Thesisbecomes. Add calls in grafite engine for the implementation of ExistsElim, AndElim, Thesisbecomes. Add parsing rule for the "let x := t" tactic. It uses the NLetIn ntactic. Add parsing rules for Thesisbecomes and Rewritingstep (conclude, obtain and =). Modify mk_just to use the new auto_lowtac entry point for automation for LCF-like tactics. Remove same_type function in declarative.ml. Add are_convertible function in declarative that uses beta-conversion. Add a lambda_abstract tactic that abstracts the common parts of suppose and assume. Add 3 Exception types for this tactic to handle error situations. Modify assume and suppose accordingly Add assert_tac that verifies that a given term is the same as the conclusion and that two given types are beta-convertible, if a second type is given. If all checks pass a continuation is exec'd, otherwise an exception is raised. Modify we_need_to_prove, by_just_we_proved to use assert_tac. Add implementation of thesisbecomes. Add implementation of existselim and andelim. Modify declarative signature to add the new tactics. Add a flag to index_local_equations and index_local_equations2 to inhibit the use of global candidates. Modify all the functions that call these two functions and the calls to those functions accordingly (auto_main, do_something, top_cache, intros, auto_clusters) Add a flag to auto_tac' to specify whether to use local candidates or not. Modify the part where the local cands are calculated to check the flag before proceeding. Add auto_params to nnAuto. Modify auto_tac to auto_tac' which takes the candidates to use explicitly as a parameter and two flags that indicate whether to use local candidates and whether to use only the given candidates. Add a candidates_from_ctx function to calculate the candidates in a given context. Add a auto_lowtac entry point for LCF-like tactics. Modify nnAuto signature to use auto_params instead of its explicit version (nterm list * (string * string) list). Add new "keywords" to matita.lang. Add debug prints for a bug where the program would freeze. (They can probably be removed) --- matita/components/content/.depend | 14 +- matita/components/content_pres/.depend | 48 +-- matita/components/disambiguation/.depend | 8 +- matita/components/extlib/.depend | 32 +- matita/components/getter/.depend | 54 +-- matita/components/grafite/.depend | 2 +- matita/components/grafite/grafiteAst.ml | 21 +- matita/components/grafite/grafiteAstPp.ml | 26 +- matita/components/grafite_engine/.depend | 12 +- .../grafite_engine/grafiteEngine.ml | 13 +- matita/components/grafite_parser/.depend | 4 +- .../grafite_parser/grafiteParser.ml | 40 +- matita/components/library/.depend | 10 +- matita/components/logger/.depend | 2 +- matita/components/ng_cic_content/.depend | 6 +- matita/components/ng_disambiguation/.depend | 16 +- matita/components/ng_extraction/.depend | 36 +- matita/components/ng_kernel/.depend | 46 +-- matita/components/ng_library/.depend | 2 +- matita/components/ng_paramodulation/.depend | 66 ++-- matita/components/ng_refiner/.depend | 34 +- matita/components/ng_tactics/.depend | 39 +- matita/components/ng_tactics/declarative.ml | 367 +++++++++++------ matita/components/ng_tactics/declarative.mli | 7 +- matita/components/ng_tactics/nTacStatus.ml | 9 + matita/components/ng_tactics/nTacStatus.mli | 2 + matita/components/ng_tactics/nTactics.mli | 1 + matita/components/ng_tactics/nnAuto.ml | 371 ++++++++++-------- matita/components/ng_tactics/nnAuto.mli | 18 +- matita/components/registry/.depend | 2 +- matita/components/thread/.depend | 6 +- matita/components/xml/.depend | 4 +- .../matita/help/C/sec_declarative_tactics.xml | 2 - matita/matita/matita.lang | 5 + matita/matita/matitaGui.ml | 10 +- 35 files changed, 800 insertions(+), 535 deletions(-) diff --git a/matita/components/content/.depend b/matita/components/content/.depend index e1dff0f85..369dbbdc4 100644 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@ -1,14 +1,14 @@ -content.cmo : content.cmi -content.cmx : content.cmi content.cmi : -notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi -notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi +notationUtil.cmi : notationPt.cmo notationEnv.cmi : notationPt.cmo -notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi -notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi notationPp.cmi : notationPt.cmo notationEnv.cmi notationPt.cmo : notationPt.cmx : +content.cmo : content.cmi +content.cmx : content.cmi notationUtil.cmo : notationPt.cmo notationUtil.cmi notationUtil.cmx : notationPt.cmx notationUtil.cmi -notationUtil.cmi : notationPt.cmo +notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi +notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi +notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi diff --git a/matita/components/content_pres/.depend b/matita/components/content_pres/.depend index c4875d55f..4deb6e591 100644 --- a/matita/components/content_pres/.depend +++ b/matita/components/content_pres/.depend @@ -1,38 +1,38 @@ -box.cmo : renderingAttrs.cmi box.cmi -box.cmx : renderingAttrs.cmx box.cmi +renderingAttrs.cmi : +cicNotationLexer.cmi : +cicNotationParser.cmi : +mpresentation.cmi : box.cmi : -boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ - boxPp.cmi -boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ - boxPp.cmi +content2presMatcher.cmi : +termContentPres.cmi : cicNotationParser.cmi boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi +cicNotationPres.cmi : mpresentation.cmi box.cmi +content2pres.cmi : termContentPres.cmi cicNotationPres.cmi +renderingAttrs.cmo : renderingAttrs.cmi +renderingAttrs.cmx : renderingAttrs.cmi cicNotationLexer.cmo : cicNotationLexer.cmi cicNotationLexer.cmx : cicNotationLexer.cmi -cicNotationLexer.cmi : cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi -cicNotationParser.cmi : +mpresentation.cmo : mpresentation.cmi +mpresentation.cmx : mpresentation.cmi +box.cmo : renderingAttrs.cmi box.cmi +box.cmx : renderingAttrs.cmx box.cmi +content2presMatcher.cmo : content2presMatcher.cmi +content2presMatcher.cmx : content2presMatcher.cmi +termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \ + cicNotationParser.cmi termContentPres.cmi +termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ + cicNotationParser.cmx termContentPres.cmi +boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ + boxPp.cmi +boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ + boxPp.cmi cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \ cicNotationPres.cmi cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ cicNotationPres.cmi -cicNotationPres.cmi : mpresentation.cmi box.cmi content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -content2pres.cmi : termContentPres.cmi cicNotationPres.cmi -content2presMatcher.cmo : content2presMatcher.cmi -content2presMatcher.cmx : content2presMatcher.cmi -content2presMatcher.cmi : -mpresentation.cmo : mpresentation.cmi -mpresentation.cmx : mpresentation.cmi -mpresentation.cmi : -renderingAttrs.cmo : renderingAttrs.cmi -renderingAttrs.cmx : renderingAttrs.cmi -renderingAttrs.cmi : -termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \ - cicNotationParser.cmi termContentPres.cmi -termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi -termContentPres.cmi : cicNotationParser.cmi diff --git a/matita/components/disambiguation/.depend b/matita/components/disambiguation/.depend index a25280569..735bea7f7 100644 --- a/matita/components/disambiguation/.depend +++ b/matita/components/disambiguation/.depend @@ -1,11 +1,11 @@ -disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi +disambiguateTypes.cmi : disambiguate.cmi : disambiguateTypes.cmi +multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo : disambiguateTypes.cmi disambiguateTypes.cmx : disambiguateTypes.cmi -disambiguateTypes.cmi : +disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \ multiPassDisambiguator.cmi multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \ multiPassDisambiguator.cmi -multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi diff --git a/matita/components/extlib/.depend b/matita/components/extlib/.depend index 36dd894f0..e7b0a3bc7 100644 --- a/matita/components/extlib/.depend +++ b/matita/components/extlib/.depend @@ -1,27 +1,27 @@ -componentsConf.cmo : componentsConf.cmi -componentsConf.cmx : componentsConf.cmi componentsConf.cmi : -discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi -discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi +hExtlib.cmi : +hMarshal.cmi : +patternMatcher.cmi : +hLog.cmi : +trie.cmi : discrimination_tree.cmi : -graphvizPp.cmo : graphvizPp.cmi -graphvizPp.cmx : graphvizPp.cmi +hTopoSort.cmi : graphvizPp.cmi : +componentsConf.cmo : componentsConf.cmi +componentsConf.cmx : componentsConf.cmi hExtlib.cmo : hExtlib.cmi hExtlib.cmx : hExtlib.cmi -hExtlib.cmi : -hLog.cmo : hLog.cmi -hLog.cmx : hLog.cmi -hLog.cmi : hMarshal.cmo : hExtlib.cmi hMarshal.cmi hMarshal.cmx : hExtlib.cmx hMarshal.cmi -hMarshal.cmi : -hTopoSort.cmo : hTopoSort.cmi -hTopoSort.cmx : hTopoSort.cmi -hTopoSort.cmi : patternMatcher.cmo : patternMatcher.cmi patternMatcher.cmx : patternMatcher.cmi -patternMatcher.cmi : +hLog.cmo : hLog.cmi +hLog.cmx : hLog.cmi trie.cmo : trie.cmi trie.cmx : trie.cmi -trie.cmi : +discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi +discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi +hTopoSort.cmo : hTopoSort.cmi +hTopoSort.cmx : hTopoSort.cmi +graphvizPp.cmo : graphvizPp.cmi +graphvizPp.cmx : graphvizPp.cmi diff --git a/matita/components/getter/.depend b/matita/components/getter/.depend index 13ca8cc29..59c0b896e 100644 --- a/matita/components/getter/.depend +++ b/matita/components/getter/.depend @@ -1,38 +1,38 @@ -http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \ - http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ - http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ - http_getter.cmi -http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter.cmi -http_getter.cmi : http_getter_types.cmo -http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi -http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi +http_getter_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 +http_getter_logger.cmx : http_getter_logger.cmi +http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi +http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi http_getter_const.cmo : http_getter_const.cmi http_getter_const.cmx : http_getter_const.cmi -http_getter_const.cmi : http_getter_env.cmo : http_getter_types.cmo http_getter_misc.cmi \ http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi -http_getter_env.cmi : http_getter_types.cmo -http_getter_logger.cmo : http_getter_logger.cmi -http_getter_logger.cmx : http_getter_logger.cmi -http_getter_logger.cmi : -http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi -http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi -http_getter_misc.cmi : http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmo \ http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_storage.cmi : -http_getter_types.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_wget.cmi : +http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \ + http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi +http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ + http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi +http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \ + http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ + http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ + http_getter.cmi +http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ + http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ + http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ + http_getter.cmi diff --git a/matita/components/grafite/.depend b/matita/components/grafite/.depend index 211eff733..e70c83c77 100644 --- a/matita/components/grafite/.depend +++ b/matita/components/grafite/.depend @@ -1,5 +1,5 @@ +grafiteAstPp.cmi : grafiteAst.cmo grafiteAst.cmo : grafiteAst.cmx : grafiteAstPp.cmo : grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi -grafiteAstPp.cmi : grafiteAst.cmo diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index ed757f601..c15414df5 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -36,10 +36,7 @@ type npattern = type auto_params = nterm list option * (string*string) list -(* The additional a is for abstract *) -type 'term aauto_params = 'term list option * (string*string) list - -type 'term just = [`Term of 'term | `Auto of 'term aauto_params] +type just = [`Term of nterm | `Auto of auto_params] type ntactic = | NApply of loc * nterm @@ -84,15 +81,19 @@ type ntactic = (* Not the best idea to use a string directly, an abstract type for identifiers would be better *) | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *) | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *) - | By_just_we_proved of loc * nterm just * nterm * string option * nterm option (* loc, + | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc, justification, conclusion, identifier, eqconcl *) | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion, identifier, equivnewcon *) - | Bydone of loc * nterm just - (* - | ExistsElim of loc * nterm just * string * nterm * nterm * string - | AndElim of loc * nterm just * nterm * string * nterm * string - *) + | Bydone of loc * just + | ExistsElim of loc * just * string * nterm * nterm * string + | AndElim of loc * just * nterm * string * nterm * string + | RewritingStep of + loc * (string option * nterm) option * nterm * + [ `Term of nterm | `Auto of (string*string) list + | `Proof | `SolveWith of nterm ] * + bool (* last step*) + | Thesisbecomes of loc * nterm * nterm option type nmacro = | NCheck of loc * nterm diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 4e685c26d..9e08fb3b5 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -131,11 +131,27 @@ let rec pp_ntactic status ~map_unicode_to_tex = (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match term1 with None -> " " | Some t1 -> "or equivalently" ^ NotationPp.pp_term status t1) | Bydone (_, just) -> pp_just status just ^ "done" - (* - | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" - ^ NotationPp.pp_term term ^ "such that " ^ NotationPp.pp_term term1 ^ "(" ^ ident1 ^ ")" - | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just ~NotationPp.pp_term just ^ "we have " ^ NotationPp.pp_term term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term term2 ^ " (" ^ ident2 ^ ")" - *) + | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":" + ^ NotationPp.pp_term status term ^ "such that " ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")" + | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^ + NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2 + ^ " (" ^ ident2 ^ ")" + | Thesisbecomes (_, term1, term2) -> "the thesis becomes " ^ NotationPp.pp_term status term1 ^ (match + term2 with None -> " " | Some term2 -> NotationPp.pp_term status term2) + | RewritingStep (_, term, term1, term2, cont) -> + (match term with + | None -> " " + | Some (None,term) -> "conclude " ^ NotationPp.pp_term status term + | Some (Some name,term) -> + "obtain (" ^ name ^ ") " ^ NotationPp.pp_term status term) + ^ "=" ^ + NotationPp.pp_term status term1 ^ + (match term2 with + | `Auto params -> pp_auto_params (None,params) status + | `Term term2 -> " exact " ^ NotationPp.pp_term status term2 + | `Proof -> " proof" + | `SolveWith term -> " using " ^ NotationPp.pp_term status term) + ^ (if cont then " done" else "") ;; let pp_nmacro status = function diff --git a/matita/components/grafite_engine/.depend b/matita/components/grafite_engine/.depend index 627227c70..e6d4942c6 100644 --- a/matita/components/grafite_engine/.depend +++ b/matita/components/grafite_engine/.depend @@ -1,11 +1,11 @@ -grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \ - grafiteEngine.cmi -grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ - grafiteEngine.cmi +grafiteTypes.cmi : +nCicCoercDeclaration.cmi : grafiteTypes.cmi grafiteEngine.cmi : grafiteTypes.cmi grafiteTypes.cmo : grafiteTypes.cmi grafiteTypes.cmx : grafiteTypes.cmi -grafiteTypes.cmi : nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmi : grafiteTypes.cmi +grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \ + grafiteEngine.cmi +grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ + grafiteEngine.cmi diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 9dd266ed9..387468f19 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -501,11 +501,16 @@ let eval_ng_tac tac = |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2)) | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len) - (* | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) -> - Declarative.existselim just id1 t1 t2 id2 - | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> - Declarative.andelim just t1 id1 t2 id2 + Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1) + (text,prefix_len,t2) id2 + | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just + text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2 + | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1) + (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2))) + (* + | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> + Declarative.rewritingstep termine (text,prefix_len,t1) t2 cont *) in aux aux tac (* trick for non uniform recursion call *) diff --git a/matita/components/grafite_parser/.depend b/matita/components/grafite_parser/.depend index fcb901973..752b0d88d 100644 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@ -1,6 +1,6 @@ +grafiteParser.cmi : +print_grammar.cmi : grafiteParser.cmi grafiteParser.cmo : grafiteParser.cmi grafiteParser.cmx : grafiteParser.cmi -grafiteParser.cmi : print_grammar.cmo : print_grammar.cmi print_grammar.cmx : print_grammar.cmi -print_grammar.cmi : grafiteParser.cmi diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 803051e69..714cb4826 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -243,6 +243,8 @@ EXTEND IDENT "equivalent"; "to"; t' = tactic_term -> t']-> G.NTactic (loc,[G.Assume (loc,id,t,t1)]) | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT "is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)]) + | "let"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + G.NTactic(loc,[G.NLetIn (loc,(None,[],Some N.UserInput),t,name)]) | just = [ IDENT "using"; t=tactic_term -> `Term t | params = auto_params -> @@ -260,14 +262,48 @@ EXTEND BYC_done -> G.Bydone (loc, just) | BYC_weproved (ty,id,t1) -> G.By_just_we_proved(loc, just, ty, id, t1) - (* | BYC_letsuchthat (id1,t1,t2,id2) -> G.ExistsElim (loc, just, id1, t1, t2, id2) | BYC_wehaveand (id1,t1,id2,t2) -> - G.AndElim (loc, just, id1, t1, id2, t2)*)) + G.AndElim (loc, just, t1, id1, t2, id2)) ]) | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)]) + | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT + "equivalently"; t2 = tactic_term -> t2] -> + G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)]) + (* DO NOT FACTORIZE with the two following, camlp5 sucks*) + | IDENT "conclude"; + termine = tactic_term; + SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> let _,params = params in `Auto params]; + cont = rewriting_step_continuation -> + G.NTactic (loc,[G.RewritingStep(loc, Some (None,termine), t1, t2, cont)]) + | IDENT "obtain" ; name = IDENT; + termine = tactic_term; + SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> let _,params = params in `Auto params]; + cont = rewriting_step_continuation -> + G.NTactic(loc,[G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)]) + | SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> let _,params = params in `Auto params]; + cont = rewriting_step_continuation -> + G.NTactic(loc,[G.RewritingStep(loc, None, t1, t2, cont)]) ] ]; auto_fixed_param: [ diff --git a/matita/components/library/.depend b/matita/components/library/.depend index 7af1a906e..6f2769b94 100644 --- a/matita/components/library/.depend +++ b/matita/components/library/.depend @@ -1,9 +1,9 @@ -librarian.cmo : librarian.cmi -librarian.cmx : librarian.cmi librarian.cmi : -libraryClean.cmo : libraryClean.cmi -libraryClean.cmx : libraryClean.cmi +libraryMisc.cmi : libraryClean.cmi : +librarian.cmo : librarian.cmi +librarian.cmx : librarian.cmi libraryMisc.cmo : libraryMisc.cmi libraryMisc.cmx : libraryMisc.cmi -libraryMisc.cmi : +libraryClean.cmo : libraryClean.cmi +libraryClean.cmx : libraryClean.cmi diff --git a/matita/components/logger/.depend b/matita/components/logger/.depend index a22bd16f1..d1b4c3716 100644 --- a/matita/components/logger/.depend +++ b/matita/components/logger/.depend @@ -1,3 +1,3 @@ +helmLogger.cmi : helmLogger.cmo : helmLogger.cmi helmLogger.cmx : helmLogger.cmi -helmLogger.cmi : diff --git a/matita/components/ng_cic_content/.depend b/matita/components/ng_cic_content/.depend index 579a21e33..01e2f5b1e 100644 --- a/matita/components/ng_cic_content/.depend +++ b/matita/components/ng_cic_content/.depend @@ -1,6 +1,6 @@ -interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi +ncic2astMatcher.cmi : interpretations.cmi : ncic2astMatcher.cmo : ncic2astMatcher.cmi ncic2astMatcher.cmx : ncic2astMatcher.cmi -ncic2astMatcher.cmi : +interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend index fa8349c58..79fd839b2 100644 --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@ -1,14 +1,14 @@ +nnumber_notation.cmi : +disambiguateChoices.cmi : +nCicDisambiguate.cmi : +grafiteDisambiguate.cmi : +nnumber_notation.cmo : nnumber_notation.cmi +nnumber_notation.cmx : nnumber_notation.cmi disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi -disambiguateChoices.cmi : +nCicDisambiguate.cmo : nCicDisambiguate.cmi +nCicDisambiguate.cmx : nCicDisambiguate.cmi grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \ grafiteDisambiguate.cmi grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ grafiteDisambiguate.cmi -grafiteDisambiguate.cmi : -nCicDisambiguate.cmo : nCicDisambiguate.cmi -nCicDisambiguate.cmx : nCicDisambiguate.cmi -nCicDisambiguate.cmi : -nnumber_notation.cmo : nnumber_notation.cmi -nnumber_notation.cmx : nnumber_notation.cmi -nnumber_notation.cmi : diff --git a/matita/components/ng_extraction/.depend b/matita/components/ng_extraction/.depend index f4d034d1b..c2ad6ff86 100644 --- a/matita/components/ng_extraction/.depend +++ b/matita/components/ng_extraction/.depend @@ -1,34 +1,34 @@ +nCicExtraction.cmi : +coq.cmi : +ocamlExtractionTable.cmi : miniml.cmo coq.cmi +mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi +common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi +extraction.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi +ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi +ocamlExtraction.cmi : ocamlExtractionTable.cmi +miniml.cmo : coq.cmi +miniml.cmx : coq.cmx +nCicExtraction.cmo : nCicExtraction.cmi +nCicExtraction.cmx : nCicExtraction.cmi +coq.cmo : coq.cmi +coq.cmx : coq.cmi +ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi +ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi +mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi +mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ common.cmi common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ common.cmi -common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi -coq.cmo : coq.cmi -coq.cmx : coq.cmi -coq.cmi : extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ common.cmi extraction.cmi extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ common.cmx extraction.cmi -extraction.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi -miniml.cmo : coq.cmi -miniml.cmx : coq.cmx -mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi -mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi -mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi -nCicExtraction.cmo : nCicExtraction.cmi -nCicExtraction.cmx : nCicExtraction.cmi -nCicExtraction.cmi : ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ common.cmi ocaml.cmi ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ common.cmx ocaml.cmi -ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \ coq.cmi ocamlExtraction.cmi ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ coq.cmx ocamlExtraction.cmi -ocamlExtraction.cmi : ocamlExtractionTable.cmi -ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi -ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi -ocamlExtractionTable.cmi : miniml.cmo coq.cmi diff --git a/matita/components/ng_kernel/.depend b/matita/components/ng_kernel/.depend index 16e1dcf8e..a55f87284 100644 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@ -1,41 +1,41 @@ +nUri.cmi : +nReference.cmi : nUri.cmi +nCicUtils.cmi : nCic.cmo +nCicSubstitution.cmi : nCic.cmo +nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmo +nCicReduction.cmi : nCic.cmo +nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo +nCicUntrusted.cmi : nCic.cmo +nCicPp.cmi : nReference.cmi nCic.cmo nCic.cmo : nUri.cmi nReference.cmi nCic.cmx : nUri.cmx nReference.cmx +nUri.cmo : nUri.cmi +nUri.cmx : nUri.cmi +nReference.cmo : nUri.cmi nReference.cmi +nReference.cmx : nUri.cmx nReference.cmi +nCicUtils.cmo : nReference.cmi nCic.cmo nCicUtils.cmi +nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi +nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmo \ + nCicSubstitution.cmi +nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \ + nCicSubstitution.cmi nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi -nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmo -nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ - nCicEnvironment.cmi nCic.cmo nCicPp.cmi -nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi -nCicPp.cmi : nReference.cmi nCic.cmo nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicEnvironment.cmi nCic.cmo nCicReduction.cmi nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicEnvironment.cmx nCic.cmx nCicReduction.cmi -nCicReduction.cmi : nCic.cmo -nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmo \ - nCicSubstitution.cmi -nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \ - nCicSubstitution.cmi -nCicSubstitution.cmi : nCic.cmo nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \ nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \ nCicTypeChecker.cmi nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ nCicTypeChecker.cmi -nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicUntrusted.cmi : nCic.cmo -nCicUtils.cmo : nReference.cmi nCic.cmo nCicUtils.cmi -nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi -nCicUtils.cmi : nCic.cmo -nReference.cmo : nUri.cmi nReference.cmi -nReference.cmx : nUri.cmx nReference.cmi -nReference.cmi : nUri.cmi -nUri.cmo : nUri.cmi -nUri.cmx : nUri.cmi -nUri.cmi : +nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ + nCicEnvironment.cmi nCic.cmo nCicPp.cmi +nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ + nCicEnvironment.cmx nCic.cmx nCicPp.cmi diff --git a/matita/components/ng_library/.depend b/matita/components/ng_library/.depend index d10bc6762..a571a865c 100644 --- a/matita/components/ng_library/.depend +++ b/matita/components/ng_library/.depend @@ -1,3 +1,3 @@ +nCicLibrary.cmi : nCicLibrary.cmo : nCicLibrary.cmi nCicLibrary.cmx : nCicLibrary.cmi -nCicLibrary.cmi : diff --git a/matita/components/ng_paramodulation/.depend b/matita/components/ng_paramodulation/.depend index 1ee59514d..5f4f1cc56 100644 --- a/matita/components/ng_paramodulation/.depend +++ b/matita/components/ng_paramodulation/.depend @@ -1,45 +1,45 @@ -foSubst.cmo : terms.cmi foSubst.cmi -foSubst.cmx : terms.cmx foSubst.cmi +terms.cmi : +pp.cmi : terms.cmi foSubst.cmi : terms.cmi -foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi +orderings.cmi : terms.cmi +foUtils.cmi : terms.cmi orderings.cmi foUnif.cmi : terms.cmi orderings.cmi +index.cmi : terms.cmi orderings.cmi +superposition.cmi : terms.cmi orderings.cmi index.cmi +stats.cmi : terms.cmi orderings.cmi +paramod.cmi : terms.cmi orderings.cmi +nCicBlob.cmi : terms.cmi +nCicProof.cmi : terms.cmi +nCicParamod.cmi : terms.cmi +terms.cmo : terms.cmi +terms.cmx : terms.cmi +pp.cmo : terms.cmi pp.cmi +pp.cmx : terms.cmx pp.cmi +foSubst.cmo : terms.cmi foSubst.cmi +foSubst.cmx : terms.cmx foSubst.cmi +orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi +orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUtils.cmi : terms.cmi orderings.cmi +foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi -index.cmi : terms.cmi orderings.cmi +superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ + foUnif.cmi foSubst.cmi superposition.cmi +superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ + foUnif.cmx foSubst.cmx superposition.cmi +stats.cmo : terms.cmi stats.cmi +stats.cmx : terms.cmx stats.cmi +paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ + foUtils.cmi foUnif.cmi paramod.cmi +paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ + foUtils.cmx foUnif.cmx paramod.cmi nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi -nCicBlob.cmi : terms.cmi +nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi +nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ nCicBlob.cmi nCicParamod.cmi nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ nCicBlob.cmx nCicParamod.cmi -nCicParamod.cmi : terms.cmi -nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi -nCicProof.cmi : terms.cmi -orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi -orderings.cmi : terms.cmi -paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -paramod.cmi : terms.cmi orderings.cmi -pp.cmo : terms.cmi pp.cmi -pp.cmx : terms.cmx pp.cmi -pp.cmi : terms.cmi -stats.cmo : terms.cmi stats.cmi -stats.cmx : terms.cmx stats.cmi -stats.cmi : terms.cmi orderings.cmi -superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi -superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -terms.cmo : terms.cmi -terms.cmx : terms.cmi -terms.cmi : diff --git a/matita/components/ng_refiner/.depend b/matita/components/ng_refiner/.depend index 2bd075dfc..d8295760a 100644 --- a/matita/components/ng_refiner/.depend +++ b/matita/components/ng_refiner/.depend @@ -1,27 +1,27 @@ +nDiscriminationTree.cmi : +nCicMetaSubst.cmi : +nCicUnifHint.cmi : +nCicCoercion.cmi : nCicUnifHint.cmi +nCicRefineUtil.cmi : +nCicUnification.cmi : nCicCoercion.cmi +nCicRefiner.cmi : nCicCoercion.cmi +nDiscriminationTree.cmo : nDiscriminationTree.cmi +nDiscriminationTree.cmx : nDiscriminationTree.cmi +nCicMetaSubst.cmo : nCicMetaSubst.cmi +nCicMetaSubst.cmx : nCicMetaSubst.cmi +nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \ + nCicUnifHint.cmi +nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ + nCicUnifHint.cmi nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \ nCicMetaSubst.cmi nCicCoercion.cmi nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ nCicMetaSubst.cmx nCicCoercion.cmi -nCicCoercion.cmi : nCicUnifHint.cmi -nCicMetaSubst.cmo : nCicMetaSubst.cmi -nCicMetaSubst.cmx : nCicMetaSubst.cmi -nCicMetaSubst.cmi : nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicRefineUtil.cmi : +nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi +nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ nCicCoercion.cmi nCicRefiner.cmi nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ nCicCoercion.cmx nCicRefiner.cmi -nCicRefiner.cmi : nCicCoercion.cmi -nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \ - nCicUnifHint.cmi -nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ - nCicUnifHint.cmi -nCicUnifHint.cmi : -nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicUnification.cmi : nCicCoercion.cmi -nDiscriminationTree.cmo : nDiscriminationTree.cmi -nDiscriminationTree.cmx : nDiscriminationTree.cmi -nDiscriminationTree.cmi : diff --git a/matita/components/ng_tactics/.depend b/matita/components/ng_tactics/.depend index 90de5733d..5196eed7d 100644 --- a/matita/components/ng_tactics/.depend +++ b/matita/components/ng_tactics/.depend @@ -1,30 +1,33 @@ -continuationals.cmo : continuationals.cmi -continuationals.cmx : continuationals.cmi continuationals.cmi : -nCicElim.cmo : nCicElim.cmi -nCicElim.cmx : nCicElim.cmi -nCicElim.cmi : -nCicTacReduction.cmo : nCicTacReduction.cmi -nCicTacReduction.cmx : nCicTacReduction.cmi nCicTacReduction.cmi : -nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ - nDestructTac.cmi -nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ - nDestructTac.cmi +nTacStatus.cmi : continuationals.cmi +nCicElim.cmi : +nTactics.cmi : nTacStatus.cmi +nnAuto.cmi : nTacStatus.cmi +declarative.cmi : nnAuto.cmi nTacStatus.cmi nDestructTac.cmi : nTacStatus.cmi -nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \ - continuationals.cmi nInversion.cmi -nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ - continuationals.cmx nInversion.cmi nInversion.cmi : nTacStatus.cmi +continuationals.cmo : continuationals.cmi +continuationals.cmx : continuationals.cmi +nCicTacReduction.cmo : nCicTacReduction.cmi +nCicTacReduction.cmx : nCicTacReduction.cmi nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi -nTacStatus.cmi : continuationals.cmi +nCicElim.cmo : nCicElim.cmi +nCicElim.cmx : nCicElim.cmi nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi -nTactics.cmi : nTacStatus.cmi nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ continuationals.cmi nnAuto.cmi nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ continuationals.cmx nnAuto.cmi -nnAuto.cmi : nTacStatus.cmi +declarative.cmo : nnAuto.cmi nTactics.cmi nTacStatus.cmi declarative.cmi +declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx declarative.cmi +nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ + nDestructTac.cmi +nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ + nDestructTac.cmi +nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \ + continuationals.cmi nInversion.cmi +nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ + continuationals.cmx nInversion.cmi diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index eb0966570..ac521186a 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -27,13 +27,18 @@ module Ast = NotationPt open NTactics open NTacStatus -type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_params ] +type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ] let mk_just = function - `Auto (l,params) -> NnAuto.auto_tac ~params:(l,params) ?trace_ref:None + `Auto (l,params) -> distribute_tac (fun status goal -> NnAuto.auto_lowtac + ~params:(l,params) status goal) | `Term t -> apply_tac t +exception NotAProduct +exception FirstTypeWrong +exception NotEquivalentTypes + let extract_conclusion_type status goal = let gty = get_goalty status goal in let ctx = ctx_of gty in @@ -53,66 +58,72 @@ let same_type_as_conclusion ty t status goal = false ;; -let same_type t1 t2 status goal = +let are_convertible ty1 ty2 status goal = let gty = get_goalty status goal in let ctx = ctx_of gty in - let status1,cicterm1 = disambiguate status ctx t1 `XTNone in - let status1,term1 = term_of_cic_term status cicterm1 (ctx_of cicterm1) in - let status2,cicterm2 = disambiguate status ctx t2 `XTNone in - let status2,term2 = term_of_cic_term status cicterm2 (ctx_of cicterm2) in - let (_,_,metasenv,subst,_) = status#obj in - if NCicReduction.alpha_eq status1 metasenv subst ctx term1 term2 then - true - else - false -;; + let status,cicterm1 = disambiguate status ctx ty1 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in + let status,cicterm2 = disambiguate status ctx ty2 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in + NTacStatus.are_convertible status ctx cicterm1 cicterm2 + +(* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that +the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with +\lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ? +*) +let lambda_abstract_tac id t1 t2 status goal = + match extract_conclusion_type status goal with + | NCic.Prod (_,t,_) -> + if same_type_as_conclusion t1 t status goal then + match t2 with + | None -> + let (_,_,t1) = t1 in + exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit + `JustOne)))) status goal + + | Some t2 -> + let status,res = are_convertible t1 t2 status goal in + if res then + let (_,_,t2) = t2 in + exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit + `JustOne)))) status goal + else + raise NotEquivalentTypes + else + raise FirstTypeWrong + | _ -> raise NotAProduct let assume name ty eqty = distribute_tac (fun status goal -> - match extract_conclusion_type status goal with - | NCic.Prod (_,t,_) -> - if same_type_as_conclusion ty t status goal then - match eqty with - | None -> - let (_,_,ty) = ty in - exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit - `JustOne)))) status goal - - | Some eqty -> - if same_type ty eqty status goal then - let (_,_,eqty) = eqty in - exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some eqty),Ast.Implicit - `JustOne)))) status goal - else - fail (lazy "The two given types are not equivalent") - else - fail (lazy "The assumed type is wrong") - | _ -> fail (lazy "You can't assume without an universal quantification") - ) + try lambda_abstract_tac name ty eqty status goal + with + | NotAProduct -> fail (lazy "You can't assume without an universal quantification") + | FirstTypeWrong -> fail (lazy "The assumed type is wrong") + | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent") + ) ;; let suppose t1 id t2 = distribute_tac (fun status goal -> - match extract_conclusion_type status goal with - | NCic.Prod (_,t,_) -> - if same_type_as_conclusion t1 t status goal then - match t2 with - | None -> - let (_,_,t1) = t1 in - exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit - `JustOne)))) status goal - - | Some t2 -> - if same_type t1 t2 status goal then - let (_,_,t2) = t2 in - exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit - `JustOne)))) status goal - else - fail (lazy "The two given proposition are not equivalent") + try lambda_abstract_tac id t1 t2 status goal + with + | NotAProduct -> fail (lazy "You can't suppose without a logical implication") + | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise") + | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent") + ) +;; + +let assert_tac t1 t2 status goal continuation = + let t = extract_conclusion_type status goal in + if same_type_as_conclusion t1 t status goal then + match t2 with + | None -> exec continuation status goal + | Some t2 -> + let status,res = are_convertible t1 t2 status goal in + if res then + exec continuation status goal else - fail (lazy "The supposed proposition is different from the premise") - | _ -> fail (lazy "You can't suppose without a logical implication") - ) + raise NotEquivalentTypes + else + raise FirstTypeWrong let we_need_to_prove t id t1 = distribute_tac (fun status goal -> @@ -120,90 +131,214 @@ let we_need_to_prove t id t1 = | None -> ( match t1 with - (* Change the conclusion of the sequent with t *) - (* Is the pattern correct? Probably not *) | None -> (* We need to prove t *) - exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t) status goal + ( + try + assert_tac t None status goal id_tac + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + ) | Some t1 -> (* We need to prove t or equivalently t1 *) - if same_type t1 t status goal then - exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1) status goal - else - fail (lazy "The two conclusions are not equivalent") + ( + try + assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1) + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") + ) ) | Some id -> ( - let (_,_,npt_t) = t in match t1 with | None -> (* We need to prove t (id) *) - exec (block_tac [cut_tac t; exact_tac ("",0,(Ast.LetIn ((Ast.Ident - (id,None),None),npt_t,Ast.Implicit - `JustOne)))]) status goal + exec (block_tac [cut_tac t; branch_tac ~force:false; shift_tac; intro_tac id; + (*merge_tac*)]) status goal | Some t1 -> (* We need to prove t (id) or equivalently t1 *) - exec (block_tac [cut_tac t; change_tac ~where:("",0,(None,[],Some Ast.UserInput)) - ~with_what:t1; exact_tac ("",0,(Ast.LetIn ((Ast.Ident (id,None),None),npt_t,Ast.Implicit - `JustOne)))]) status goal + exec (block_tac [cut_tac t; branch_tac ~force:false; change_tac ~where:("",0,(None,[],Some Ast.UserInput)) + ~with_what:t1; shift_tac; intro_tac id; merge_tac]) status goal ) ) ;; let by_just_we_proved just ty id ty' = - let just = mk_just just in - match id with - | None -> - (match ty' with - | None -> (* just we proved P done *) - just - | Some ty' -> (* just we proved P that is equivalent to P' done *) - (* I should probably check that ty' is the same thing as the conclusion of the - sequent of the open goal and that ty and ty' are equivalent *) - block_tac [ change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just] - ) - | Some id -> - let ty',continuation = - match ty' with - | None -> ty,just - | Some ty' -> ty', block_tac [change_tac ~where:("",0,(None,[id,Ast.Implicit `JustOne],None)) - ~with_what:ty; just] - in block_tac [cut_tac ty'; continuation ] + distribute_tac (fun status goal -> + let just = mk_just just in + match id with + | None -> + (match ty' with + | None -> (* just we proved P done *) + ( + try + assert_tac ty None status goal just + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") + ) + | Some ty' -> (* just we proved P that is equivalent to P' done *) + ( + try + assert_tac ty' (Some ty) status goal (block_tac [change_tac + ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just]) + with + | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion") + | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") + ) + ) + | Some id -> + ( + match ty' with + | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac + id; merge_tac ]) status goal + | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac + id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None)) + ~with_what:ty'; merge_tac]) status goal + ) + ) ;; +let thesisbecomes t1 t2 = we_need_to_prove t1 None t2 ;; + let bydone just = mk_just just ;; -(* let existselim just id1 t1 t2 id2 = - let aux (proof, goal) = - let (n,metasenv,_subst,bo,ty,attrs) = proof in - let metano,context,_ = CicUtil.lookup_meta goal metasenv in - let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in - let proof' = (n,metasenv,_subst,bo,ty,attrs) in - ProofEngineTypes.apply_tactic ( - Tacticals.thens - ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)])) - ~continuations: - [ Tactics.elim_intros (Cic.Rel 1) - ~mk_fresh_name_callback: - (let i = ref 0 in - fun _ _ _ ~typ -> - incr i; - if !i = 1 then Cic.Name id1 else Cic.Name id2) ; - (mk_just ~dbd ~automation_cache just) - ]) (proof', goal) - in - ProofEngineTypes.mk_tactic aux -;; + let (_,_,t1) = t1 in + let (_,_,t2) = t2 in + let just = mk_just just in + block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident + (id1,None), Some t1),t2)])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac + ] let andelim just t1 id1 t2 id2 = - Tacticals.thens - ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2])) - ~continuations: - [ Tactics.elim_intros (Cic.Rel 1) - ~mk_fresh_name_callback: - (let i = ref 0 in - fun _ _ _ ~typ -> - incr i; - if !i = 1 then Cic.Name id1 else Cic.Name id2) ; - (mk_just ~dbd ~automation_cache just) ] + let (_,_,t1) = t1 in + let (_,_,t2) = t2 in + let just = mk_just just in + block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac + ] +;; + + + +let rewritingstep lhs rhs just last_step = fail (lazy "Not implemented"); + (* + let aux ((proof,goal) as status) = + let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in + let _,context,gty = CicUtil.lookup_meta goal metasenv in + let eq,trans = + match LibraryObjects.eq_URI () with + None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command")) + | Some uri -> + Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[]) + in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in + let just' = + match just with + `Auto (univ, params) -> + let params = + if not (List.exists (fun (k,_) -> k = "timeout") params) then + ("timeout","3")::params + else params + in + let params' = + if not (List.exists (fun (k,_) -> k = "paramodulation") params) then + ("paramodulation","1")::params + else params + in + if params = params' then + Tactics.auto ~dbd ~params:(univ, params) ~automation_cache + else + Tacticals.first + [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ; + Tactics.auto ~dbd ~params:(univ, params') ~automation_cache] + | `Term just -> Tactics.apply just + | `SolveWith term -> + Tactics.demodulate ~automation_cache ~dbd + ~params:(Some [term], + ["all","1";"steps","1"; "use_context","false"]) + | `Proof -> + Tacticals.id_tac + in + let plhs,prhs,prepare = + match lhs with + None -> + let plhs,prhs = + match gty with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false + in + plhs,prhs, + (fun continuation -> + ProofEngineTypes.apply_tactic continuation status) + | Some (None,lhs) -> + let plhs,prhs = + match gty with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false + in + (*CSC: manca check plhs convertibile con lhs *) + plhs,prhs, + (fun continuation -> + ProofEngineTypes.apply_tactic continuation status) + | Some (Some name,lhs) -> + let newmeta = CicMkImplicit.new_meta metasenv [] in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let plhs = lhs in + let prhs = Cic.Meta(newmeta,irl) in + plhs,prhs, + (fun continuation -> + let metasenv = (newmeta, context, ty)::metasenv in + let mk_fresh_name_callback = + fun metasenv context _ ~typ -> + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context + (Cic.Name name) ~typ + in + let proof = curi,metasenv,_subst,proofbo,proofty, attrs in + let proof,goals = + ProofEngineTypes.apply_tactic + (Tacticals.thens + ~start:(Tactics.cut ~mk_fresh_name_callback + (Cic.Appl [eq ; ty ; lhs ; prhs])) + ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal) + in + let goals = + match just,goals with + `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1] + | _, [g1;g2] -> [g2;newmeta;g1] + | _, l -> + prerr_endline (String.concat "," (List.map string_of_int l)); + prerr_endline (CicMetaSubst.ppmetasenv [] metasenv); + assert false + in + proof,goals) + in + let continuation = + if last_step then + (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*) + just' + else + Tacticals.thens + ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs])) + ~continuations:[just' ; Tacticals.id_tac] + in + prepare continuation + in + ProofEngineTypes.mk_tactic aux ;; - *) + *) diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli index d345275b4..d96a8fd73 100644 --- a/matita/components/ng_tactics/declarative.mli +++ b/matita/components/ng_tactics/declarative.mli @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_params ] +type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ] val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic @@ -31,3 +31,8 @@ val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tac val bydone : just -> 's NTacStatus.tactic val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic +val andelim : just -> NTacStatus.tactic_term -> string -> NTacStatus.tactic_term -> string -> 's +NTacStatus.tactic +val existselim : just -> string -> NTacStatus.tactic_term -> NTacStatus.tactic_term -> string -> 's +NTacStatus.tactic +val thesisbecomes : NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 2fa02c307..f12b50d5d 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -232,6 +232,15 @@ let normalize status ?delta ctx t = status, (ctx, t) ;; +let are_convertible status ctx a b = + let status, (_,a) = relocate status ctx a in + let status, (_,b) = relocate status ctx b in + let n,h,metasenv,subst,o = status#obj in + let res = NCicReduction.are_convertible status metasenv subst ctx a b in + status, res +;; +let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;; + let unify status ctx a b = let status, (_,a) = relocate status ctx a in let status, (_,b) = relocate status ctx b in diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index da50ea2ac..44c953045 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -85,6 +85,8 @@ val whd: val normalize: #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term -> 'status * cic_term +val are_convertible: + #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status * bool val typeof: #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term val unify: diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli index c492b8c64..fd5916c8d 100644 --- a/matita/components/ng_tactics/nTactics.mli +++ b/matita/components/ng_tactics/nTactics.mli @@ -13,6 +13,7 @@ val print_tac: bool -> string -> 's NTacStatus.tactic +val id_tac: 's NTacStatus.tactic val dot_tac: 's NTacStatus.tactic val branch_tac: ?force:bool -> 's NTacStatus.tactic val shift_tac: 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 1937229af..d0ff9c082 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -54,7 +54,7 @@ let incr_uses tbl item = let toref f tbl t = match t with | Ast.NRef n -> - f tbl n + f tbl n | Ast.NCic _ (* local candidate *) | _ -> () @@ -82,7 +82,7 @@ let print_stat status tbl = "; uses = " ^ (string_of_int !(v.uses)) ^ "; nom = " ^ (string_of_int !(v.nominations)) in lazy ("\n\nSTATISTICS:\n" ^ - String.concat "\n" (List.map vstring l)) + String.concat "\n" (List.map vstring l)) (* ======================= utility functions ========================= *) module IntSet = Set.Make(struct type t = int let compare = compare end) @@ -238,7 +238,7 @@ let solve f status eq_cache goal = debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = - (* NCicRefiner.typeof status + (* NCicRefiner.typeof status (* (status#set_coerc_db NCicCoercion.empty_db) *) metasenv subst ctx pt None in debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt))); @@ -259,14 +259,14 @@ let solve f status eq_cache goal = NCicRefiner.RefineFailure msg | NCicRefiner.Uncertain msg -> debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^ - snd (Lazy.force msg) ^ - "\n in the environment\n" ^ - status#ppmetasenv subst metasenv)); None + snd (Lazy.force msg) ^ + "\n in the environment\n" ^ + status#ppmetasenv subst metasenv)); None | NCicRefiner.AssertFailure msg -> debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^ Lazy.force msg ^ - "\n in the environment\n" ^ - status#ppmetasenv subst metasenv)); None + "\n in the environment\n" ^ + status#ppmetasenv subst metasenv)); None | Sys.Break as e -> raise e | _ -> None in @@ -292,7 +292,10 @@ let auto_eq_check eq_cache status = | Error _ -> debug_print (lazy ("no paramod proof found"));[] ;; -let index_local_equations eq_cache status = +let index_local_equations eq_cache ?(flag=false) status = + if flag then + NCicParamod.empty_state + else begin noprint (lazy "indexing equations"); let open_goals = head_goals status#stack in let open_goal = List.hd open_goals in @@ -316,9 +319,13 @@ let index_local_equations eq_cache status = | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> eq_cache) eq_cache ctx + end ;; -let index_local_equations2 eq_cache status open_goal lemmas nohyps = +let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps = + if flag then + NCicParamod.empty_state + else begin noprint (lazy "indexing equations"); let eq_cache,lemmas = match lemmas with @@ -354,6 +361,7 @@ let index_local_equations2 eq_cache status open_goal lemmas nohyps = | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> eq_cache) eq_cache lemmas + end ;; let fast_eq_check_tac ~params s = @@ -575,13 +583,13 @@ let saturate_to_ref status metasenv subst ctx nref ty = NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in match ty with | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) - when nre<>nref -> - let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in - aux metasenv bo (args@moreargs) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in + aux metasenv bo (args@moreargs) | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) - when nre<>nref -> - let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in - aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in + aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) | _ -> ty,metasenv,(args@moreargs) in aux metasenv ty [] @@ -598,9 +606,9 @@ let smart_apply t unit_eq status g = match gty with | NCic.Const(nref) | NCic.Appl(NCic.Const(nref)::_) -> - saturate_to_ref status metasenv subst ctx nref ty + saturate_to_ref status metasenv subst ctx nref ty | _ -> - NCicMetaSubst.saturate status metasenv subst ctx ty 0 in + NCicMetaSubst.saturate status metasenv subst ctx ty 0 in let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in let status = status#set_obj (n,h,metasenv,subst,o) in let pterm = if args=[] then t else @@ -892,6 +900,7 @@ type flags = { do_types : bool; (* solve goals in Type *) last : bool; (* last goal: take first solution only *) candidates: Ast.term list option; + local_candidates: bool; maxwidth : int; maxsize : int; maxdepth : int; @@ -908,20 +917,20 @@ type cache = let add_to_trace status ~depth cache t = match t with | Ast.NRef _ -> - debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); - {cache with trace = t::cache.trace} + debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); + {cache with trace = t::cache.trace} | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache let pptrace status tr = (lazy ("Proof Trace: " ^ (String.concat ";" - (List.map (NotationPp.pp_term status) tr)))) + (List.map (NotationPp.pp_term status) tr)))) (* not used let remove_from_trace cache t = match t with | Ast.NRef _ -> - (match cache.trace with - | _::tl -> {cache with trace = tl} + (match cache.trace with + | _::tl -> {cache with trace = tl} | _ -> assert false) | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache *) @@ -982,7 +991,7 @@ let sort_candidates status ctx candidates = let ty = NCicTypeChecker.typeof status subst metasenv ctx t in let res = branch status (mk_cic_term ctx ty) in noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " - ^ (string_of_int res))); + ^ (string_of_int res))); res in let candidates = List.map (fun t -> branch t,t) candidates in @@ -990,7 +999,7 @@ let sort_candidates status ctx candidates = List.sort (fun (a,_) (b,_) -> a - b) candidates in let candidates = List.map snd candidates in noprint (lazy ("candidates =\n" ^ (String.concat "\n" - (List.map (NotationPp.pp_term status) candidates)))); + (List.map (NotationPp.pp_term status) candidates)))); candidates let sort_new_elems l = @@ -1005,7 +1014,7 @@ let rec stack_goals level gs = | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None in - HExtlib.filter_map is_open g @ stack_goals (level-1) s + HExtlib.filter_map is_open g @ stack_goals (level-1) s ;; let open_goals level status = stack_goals level status#stack @@ -1045,7 +1054,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = (* some flexibility *) if og_no - old_og_no > res then (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " - ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); + ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); debug_print ~depth (lazy "strange application"); None) else *) (incr candidate_no; Some ((!candidate_no,t),status)) @@ -1065,14 +1074,14 @@ let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ") let perforate_small status subst metasenv context t = let rec aux = function | NCic.Appl (hd::tl) -> - let map t = - let s = sort_of status subst metasenv context t in - match s with - | NCic.Sort(NCic.Type [`Type,u]) - when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) - | _ -> aux t - in - NCic.Appl (hd::List.map map tl) + let map t = + let s = sort_of status subst metasenv context t in + match s with + | NCic.Sort(NCic.Type [`Type,u]) + when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) + | _ -> aux t + in + NCic.Appl (hd::List.map map tl) | t -> t in aux t @@ -1093,11 +1102,11 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty let context = ctx_of gty in let _, raw_gty = term_of_cic_term status gty context in let is_prod, is_eq = - let status, t = term_of_cic_term status gty context in - let t = NCicReduction.whd status subst context t in - match t with - | NCic.Prod _ -> true, false - | _ -> false, NCicParamod.is_equation status metasenv subst context t + let status, t = term_of_cic_term status gty context in + let t = NCicReduction.whd status subst context t in + match t with + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t in debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty)); let is_eq = @@ -1106,46 +1115,50 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty let raw_weak_gty, weak_gty = if smart then match raw_gty with - | NCic.Appl _ - | NCic.Const _ - | NCic.Rel _ -> + | NCic.Appl _ + | NCic.Const _ + | NCic.Rel _ -> let raw_weak = perforate_small status subst metasenv context raw_gty in let weak = mk_cic_term context raw_weak in noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); Some raw_weak, Some (weak) - | _ -> None,None + | _ -> None,None else None,None in (* we now compute global candidates *) let global_cands, smart_global_cands = + if flags.local_candidates then let mapf s = let to_ast = function | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r) (* | NCic.Const _ -> None *) - | _ -> assert false in - HExtlib.filter_map - to_ast (NDiscriminationTree.TermSet.elements s) in + | _ -> assert false in + HExtlib.filter_map + to_ast (NDiscriminationTree.TermSet.elements s) in let g,l = - get_cands - (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe) - NDiscriminationTree.TermSet.diff - NDiscriminationTree.TermSet.empty - raw_gty raw_weak_gty in - mapf g, mapf l in + get_cands + (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe) + NDiscriminationTree.TermSet.diff + NDiscriminationTree.TermSet.empty + raw_gty raw_weak_gty in + mapf g, mapf l + else [],[] in (* we now compute local candidates *) let local_cands,smart_local_cands = + if flags.local_candidates then let mapf s = let to_ast t = - let _status, t = term_of_cic_term status t context - in Ast.NCic t in - List.map to_ast (Ncic_termSet.elements s) in + let _status, t = term_of_cic_term status t context + in Ast.NCic t in + List.map to_ast (Ncic_termSet.elements s) in let g,l = get_cands - (fun ty -> search_in_th ty cache) - Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in - mapf g, mapf l in + (fun ty -> search_in_th ty cache) + Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in + mapf g, mapf l + else [],[] in (* we now splits candidates in facts or not facts *) let test = is_a_fact_ast status subst metasenv context in let by,given_candidates = @@ -1198,8 +1211,8 @@ let applicative_case ~pfailed depth signature status flags gty cache = let status, t = term_of_cic_term status gty context in let t = NCicReduction.whd status subst context t in match t with - | NCic.Prod _ -> true, false - | _ -> false, NCicParamod.is_equation status metasenv subst context t + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t in debug_print ~depth (lazy (string_of_bool is_eq)); (* new *) @@ -1358,11 +1371,11 @@ let rec intros_facts ~depth status facts = | _ -> status, facts ;; -let intros ~depth status cache = +let intros ~depth status ?(use_given_only=false) cache = match is_prod status with | `Inductive _ | `Some _ -> - let trace = cache.trace in + let trace = cache.trace in let status,facts = intros_facts ~depth status cache.facts in @@ -1371,7 +1384,7 @@ let intros ~depth status cache = [(0,Ast.Ident("__intros",None)),status], cache else (* we reindex the equation from scratch *) - let unit_eq = index_local_equations status#eq_cache status in + let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in let status = NTactics.merge_tac status in [(0,Ast.Ident("__intros",None)),status], init_cache ~facts ~unit_eq () ~trace @@ -1407,7 +1420,7 @@ let is_meta status gty = | _ -> false ;; -let do_something signature flags status g depth gty cache = +let do_something signature flags status g depth gty ?(use_given_only=false) cache = (* if the goal is meta we close it with I:True. This should work thanks to the toplogical sorting of goals. *) if is_meta status gty then @@ -1416,7 +1429,7 @@ let do_something signature flags status g depth gty cache = let s = NTactics.apply_tac ("",0,t) status in [(0,t),s], cache else - let l0, cache = intros ~depth status cache in + let l0, cache = intros ~depth status cache ~use_given_only in if l0 <> [] then l0, cache else (* whd *) @@ -1532,8 +1545,8 @@ let deep_focus_tac level focus status = let rec slice level gs = if level = 0 then [],[],gs else match gs with - | [] -> assert false - | (g, t, k, tag) :: s -> + | [] -> assert false + | (g, t, k, tag) :: s -> let f,o,gs = slice (level-1) s in let f1,o1 = List.partition in_focus g in @@ -1555,18 +1568,17 @@ match status#stack with in let others = menv_closure status (stack_goals (level-1) tl) in List.for_all (fun i -> IntSet.mem i others) - (HExtlib.filter_map is_open g) + (HExtlib.filter_map is_open g) -let top_cache ~depth top status cache = +let top_cache ~depth top status ?(use_given_only=false) cache = if top then - let unit_eq = index_local_equations status#eq_cache status in + let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in {cache with unit_eq = unit_eq} else cache -let rec auto_clusters ?(top=false) - flags signature cache depth status : unit = +let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only=false) status : unit = debug_print ~depth (lazy ("entering auto clusters at depth " ^ - (string_of_int depth))); + (string_of_int depth))); debug_print ~depth (pptrace status cache.trace); (* ignore(Unix.select [] [] [] 0.01); *) let status = clean_up_tac status in @@ -1577,15 +1589,15 @@ let rec auto_clusters ?(top=false) let status = NTactics.merge_tac status in let cache = let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache *) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} + match l with + | [] -> cache (* possible because of intros that cleans the cache *) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} in - auto_clusters flags signature cache (depth-1) status + auto_clusters flags signature cache (depth-1) status ~use_given_only else if List.length goals < 2 then - let cache = top_cache ~depth top status cache in - auto_main flags signature cache depth status + let cache = top_cache ~depth top status cache ~use_given_only in + auto_main flags signature cache depth status ~use_given_only else let all_goals = open_goals (depth+1) status in debug_print ~depth (lazy ("goals = " ^ @@ -1596,17 +1608,17 @@ let rec auto_clusters ?(top=false) (fun gl -> if List.length gl > flags.maxwidth then begin - debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); - HLog.warn (sprintf "global width (%u) exceeded: %u" - flags.maxwidth (List.length gl)); - raise (Gaveup cache.failures) - end else ()) classes; + debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); + HLog.warn (sprintf "global width (%u) exceeded: %u" + flags.maxwidth (List.length gl)); + raise (Gaveup cache.failures) + end else ()) classes; if List.length classes = 1 then let flags = {flags with last = (List.length all_goals = 1)} in - (* no need to cluster *) - let cache = top_cache ~depth top status cache in - auto_main flags signature cache depth status + (* no need to cluster *) + let cache = top_cache ~depth top status cache ~use_given_only in + auto_main flags signature cache depth status ~use_given_only else let classes = if top then List.rev classes else classes in debug_print ~depth @@ -1623,21 +1635,21 @@ let rec auto_clusters ?(top=false) let flags = {flags with last = (List.length gl = 1)} in let lold = List.length status#stack in - debug_print ~depth (lazy ("stack length = " ^ - (string_of_int lold))); + debug_print ~depth (lazy ("stack length = " ^ + (string_of_int lold))); let fstatus = deep_focus_tac (depth+1) gl status in - let cache = top_cache ~depth top fstatus cache in + let cache = top_cache ~depth top fstatus cache ~use_given_only in try debug_print ~depth (lazy ("focusing on" ^ String.concat "," (List.map string_of_int gl))); - auto_main flags signature cache depth fstatus; assert false + auto_main flags signature cache depth fstatus ~use_given_only; assert false with | Proved(status,trace) -> - let status = NTactics.merge_tac status in - let cache = {cache with trace = trace} in - let lnew = List.length status#stack in - assert (lold = lnew); - (status,cache,true) + let status = NTactics.merge_tac status in + let cache = {cache with trace = trace} in + let lnew = List.length status#stack in + assert (lold = lnew); + (status,cache,true) | Gaveup failures when top -> let cache = {cache with failures = failures} in (status,cache,b) @@ -1645,55 +1657,55 @@ let rec auto_clusters ?(top=false) (status,cache,false) classes in let rec final_merge n s = - if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) + if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) in let status = final_merge depth status in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures) and (* BRAND NEW VERSION *) -auto_main flags signature cache depth status: unit = +auto_main flags signature cache depth status ?(use_given_only=false): unit= debug_print ~depth (lazy "entering auto main"); debug_print ~depth (pptrace status cache.trace); debug_print ~depth (lazy ("stack length = " ^ - (string_of_int (List.length status#stack)))); + (string_of_int (List.length status#stack)))); (* ignore(Unix.select [] [] [] 0.01); *) let status = sort_tac (clean_up_tac status) in let goals = head_goals status#stack in match goals with | [] when depth = 0 -> raise (Proved (status,cache.trace)) | [] -> - let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache *) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status + let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache *) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in + auto_clusters flags signature cache (depth-1) status ~use_given_only | orig::_ -> - if depth > 0 && move_to_side depth status - then - let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache*) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status - else + if depth > 0 && move_to_side depth status + then + let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache*) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in + auto_clusters flags signature cache (depth-1) status ~use_given_only + else let ng = List.length goals in (* moved inside auto_clusters *) if ng > flags.maxwidth then begin debug_print ~depth (lazy "FAIL LOCAL WIDTH"); - HLog.warn (sprintf "local width (%u) exceeded: %u" - flags.maxwidth ng); - raise (Gaveup cache.failures) + HLog.warn (sprintf "local width (%u) exceeded: %u" + flags.maxwidth ng); + raise (Gaveup cache.failures) end else if depth = flags.maxdepth then - raise (Gaveup cache.failures) + raise (Gaveup cache.failures) else let status = NTactics.branch_tac ~force:true status in let g,gctx, gty = current_goal status in @@ -1713,7 +1725,7 @@ auto_main flags signature cache depth status: unit = (* for efficiency reasons, in this case we severely cripple the search depth *) (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1))); - auto_main flags signature cache (depth+1) status) + auto_main flags signature cache (depth+1) status ~use_given_only) (* check for loops *) else if is_subsumed depth false status closegty (snd cache.under_inspection) then (debug_print ~depth (lazy "SUBSUMED"); @@ -1723,40 +1735,40 @@ auto_main flags signature cache depth status: unit = (debug_print ~depth (lazy "ALREADY MET"); raise (Gaveup cache.failures)) else - let new_sig = height_of_goal g status in + let new_sig = height_of_goal g status in if new_sig < signature then - (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); - debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); + (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); + debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); let alternatives, cache = - do_something signature flags status g depth gty cache in + do_something signature flags status g depth gty cache ~use_given_only in let loop_cache = if flags.last then - let l,tree = cache.under_inspection in - let l,tree = closegty::l, add_to_th closegty tree closegty in + let l,tree = cache.under_inspection in + let l,tree = closegty::l, add_to_th closegty tree closegty in {cache with under_inspection = l,tree} else cache in let failures = List.fold_left (fun allfailures ((_,t),status) -> debug_print ~depth - (lazy ("(re)considering goal " ^ - (string_of_int g) ^" : "^ppterm status gty)); + (lazy ("(re)considering goal " ^ + (string_of_int g) ^" : "^ppterm status gty)); debug_print (~depth:depth) (lazy ("Case: " ^ NotationPp.pp_term status t)); let depth,cache = - if t=Ast.Ident("__whd",None) || + if t=Ast.Ident("__whd",None) || t=Ast.Ident("__intros",None) then depth, cache - else depth+1,loop_cache in - let cache = add_to_trace status ~depth cache t in + else depth+1,loop_cache in + let cache = add_to_trace status ~depth cache t in let cache = {cache with failures = allfailures} in - try - auto_clusters flags signature cache depth status; + try + auto_clusters flags signature cache depth status ~use_given_only; assert false; - with Gaveup fail -> - debug_print ~depth (lazy "Failed"); - fail) - cache.failures alternatives in + with Gaveup fail -> + debug_print ~depth (lazy "Failed"); + fail) + cache.failures alternatives in let failures = if flags.last then let newfail = @@ -1767,7 +1779,7 @@ auto_main flags signature cache depth status: unit = add_to_th newfail failures closegty else failures in debug_print ~depth (lazy "no more candidates"); - raise (Gaveup failures) + raise (Gaveup failures) ;; let int name l def = @@ -1787,12 +1799,34 @@ let cleanup_trace s trace = (* filtering facts *) in List.filter (fun t -> - match t with - | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u) - | _ -> false) trace + match t with + | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u) + | _ -> false) trace ;; -let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = +(*CSC: TODO + +- auto_params e' una high tactic che prende in input i parametri e poi li + processa nel contesto vuoto calcolando i candidate + +- astrarla su una auto_params' che prende in input gia' i candidate e un + nuovo parametro per evitare il calcolo dei candidate locali che invece + diventano vuoti (ovvero: non usare automaticamente tutte le ipotesi, bensi' + nessuna) + +- reimplementi la auto_params chiamando la auto_params' con il flag a + false e il vecchio codice per andare da parametri a candiddati + OVVERO: usa tutti le ipotesi locali + candidati globali + +- crei un nuovo entry point lowtac che calcola i candidati usando il contesto + corrente e poi fa exec della auto_params' con i candidati e il flag a true + OVVERO: usa solo candidati globali che comprendono ipotesi locali +*) + +type auto_params = NTacStatus.tactic_term list option * (string * string) list + +(*let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =*) +let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace_ref=ref []) status = let oldstatus = status in let status = (status:> NTacStatus.tac_status) in let goals = head_goals status#stack in @@ -1809,17 +1843,6 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (NDiscriminationTree.TermSet.elements t)) ))); *) - let candidates = - match univ with - | None -> None - | Some l -> - let to_Ast t = -(* FG: `XTSort here? *) - let status, res = disambiguate status [] t `XTNone in - let _,res = term_of_cic_term status res (ctx_of res) - in Ast.NCic res - in Some (List.map to_Ast l) - in let depth = int "depth" flags 3 in let size = int "size" flags 10 in let width = int "width" flags 4 (* (3+List.length goals)*) in @@ -1829,6 +1852,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let flags = { last = true; candidates = candidates; + local_candidates = local_candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1847,7 +1871,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in let flags = { flags with maxdepth = x } in - try auto_clusters (~top:true) flags signature cache 0 status;assert false + try auto_clusters (~top:true) flags signature cache 0 status ~use_given_only;assert false (* try auto_main flags signature cache 0 status;assert false *) @@ -1855,9 +1879,9 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | Gaveup _ -> up_to (x+1) y | Proved (s,trace) -> debug_print (lazy ("proved at depth " ^ string_of_int x)); - List.iter (toref incr_uses statistics) trace; + List.iter (toref incr_uses statistics) trace; let trace = cleanup_trace s trace in - let _ = debug_print (pptrace status trace) in + let _ = debug_print (pptrace status trace) in let stack = match s#stack with | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest @@ -1876,6 +1900,27 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = s ;; +let candidates_from_ctx univ ctx status = + match univ with + | None -> None + | Some l -> + let to_Ast t = + (* FG: `XTSort here? *) + let status, res = disambiguate status ctx t `XTNone in + let _,res = term_of_cic_term status res (ctx_of res) + in Ast.NCic res + in Some (List.map to_Ast l) + +let auto_lowtac ~params:(univ,flags) status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let candidates = candidates_from_ctx univ ctx status in + NTactics.exec (auto_tac' candidates ~local_candidates:false ~use_given_only:true flags) status goal + +let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = + let candidates = candidates_from_ctx univ [] status in + auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status + let auto_tac ~params:(_,flags as params) ?trace_ref = if List.mem_assoc "demod" flags then demod_tac ~params diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli index 87b2e8e4b..b0d724379 100644 --- a/matita/components/ng_tactics/nnAuto.mli +++ b/matita/components/ng_tactics/nnAuto.mli @@ -9,29 +9,27 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +type auto_params = NTacStatus.tactic_term list option * (string * string) list + val is_a_fact_obj: #NTacStatus.pstatus -> NUri.uri -> bool -val fast_eq_check_tac: - params:(NTacStatus.tactic_term list option * (string * string) list) -> - 's NTacStatus.tactic +val fast_eq_check_tac: params:auto_params -> 's NTacStatus.tactic -val paramod_tac: - params:(NTacStatus.tactic_term list option * (string * string) list) -> - 's NTacStatus.tactic +val paramod_tac: params:auto_params -> 's NTacStatus.tactic -val demod_tac: - params:(NTacStatus.tactic_term list option* (string * string) list) -> - 's NTacStatus.tactic +val demod_tac: params:auto_params -> 's NTacStatus.tactic val smart_apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic val auto_tac: - params:(NTacStatus.tactic_term list option * (string * string) list) -> + params:auto_params -> ?trace_ref:NotationPt.term list ref -> 's NTacStatus.tactic +val auto_lowtac: params:auto_params -> NTacStatus.lowtac_status -> int -> NTacStatus.lowtac_status + val keys_of_type: (#NTacStatus.pstatus as 'a) -> NTacStatus.cic_term -> 'a * NTacStatus.cic_term list diff --git a/matita/components/registry/.depend b/matita/components/registry/.depend index 2a8e36776..67113e67f 100644 --- a/matita/components/registry/.depend +++ b/matita/components/registry/.depend @@ -1,3 +1,3 @@ +helm_registry.cmi : helm_registry.cmo : helm_registry.cmi helm_registry.cmx : helm_registry.cmi -helm_registry.cmi : diff --git a/matita/components/thread/.depend b/matita/components/thread/.depend index e8bc4a106..d68336af1 100644 --- a/matita/components/thread/.depend +++ b/matita/components/thread/.depend @@ -1,6 +1,6 @@ -extThread.cmo : extThread.cmi -extThread.cmx : extThread.cmi +threadSafe.cmi : extThread.cmi : threadSafe.cmo : threadSafe.cmi threadSafe.cmx : threadSafe.cmi -threadSafe.cmi : +extThread.cmo : extThread.cmi +extThread.cmx : extThread.cmi diff --git a/matita/components/xml/.depend b/matita/components/xml/.depend index 60964e765..fd3f626b9 100644 --- a/matita/components/xml/.depend +++ b/matita/components/xml/.depend @@ -1,6 +1,6 @@ +xml.cmi : +xmlPushParser.cmi : xml.cmo : xml.cmi xml.cmx : xml.cmi -xml.cmi : xmlPushParser.cmo : xmlPushParser.cmi xmlPushParser.cmx : xmlPushParser.cmi -xmlPushParser.cmi : diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml index d77c276c4..bc0b424e0 100644 --- a/matita/matita/help/C/sec_declarative_tactics.xml +++ b/matita/matita/help/C/sec_declarative_tactics.xml @@ -1,5 +1,4 @@ - diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index c6d55ae38..8437cd081 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -120,6 +120,11 @@ by done proved + have + such + the + thesis + becomes alias diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 94e3e751d..ce3dcc6fe 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -611,11 +611,15 @@ class gui () = let saved_use_library= !MultiPassDisambiguator.use_library in try MultiPassDisambiguator.use_library := !all_disambiguation_passes; + prerr_endline "PRIMA"; f script; MultiPassDisambiguator.use_library := saved_use_library; - unlock_world () + prerr_endline "DOPO"; + unlock_world () ; + prerr_endline "FINE"; with | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> + prerr_endline "EXC1"; (try interactive_error_interp ~all_passes:!all_disambiguation_passes source_view#source_buffer @@ -632,7 +636,9 @@ class gui () = notify_exn source_view exc); | exc -> notify_exn source_view exc); MultiPassDisambiguator.use_library := saved_use_library; - unlock_world () + prerr_endline "DOPO1"; + unlock_world (); + prerr_endline "FINE1" | exc -> (try notify_exn source_view exc with Sys.Break as e -> notify_exn source_view e); -- 2.39.2