- hExtlib: added debugging information for split_nth

[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 40eaa1ba6351533ce31173749f6b4c5f1ccece7a..537290dc6d062af26e090f61d403e2d87c1a3d07 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -337,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
@@ -1553,7 +1553,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                      let get_l_r_p n = function
                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
-                           HExtlib.split_nth n args
+                           HExtlib.split_nth "R 1" n args
                        | _ -> assert false
                      in
                      let _, _, ty, cl = List.nth tl tyno in
@@ -1626,7 +1626,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                          (CR.head_beta_reduce ~delta:false 
                           (Cic.Appl [outty;k])))),k
                    | Cic.Appl (Cic.MutInd _::pl) ->
-                       let left_p,right_p = HExtlib.split_nth leftno pl in
+                       let left_p,right_p = HExtlib.split_nth "R 2" leftno pl in
                        let has_rights = right_p <> [] in
                        let k = 
                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
@@ -1638,7 +1638,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                              CicUniv.oblivion_ugraph 
                          with
                          | Cic.Appl (Cic.MutInd _::args),_ ->
-                             snd (HExtlib.split_nth leftno args)
+                             snd (HExtlib.split_nth "R 3" leftno args)
                          | _ -> assert false
                          with CicTypeChecker.TypeCheckerFailure _-> assert false
                        in
@@ -1694,7 +1694,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    with
                    | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
                    | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
-                       snd (HExtlib.split_nth leftno args), mty
+                       snd (HExtlib.split_nth "R 4" leftno args), mty
                    | _ -> assert false
                  with CicTypeChecker.TypeCheckerFailure _ -> 
                     raise (AssertFailure(lazy "already ill-typed matched term"))
@@ -1828,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
@@ -1872,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 =