X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=d6a6c91b9d8e60ad78d5b95fea237865869a37af;hb=4d0ef1046012225b44ee5a1768265c52e534109f;hp=7014a59417ceb21743aaa073ef17526a74528df3;hpb=36842ee77114d2fa896d7ffd2333c07cff22b053;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 7014a5941..d6a6c91b9 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -366,6 +366,12 @@ let apply_tac ~term =
  in
   PET.mk_tactic (apply_tac ~term)
 
+let applyP_tac ~term =
+   let applyP_tac status =
+      let res = PET.apply_tactic (apply_tac ~term) status in res
+   in
+   PET.mk_tactic applyP_tac
+
 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
  let intros_tac (proof, goal)
  =
@@ -618,7 +624,7 @@ let generalize_tac
  =
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback
-       ~pattern:(term,hyps_pat,concl_pat) status
+       ~pattern:(term,hyps_pat,_) status
   =
    if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
    let (proof, goal) = status in
@@ -631,7 +637,7 @@ let generalize_tac
       ~conjecture ~pattern in
     let context = CicMetaSubst.apply_subst_context subst context in
     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-    let pbo = CicMetaSubst.apply_subst subst pbo in
+    let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
     let pty = CicMetaSubst.apply_subst subst pty in
     let term =
      match term with
@@ -743,7 +749,7 @@ let generalize_pattern_tac pattern =
     List.map
      (fun id ->
        let rel,_ = ProofEngineHelpers.find_hyp id context in
-        id,(Some (PET.const_lazy_term rel), [], None)
+        id,(Some (fun ctx m u -> CicSubstitution.lift (List.length ctx - List.length context) rel,m,u), [], Some (ProofEngineTypes.hole))
      ) generalize_hyps in
    let tactics =
     List.map
@@ -886,14 +892,27 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
     PET.mk_tactic reorder_pattern
 ;;
 
-let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
- let cases_tac ~term (proof, goal) =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?(pattern = PET.conclusion_pattern None) term =
+ let cases_tac pattern (proof, goal) =
   let module TC = CicTypeChecker in
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
   let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let pattern = pattern_after_generalize_pattern_tac pattern in
+  let _cpattern =
+   match pattern with 
+     | None, [], Some cpattern ->
+        let rec is_hole =
+         function
+            Cic.Implicit (Some `Hole) -> true
+          | Cic.Prod (Cic.Anonymous,so,tgt) -> is_hole so && is_hole tgt
+          | _ -> false
+        in
+         if not (is_hole cpattern) then
+          raise (PET.Fail (lazy "not implemented"))
+     | _ -> raise (PET.Fail (lazy "not implemented")) in    
   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let termty = CicReduction.whd context termty in
   let (termty,metasenv',arguments,fresh_meta) =
@@ -1016,7 +1035,16 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     in
     proof'', patched_new_goals
   in
-  PET.mk_tactic (cases_tac ~term)
+   let reorder_pattern ((proof, goal) as status) =
+     let _,metasenv,_,_,_,_ = proof in
+     let conjecture = CicUtil.lookup_meta goal metasenv in
+     let _,context,_ = conjecture in
+     let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
+      PET.apply_tactic
+       (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
+         ~continuation:(PET.mk_tactic (cases_tac pattern))) status
+   in
+    PET.mk_tactic reorder_pattern
 ;;