Patch to add a debugging string to HExtlib.split_nth reverted

[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 45b2bce8f79b97bdd29e02e795d37cd8e32a549c..b535b9ebe987677505d7d9b40a2c59731a4c2606 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -131,6 +131,20 @@ let exp_impl metasenv subst context =
   | _ -> assert false
 ;;
 
+let unvariant newt =
+ match newt with
+ | Cic.Appl (hd::args) ->
+    let uri = CicUtil.uri_of_term hd in
+    (match 
+      CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
+    with
+    | Cic.Constant (_,Some t,_,[],attrs),_ 
+      when List.exists ((=) (`Flavour `Variant)) attrs -> 
+       Cic.Appl (t::args)
+    | _ -> newt)
+ | _ -> newt
+;;
+
 let is_a_double_coercion t =
   let rec subst_nth n x l =
     match n,l with
@@ -323,8 +337,8 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
-     ugraph
+and type_of_aux' ?(clean_dummy_dependent_types=true) 
+  ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
     let module C = Cic in
@@ -491,7 +505,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
              exn ->
               enrich localization_tbl s' exn
                ~f:(function _ ->
-                 lazy ("The term " ^
+                 lazy ("(2) The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
@@ -617,7 +631,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
              exn ->
               enrich localization_tbl term' exn
                ~f:(function _ ->
-                 lazy ("The term " ^
+                 lazy ("(3) The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
@@ -663,7 +677,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                     exn ->
                      enrich localization_tbl constructor'
                       ~f:(fun _ ->
-                        lazy ("The term " ^
+                        lazy ("(4) The term " ^
                          CicMetaSubst.ppterm_in_context metasenv subst p'
                           context ^ " has type " ^
                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
@@ -851,7 +865,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                       exn ->
                        enrich localization_tbl p exn
                         ~f:(function _ ->
-                          lazy ("The term " ^
+                          lazy ("(5) The term " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
@@ -892,7 +906,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(7) The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -945,7 +959,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(8) The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1192,11 +1206,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
          let selected =
            HExtlib.list_findopt
              (fun (metasenv,last,c) _ ->
-               match c with 
-               | c when not (CoercGraph.is_composite c) -> 
-                   debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
-                   None
-               | c ->
                let subst,metasenv,ugraph =
                 fo_unif_subst subst context metasenv last head ugraph in
                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
@@ -1305,7 +1314,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                   ugraph
                 in 
                  debug_print (lazy (" has type: "^ pp tty));
-                 Some (coerc,tty,subst,metasenv,ugraph)
+
+                 Some (unvariant coerc,tty,subst,metasenv,ugraph)
               with
               | Uncertain _ | RefineFailure _
               | HExtlib.Localized (_,Uncertain _)
@@ -1457,6 +1467,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 if b then 
                   Some ((t,infty), subst, metasenv, ugraph)
                 else 
+                 let newt =  unvariant newt in
                   Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None
@@ -1779,7 +1790,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
       coerce_to_something_aux t infty expty subst metasenv context ugraph
     with Uncertain _ | RefineFailure _ as exn ->
       let f _ =
-        lazy ("The term " ^
+        lazy ("(9) The term " ^
           CicMetaSubst.ppterm_in_context metasenv subst t context ^ 
           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
           infty context ^ " but is here used with type " ^ 
@@ -1817,7 +1828,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
   (* eat prods ends here! *)
   
   let t',ty,subst',metasenv',ugraph1 =
-   type_of_aux [] metasenv context t ugraph
+   type_of_aux subst metasenv context t ugraph
   in
   let substituted_t = CicMetaSubst.apply_subst subst' t' in
   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
@@ -1861,7 +1872,21 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
    else
     substituted_metasenv
   in
-    (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
+    (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) 
+;;
+
+let type_of metasenv subst context t ug =
+  type_of_aux' metasenv subst context t ug
+;;
+
+let type_of_aux' 
+  ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug
+=
+  let t,ty,m,s,ug = 
+    type_of_aux' ?clean_dummy_dependent_types ?localization_tbl 
+      metasenv [] context t ug
+  in
+  t,ty,m,ug
 ;;
 
 let undebrujin uri typesno tys t =
@@ -1962,7 +1987,7 @@ let typecheck metasenv uri obj ~localization_tbl =
          RefineFailure _
        | Uncertain _ as exn ->
           let msg = 
-            lazy ("The term " ^
+            lazy ("(1) The term " ^
              CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
              " has type " ^
              CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^