X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=c38c15b931cdea943fda830e4097790503ef5501;hb=da5dd88bbcc43d9f4342e47c922b820abf91c92f;hp=111d20126e0bba1f59272d61c493e452d7a3ccf9;hpb=190c0efe22d097c4b4e85207342224622b1fccb9;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 111d20126..c38c15b93 100644
--- 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 
@@ -2065,12 +2087,12 @@ let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
    check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
 ;;
 
-let typecheck uri =
+let typecheck ?(trust=true) uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let logger = new CicLogger.logger in
-   match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
    | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
    | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
       (* let's typecheck the uncooked object *)
@@ -2078,7 +2100,7 @@ let typecheck uri =
       let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
       CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
       logger#log (`Type_checking_completed uri);
-      match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+      match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
       | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | _ -> raise CicEnvironmentError
 ;;