condition de positivite moins stricte vis-a-vis des parametres (cf bug de Eduardo)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2441 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 52 insertions, 27 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 07608a4b95..4729598c76 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -86,6 +86,9 @@ let mind_check_names mie =
 	  check (Idset.add id indset) cstset' inds
   in
   check Idset.empty Idset.empty mie.mind_entry_inds
+(* The above verification is not necessary from the kernel point of
+  vue since inductive and constructors are not referred to by their
+  name, but only by the name of the inductive packet and an index. *)
 
 (* [mind_extract_params mie] extracts the params from an inductive types
    declaration, and checks that they are all present (and all the same)
@@ -102,11 +105,6 @@ let mind_check_arities env mie =
     (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
     mie.mind_entry_inds
 
-let mind_check_wellformed env mie =
-  if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
-  mind_check_names mie;
-  mind_check_arities env mie
-
 (***********************************************************************)
 (***********************************************************************)
 
@@ -194,7 +192,13 @@ let infer_constructor_packet env_ar params short_arity arsort vc =
   let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
   (issmall,isunit,vc', cst)
 
+(* Type-check an inductive definition. Does not check positivity
+   conditions. *)
 let type_inductive env mie =
+  if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
+  (* Check unicity of names *)
+  mind_check_names mie;
+  mind_check_arities env mie
   (* We first type params and arity of each inductive definition *)
   (* This allows to build the environment of arities and to share *)
   (* the set of constraints *)
@@ -287,6 +291,7 @@ let failwith_non_pos_vect n ntypes v =
   done;
   anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
 
+(* Check the inductive type is called with the expected parameters *)
 let check_correct_par env hyps nparams ntypes n l largs =
   let largs = Array.of_list largs in
   if Array.length largs < nparams then 
@@ -315,7 +320,9 @@ let abstract_mind_lc env ntyps npars lc =
     in 
     Array.map (substl make_abs) lc
 
-let listrec_mconstr env ntypes hyps nparams i indlc =
+(* The recursive function that checks positivity and builds the list
+   of recursive arguments *)
+let check_positivity env ntypes hyps nparams i indlc =
   let nhyps = List.length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos env n c = 
@@ -336,13 +343,18 @@ let listrec_mconstr env ntypes hyps nparams i indlc =
             else Norec
 	  else
 	    raise (IllFormedInd (LocalNonPos n))
-      | Ind ind_sp -> 
+      | Ind ind_sp ->
           (* If the inductive type being defined or a parameter appears as
              parameter, then we have an imbricated type *)
-          if List.for_all (noccur_between n ntypes) largs &&
-	     List.for_all (noccur_between (n-nhyps) nhyps) largs
-          then Norec
-          else Imbr(ind_sp,imbr_positive env n ind_sp largs)
+          if List.for_all (noccur_between n ntypes) largs then
+            (* If parameters are passed but occur negatively, then
+               the argument is considered non recursive *)
+            if List.for_all (noccur_between (n-nhyps) nhyps) largs 
+            then Norec
+            else
+              try check_positive_imbr env n ind_sp largs
+              with IllFormedInd _ -> Norec
+          else check_positive_imbr env n ind_sp largs
       | err -> 
 	  if noccur_between n ntypes x &&
              List.for_all (noccur_between n ntypes) largs 
@@ -351,32 +363,39 @@ let listrec_mconstr env ntypes hyps nparams i indlc =
 
   (* accesses to the environment are not factorised, but does it worth
      it? *)
-  and imbr_positive env n mi largs =
+  and check_positive_imbr env n mi largs =
     let (mib,mip) = lookup_mind_specif env mi in
     let auxnpar = mip.mind_nparams in
-    let (lpar,auxlargs) = list_chop auxnpar largs in 
+    let (lpar,auxlargs) =
+      try list_chop auxnpar largs 
+      with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in 
+    (* If the inductive appears in the args (non params) then the
+       definition is not positive. *)
     if not (List.for_all (noccur_between n ntypes) auxlargs) then
       raise (IllFormedInd (LocalNonPos n));
+    (* If the inductive type appears non positively in the
+       parameters then the def is not positive *)
+    let lrecargs = List.map (check_weak_pos env n) lpar in
     let auxlc = mip.mind_nf_lc in
     let auxntyp = mib.mind_ntypes in 
+    (* We do not deal with imbricated mutual inductive types *)
     if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
-    let lrecargs = List.map (check_weak_pos env n) lpar in
     (* The abstract imbricated inductive type with parameters substituted *)
     let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
-    let newidx = n + auxntyp in
-(* Extends the environment with a variable corresponding to the inductive def *)
+    (* Extends the environment with a variable corresponding to
+       the inductive def *)
     let env' = push_rel (Anonymous,None,type_of_inductive env mi) env in
+    let newidx = n + auxntyp in
     let _ = 
       (* fails if the inductive type occurs non positively *)
       (* when substituted *) 
       Array.map 
 	(function c -> 
-	   let c' = hnf_prod_applist env c 
-		      (List.map (lift auxntyp) lpar) in 
-	   check_construct env' false newidx c') 
+	  let c' = hnf_prod_applist env c (List.map (lift auxntyp) lpar) in 
+	  check_construct env' false newidx c') 
 	auxlcvect
     in 
-    lrecargs
+    Imbr(mi,lrecargs)
 
   (* The function check_weak_pos is exactly the same as check_pos, but
      with an extra case for traversing abstractions, like in Marseille's
@@ -453,8 +472,10 @@ let is_recursive listind =
   in 
   array_exists one_is_rec
 
+(* Check positivity of an inductive definition *)
 let cci_inductive env env_ar finite inds cst =
   let ntypes = List.length inds in
+  (* Compute the set of used section variables *)
   let ids = 
     List.fold_left 
       (fun acc (_,_,_,ar,_,_,_,lc) -> 
@@ -464,23 +485,26 @@ let cci_inductive env env_ar finite inds cst =
                 Idset.union (global_vars_set env (body_of_type c)) acc)
 	      acc
 	      lc))
-      Idset.empty inds
-  in
+      Idset.empty inds in
   let hyps = keep_hyps env ids in
+  (* Check one inductive *)
   let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) =
-    let recargs = listrec_mconstr env_ar ntypes params nparams i lc in
-    let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
+    (* Check positivity *)
+    let recargs = check_positivity env_ar ntypes params nparams i lc in
+    (* Arity in normal form *)
     let (ar_sign,ar_sort) = dest_arity env ar in
-    
     let nf_ar =
       if isArity (body_of_type ar) then ar
       else it_mkProd_or_LetIn (mkSort ar_sort) ar_sign in
+    (* Elimination sorts *)
+    let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
     let kelim = allowed_sorts issmall isunit ar_sort in
-
+    (* Type of constructors in normal form *)
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc =
       array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in
     let nf_lc = if nf_lc = lc then lc else nf_lc in
+    (* Build the inductive *)
     { mind_consnames = Array.of_list cnames;
       mind_typename = id;
       mind_user_lc = lc;
@@ -506,6 +530,7 @@ let cci_inductive env env_ar finite inds cst =
 (***********************************************************************)
 
 let check_inductive env mie =
-  mind_check_wellformed env mie;
+  (* First type the inductive definition *)
   let (env_arities, inds, cst) = type_inductive env mie in
+  (* Then check positivity *)
   cci_inductive env env_arities mie.mind_entry_finite inds cst