]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/destructTactic.ml
Patch to add a debugging string to HExtlib.split_nth reverted
[helm.git] / helm / software / components / tactics / destructTactic.ml
index 8164fc5f68a2165029697fc74b4fbff6e31060c9..f6fb61ac1ddf0e4a5511cf4c639bcc0bb0d17423 100644 (file)
@@ -92,7 +92,7 @@ let discriminate_tac ~term =
  let mk_branches_and_outtype turi typeno consno context args =
     (* a list of "True" except for the element in position consno which
      * is "False" *)
-    match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+    match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
     | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
         let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
         let false_constr_id,_ = List.nth constructor_list (consno - 1) in
@@ -158,7 +158,7 @@ let discriminate_tac ~term =
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
-    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+    CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
   in
   match termty with
    | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
@@ -226,7 +226,7 @@ let clear_term first_time lterm =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
-      let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+      let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
       debug_print (lazy ("\nclear di: " ^ pp context term));
       debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); 
       let g () = if first_time then raise exn_nothingtodo else T.id_tac in
@@ -247,7 +247,7 @@ let exists context = function
    | C.Rel i -> List.nth context (pred i) <> None
    | _       -> true
 
-let rec recur_on_child_tac ~before =
+let recur_on_child_tac ~before ~after =
    let recur_on_child status = 
       let (proof, goal) = status in
       let _, metasenv, _subst, _, _, _ = proof in
@@ -259,13 +259,12 @@ let rec recur_on_child_tac ~before =
          S.lift distance term, m, ug
       in
       let lterm = mk_lterm (Cic.Rel 1) in
-      let continuation = destruct ~first_time:false lterm in
-      let tactic = T.then_ ~start:before ~continuation in
+      let tactic = T.then_ ~start:before ~continuation:(after lterm) in
       PET.apply_tactic tactic status  
    in
    PET.mk_tactic recur_on_child
    
-and injection_tac ~lterm ~i ~continuation =
+let injection_tac ~lterm ~i ~continuation ~recur =
  let give_name seed = function
    | C.Name _ as name -> name
    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
@@ -278,9 +277,9 @@ and injection_tac ~lterm ~i ~continuation =
    * del costruttore *)
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+  let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
   let termty,_ =
-    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+    CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
   in
   debug_print (lazy ("\ninjection su : " ^ pp context termty)); 
   match termty with (* an equality *)
@@ -302,9 +301,9 @@ and injection_tac ~lterm ~i ~continuation =
             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
+      let tty',_ = CTC.type_of_aux' metasenv context t1' CU.oblivion_ugraph in
       let patterns,outtype =
-        match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+        match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
         | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
            let left_params, right_params = HExtlib.split_nth paramsno params in
            let _,_,_,constructor_list = List.nth ind_type_list typeno in
@@ -384,7 +383,7 @@ and injection_tac ~lterm ~i ~continuation =
       let go_on =
         try
           let _,g = CTC.type_of_aux' metasenv context  cutted
-            CU.empty_ugraph
+            CU.oblivion_ugraph
           in
           let _,g = CTC.type_of_aux' metasenv context changed g in
           fst (CR.are_convertible ~metasenv context  t1' changed g)
@@ -429,7 +428,7 @@ and injection_tac ~lterm ~i ~continuation =
        let tactic = 
           T.thens ~start: (P.cut_tac cutted)
                    ~continuations:[
-                     recur_on_child_tac continuation;
+                     recur_on_child_tac continuation recur;
                      fill_cut_tac term
                   ]
         in
@@ -438,12 +437,12 @@ and injection_tac ~lterm ~i ~continuation =
  in
   PET.mk_tactic injection_tac
 
-and subst_tac ~lterm ~direction ~where ~continuation =
+let subst_tac ~lterm ~direction ~where ~continuation ~recur =
    let subst_tac status =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
-      let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+      let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
       debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term));
       let tactic = match where with
          | None      -> 
@@ -455,26 +454,27 @@ and subst_tac ~lterm ~direction ~where ~continuation =
             debug_print (lazy ("nella premessa: " ^ name));
            let pattern = None, [name, PET.hole], None in
             let start = ET.rewrite_tac ~direction ~pattern term [] in
-            let ok_tactic = recur_on_child_tac continuation in
+            let ok_tactic = recur_on_child_tac continuation recur in
            T.if_ ~start ~continuation:ok_tactic ~fail:continuation         
       in 
       PET.apply_tactic tactic status
    in
    PET.mk_tactic subst_tac
 
-and destruct ~first_time lterm =
+let rec destruct ~first_time lterm =
  let are_convertible hd1 hd2 metasenv context = 
-   fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
+   fst (CR.are_convertible ~metasenv context hd1 hd2 CU.oblivion_ugraph)
  in
+ let recur = destruct ~first_time:false in
  let destruct status = 
   let (proof, goal) = status in
   let _,metasenv,_subst, _,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+  let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
   let tactic = if not (first_time || exists context term) then T.id_tac else begin
      debug_print (lazy ("\ndestruct di: " ^ pp context term)); 
      debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
-     let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in
+     let termty,_ = CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in
      debug_print (lazy ("\ndestruct su: " ^ pp context termty)); 
      let mk_lterm term c m ug =
         let distance = List.length c - List.length context in
@@ -492,10 +492,10 @@ and destruct ~first_time lterm =
                    clear_term false (mk_lterm with_what)
                 ]
              in
-             subst_tac ~direction ~lterm ~where:None ~continuation
+             subst_tac ~direction ~lterm ~where:None ~continuation ~recur
            | Some (C.Name name, _) :: tl when j < index && j <> k ->
              debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
-             subst_tac ~direction ~lterm ~where:(Some name) 
+             subst_tac ~direction ~lterm ~where:(Some name) ~recur 
                        ~continuation:(traverse_context false (succ j) tl)
            | _ :: tl -> traverse_context first_time (succ j) tl
         in
@@ -519,7 +519,7 @@ and destruct ~first_time lterm =
                         if are_convertible hd1 hd2 metasenv context then
                            traverse_list first_time (succ i) tl1 tl2
                         else
-                          injection_tac ~i ~lterm ~continuation:
+                          injection_tac ~i ~lterm ~recur ~continuation:
                              (traverse_list false (succ i) tl1 tl2)
                       | _ -> assert false 
                       (* i 2 termini hanno in testa lo stesso costruttore, 
@@ -563,7 +563,7 @@ and destruct ~first_time lterm =
    PET.mk_tactic destruct
 
 (* destruct performs either injection or discriminate or subst *)
-let destruct_tac xterm =
+let destruct_tac xterms =
    let destruct status =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
@@ -572,9 +572,11 @@ let destruct_tac xterm =
          let distance = List.length c - List.length context in
           S.lift distance term, m, ug
       in
-      let tactics = match xterm with 
-         | Some term -> [destruct ~first_time:true (mk_lterm term)]
-         | None      ->
+      let tactics = match xterms with 
+         | Some terms -> 
+           let map term = destruct ~first_time:false (mk_lterm term) in
+           List.map map terms
+         | None       ->
             let rec mk_tactics first_time i tacs = function
               | []           -> List.rev tacs
               | Some _ :: tl ->