Fixed inference of outtype for match when the inductive type has left and/or

right parameters.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 1e655b35248dc36ca2f3d32939c76bdf5087c709..351104f56f7806917a9e4a89ea6b92ef3ed7b8d4 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -388,6 +388,17 @@ and type_of_aux' metasenv context t ugraph =
              fo_unif_subst subst context metasenv 
                expected_type' actual_type ugraph2
           in
+           let rec instantiate_prod t =
+            function
+               [] -> t
+             | he::tl ->
+                match CicReduction.whd ~subst context t with
+                   C.Prod (_,_,t') ->
+                    instantiate_prod (CicSubstitution.subst he t') tl
+                 | _ -> assert false
+           in
+           let arity_instantiated_with_left_args =
+            instantiate_prod arity left_args in
             (* TODO: check if the sort elimination 
               * is allowed: [(I q1 ... qr)|B] *)
           let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
@@ -441,7 +452,18 @@ and type_of_aux' metasenv context t ugraph =
                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
                     ) uris ([],metasenv)
                  in
-                 let ty = Cic.MutInd(uri, i, exp_name_subst) in
+                 let ty =
+                  match left_args,right_args with
+                     [],[] -> Cic.MutInd(uri, i, exp_name_subst)
+                   | _,_ ->
+                      let rec mk_right_args =
+                       function
+                          0 -> []
+                        | n -> (Cic.Rel n)::(mk_right_args (n - 1))
+                      in
+                       Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
+                        (left_args @ mk_right_args (List.length right_args)))
+                 in
                  let fresh_name = 
                    FreshNamesGenerator.mk_fresh_name ~subst metasenv 
                      context Cic.Anonymous ~typ:ty
@@ -449,7 +471,13 @@ and type_of_aux' metasenv context t ugraph =
                  match outtypeinstances with
                  | [] -> 
                      let extended_context = 
-                       Some (fresh_name,Cic.Decl ty)::context 
+                      let rec add_right_args b =
+                       function
+                          Cic.Prod (name,ty,t) ->
+                           Some (name,Cic.Decl ty)::(add_right_args b t)
+                        | _ -> (Some (fresh_name,Cic.Decl ty))::b
+                      in
+                       add_right_args context arity_instantiated_with_left_args
                      in
                      let metasenv,new_meta = 
                        CicMkImplicit.mk_implicit metasenv subst extended_context
@@ -458,8 +486,15 @@ and type_of_aux' metasenv context t ugraph =
                        CicMkImplicit.identity_relocation_list_for_metavariable 
                          extended_context
                      in
+                     let rec add_lambdas b =
+                      function
+                         Cic.Prod (name,ty,t) ->
+                          Cic.Lambda (name,ty,(add_lambdas b t))
+                       | _ -> Cic.Lambda (fresh_name, ty, b)
+                     in
                      let candidate = 
-                       Cic.Lambda(fresh_name, ty, Cic.Meta (new_meta,irl))
+                      add_lambdas (Cic.Meta (new_meta,irl))
+                       arity_instantiated_with_left_args
                      in
                      (Some candidate),ugraph4,metasenv
                  | (constructor_args_no,_,instance,_)::tl -> 
@@ -495,8 +530,17 @@ and type_of_aux' metasenv context t ugraph =
                        match candidate with
                        | None -> None, ugraph,metasenv
                        | Some t -> 
-                           Some (Cic.Lambda (fresh_name, ty, 
-                             CicSubstitution.lift 1 t)),ugraph,metasenv 
+                          let rec add_lambdas n b =
+                           function
+                              Cic.Prod (name,ty,t) ->
+                               Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
+                            | _ ->
+                              Cic.Lambda (fresh_name, ty,
+                               CicSubstitution.lift (n + 1) t)
+                          in
+                           Some
+                            (add_lambdas 0 t arity_instantiated_with_left_args),
+                           ugraph,metasenv 
                      with Failure s -> 
                        None,ugraph4,metasenv
                in
@@ -508,7 +552,7 @@ and type_of_aux' metasenv context t ugraph =
                        candidate outtype ugraph5
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
-                       (Cic.Appl [outtype; term']),s,m,u)
+                       (Cic.Appl (outtype::right_args@[term'])),s,m,u)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context