Bug fixed in LetIn: the cumulativity test was performed switching the order

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 111d20126e0bba1f59272d61c493e452d7a3ccf9..ca76827068c7b893326369800910c27676ebf1e0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1135,6 +1135,21 @@ and guarded_by_constructors ~logger ~subst ~metasenv indURI =
  in
    aux 
 
+and is_non_recursive ctx paramsno t uri =
+  let t = debrujin_constructor uri 1 [] t in
+(*   let ctx, t =  split_prods ~subst:[] ctx paramsno t in *)
+  let len = List.length ctx in
+  let rec aux ctx n nn t =
+    match CicReduction.whd ctx t with
+    | Cic.Prod (name,src,tgt) -> 
+        does_not_occur ctx n nn src &&
+         aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt
+    | (Cic.Rel k) 
+    | Cic.Appl (Cic.Rel k :: _) when k = nn -> true
+    | t -> assert false
+  in
+    aux ctx (len-1) len t
+
 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
  let module C = Cic in
@@ -1174,14 +1189,17 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
              let non_informative,ugraph =
               if cl_len = 0 then true,ugraph
               else
-               is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
-                paramsno (snd (List.nth cl 0)) ugraph
+               let b, ug =
+                is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
+                 paramsno (snd (List.nth cl 0)) ugraph
+               in
+                b && 
+                is_non_recursive [Some (C.Name name,C.Decl ty)]
+                  paramsno  (snd (List.nth cl 0)) uri, ug
              in
               (* is it a singleton or empty non recursive and non informative
                  definition? *)
-              non_informative &&
-               does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
-                (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ugraph
+              non_informative, ugraph
             else
               false,ugraph
          | _ ->
@@ -1332,6 +1350,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
+(* FG: DEBUG ONLY   
+   prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
+   prerr_endline ("TC: term   :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
+*)   
    match t with
       C.Rel n ->
        (try
@@ -1424,7 +1446,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
       let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
       let b,ugraph1 =
-       R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+       R.are_convertible ~subst ~metasenv context ty' ty ugraph1
       in 
        if not b then
         raise