Bug fixing. If the inductive types do not occur in t, t is

strictly positive.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 531705a3c2d40abf7d2699291e683b5da0b2e70f..c0e90a5c6a20157284bf9de115611da4bef94bf6 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -377,7 +377,10 @@ and weakly_positive context n nn uri te =
     | t -> t
   in
   match CicReduction.whd context te with
+(*
      C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
+*)
+     C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
    | C.Prod (C.Anonymous,source,dest) ->
       strictly_positive context n nn
@@ -389,13 +392,13 @@ and weakly_positive context n nn uri te =
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive context n nn
         (subst_inductive_type_with_dummy_mutind source) &&
-        weakly_positive ((Some (name,(C.Decl source)))::context)
+         weakly_positive ((Some (name,(C.Decl source)))::context)
          (n + 1) (nn + 1) uri dest
    | C.Prod (name,source,dest) ->
-      does_not_occur context n nn
-       (subst_inductive_type_with_dummy_mutind source)&&
-       weakly_positive ((Some (name,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
+       does_not_occur context n nn
+        (subst_inductive_type_with_dummy_mutind source)&&
+        weakly_positive ((Some (name,(C.Decl source)))::context)
+         (n + 1) (nn + 1) uri dest
    | _ ->
      raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
 
@@ -415,7 +418,8 @@ and strictly_positive context n nn te =
  let module C = Cic in
  let module U = UriManager in
   match CicReduction.whd context te with
-     C.Rel _ -> true
+   | t when does_not_occur context n nn t -> true
+   | C.Rel _ -> true
    | C.Cast (te,ty) ->
       (*CSC: bisogna controllare ty????*)
       strictly_positive context n nn te
@@ -427,37 +431,39 @@ and strictly_positive context n nn te =
    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
       let (ok,paramsno,ity,cl,name) =
        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-       match o with
-           C.InductiveDefinition (tl,_,paramsno,_) ->
-            let (name,_,ity,cl) = List.nth tl i in
-             (List.length tl = 1, paramsno, ity, cl, name)
-         | _ ->
-           raise (TypeCheckerFailure
-            (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
-      in
-       let (params,arguments) = split tl paramsno in
-       let lifted_params = List.map (CicSubstitution.lift 1) params in
-       let cl' =
+         match o with
+              C.InductiveDefinition (tl,_,paramsno,_) ->
+               let (name,_,ity,cl) = List.nth tl i in
+                (List.length tl = 1, paramsno, ity, cl, name) 
+                (* (true, paramsno, ity, cl, name) *)
+            | _ ->
+               raise 
+                 (TypeCheckerFailure
+                    (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
+      in 
+      let (params,arguments) = split tl paramsno in
+      let lifted_params = List.map (CicSubstitution.lift 1) params in
+      let cl' =
         List.map
-         (fun (_,te) ->
-           instantiate_parameters lifted_params
-            (CicSubstitution.subst_vars exp_named_subst te)
-         ) cl
-       in
+          (fun (_,te) ->
+             instantiate_parameters lifted_params
+               (CicSubstitution.subst_vars exp_named_subst te)
+          ) cl
+      in
         ok &&
-         List.fold_right
+          List.fold_right
           (fun x i -> i && does_not_occur context n nn x)
           arguments true &&
          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
-         List.fold_right
+          List.fold_right
           (fun x i ->
-            i &&
-             weakly_positive
-              ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
-              x
+             i &&
+               weakly_positive
+               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+               x
           ) cl' true
-   | t -> does_not_occur context n nn t
-
+   | t -> false
+       
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive context uri indparamsno i n nn te =
  let module C = Cic in
@@ -494,7 +500,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
    | C.Prod (C.Anonymous,source,dest) ->
-      strictly_positive context n nn source &&
+       let b = strictly_positive context n nn source in
+       b &&
        are_all_occurrences_positive
         ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
         (i+1) (n + 1) (nn + 1) dest
@@ -553,9 +560,12 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
                  (are_all_occurrences_positive tys uri indparamsno i 0 len
                      debrujinedte)
               then
+                begin
+                prerr_endline (UriManager.string_of_uri uri);
+                prerr_endline (string_of_int (List.length tys));
                raise
                  (TypeCheckerFailure
-                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))
+                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
               else
                ugraph'
             ) ugraph cl in