Two bugs fixed in the apply tactic:

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2b67b521f6d0e1ea1cc26f184237280abc48ab11..97f40205201446fdf82cebd6ad5a67278edec6c7 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -223,9 +223,9 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
+let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
-   saturate_term newmeta' metasenv' context termty in
+   saturate_term newmeta' metasenv' context termty goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
   in
@@ -234,6 +234,11 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
   in
   subst,newmetasenv',t
 
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+    Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+  | _ -> 0
+
 let apply_tac_verbose ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
@@ -278,18 +283,17 @@ let apply_tac_verbose ~term (proof, goal) =
    let termty,_ = 
      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
    let termty =
-     CicSubstitution.subst_vars exp_named_subst_diff termty
-   in
-(*CSC: this code is suspect and/or bugged: we try first without reduction
-  and then using whd. However, the saturate_term always tries with full
-  reduction without delta. *)
+     CicSubstitution.subst_vars exp_named_subst_diff termty in
+   let goal_arity = count_prods context ty in
    let subst,newmetasenv',t = 
-    try
+    let rec add_one_argument n =
+     try
       new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
-        termty
-    with CicUnification.UnificationFailure _ ->
-      new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
-        (CicReduction.whd context termty)
+        termty n
+     with CicUnification.UnificationFailure _ when n > 0 ->
+      add_one_argument (n - 1)
+    in
+     add_one_argument goal_arity
    in
    let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
    let apply_subst = CicMetaSubst.apply_subst subst in
@@ -455,6 +459,10 @@ let elim_tac ~term =
    let (curi,metasenv,proofbo,proofty) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    let (termty,metasenv',arguments,fresh_meta) =
+     ProofEngineHelpers.saturate_term
+      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+    let term = if arguments = [] then term else Cic.Appl (term::arguments) in
     let uri,exp_named_subst,typeno,args =
      match termty with
         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
@@ -472,7 +480,7 @@ let elim_tac ~term =
             name
         | _ -> assert false
       in
-      let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in
+      let ty_ty,_ = T.type_of_aux' metasenv' context ty CicUniv.empty_ugraph in
       let ext =
        match ty_ty with
           C.Sort C.Prop -> "_ind"
@@ -486,7 +494,7 @@ let elim_tac ~term =
      in
       let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
        let ety,_ = 
-         T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in
+         T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
         let rec find_args_no =
          function
             C.Prod (_,_,t) -> 1 + find_args_no t
@@ -504,7 +512,7 @@ let elim_tac ~term =
            C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
           let metasenv', term_to_refine' =
-           CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
+           CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
           let refined_term,_,metasenv'',_ = 
            CicRefine.type_of_aux' metasenv' context term_to_refine' 
              CicUniv.empty_ugraph