matitaGui: some missing cases during disambiguation now treated

[helm.git] / components / content_pres / cicClassify.ml

diff --git a/components/content_pres/cicClassify.ml b/components/content_pres/cicClassify.ml
index 0c464c7d94d4c8d7500aca63028a2fa4c228934f..4cfd47e5abcac8309337f7f808b87c37f750bd50 100644 (file)
--- a/components/content_pres/cicClassify.ml
+++ b/components/content_pres/cicClassify.ml
@@ -24,7 +24,7 @@
  *)
 
 module C = Cic
-module CS = CicSubstitution
+module R = CicReduction
 module D = Deannotate
 module Int = struct
    type t = int
@@ -57,6 +57,8 @@ let out_table b =
    
 (****************************************************************************)
 
+let id x = x
+
 let rec list_fold_left g map = function
   | []       -> g
   | hd :: tl -> map (list_fold_left g map tl) hd
@@ -98,28 +100,29 @@ let get_rels h t =
    let g a = a in
    aux 1 g t S.empty
 
-let split t =
-   let rec aux a n = function
-      | C.Prod (_, v, t)  -> aux (v :: a) (succ n) t
-      | C.Cast (t, v)     -> aux a n t
-      | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
-      | v                 -> v :: a, n
+let split c t =
+   let add s v c = Some (s, C.Decl v) :: c in
+   let rec aux whd a n c = function
+      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
+      | v when whd        -> v :: a, n
+      | v                 -> aux true a n c (R.whd ~delta:true c v)
     in
-    aux [] 0 t
+    aux false [] 0 c t
 
 let classify_conclusion = function
    | C.Rel i                -> Some (i, 0)
    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
    | _                      -> None
 
-let classify t =
-   let vs, h = split t in
+let classify c t =
+try   
+   let vs, h = split c t in
    let rc = classify_conclusion (List.hd vs) in
    let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in
    let mk_closure b h =
-      let map j = S.union (fst b.(j)) in 
+      let map j = if j < h then S.union (fst b.(j)) else id in 
       for i = pred h downto 0 do
          let direct, unused = b.(i) in
         b.(i) <- S.fold map direct direct, unused 
@@ -129,16 +132,17 @@ let classify t =
    let rec mk_inverse i direct =
       if S.is_empty direct then () else
       let j = S.choose direct in
-      let unused, inverse = b.(j) in 
-      b.(j) <- unused, S.add i inverse;
-      mk_inverse i (S.remove j direct)
+      if j < h then
+         let unused, inverse = b.(j) in 
+         b.(j) <- unused, S.add i inverse
+       else ();
+       mk_inverse i (S.remove j direct)
    in
    let map i (direct, _) = mk_inverse i direct in
    Array.iteri map b;
 (*   out_table b; *)
    List.rev_map snd (List.tl (Array.to_list b)), rc
-
-let aclassify t = classify (D.deannotate_term t)
+with Invalid_argument _ -> failwith "Classify.classify"
 
 let overlaps s1 s2 =
    let predicate x = S.mem x s1 in