X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=89a1dd1af65b33bdb126e68575e79358c72d12d6;hb=60c92de1ace192d20b818bd71ec420d74e0176d2;hp=627885cb743628ed01c7b8b2ec04d6122ed2f23f;hpb=18ff03b9480b4cc3fec155db743b37f3a4675509;p=helm.git

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 627885cb7..89a1dd1af 100644
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -76,24 +76,25 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
  let _,ind_name,ty,cl = it in
  pp (lazy ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
  let ncons = List.length cl in
- (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
+ (**)let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
  let params = List.rev_map (function name,_ -> mk_id name) params in
- pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));*)
+ pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**)
  let args,sort= split_arity ~subst:[] [] ty in
  pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort));
- (*let args = List.rev_map (function name,_ -> mk_id name) args in
- pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));*)
+ (**)let args = List.rev_map (function name,_ -> mk_id name) args in
+ pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**)
  let nparams = List.length args in
+
  pp (lazy ("nparams = " ^ string_of_int nparams));
- if nparams <= leftno 
+ if nparams = 0 
    then raise (Failure "inverter: the type must have at least one right parameter") 
    else 
-     let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
+     let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
      pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
      let ls, rs = HExtlib.split_nth leftno xs in
      pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
      pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
-     let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
+     let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (leftno+nparams+1)) in
     
      let _id_xs = List.map mk_id xs in
      let id_ls = List.map mk_id ls in
@@ -128,10 +129,12 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
                     mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
                                       Some (CicNotationPt.Implicit `JustOne)),
                                       mk_appl (mk_id "P"::id_rs)))))
-     in 
+     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 @
-                       CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
+                       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
@@ -147,7 +150,8 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
          mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
     
      let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
-                        CicNotationPt.Implicit (`Tagged "end"));
+                        
+CicNotationPt.Implicit (`Tagged "end"));
                         CicNotationPt.Implicit (`Tagged "cut")] in
      let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
      let status = NTactics.block_tac 
@@ -158,7 +162,7 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
                                NTactics.branch_tac;
                                NTactics.case_tac "end";
                                NTactics.apply_tac ("",0,mk_id "Hcut");
-                               NTactics.apply_tac ("",0,mk_id "refl_eq"); 
+                               NTactics.apply_tac ("",0,mk_id "refl"); 
                                NTactics.shift_tac;
                                (*NTactics.case_tac "cut";*)
                                NTactics.apply_tac ("",0,t);