X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=f25114817de9256f58ed85eb66167a38f30b3daa;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=12a1efd7ed32cc8a6ba2fd37c78a02de3a1a5ec7;hpb=32f9135944b5d2979f12d2a66135702c7d230341;p=helm.git

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index 12a1efd7e..f25114817 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -130,7 +130,7 @@ let arg_list nleft t =
 
 let nargs it nleft consno =
   pp (lazy (Printf.sprintf "nargs %d %d" nleft consno));
-  let _,indname,_,cl = it in
+  let _,_indname,_,cl = it in
   let _,_,t_k = List.nth cl consno in
   List.length (arg_list nleft t_k) ;;
 
@@ -174,7 +174,7 @@ let hp_pattern_jm n =
 (* creates the discrimination = injection+contradiction principle *)
 exception ConstructorTooBig of string;;
 
-let mk_discriminator ~use_jmeq name it leftno status baseuri =
+let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri =
   let itnargs = 
     let _,_,arity,_ = it in 
     List.length (arg_list 0 arity) in
@@ -291,7 +291,7 @@ let mk_discriminator ~use_jmeq name it leftno status baseuri =
                  List.map
                    (fun i -> 
                       let nargs_kty = nargs it leftno i in
-                      if (nargs_kty > 5 && not use_jmeq) then raise (ConstructorTooBig (kname i)); 
+                      if (nargs_kty > 5 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i)); 
                       let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
                                  (nargs_kty - 1) [] in
                      let nones = 
@@ -321,20 +321,20 @@ let mk_discriminator ~use_jmeq name it leftno status baseuri =
   (* PHASE 2: create the object for the proof of the principle: we'll name it
    * "theorem" *)
   let status, theorem =
-   GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
+   let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+   GrafiteDisambiguate.disambiguate_nobj status ~baseuri
     (baseuri ^ name ^ ".def",0,
       NotationPt.Theorem
-       (`Theorem,name,principle,
-         Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+       (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
   in 
-  let uri,height,nmenv,nsubst,nobj = theorem in
+  let _uri,_height,nmenv,_nsubst,_nobj = theorem in
   let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
   let status = status#set_obj theorem in
   let status = status#set_stack ninitial_stack in
   let status = subst_metasenv_and_fix_names status in
 
   (* PHASE 3: we finally prove the discrimination principle *)
-  let dbranch it ~use_jmeq leftno consno =
+  let dbranch it ~use_jmeq:__ leftno consno =
     let refl_id = mk_sym "refl" in
     pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
     let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
@@ -469,13 +469,20 @@ let subst_tac ~context ~dir skip cur_eq =
       | NCic.Rel var ->
         cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
       | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+    let varname = match var with
+      | NCic.Rel var -> 
+          let name,_ = List.nth context (var+cur_eq-1) in
+	  HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name);
+	  [name]
+      | _ -> []
+    in      
     let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
     if (List.exists (fun x -> List.mem x skip) names_to_gen)
       then oldstatus
     else 
     let gen_tac x =
       (fun s -> 
-      let x' = String.concat " " x in
+      (*let x' = String.concat " " x in*)
       let x = List.map mk_id x in
       (* let s = NTactics.print_tac false ("@generalize " ^ x') s in *)
       generalize0_tac x s) in
@@ -487,7 +494,12 @@ let subst_tac ~context ~dir skip cur_eq =
                    ~what:("",0,mk_id eq_name) ~where:default_pattern;
 (*                 NTactics.reduce_tac ~reduction:(`Normalize true)
                    ~where:default_pattern;*)
+                 (* XXX: temo che la clear multipla funzioni bene soltanto se
+                  * gli identificatori sono nell'ordine giusto.
+                  * Per non saper né leggere né scrivere, usiamo due clear
+                  * invece di una *)
                  NTactics.try_tac (NTactics.clear_tac [eq_name]);
+		 NTactics.try_tac (NTactics.clear_tac varname);
 ]@
                  (List.map NTactics.intro_tac (List.rev names_to_gen))) status
 ;;
@@ -607,7 +619,7 @@ let select_eq ctx acc domain status goal =
            | _ -> status, `NonEq 
            in match kind with
               | `Identity ->
-                  let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+                  let status, _goalty = term_of_cic_term status (get_goalty status goal) ctx in
                      status, Some (List.length ctx - i), kind
               | `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
               | _ -> 
@@ -700,7 +712,9 @@ let rec destruct_tac0 tags acc domain skip status goal =
     let has_cleared = 
      try 
        let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
-     with _ -> true in
+     with 
+      | Sys.Break as e -> raise e
+      |_ -> true in
     let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
     let acc = rm_eq has_cleared acc in
     let skip = rm_eq has_cleared skip in
@@ -716,7 +730,9 @@ let rec destruct_tac0 tags acc domain skip status goal =
       let has_cleared = 
        try 
          let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
-       with _ -> true in
+       with 
+         | Sys.Break as e -> raise e         
+	 | _ -> true in
       let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
       let acc = rm_eq has_cleared acc in
       let skip = rm_eq has_cleared skip in