From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 15:17:15 +0000 (+0000)
Subject: Yet another bug fixed in the inference of the outtype for match: convertibility
X-Git-Tag: PRE_INDEX_1~36
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c8c7bcfd5fd3086be09c2f949b90c614596489b2;p=helm.git

Yet another bug fixed in the inference of the outtype for match: convertibility
was used in place of unification, making type inference much less powerful
in several useful cases.
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8828a417e..25af88f4f 100644
--- 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 
@@ -503,19 +503,19 @@ 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)
                        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' = 
@@ -523,6 +523,14 @@ and type_of_aux' metasenv context t ugraph =
                                       constructor_args_no
                                        (CicMetaSubst.apply_subst subst instance)
                                    in
+prerr_endline ("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
+prerr_endline ("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
@@ -531,11 +539,16 @@ and type_of_aux' metasenv context t ugraph =
                                      candidate_oty,ugraph1,metasenv 
                                    else 
                                      None,ugraph,metasenv
-                                 with Failure s -> None,ugraph,metasenv
-                         ) (Some instance',ugraph4,metasenv) tl
+*)
+                                 with
+                                    Failure _
+                                  | 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
@@ -547,19 +560,20 @@ and type_of_aux' metasenv context t ugraph =
                           in
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
-                           ugraph,metasenv 
+                           ugraph,metasenv,subst
                      with Failure s -> 
-                       None,ugraph4,metasenv
+                       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)
+                       (Cic.Appl (outtype::right_args@[term'])),
+                     subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context