X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=f38dd10b3108c13a991d6ad00b73b0868bbb0ca3;hb=04ade947888ac1115dfe104714bed61c32e1c9c3;hp=c43034f93dfd7f672ade503c0723e9474bd021ea;hpb=e6005301fcbccbca31571795ed6071283f45d5a8;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c43034f93..f38dd10b3 100644
--- 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,7 +234,12 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
   in
   subst,newmetasenv',t
 
-let apply_tac_verbose ~term (proof, goal) =
+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_with_subst ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -276,20 +281,20 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
-   let termty =
-     CicSubstitution.subst_vars exp_named_subst_diff termty
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
    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. *)
+   let termty =
+     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
@@ -300,7 +305,6 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let bo' = apply_subst t in
    let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
-(*    prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
               we may use Implicit, since it will be dropped *)
@@ -309,15 +313,16 @@ let apply_tac_verbose ~term (proof, goal) =
    let (newproof, newmetasenv''') = 
      subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
    in
-     (subst_in,
-       (newproof, 
-          List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
+    (newproof, 
+     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
 
-let apply_tac ~term status = snd (apply_tac_verbose ~term status)
 
-let apply_tac_verbose ~term status =
+(* ALB *)
+let apply_tac_verbose_with_subst ~term status =
   try
-    apply_tac_verbose ~term status
+(*     apply_tac_verbose ~term status *)
+    apply_tac_verbose_with_subst ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure _ as e -> 
@@ -325,6 +330,13 @@ let apply_tac_verbose ~term status =
   | CicTypeChecker.TypeCheckerFailure _ as e ->
       raise (Fail (Printexc.to_string e))
 
+(* ALB *)
+let apply_tac_verbose ~term status =
+  let subst, status = apply_tac_verbose_with_subst ~term status in
+  (CicMetaSubst.apply_subst subst), status
+
+let apply_tac ~term status = snd (apply_tac_verbose ~term status)
+
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
 let apply_tac ~term =
@@ -457,7 +469,7 @@ let elim_tac ~term =
     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 in
+      (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