bug fix in injection e relocate term

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index f12e4b3f5d2c8da1da429ba14bba162914e52f70..f31b52a2e329b9a5dccd0566db9202adb1f296e5 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -41,7 +41,6 @@ module PEH = ProofEngineHelpers
 let debug = false
 let debug_print = 
   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
-;;
 
 (* funzione generale di rilocazione dei riferimenti locali *)
 
@@ -81,11 +80,15 @@ let relocate_term map t =
       | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs)
       | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs)
    in
-   map_term 1 t
+   map_term 0 t
 
 let id n = n
 
-let comp f g n = f (g n) 
+let after continuation aftermap beforemap = 
+   continuation ~map:(fun n -> aftermap (beforemap n))
+
+let after2 continuation aftermap beforemap ~map = 
+   continuation ~map:(fun n -> map (aftermap (beforemap n)))
 
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
@@ -286,10 +289,10 @@ let simpl_in_term context = function
       RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)
    | _ -> raise exn_nonproj
 
-(* ~term vive nel contesto della tattica
- * ~continuation riceve la mappa relativa
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
  *)
-let rec injection_tac ~term ~i ~continuation =
+let rec injection_tac ~map ~term ~i ~continuation =
  let give_name seed = function
    | C.Name _ as name -> name
    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
@@ -302,6 +305,7 @@ let rec injection_tac ~term ~i ~continuation =
    * del costruttore *)
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let term = relocate_term map term in
   let termty,_ = 
     CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph
   in
@@ -322,7 +326,7 @@ let rec injection_tac ~term ~i ~continuation =
           when (uri1 = uri2) && (typeno1 = typeno2) && 
                (consno1 = consno2) && (ens1 = ens2) -> 
                (* controllo ridondante *)
-            List.nth applist1 (i-1),List.nth applist2 (i-1),consno2
+            List.nth applist1 (pred i),List.nth applist2 (pred i),consno2
         | _ -> assert false
       in
       let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
@@ -447,13 +451,13 @@ let rec injection_tac ~term ~i ~continuation =
           in
           PET.mk_tactic tac
        in
-       debug_print (lazy ("CUT: " ^ pp context cutted));   
-       let continuation ~map = continuation ~map:(comp succ map) in  
+       debug_print (lazy ("CUT: " ^ pp context cutted));  
        PET.apply_tactic   
           (T.thens ~start: (P.cut_tac cutted)
                    ~continuations:[
                      (qnify_tac ~first_time:false ~term:(C.Rel 1) ~map:id 
-                                ~continuation);  
+                                ~continuation:(after2 continuation succ map) 
+                     );  
                      tac term] 
          ) status
    | _ -> raise exn_noneq
@@ -461,7 +465,7 @@ let rec injection_tac ~term ~i ~continuation =
   PET.mk_tactic injection_tac
 
 (* ~term vive nel contesto della tattica una volta ~mappato
- * ~continuation riceve la mappa relativa
+ * ~continuation riceve la mappa assoluta
  *)
 and qnify_tac ~first_time ~map ~term ~continuation =
  let are_convertible hd1 hd2 metasenv context = 
@@ -472,6 +476,8 @@ and qnify_tac ~first_time ~map ~term ~continuation =
   let _,metasenv,_subst, _,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let term = relocate_term map term in
+  debug_print (lazy ("\nqnify di: " ^ pp context term)); 
+  debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
   let termty,_ = 
     CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph
   in
@@ -487,25 +493,27 @@ and qnify_tac ~first_time ~map ~term ~continuation =
               C.MutConstruct _
               when t1 = t2 ->
                T.then_ ~start:(clear_term first_time context term)
-                        ~continuation:(continuation ~map:id)
+                        ~continuation:(continuation ~map)
             | C.Appl (C.MutConstruct _ as mc1 :: applist1),
               C.Appl (C.MutConstruct _ as mc2 :: applist2)
               when mc1 = mc2 ->
-                let rec traverse_list i l1 l2 = match l1, l2 with
-                  | [], [] -> 
-                    T.then_ ~start:(clear_term first_time context term)
-                             ~continuation:(continuation ~map:id)
-                  | hd1 :: tl1, hd2 :: tl2 -> 
-                     if are_convertible hd1 hd2 metasenv context then
-                       traverse_list (succ i) tl1 tl2
-                     else
-                       injection_tac ~i ~term ~continuation:
-                         (qnify_tac ~first_time:false ~term ~continuation)
-                  | _ -> assert false 
+                let rec traverse_list first_time i l1 l2 = 
+                  match l1, l2 with
+                      | [], [] ->
+                        fun ~map:aftermap ->
+                           T.then_ ~start:(clear_term first_time context term)
+                                    ~continuation:(after continuation aftermap map)
+                      | hd1 :: tl1, hd2 :: tl2 -> 
+                        if are_convertible hd1 hd2 metasenv context then
+                           traverse_list first_time (succ i) tl1 tl2
+                        else
+                          injection_tac ~i ~term ~continuation:
+                             (traverse_list false (succ i) tl1 tl2)
+                      | _ -> assert false 
                       (* i 2 termini hanno in testa lo stesso costruttore, 
                        * ma applicato a un numero diverso di termini *)
                 in
-                  traverse_list 1 applist1 applist2
+                  traverse_list first_time 1 applist1 applist2 ~map:id
             | C.MutConstruct (_,_,consno1,ens1),
               C.MutConstruct (_,_,consno2,ens2)
             | C.MutConstruct (_,_,consno1,ens1),
@@ -516,12 +524,12 @@ and qnify_tac ~first_time ~map ~term ~continuation =
               C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_)
               when (consno1 <> consno2) || (ens1 <> ens2) -> 
                 discriminate_tac ~term
-            | _ when not first_time -> continuation ~map:id
+            | _ when not first_time -> continuation ~map
             | _ (* when first_time *) -> 
                T.then_ ~start:(simpl_in_term context term)
-                       ~continuation:(qnify_tac ~first_time:false ~term ~map:id ~continuation)
+                       ~continuation:(qnify_tac ~first_time:false ~term ~map ~continuation)
            end
-        | _ when not first_time -> continuation ~map:id
+        | _ when not first_time -> continuation ~map
         | _ (* when first_time *) -> raise exn_nonproj
         end 
     | _ -> raise exn_nonproj