X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=bde5d63e413978703bf8ef0d58a9908f478d1d34;hb=186c1171d37f5d1cde9bb6f38a863be16debf3f0;hp=a70fe03aedd0d975dee70fb169dc13bdba90edb4;hpb=102a4101f6b4b7da9861de73054188df470c4462;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a70fe03ae..bde5d63e4 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -132,25 +132,27 @@ let exp_impl metasenv subst context =
 ;;
 
 let is_a_double_coercion t =
-  let last_of l = 
-    let rec aux acc = function
-      | x::[] -> acc,x
-      | x::tl -> aux (acc@[x]) tl
-      | [] -> assert false
-    in
-    aux [] l
+  let rec subst_nth n x l =
+    match n,l with
+    | _, [] -> []
+    | 0, _::tl -> x :: tl
+    | n, hd::tl -> hd :: subst_nth (n-1) x tl
   in
   let imp = Cic.Implicit None in
   let dummyres = false,imp, imp,imp,imp in
   match t with
-  | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
-      (match last_of tl with
-      | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
-          let sib2,head = last_of tl2 in
-          true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
-            (c2::sib2@[imp])]) 
+  | Cic.Appl l1 ->
+     (match CoercGraph.coerced_arg l1 with
+     | Some (Cic.Appl l2, pos1) -> 
+         (match CoercGraph.coerced_arg l2 with
+         | Some (x, pos2) ->
+             true, List.hd l1, List.hd l2, x,
+              Cic.Appl (subst_nth (pos1 + 1) 
+                (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
+         | _ -> dummyres)
       | _ -> dummyres)
   | _ -> dummyres
+;;
 
 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
 =
@@ -384,7 +386,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
               with
                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
-        | C.Sort _ -> 
+        | C.Sort (C.CProp tno) -> 
+            let tno' = CicUniv.fresh() in 
+             (try
+               let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+                 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | C.Sort (C.Prop|C.Set) -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
         | C.Implicit infos ->
            let metasenv',t' = exp_impl metasenv subst context infos in
@@ -1242,12 +1251,13 @@ 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 in 
-      let tgt = CoercDb.Fun 0 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.NotMetaClosed 
-      | CoercGraph.NotHandled _ ->
+      | CoercGraph.NotHandled ->
          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
       | CoercGraph.SomeCoercionToTgt candidates
       | CoercGraph.SomeCoercion candidates ->
@@ -1366,11 +1376,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
         CoercGraph.look_for_coercion metasenv subst context infty expty
       in
       match coer with
-      | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
-          "coerce_atom_to_something fails since not meta closed"))
       | CoercGraph.NoCoercion 
-      | CoercGraph.SomeCoercionToTgt _
-      | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+      | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
+          "coerce_atom_to_something fails since no coercions found"))
+      | CoercGraph.NotHandled when 
+          not (CicUtil.is_meta_closed infty) || 
+          not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
+          "coerce_atom_to_something fails since carriers have metas"))
+      | CoercGraph.NotHandled -> raise (RefineFailure (lazy
           "coerce_atom_to_something fails since no coercions found"))
       | CoercGraph.SomeCoercion candidates -> 
           debug_print (lazy (string_of_int (List.length candidates) ^ 
@@ -1627,7 +1640,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
                        snd (HExtlib.split_nth leftno args), mty
                    | _ -> assert false
-                 with CicTypeChecker.TypeCheckerFailure _ -> assert false
+                 with CicTypeChecker.TypeCheckerFailure _ -> 
+                    raise (AssertFailure(lazy "already ill-typed matched term"))
                in
                let new_outty =
                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)