CProp hierarchy fixed:

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 87b3f7f42a319f227f06ce9d9c7b3db5bfc85e53..fc9dc840d1bb5323ff9526ce57d561664b5999ac 100644 (file)
--- 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,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 in 
-      let tgt = CoercDb.Fun 0 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
       | CoercGraph.NoCoercion -> []
-      | CoercGraph.NotMetaClosed 
-      | CoercGraph.NotHandled _ ->
+      | CoercGraph.NotHandled ->
          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
       | CoercGraph.SomeCoercionToTgt candidates
       | CoercGraph.SomeCoercion candidates ->
@@ -1366,11 +1374,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) ^