1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 00b6dac7edab74929d8b8e3ea9fd693b8cf93f65..2b67b521f6d0e1ea1cc26f184237280abc48ab11 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -163,59 +163,6 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
        old_uninst,((i,canonical_context',ty')::new_uninst)
   ) metasenv ([],[])
 
-(* Auxiliary function for apply: given a type (a backbone), it returns its   *)
-(* head, a META environment in which there is new a META for each hypothesis,*)
-(* a list of arguments for the new applications and the indexes of the first *)
-(* and last new METAs introduced. The nth argument in the list of arguments  *)
-(* is just the nth new META.                                                 *)
-let new_metasenv_for_apply newmeta proof context ty =
- let module C = Cic in
- let module S = CicSubstitution in
-  let rec aux newmeta ty =
-   let ty' = ty in
-   match ty' with
-      C.Cast (he,_) -> aux newmeta he
-(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
-      (* If the expected type is a Type, then also Set is OK ==>
-      *  we accept any term of type Type *)
-      (*CSC: BUG HERE: in this way it is possible for the term of
-      * type Type to be different from a Sort!!! *)
-    | C.Prod (name,(C.Sort (C.Type _) as s),t) ->
-       (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *)
-       let irl =
-         CicMkImplicit.identity_relocation_list_for_metavariable context
-       in
-        let newargument = C.Meta (newmeta+1,irl) in
-         let (res,newmetasenv,arguments,lastmeta) =
-          aux (newmeta + 2) (S.subst newargument t)
-         in
-          res,
-           (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv,
-           newargument::arguments,lastmeta
-*)
-    | C.Prod (name,s,t) ->
-       let irl =
-         CicMkImplicit.identity_relocation_list_for_metavariable context
-       in
-        let newargument = C.Meta (newmeta,irl) in
-         let (res,newmetasenv,arguments,lastmeta) =
-          aux (newmeta + 1) (S.subst newargument t)
-         in
-         let s' = CicReduction.normalize ~delta:false context s in
-          res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
-          (** NORMALIZE RATIONALE 
-           * we normalize the target only NOW since we may be in this case:
-           * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k  
-           * and we want a mesasenv with ?1:A1 and ?2:A2 and not
-           * ?1, ?2, ?3 (that is the one we whould get if we start from the
-           * beta-normalized A1 -> A2 -> A3 -> P **)
-    | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
-  in
-   (* WARNING: here we are using the invariant that above the most *)
-   (* recente new_meta() there are no used metas.                  *)
-   let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
-    res,newmetasenv,arguments,lastmeta
-
 (* Useful only inside apply_tac *)
 let
  generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst
@@ -276,16 +223,14 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty termty =
-  let (consthead,newmetas,arguments,_) =
-    new_metasenv_for_apply newmeta' proof context termty
-  in
-  let newmetasenv = metasenv'@newmetas in
+let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
+  let (consthead,newmetasenv,arguments,_) =
+   saturate_term newmeta' metasenv' context termty in
   let subst,newmetasenv',_ = 
-    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+   CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
   in
   let t = 
-    if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)
+    if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
   in
   subst,newmetasenv',t
 
@@ -335,13 +280,16 @@ let apply_tac_verbose ~term (proof, goal) =
    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. *)
    let subst,newmetasenv',t = 
-     try
-       new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
-         termty
-     with CicUnification.UnificationFailure _ -> 
-       new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
-         (CicReduction.whd context termty)
+    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)
    in
    let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
    let apply_subst = CicMetaSubst.apply_subst subst in