Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.

4 files changed, 24 insertions, 11 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 80f1988a97..0b488308a1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-	Inductive.check_cofix e cofix
+      Inductive.check_cofix ~flags:{check_guarded=true} e cofix
     | Fix (_,(_,_,_) as fix) ->
-	Inductive.check_fix e fix
+      Inductive.check_fix ~flags:{check_guarded=true} e fix
     | _ -> ()
   in
   let rec iter env c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 378294c984..c894d96a78 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -72,14 +72,17 @@ open Inductiveops
 
 exception Found of int array
 
-let search_guard loc env possible_indexes fixdefs =
+(* spiwack: I chose [tflags] rather than [flags], like in the rest of
+   the code, for the argument name to avoid interference with the
+   argument for [inference_flags] also used in this module. *)
+let search_guard ~tflags loc env possible_indexes fixdefs =
   (* Standard situation with only one possibility for each fix. *)
   (* We treat it separately in order to get proper error msg. *)
   let is_singleton = function [_] -> true | _ -> false in
   if List.for_all is_singleton possible_indexes then
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
-    (try check_fix env fix
+    (try check_fix env ~flags:tflags fix
      with reraise ->
        let (e, info) = Errors.push reraise in
        let info = Loc.add_loc info loc in
@@ -91,8 +94,14 @@ let search_guard loc env possible_indexes fixdefs =
        List.iter
 	 (fun l ->
 	    let indexes = Array.of_list l in
-	    let fix = ((indexes, 0),fixdefs) in
-	    try check_fix env fix; raise (Found indexes)
+            let fix = ((indexes, 0),fixdefs) in
+            (* spiwack: We search for a unspecified structural
+               argument under the assumption that we need to check the
+               guardedness condition (otherwise the first inductive argument
+               will be chosen). A more robust solution may be to raise an
+               error when totality is assumed but the strutural argument is
+               not specified. *)
+            try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes)
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
@@ -606,11 +615,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 			     vn)
 	  in
 	  let fixdecls = (names,ftys,fdefs) in
-	  let indexes = search_guard loc env possible_indexes fixdecls in
+          let indexes =
+            search_guard
+              ~tflags:{Declarations.check_guarded=true}
+              loc env possible_indexes fixdecls
+          in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
-	    (try check_cofix env cofix
+            (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix
              with reraise ->
                let (e, info) = Errors.push reraise in
                let info = Loc.add_loc info loc in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa4..2c02b4a217 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Misctypes
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
-val search_guard :
+val search_guard : tflags:Declarations.typing_flags ->
   Loc.t -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 52afa7f83a..598dd16d06 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -189,13 +189,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env fix;
+        check_fix env ~flags:{Declarations.check_guarded=true} fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env cofix;
+        check_cofix env ~flags:{Declarations.check_guarded=true} cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->