Allow `Pretyping.search_guard` to not check guard

This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.

Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.

5 files changed, 25 insertions, 9 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8fbcc8e5e7..c86a4e3e48 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -68,14 +68,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 ~flags:{Declarations.check_guarded=true} 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
@@ -87,7 +90,13 @@ 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
+            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);
@@ -533,7 +542,11 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 			     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
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 142b54513e..1ef3da1509 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/stm/lemmas.ml b/stm/lemmas.ml
index c766f3fab3..1d591e1be8 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -76,7 +76,7 @@ let adjust_guardness_conditions const = function
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                 env (Declareops.uniquize_side_effects eff) in
               let indexes =
-	        search_guard Loc.ghost env
+                search_guard ~tflags:{Declarations.check_guarded=true} Loc.ghost env
                   possible_indexes fixdecls in
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b6dd2718fa..c4f0b7b17f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1065,7 +1065,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps)
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let env = Global.env() in
-    let indexes = search_guard Loc.ghost env indexes fixdecls in
+    let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
@@ -1169,7 +1169,9 @@ let do_program_recursive local p fixkind fixl ntns =
 	Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
       in
       let indexes = 
-	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
+        Pretyping.search_guard
+          ~tflags:{Declarations.check_guarded=true}
+          Loc.ghost (Global.env ()) possible_indexes fixdecls in
       List.iteri (fun i _ ->
           Inductive.check_fix env
                               ~flags:{Declarations.check_guarded=true}
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9df5a411ba..ec58392d51 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -582,7 +582,8 @@ let declare_mutual_definition l =
 	    List.map3 compute_possible_guardness_evidences
               wfl fixdefs fixtypes in
 	  let indexes = 
-            Pretyping.search_guard Loc.ghost (Global.env())
+              Pretyping.search_guard ~tflags:{Declarations.check_guarded=true}
+              Loc.ghost (Global.env())
               possible_indexes fixdecls in
           Some indexes, 
           List.map_i (fun i _ ->