Added syntax for ninversion tactic (still experimental).

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index d436977e381270bf415117c99b9dac3e2534406a..1910e34ac949d279cae975f146920745f2368189 100644 (file)
--- 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
+   | NInversion of loc * CicNotationPt.term * npattern  
    | NLApply of loc * CicNotationPt.term
    | NLetIn of loc * npattern * CicNotationPt.term * string
    | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 0db8efc1aa9f2eb020cf8a0d8fdc64e067c58a7d..e022c6f33114c122bac42f2e1ba6e6a99918b3d7 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -118,6 +118,8 @@ let rec pp_ntactic ~map_unicode_to_tex =
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
   | NIntro (_,n) -> "#" ^ n
+  | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^
+      assert false ^ " " ^ assert false
   | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
   | NRewrite (_,dir,n,where) -> "nrewrite " ^
      (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 239d30d2d1480ff0b0c354a757cacbf4105cc058..783d7e6fc5e624b7dd9d21ebaf9af1c621f95ccd 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -805,6 +805,10 @@ 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.NInversion (_loc, what, where) ->
+      NTactics.inversion_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
   | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) 
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 7be30e407db19b1f918e46eb367080422e3114bd..ef354789a25dab4d0304990ebfd6a23b257c4575 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -268,6 +268,8 @@ EXTEND
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->
         G.NGeneralize (loc, p)
+    | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
+        G.NInversion (loc, what, where)
     | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 89a1dd1af65b33bdb126e68575e79358c72d12d6..4b4b7246d29023962c35dddc3e8dfc2b6a05b72b 100644 (file)
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -11,8 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-let pp m = prerr_endline (Lazy.force m);;
-(* let pp _ = ();; *)
+(* let pp m = prerr_endline (Lazy.force m);;*)
+let pp _ = ();;
 
 let fresh_name =
  let i = ref 0 in
@@ -130,11 +130,9 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
                                       Some (CicNotationPt.Implicit `JustOne)),
                                       mk_appl (mk_id "P"::id_rs)))))
      in
-     pp (lazy ("and the theorem is: \n" ^ (CicNotationPp.pp_term theorem))); 
      let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @
                        List.map mk_id hyplist @ 
                        HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [mk_id "Hterm"] ) in
-     pp (lazy ("and t is: \n" ^ (CicNotationPp.pp_term t))); 
      let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
                              (baseuri ^ name ^ ".def",
                                0,CicNotationPt.Theorem (`Theorem,name,theorem,Some

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f5ae3a721e4880a955d4be5463252cf4423e2a36..67568154088e1d54f47c7b6de7662044166354ce 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -652,3 +652,26 @@ let assert_tac seqs status =
      ) status
 ;;
 
+let inversion_tac ~what:(txt,len,what) ~where = 
+  let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let sort = ref (NCic.Rel 1) in
+  atomic_tac (block_tac [
+    analyze_indty_tac ~what indtyinfo;    
+    (fun s -> select_tac 
+      ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
+    sort_of_goal_tac sort;
+    (fun status ->
+     let ity = HExtlib.unopt !indtyinfo in
+     let NReference.Ref (uri, _) = ity.reference in
+     let name = 
+       NUri.name_of_uri uri ^ "_inv_" ^
+        snd (NCicElim.ast_of_sort 
+          (match !sort with NCic.Sort x -> x | _ -> assert false))
+     in
+     let eliminator = 
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+     in
+     exact_tac ("",0,eliminator) status) ]) 
+;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 74bbcbcb4214a3565506a04d1dc81695bf746970..e1a5de8957735d52ea20863a38c8e54ee080e40f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -95,3 +95,7 @@ val analyze_indty_tac :
 
 
 val find_in_context : 'a -> ('a * 'b) list -> int
+
+val inversion_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     's NTacStatus.tactic