From: Enrico Tassi Date: Mon, 10 May 2010 09:48:33 +0000 (+0000) Subject: new intro: X-Git-Tag: make_still_working~2904 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;p=helm.git new intro: - #; -- introduces into the context every possible assumption giving to it an unusable name - #h1 .. h2; -- multi intros - intros; -- macro che espande a #h1...hn. --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 97dbb0486..ae4dc23f7 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -65,6 +65,7 @@ type ntactic = | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string + | NIntros of loc * string list | NInversion of loc * CicNotationPt.term * npattern | NLApply of loc * CicNotationPt.term | NLetIn of loc * npattern * CicNotationPt.term * string @@ -201,6 +202,7 @@ type nmacro = | NCheck of loc * CicNotationPt.term | Screenshot of loc * string | NAutoInteractive of loc * CicNotationPt.term auto_params + | NIntroGuess of loc (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index e8abb0572..e55df286b 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -808,6 +808,7 @@ let eval_ng_tac tac = NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n + | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns | GrafiteAst.NInversion (_loc, what, where) -> NTactics.inversion_tac ~what:(text,prefix_len,what) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index faa17124e..d7aae9ee8 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -276,6 +276,7 @@ EXTEND | Some `Trace -> G.NMacro(loc, G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params)))) + | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc) | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t)) | IDENT "screenshot"; fname = QSTRING -> G.NMacro(loc,G.Screenshot (loc, fname)) @@ -315,7 +316,7 @@ EXTEND (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in G.NTactic(loc,[G.NBlock (loc,l)]) | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc]) - | SYMBOL "#"; n=IDENT -> G.NTactic(loc,[ G.NIntro (loc,n)]) + | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)]) | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")]) | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")]) | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index f6d8bfaec..f3d74050f 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -556,6 +556,25 @@ let intro_tac name = if name = "_" then clear_tac [name] else id_tac ] ;; +let name_counter = ref 0;; +let intros_tac ?names_ref names s = + let names_ref, prefix = + match names_ref with | None -> ref [], "__" | Some r -> r, "H" + in + if names = [] then + repeat_tac + (fun s -> + incr name_counter; + (* TODO: generate better names *) + let name = prefix ^ string_of_int !name_counter in + let s = intro_tac name s in + names_ref := !names_ref @ [name]; + s) + s + else + block_tac (List.map intro_tac names) s +;; + let cases ~what status goal = let gty = get_goalty status goal in let status, what = disambiguate status (ctx_of gty) what None in diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index a4c48e686..822421a24 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -43,6 +43,8 @@ val elim_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic val intro_tac: string -> 's NTacStatus.tactic +val intros_tac: + ?names_ref:string list ref -> string list -> 's NTacStatus.tactic val cases_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 4449d3b1d..1e63cc3d1 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -393,6 +393,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us in guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); [status, parsed_text], "", parsed_text_length + | TA.NIntroGuess _loc -> + let names_ref = ref [] in + let s = + NTactics.intros_tac ~names_ref [] script#grafite_status + in + let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in + let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in + [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length | TA.NAutoInteractive (_loc, (None,a)) -> let trace_ref = ref [] in let s = diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma index f8916ee5a..300812ce8 100644 --- a/helm/software/matita/nlibrary/re/re.ma +++ b/helm/software/matita/nlibrary/re/re.ma @@ -65,14 +65,7 @@ nqed. *) nlemma in_l_inv_e: ∀S,w. in_l S w (e ?) → w = []. - #S; #w; #H; ninversion H - [ #a; #b; ndestruct; // - | #a; #b; #c; ndestruct - | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct - | #a; #b; #c; #d; #e; #f; #g; ndestruct - | #a; #b; #c; #d; #e; #f; #g; ndestruct - | #a; #b; #c; ndestruct - | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ] + #S; #w; #H; ninversion H; #; ndestruct; //. nqed. naxiom in_l_inv_s: @@ -141,7 +134,7 @@ ntheorem eclose_true: true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E). #S; #E; nelim E; nnormalize; // [ #H; ncases (?: False); /2/ - | #x; #H; ncases (?: False); /2/ + | #x H; #H; ncases (?: False); /2/ | #x; #H; ncases (?: False); /2/ | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/; #_; #_; #H; ncases (?:False); /2/ @@ -165,15 +158,10 @@ nqed. ntheorem in_l_empty_c: ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2. #S; #E1; #E2; #H; ninversion H - [ #_; #H2; ndestruct - | #x; #K; ndestruct + [##1,2,4,5,6,7: #; ndestruct | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6; nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //; - ndestruct; // - | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct - | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct - | #E; #_; #K; ndestruct - | #w1; #w2; #w3; #H1; #H2; #H3; #H4; #H5; #H6; ndestruct ] + ndestruct; // ] nqed. ntheorem eclose_true': @@ -185,25 +173,15 @@ ntheorem eclose_true': | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize [ #H1; #H2; #H3; ninversion H3; /3/; ##| #H1; #H2; #H3; ninversion H3 - [ #_; #K; ndestruct - | #x; #K; ndestruct + [ ##1,2,4,5,6,7: #; ndestruct | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct; - napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); // - | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct - | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct - | #E'; #_; #K; ndestruct - | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]##] + napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##] ##| #E1; ncases (fst … (eclose S E1)); nnormalize; //; #E2; #H1; #H2; #H3; ninversion H3 - [ #_; #K; ndestruct - | #w; #_; #K; ndestruct - | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct + [ ##1,2,3,5,6,7: #; ndestruct; /2/ | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; ncases (?: False); napply (absurd ?? (not_eq_true_false …)); - /2/ - | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/ - | #a; #b; #c; ndestruct - | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##] + /2/ ]##] nqed. (*