* (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 351104f56f7806917a9e4a89ea6b92ef3ed7b8d4..76642ee3d51e553309d67b6294e4a475761b4613 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -434,7 +434,7 @@ and type_of_aux' metasenv context t ugraph =
              
            (match outtype with
            | C.Meta (n,l) ->
-               (let candidate,ugraph5,metasenv = 
+               (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
                       CicEnvironment.get_obj CicUniv.empty_ugraph uri 
@@ -460,9 +460,13 @@ and type_of_aux' metasenv context t ugraph =
                        function
                           0 -> []
                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
+                      in
+                      let right_args_no = List.length right_args in
+                      let lifted_left_args =
+                       List.map (CicSubstitution.lift right_args_no) left_args
                       in
                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
-                        (left_args @ mk_right_args (List.length right_args)))
+                        (lifted_left_args @ mk_right_args right_args_no))
                  in
                  let fresh_name = 
                    FreshNamesGenerator.mk_fresh_name ~subst metasenv 
@@ -471,13 +475,16 @@ and type_of_aux' metasenv context t ugraph =
                  match outtypeinstances with
                  | [] -> 
                      let extended_context = 
-                      let rec add_right_args b =
+                      let rec add_right_args =
                        function
                           Cic.Prod (name,ty,t) ->
-                           Some (name,Cic.Decl ty)::(add_right_args b t)
-                        | _ -> (Some (fresh_name,Cic.Decl ty))::b
+                           Some (name,Cic.Decl ty)::(add_right_args t)
+                        | _ -> []
                       in
-                       add_right_args context arity_instantiated_with_left_args
+                       (Some (fresh_name,Cic.Decl ty))::
+                       (List.rev
+                        (add_right_args arity_instantiated_with_left_args))@
+                       context
                      in
                      let metasenv,new_meta = 
                        CicMkImplicit.mk_implicit metasenv subst extended_context
@@ -496,39 +503,39 @@ and type_of_aux' metasenv context t ugraph =
                       add_lambdas (Cic.Meta (new_meta,irl))
                        arity_instantiated_with_left_args
                      in
-                     (Some candidate),ugraph4,metasenv
+                     (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 =
+                       let candidate,ugraph,metasenv,subst =
                          List.fold_left (
-                           fun (candidate_oty,ugraph,metasenv) 
+                           fun (candidate_oty,ugraph,metasenv,subst) 
                              (constructor_args_no,_,instance,_) ->
                                match candidate_oty with
-                               | None -> None,ugraph,metasenv
+                               | 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
-                                   let b,ugraph1 =
-                                      CicReduction.are_convertible context 
-                                        instance' ty ugraph
+                                   let subst,metasenv,ugraph =
+                                    fo_unif_subst subst context metasenv 
+                                      instance' ty ugraph
                                    in
-                                   if b then 
-                                     candidate_oty,ugraph1,metasenv 
-                                   else 
-                                     None,ugraph,metasenv
-                                 with Failure s -> None,ugraph,metasenv
-                         ) (Some instance',ugraph4,metasenv) tl
+                                    candidate_oty,ugraph,metasenv,subst
+                                 with
+                                    CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
+                                  | CicUnification.UnificationFailure _
+                                  | CicUnification.Uncertain _ ->
+                                     None,ugraph,metasenv,subst
+                         ) (Some instance',ugraph4,metasenv,subst) tl
                        in
                        match candidate with
-                       | None -> None, ugraph,metasenv
+                       | None -> None, ugraph,metasenv,subst
                        | Some t -> 
                           let rec add_lambdas n b =
                            function
@@ -540,19 +547,22 @@ and type_of_aux' metasenv context t ugraph =
                           in
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
-                           ugraph,metasenv 
-                     with Failure s -> 
-                       None,ugraph4,metasenv
+                           ugraph,metasenv,subst
+                     with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+                       None,ugraph4,metasenv,subst
                in
                match candidate with
                | None -> raise (Uncertain "can't solve an higher order unification problem") 
                | Some candidate ->
-                   let s,m,u = 
+                   let subst,metasenv,ugraph = 
                      fo_unif_subst subst context metasenv 
                        candidate outtype ugraph5
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
-                       (Cic.Appl (outtype::right_args@[term'])),s,m,u)
+                      CicReduction.head_beta_reduce
+                       (CicMetaSubst.apply_subst subst
+                        (Cic.Appl (outtype::right_args@[term']))),
+                     subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
@@ -576,8 +586,9 @@ and type_of_aux' metasenv context t ugraph =
                  (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 =