X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=fe5ee7fe378942f14c08ebe923a7a689698af4b4;hb=ff6a1396270493dcf0e1f673f32a8213a8ce3751;hp=fc9dc840d1bb5323ff9526ce57d561664b5999ac;hpb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index fc9dc840d..fe5ee7fe3 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -405,6 +405,39 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
+            let rec count_prods context ty =
+              match CicReduction.whd context ty with
+              | Cic.Prod (n,s,t) -> 
+                 1 + count_prods (Some (n,Cic.Decl s)::context) t
+              | _ -> 0
+            in
+            let exp_prods = count_prods context ty' in
+            let inf_prods = count_prods context inferredty in
+            let te', inferredty, metasenv'', subst'', ugraph2 =
+               let rec aux t m s ug it = function
+                 | 0 -> t,it,m,s,ug
+                 | n ->
+                      match CicReduction.whd context it with
+                      | Cic.Prod (_,src,tgt) -> 
+                          let newmeta, metaty, s, m, ug =
+                            type_of_aux s m context (Cic.Implicit None) ug
+                          in
+                          let s,m,ug = 
+                            fo_unif_subst s context m metaty src ug
+                          in
+(*                           prerr_endline "saturo"; *)
+                          let t =
+                            match t with
+                            | Cic.Appl l -> Cic.Appl (l @ [newmeta])
+                            | _ -> Cic.Appl [t;newmeta]
+                          in
+                          aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
+                      | _ -> t,it,m,s,ug     
+               in
+                 aux te' metasenv'' subst'' ugraph2 inferredty
+                   (max 0 (inf_prods - exp_prods))
+            in
+(*             prerr_endline ("ottengo: " ^ CicPp.ppterm te'); *)
             let (te', ty'), subst''',metasenv''',ugraph3 =
               coerce_to_something true localization_tbl te' inferredty ty'
                 subst'' metasenv'' context ugraph2
@@ -1104,7 +1137,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
             let t' = CicUniv.fresh() in 
              (try
-              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with
@@ -1251,9 +1284,11 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
     let fix_arity n metasenv context subst he hetype ugraph =
       let hetype = CicMetaSubst.apply_subst subst hetype in
-      let src = CoercDb.coerc_carr_of_term hetype 0 in 
-      let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
-      match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+      (* instead of a dummy functional type we may create the real product
+       * using args_bo_and_ty, but since coercions lookup ignores the 
+       * actual ariety we opt for the simple solution *)
+      let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
+      match CoercGraph.look_for_coercion metasenv subst context hetype fty with
       | CoercGraph.NoCoercion -> []
       | CoercGraph.NotHandled ->
          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
@@ -1306,6 +1341,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
                "\n but is applyed to: " ^ String.concat ";" 
                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
+              let error = ref None in
               let possible_fixes = 
                fix_arity (List.length args) metasenv context subst he hetype
                 ugraph in
@@ -1323,14 +1359,18 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    with
                     | RefineFailure _ | Uncertain _
                     | HExtlib.Localized (_,RefineFailure _)
-                    | HExtlib.Localized (_,Uncertain _) -> None)
+                    | HExtlib.Localized (_,Uncertain _) as exn ->
+                       error := Some exn; None)
                 possible_fixes
               with
               | Some x -> x
               | None ->
-                 raise 
-                  (MoreArgsThanExpected
-                    (List.length args, RefineFailure (lazy "")))
+                 match !error with
+                    None ->
+                     raise 
+                      (MoreArgsThanExpected
+                        (List.length args, RefineFailure (lazy "")))
+                  | Some exn -> raise exn
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =