one more step toward a decent destruct

lifting should now be ok, but handling of wight params is still
shaky

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 9bcdf60409a5380d47b4c8de5d04d53fc2c66df6..5a25c00fa95fbf4b2d21a124b3fca2b3dd4df321 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -207,6 +207,11 @@ let exn_injwronggoal =
 let exn_noneqind =
   ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type");;
 
+let pp ctx t = 
+  let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
+  CicPp.pp t names
+;;
+
 let rec injection_tac ~first_time ~term ~liftno ~continuation =
  let module C = Cic in
  let module CR = CicReduction in
@@ -215,7 +220,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
  let module T = Tacticals in
  let module PST = ProofEngineStructuralRules in
  let module PET = ProofEngineTypes in
- let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in
+(*  let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in *)
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
  in
@@ -227,7 +232,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
   in
-  prerr_endline ("injection su: " ^ CicPp.ppterm termty);
+(*   prerr_endline ("\ninjection su: " ^ pp context termty); *)
   let tac =
     match termty with
     | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] 
@@ -317,7 +322,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
  let module P = PrimitiveTactics in
  let module PET = ProofEngineTypes in
  let module T = Tacticals in
- let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in
+(*  let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in *)
  let give_name seed = function
    | C.Name _ as name -> name
    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
@@ -334,7 +339,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
   in
-  prerr_endline ("injection1 su : " ^ CicPp.ppterm termty);
+(*   prerr_endline ("\ninjection1 su : " ^ pp context termty); *)
   match termty with (* an equality *)
   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
     when LibraryObjects.is_eq_URI equri -> 
@@ -374,14 +379,15 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                       let binder' = give_name seed binder in
                       C.Lambda (binder',source,(aux (k+1) target))
                    | _ ->
-                     let nr_param_constr = k - paramsno in
+                     let nr_param_constr = k - paramsno - 1 in
                      if id = i_constr_id then C.Rel (k - i)
                      else S.lift nr_param_constr t1' 
                      (* + 1 per liftare anche il lambda aggiunto
                       * esternamente al case *)
-                 in aux 1 reduced_cty)
+                 in CicSubstitution.lift 1 (aux 1 reduced_cty))
                constructor_list 
            in
+           (* this code should be taken from cases_tac *)
            let outtype =
              let seed = ref 0 in
              let rec to_lambdas te head =
@@ -399,7 +405,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                | _, _ -> assert false
              in
              let abstracted_tty =
-               match CicSubstitution.lift (paramsno(* + 1*)) tty with
+               match CicSubstitution.lift paramsno tty with
                | C.MutInd _ as tty' -> tty'
                | C.Appl l ->
                    let keep,abstract = HExtlib.split_nth (paramsno +1) l in
@@ -409,15 +415,20 @@ and injection1_tac ~term ~i ~liftno ~continuation =
              match ind_type_list with
              | [] -> assert false
              | (_,_,ty,_)::_ ->
+               (* this is in general wrong, do as in cases_tac *)
                to_lambdas (skip_prods left_params ty)
                  (C.Lambda 
-                   (C.Name "x", abstracted_tty, S.lift 1 tty'))
+                   (C.Name "x", abstracted_tty,
+                     (* here we should capture right parameters *)
+                     (* 1 for his Lambda, one for the Lambda outside the match
+                      * and then one for each to_lambda *)
+                     S.lift (2+List.length right_params) tty'))
           in
             patterns,outtype
         | _ -> raise exn_discrnonind
       in
       let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
-      prerr_endline ("CUT: " ^ CicPp.ppterm cutted);
+(*       prerr_endline ("CUT: " ^ pp context cutted); *)
         PET.apply_tactic   
           (T.thens ~start: (P.cut_tac cutted)
              ~continuations:
@@ -430,7 +441,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                ;T.then_ 
                   ~start:(PET.mk_tactic 
                     (fun status ->    
-                      prerr_endline "riempo il cut";
+(*                       prerr_endline "riempo il cut"; *)
                       let (proof, goal) = status in
                       let _,metasenv,_,_, _ = proof in
                       let _,context,gty =CicUtil.lookup_meta goal metasenv in
@@ -446,14 +457,18 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                             C.MutCase (turi,typeno,outtype,C.Rel 1,patterns))
                           ; t1]
                       in
+(*
                       prerr_endline 
-                        ("metto questo: " ^ CicPp.ppterm changed);
+                        ("metto questo: " ^ pp context changed);
                       prerr_endline 
-                        ("al posto di questo: " ^ CicPp.ppterm new_t1');
+                        ("al posto di questo: " ^ pp context new_t1');
                       prerr_endline 
-                        ("nel goal: " ^ CicPp.ppterm gty);
+                        ("nel goal: " ^ pp context gty);
                       prerr_endline 
                         ("nel contesto:\n" ^ CicPp.ppcontext context);
+                      prerr_endline 
+                      ("e poi rewrite con: "^pp context term);
+*)
                         let rc = 
                         PET.apply_tactic 
                           (ReductionTactics.change_tac
@@ -462,7 +477,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                               ~term:gty [new_t1']))
                             (fun _ m u -> changed,m,u))
                           status
-                        in prerr_endline "fine";rc
+                        in rc
                       ))
                   ~continuation:
                     (T.then_