positivity check fixed, some subterms were erroneously skipped

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 289ef4b76dc91d5d1c89593c628b29f7e463094e..f450dcd896a6dcaf10495e36cbe4053ccd1b77e0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -337,92 +337,95 @@ and does_not_occur ?(subst=[]) context n nn te =
 and weakly_positive context n nn uri te =
  let module C = Cic in
 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
-  let dummy_mutind =
-   C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
+  let leftno = 
+    match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
+    | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno
+    | _ -> assert false
   in
+  let dummy = Cic.Sort Cic.Prop in
   (*CSC: mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_mutind =
+  let rec subst_inductive_type_with_dummy =
    function
       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
-       dummy_mutind
+       dummy
     | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
+       let _, rargs = HExtlib.split_nth leftno tl in
+       if rargs = [] then dummy else Cic.Appl (dummy :: rargs)
+    | C.Cast (te,ty) -> subst_inductive_type_with_dummy te
     | C.Prod (name,so,ta) ->
-       C.Prod (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
+       C.Prod (name, subst_inductive_type_with_dummy so,
+        subst_inductive_type_with_dummy ta)
     | C.Lambda (name,so,ta) ->
-       C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
+       C.Lambda (name, subst_inductive_type_with_dummy so,
+        subst_inductive_type_with_dummy ta)
     | C.LetIn (name,so,ty,ta) ->
-       C.LetIn (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind ta)
+       C.LetIn (name, subst_inductive_type_with_dummy so,
+        subst_inductive_type_with_dummy ty,
+        subst_inductive_type_with_dummy ta)
     | C.Appl tl ->
-       C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
+       C.Appl (List.map subst_inductive_type_with_dummy tl)
     | C.MutCase (uri,i,outtype,term,pl) ->
        C.MutCase (uri,i,
-        subst_inductive_type_with_dummy_mutind outtype,
-        subst_inductive_type_with_dummy_mutind term,
-        List.map subst_inductive_type_with_dummy_mutind pl)
+        subst_inductive_type_with_dummy outtype,
+        subst_inductive_type_with_dummy term,
+        List.map subst_inductive_type_with_dummy pl)
     | C.Fix (i,fl) ->
        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
+        subst_inductive_type_with_dummy ty,
+        subst_inductive_type_with_dummy bo)) fl)
     | C.CoFix (i,fl) ->
        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
+        subst_inductive_type_with_dummy ty,
+        subst_inductive_type_with_dummy bo)) fl)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
         List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+         (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
          exp_named_subst
        in
         C.Const (uri,exp_named_subst')
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+         (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
          exp_named_subst
        in
         C.Var (uri,exp_named_subst')
     | C.MutInd (uri,typeno,exp_named_subst) ->
        let exp_named_subst' =
         List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+         (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
          exp_named_subst
        in
         C.MutInd (uri,typeno,exp_named_subst')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
        let exp_named_subst' =
         List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+         (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
          exp_named_subst
        in
         C.MutConstruct (uri,typeno,consno,exp_named_subst')
     | 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 (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
-       (* 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)
-         (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
-   | _ ->
-     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+  let rec aux context n nn te = 
+    match CicReduction.whd context te with
+     | C.Appl (C.Sort C.Prop::tl) -> 
+         List.for_all (does_not_occur context n nn) tl
+     | C.Sort C.Prop -> true
+     | C.Prod (name,source,dest) when
+        does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
+         (* dummy abstraction, so we behave as in the anonimous case *)
+         strictly_positive context n nn source &&
+           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 source &&
+           weakly_positive ((Some (name,(C.Decl source)))::context)
+           (n + 1) (nn + 1) uri dest
+     | _ ->
+       raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+ in 
+   aux context n nn (subst_inductive_type_with_dummy te)
 
 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
@@ -592,12 +595,9 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
                   (are_all_occurrences_positive context uri indparamsno
                     (i+indparamsno) indparamsno (len+indparamsno) te)
               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)))                end 
+                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) 
               else
                 ugraph
             ) ugraph cl in