* (Head) beta reduction functions factorized

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 98bafe9b89a0ac7f06db213e172ca84154f19a25..76642ee3d51e553309d67b6294e4a475761b4613 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -506,9 +506,9 @@ and type_of_aux' metasenv context t ugraph =
                      (Some candidate),ugraph4,metasenv,subst
                  | (constructor_args_no,_,instance,_)::tl -> 
                      try
-                       let instance' = 
-                         CicSubstitution.delift constructor_args_no
-                           (CicMetaSubst.apply_subst subst instance)
+                       let instance',subst,metasenv = 
+                         CicMetaSubst.delift_rels subst metasenv
+                          constructor_args_no instance
                        in
                        let candidate,ugraph,metasenv,subst =
                          List.fold_left (
@@ -518,30 +518,17 @@ and type_of_aux' metasenv context t ugraph =
                                | None -> None,ugraph,metasenv,subst
                                | Some ty ->
                                  try 
-                                   let instance' = 
-                                     CicSubstitution.delift
-                                      constructor_args_no
-                                       (CicMetaSubst.apply_subst subst instance)
+                                   let instance',subst,metasenv = 
+                                     CicMetaSubst.delift_rels subst metasenv
+                                      constructor_args_no instance
                                    in
-debug_print ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
                                    let subst,metasenv,ugraph =
                                     fo_unif_subst subst context metasenv 
                                       instance' ty ugraph
                                    in
-debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
                                     candidate_oty,ugraph,metasenv,subst
-(* CSC: XXX
-                                   let b,ugraph1 =
-                                      CicReduction.are_convertible context 
-                                        instance' ty ugraph
-                                   in
-                                   if b then 
-                                     candidate_oty,ugraph1,metasenv 
-                                   else 
-                                     None,ugraph,metasenv
-*)
                                  with
-                                    Failure _
+                                    CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
                                   | CicUnification.UnificationFailure _
                                   | CicUnification.Uncertain _ ->
                                      None,ugraph,metasenv,subst
@@ -561,7 +548,7 @@ debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ Ci
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
                            ugraph,metasenv,subst
-                     with Failure s -> 
+                     with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                        None,ugraph4,metasenv,subst
                in
                match candidate with
@@ -572,7 +559,9 @@ debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ Ci
                        candidate outtype ugraph5
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
-                       (Cic.Appl (outtype::right_args@[term'])),
+                      CicReduction.head_beta_reduce
+                       (CicMetaSubst.apply_subst subst
+                        (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
@@ -597,8 +586,9 @@ debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ Ci
                  (subst,metasenv,ugraph5) outtypeinstances 
              in
                C.MutCase (uri, i, outtype, term', pl'),
-                 CicReduction.whd ~subst       context 
-                   (C.Appl(outtype::right_args@[term])),
+                 CicReduction.head_beta_reduce
+                  (CicMetaSubst.apply_subst subst
+                   (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
        | C.Fix (i,fl) ->
            let fl_ty',subst,metasenv,types,ugraph1 =