1. bug fixed: injection now performs recursion lifting correctly

2. bug introduced: injections now behaves as id_tac when it has nothing to do

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 42da52bd60101f2c996fbc1eaed08cd0973006bf..e6682709c1b75edff7bda053889a19bde01f9238 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -27,7 +27,7 @@
 
 let debug_print = fun _ -> ()
 
-let rec injection_tac ~term =
+let rec injection_tac ~term ~liftno ~continuation =
  let injection_tac ~term status = 
   let (proof, goal) = status in
   let module C = Cic in
@@ -36,6 +36,7 @@ let rec injection_tac ~term =
   let module T = Tacticals in
   let _,metasenv,_,_ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let term = CicSubstitution.lift liftno term in
   let termty,_ = (* TASSI: FIXME *)
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
   in
@@ -51,29 +52,25 @@ let rec injection_tac ~term =
                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
                          when (uri1 = uri2) && (typeno1 = typeno2) && 
                              (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
-                       (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac
+                       (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) continuation ~liftno
                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
                          when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
-                       let rec traverse_list i liftno l1 l2 =
+                       let rec traverse_list i l1 l2 =
                          match l1,l2 with
-                            [],[] -> T.id_tac
+                            [],[] -> continuation
                           | hd1::tl1,hd2::tl2 -> 
                              if
                               fst
                                (CicReduction.are_convertible ~metasenv
                                  context hd1 hd2 CicUniv.empty_ugraph)
                              then
-                              traverse_list (i+1) liftno tl1 tl2
+                              traverse_list (i+1) tl1 tl2
                              else
-                              T.then_ 
-                               ~start:
-                                 (injection1_tac ~i ~liftno
-                                   ~term:(CicSubstitution.lift liftno term))
-                               ~continuation:
-                                 (traverse_list (i+1) (liftno+1) tl1 tl2)
+                              injection1_tac ~i ~term
+                               ~continuation:(traverse_list (i+1) tl1 tl2)
                           | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
-                       in traverse_list 1 0 applist1 applist2
+                       in traverse_list 1 applist1 applist2 ~liftno
                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
@@ -84,16 +81,16 @@ let rec injection_tac ~term =
                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
                          when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) ->
                        raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one"))
-                    | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
+                    | _ -> continuation ~liftno (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))*)
                    )
-            | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
+            | _ -> continuation ~liftno (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))*)
            )
         | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
       ) status
  in 
   ProofEngineTypes.mk_tactic (injection_tac ~term)
 
-and injection1_tac ~term ~i ~liftno = 
+and injection1_tac ~term ~i ~liftno ~continuation =
  let injection1_tac ~term ~i status =
   let (proof, goal) = status in
   (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
@@ -102,10 +99,12 @@ and injection1_tac ~term ~i ~liftno =
    let module U = UriManager in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
+   let term = CicSubstitution.lift liftno term in
    let _,metasenv,_,_ = proof in
    let _,context,_ = CicUtil.lookup_meta goal metasenv in
    let termty,_ = (* TASSI: FIXME *)
-     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+   in
      match termty with (* an equality *)
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
              when LibraryObjects.is_eq_URI equri -> (
@@ -151,12 +150,6 @@ and injection1_tac ~term ~i ~liftno =
                                in
                                 C.Lambda (binder',source,(aux target (k+1)))
                             | _ ->
-if id = i_constr_id then (
-prerr_endline ("k= " ^ string_of_int k);
-prerr_endline ("paramsno= " ^ string_of_int paramsno);
-prerr_endline ("nr_param_constr " ^ string_of_int (k - 1 - paramsno));
-prerr_endline ("rel= " ^ string_of_int (k - i));
-);
                                let nr_param_constr = k - 1 - paramsno in
                                 if id = i_constr_id
                                  then C.Rel (k - i)
@@ -211,7 +204,8 @@ prerr_endline ("rel= " ^ string_of_int (k - i));
                   ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2']))
                   ~continuations:[
                     T.then_ 
-                     ~start:T.id_tac (*(injection_tac ~term:(C.Rel 1))*)
+                     ~start:(injection_tac ~liftno:0 ~term:(C.Rel 1)
+                       ~continuation:(fun ~liftno:x -> continuation ~liftno:(liftno + 1 + x)))
                      ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) 
                     ;
                     T.then_ 
@@ -232,30 +226,20 @@ prerr_endline ("rel= " ^ string_of_int (k - i));
                                   (lazy
                                     "Injection: goal after cut is not correct"))
                            in
-let aaa =
                             ProofEngineTypes.apply_tactic 
                             (ReductionTactics.change_tac
                                ~pattern:(ProofEngineTypes.conclusion_pattern
                                 (Some new_t1'))
                                (fun _ m u ->
-let xxx =
                                  C.Appl [
                                   C.Lambda
                                    (C.Name "x",
                                      tty,
                                      C.MutCase
                                       (turi,typeno,outtype,C.Rel 1,patterns)) ;
-                                  t1]
-in
-prerr_endline ("i=" ^ string_of_int i ^ "; liftno=" ^ string_of_int liftno);
-prerr_endline ("XXX: " ^ CicPp.ppterm xxx);
-prerr_endline ("WITH: " ^ CicPp.ppterm new_t1');
-xxx,
+                                  t1],
                                  m, u))
                         status
-in
-prerr_endline "OK";
-aaa
                        ))
                      ~continuation:
                        (T.then_
@@ -275,6 +259,10 @@ aaa
   ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 ;;
 
+let injection_tac =
+ injection_tac ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
+;;
+
 exception TwoDifferentSubtermsFound of int 
 
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori