1) Include files for NG were neither recursively processes nor accumulated.

[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 7fed3ddf3b8b0aa1582b76cb7b9a8c0b6f1aba2a..c38c15b931cdea943fda830e4097790503ef5501 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
@@ -1179,8 +1194,8 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
                  paramsno (snd (List.nth cl 0)) ugraph
                in
                 b && 
-               does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
-                (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ug
+                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? *)
@@ -1335,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
@@ -1427,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 
@@ -2068,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 *)
@@ -2081,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
 ;;